Skip to main content

🎫 Ticket_balance_key.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_token.

Definition make
  (ctxt : Alpha_context.context) (owner : Alpha_context.Destination.t)
  (ticketer : Alpha_context.Contract.t)
  (contents_type : Alpha_context.Script.node)
  (contents : Alpha_context.Script.node)
  : M? (Alpha_context.Ticket_hash.t × Alpha_context.context) :=
  let ticketer_address :=
    {|
      Script_typed_ir.address.destination :=
        Alpha_context.Destination.Contract ticketer;
      Script_typed_ir.address.entrypoint := Alpha_context.Entrypoint.default; |}
    in
  let owner_address :=
    {| Script_typed_ir.address.destination := owner;
      Script_typed_ir.address.entrypoint := Alpha_context.Entrypoint.default; |}
    in
  let? '(ticketer, ctxt) :=
    Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized_legacy
      Script_typed_ir.address_t ticketer_address in
  let? '(owner, ctxt) :=
    Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized_legacy
      Script_typed_ir.address_t owner_address in
  Alpha_context.Ticket_hash.make ctxt (Micheline.root_value ticketer)
    contents_type contents (Micheline.root_value owner).

Definition of_ex_token
  (ctxt : Alpha_context.context) (owner : Alpha_context.Destination.t)
  (function_parameter : Ticket_token.ex_token)
  : M? (Alpha_context.Ticket_hash.t × Alpha_context.context) :=
  let
    'Ticket_token.Ex_token {|
      Ticket_token.parsed_token.ticketer := ticketer;
        Ticket_token.parsed_token.contents_type := contents_type;
        Ticket_token.parsed_token.contents := contents
        |} := function_parameter in
  let loc_value := Micheline.dummy_location in
  let? '(cont_ty_unstripped, ctxt) :=
    Script_ir_unparser.unparse_ty loc_value ctxt contents_type in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.strip_annotations_cost cont_ty_unstripped) in
  let ty_value := Alpha_context.Script.strip_annotations cont_ty_unstripped in
  let? '(contents, ctxt) :=
    Script_ir_unparser.unparse_comparable_data ctxt
      Script_ir_unparser.Optimized_legacy contents_type contents in
  make ctxt owner ticketer ty_value (Micheline.root_value contents).