🎫 Ticket_token_unparser.v
Translated 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).
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).