Skip to main content

🎫 Ticket_transfer.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.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
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_amount.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_token.

Definition parse_ticket
  (consume_deserialization_gas :
    Alpha_context.Script.consume_deserialization_gas)
  (ticketer : Alpha_context.Contract.t)
  (contents : Alpha_context.Script.lazy_expr)
  (ty_value : Alpha_context.Script.lazy_expr) (ctxt : Alpha_context.context)
  : M? (Alpha_context.context × Ticket_token.ex_token) :=
  let? '(ty_value, ctxt) :=
    Alpha_context.Script.force_decode_in_context consume_deserialization_gas
      ctxt ty_value in
  let? '(contents, ctxt) :=
    Alpha_context.Script.force_decode_in_context consume_deserialization_gas
      ctxt contents in
  let? '(Script_ir_translator.Ex_comparable_ty contents_type, ctxt) :=
    Script_ir_translator.parse_comparable_ty ctxt
      (Micheline.root_value ty_value) in
  let 'existT _ __Ex_comparable_ty_'a [ctxt, contents_type] :=
    cast_exists (Es := Set)
      (fun __Ex_comparable_ty_'a
        [Alpha_context.context ** Script_typed_ir.comparable_ty])
      [ctxt, contents_type] in
  let? '(contents, ctxt) :=
    ((Script_ir_translator.parse_comparable_data None ctxt contents_type
      (Micheline.root_value contents)) :
      M? (__Ex_comparable_ty_'a × Alpha_context.context)) in
  let token :=
    Ticket_token.Ex_token
      {| Ticket_token.parsed_token.ticketer := ticketer;
        Ticket_token.parsed_token.contents_type := contents_type;
        Ticket_token.parsed_token.contents := contents; |} in
  return? (ctxt, token).

Definition parse_ticket_and_operation
  (consume_deserialization_gas :
    Alpha_context.Script.consume_deserialization_gas)
  (ticketer : Alpha_context.Contract.t)
  (contents : Alpha_context.Script.lazy_expr)
  (ty_value : Alpha_context.Script.lazy_expr)
  (source : Alpha_context.Contract.t) (destination : Contract_hash.t)
  (entrypoint : Alpha_context.Entrypoint.t)
  (amount : Script_typed_ir.ticket_amount) (ctxt : Alpha_context.context)
  : M?
    (Alpha_context.context × Ticket_token.ex_token ×
      Script_typed_ir.packed_internal_operation) :=
  let?
    '(ctxt,
      (Ticket_token.Ex_token {|
        Ticket_token.parsed_token.ticketer := ticketer;
          Ticket_token.parsed_token.contents_type := contents_type;
          Ticket_token.parsed_token.contents := contents
          |}) as token) :=
    parse_ticket consume_deserialization_gas ticketer contents ty_value ctxt in
  let? ticket_ty :=
    Script_typed_ir.ticket_t Micheline.dummy_location contents_type in
  let ticket :=
    {| Script_typed_ir.ticket.ticketer := ticketer;
      Script_typed_ir.ticket.contents := contents;
      Script_typed_ir.ticket.amount := amount; |} in
  let? '(unparsed_parameters, ctxt) :=
    Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
      ticket_ty ticket in
  let? '(ctxt, nonce_value) := Alpha_context.fresh_internal_nonce ctxt in
  let op :=
    Script_typed_ir.Internal_operation
      {| Script_typed_ir.internal_operation.source := source;
        Script_typed_ir.internal_operation.operation :=
          Script_typed_ir.Transaction_to_smart_contract
            {|
              Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.destination
                := destination;
              Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.amount
                := Alpha_context.Tez.zero;
              Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.entrypoint
                := entrypoint;
              Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.location
                := Micheline.dummy_location;
              Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters_ty
                := ticket_ty;
              Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters
                := ticket;
              Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.unparsed_parameters
                := unparsed_parameters; |};
        Script_typed_ir.internal_operation.nonce := nonce_value; |} in
  return? (ctxt, token, op).

Definition transfer_ticket_with_hashes
  (ctxt : Alpha_context.context) (src_hash : Alpha_context.Ticket_hash.t)
  (dst_hash : Alpha_context.Ticket_hash.t) (qty : Ticket_amount.t)
  : M? (Alpha_context.context × Z.t) :=
  let qty := Script_int.to_zint qty in
  let? '(src_storage_diff, ctxt) :=
    Alpha_context.Ticket_balance.adjust_balance ctxt src_hash (Z.neg qty) in
  let? '(dst_storage_diff, ctxt) :=
    Alpha_context.Ticket_balance.adjust_balance ctxt dst_hash qty in
  let? '(diff_value, ctxt) :=
    Alpha_context.Ticket_balance.adjust_storage_space ctxt
      (src_storage_diff +Z dst_storage_diff) in
  return? (ctxt, diff_value).

Definition transfer_ticket
  (ctxt : Alpha_context.context) (src : Alpha_context.Destination.t)
  (dst : Alpha_context.Destination.t) (ex_token : Ticket_token.ex_token)
  (qty : Ticket_amount.t) : M? (Alpha_context.context × Z.t) :=
  let? '(src_hash, ctxt) := Ticket_balance_key.of_ex_token ctxt src ex_token in
  let? '(dst_hash, ctxt) := Ticket_balance_key.of_ex_token ctxt dst ex_token in
  transfer_ticket_with_hashes ctxt src_hash dst_hash qty.