🎫 Ticket_scanner.v

Translated OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_costs.

Init function; without side-effects in Coq

Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "Unsupported_non_empty_overlay" "Unsupported non empty overlay"
      "Unsupported big-map value with non-empty overlay"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Unsupported big-map value with non-empty overlay"
                  CamlinternalFormatBasics.End_of_format)
                "Unsupported big-map value with non-empty overlay")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unsupported_non_empty_overlay" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Unsupported_non_empty_overlay" unit tt) in
  Error_monad.register_error_kind Error_monad.Branch
    "Unsupported_type_operation" "Unsupported type operation"
    "Types embedding operations are not supported"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Types embedding operations are not supported"
                CamlinternalFormatBasics.End_of_format)
              "Types embedding operations are not supported")))
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Unsupported_type_operation" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Unsupported_type_operation" unit tt).

Inductive ex_ticket : Set :=
| Ex_ticket : ∀ {a : Set},
  Script_typed_ir.comparable_ty → Script_typed_ir.ticket a → ex_ticket.

Module Ticket_inspection.

Witness flag for whether a type can be populated by a value containing a ticket. [False_ht] must be used only when a value of the type cannot contain a ticket.

This flag is necessary for avoiding ticket collection (see below) to have quadratic complexity in the order of: size-of-the-type * size-of-value.

This type is local to the [Ticket_scanner] module and should not be exported.