🎫 Ticket_balance_key.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_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).
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).