Skip to main content

🎫 Ticket_token_unparser.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_unparser.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_token.

Definition unparse
  (ctxt : Alpha_context.context) (function_parameter : Ticket_token.ex_token)
  : M? (Ticket_token.unparsed_token × 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? '(contents, ctxt) :=
    Script_ir_unparser.unparse_comparable_data ctxt
      Script_ir_unparser.Optimized_legacy contents_type contents in
  let? '(ty_unstripped, ctxt) :=
    Script_ir_unparser.unparse_ty Micheline.dummy_location ctxt contents_type in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.strip_annotations_cost ty_unstripped) in
  let ty_value := Alpha_context.Script.strip_annotations ty_unstripped in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.strip_locations_cost ty_value) in
  let contents_type := Micheline.strip_locations ty_value in
  let ticket_token :=
    {| Ticket_token.unparsed_token.ticketer := ticketer;
      Ticket_token.unparsed_token.contents_type := contents_type;
      Ticket_token.unparsed_token.contents := contents; |} in
  return? (ticket_token, ctxt).