Skip to main content

🍬 Script_ir_unparser.v

Translated OCaml

See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_internal_results.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Script_comparable.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_map.
Require TezosOfOCaml.Proto_alpha.Script_set.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.

Module Unparse_costs := Michelson_v1_gas.Cost_of.Unparsing.

Inductive unparsing_mode : Set :=
| Optimized : unparsing_mode
| Readable : unparsing_mode
| Optimized_legacy : unparsing_mode.

Definition unparse_memo_size {A B : Set}
  (loc_value : A) (memo_size : Alpha_context.Sapling.Memo_size.t)
  : Micheline.node A B :=
  let z_value := Alpha_context.Sapling.Memo_size.unparse_to_z memo_size in
  Micheline.Int loc_value z_value.

Reserved Notation "'unparse_comparable_ty_uncarbonated".

Fixpoint unparse_ty_and_entrypoints_uncarbonated {loc : Set}
  (loc_value : loc) (ty_value : Script_typed_ir.ty)
  (function_parameter : Script_typed_ir.entrypoints_node)
  : Alpha_context.Script.michelson_node loc :=
  let unparse_comparable_ty_uncarbonated {loc} :=
    'unparse_comparable_ty_uncarbonated loc in
  let '{|
    Script_typed_ir.entrypoints_node.at_node := at_node;
      Script_typed_ir.entrypoints_node.nested := nested_entrypoints
      |} := function_parameter in
  let '(name, args) :=
    match ty_value with
    | Script_typed_ir.Unit_t(Michelson_v1_primitives.T_unit, nil)
    | Script_typed_ir.Int_t(Michelson_v1_primitives.T_int, nil)
    | Script_typed_ir.Nat_t(Michelson_v1_primitives.T_nat, nil)
    | Script_typed_ir.Signature_t(Michelson_v1_primitives.T_signature, nil)
    | Script_typed_ir.String_t(Michelson_v1_primitives.T_string, nil)
    | Script_typed_ir.Bytes_t(Michelson_v1_primitives.T_bytes, nil)
    | Script_typed_ir.Mutez_t(Michelson_v1_primitives.T_mutez, nil)
    | Script_typed_ir.Bool_t(Michelson_v1_primitives.T_bool, nil)
    | Script_typed_ir.Key_hash_t(Michelson_v1_primitives.T_key_hash, nil)
    | Script_typed_ir.Key_t(Michelson_v1_primitives.T_key, nil)
    | Script_typed_ir.Timestamp_t(Michelson_v1_primitives.T_timestamp, nil)
    | Script_typed_ir.Address_t(Michelson_v1_primitives.T_address, nil)
    | Script_typed_ir.Tx_rollup_l2_address_t
      (Michelson_v1_primitives.T_tx_rollup_l2_address, nil)
    | Script_typed_ir.Operation_t(Michelson_v1_primitives.T_operation, nil)
    | Script_typed_ir.Chain_id_t(Michelson_v1_primitives.T_chain_id, nil)
    | Script_typed_ir.Never_t(Michelson_v1_primitives.T_never, nil)
    | Script_typed_ir.Bls12_381_g1_t
      (Michelson_v1_primitives.T_bls12_381_g1, nil)
    | Script_typed_ir.Bls12_381_g2_t
      (Michelson_v1_primitives.T_bls12_381_g2, nil)
    | Script_typed_ir.Bls12_381_fr_t
      (Michelson_v1_primitives.T_bls12_381_fr, nil)
    | Script_typed_ir.Contract_t ut _meta
      let t_value :=
        unparse_ty_and_entrypoints_uncarbonated loc_value ut
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_contract, [ t_value ])
    | Script_typed_ir.Pair_t utl utr _meta _
      let tl :=
        unparse_ty_and_entrypoints_uncarbonated loc_value utl
          Script_typed_ir.no_entrypoints in
      let tr :=
        unparse_ty_and_entrypoints_uncarbonated loc_value utr
          Script_typed_ir.no_entrypoints in
      match tr with
      | Micheline.Prim _ Michelson_v1_primitives.T_pair ts []
        (Michelson_v1_primitives.T_pair, (cons tl ts))
      | _(Michelson_v1_primitives.T_pair, [ tl; tr ])
      end
    | Script_typed_ir.Union_t utl utr _meta _
      let '(entrypoints_l, entrypoints_r) :=
        match nested_entrypoints with
        | Script_typed_ir.Entrypoints_None
          (Script_typed_ir.no_entrypoints, Script_typed_ir.no_entrypoints)
        |
          Script_typed_ir.Entrypoints_Union {|
            Script_typed_ir.nested_entrypoints.Entrypoints_Union._left := _left;
              Script_typed_ir.nested_entrypoints.Entrypoints_Union._right :=
                _right
              |} ⇒ (_left, _right)
        end in
      let tl :=
        unparse_ty_and_entrypoints_uncarbonated loc_value utl entrypoints_l in
      let tr :=
        unparse_ty_and_entrypoints_uncarbonated loc_value utr entrypoints_r in
      (Michelson_v1_primitives.T_or, [ tl; tr ])
    | Script_typed_ir.Lambda_t uta utr _meta
      let ta :=
        unparse_ty_and_entrypoints_uncarbonated loc_value uta
          Script_typed_ir.no_entrypoints in
      let tr :=
        unparse_ty_and_entrypoints_uncarbonated loc_value utr
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_lambda, [ ta; tr ])
    | Script_typed_ir.Option_t ut _meta _
      let ut :=
        unparse_ty_and_entrypoints_uncarbonated loc_value ut
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_option, [ ut ])
    | Script_typed_ir.List_t ut _meta
      let t_value :=
        unparse_ty_and_entrypoints_uncarbonated loc_value ut
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_list, [ t_value ])
    | Script_typed_ir.Ticket_t ut _meta
      let t_value := unparse_comparable_ty_uncarbonated loc_value ut in
      (Michelson_v1_primitives.T_ticket, [ t_value ])
    | Script_typed_ir.Set_t ut _meta
      let t_value := unparse_comparable_ty_uncarbonated loc_value ut in
      (Michelson_v1_primitives.T_set, [ t_value ])
    | Script_typed_ir.Map_t uta utr _meta
      let ta := unparse_comparable_ty_uncarbonated loc_value uta in
      let tr :=
        unparse_ty_and_entrypoints_uncarbonated loc_value utr
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_map, [ ta; tr ])
    | Script_typed_ir.Big_map_t uta utr _meta
      let ta := unparse_comparable_ty_uncarbonated loc_value uta in
      let tr :=
        unparse_ty_and_entrypoints_uncarbonated loc_value utr
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_big_map, [ ta; tr ])
    | Script_typed_ir.Sapling_transaction_t memo_size
      (Michelson_v1_primitives.T_sapling_transaction,
        [ unparse_memo_size loc_value memo_size ])
    | Script_typed_ir.Sapling_transaction_deprecated_t memo_size
      (Michelson_v1_primitives.T_sapling_transaction_deprecated,
        [ unparse_memo_size loc_value memo_size ])
    | Script_typed_ir.Sapling_state_t memo_size
      (Michelson_v1_primitives.T_sapling_state,
        [ unparse_memo_size loc_value memo_size ])
    | Script_typed_ir.Chest_key_t(Michelson_v1_primitives.T_chest_key, nil)
    | Script_typed_ir.Chest_t(Michelson_v1_primitives.T_chest, nil)
    end in
  let annot :=
    match at_node with
    | Nonenil
    |
      Some {|
        Script_typed_ir.entrypoint_info.name := name;
          Script_typed_ir.entrypoint_info.original_type_expr := _
          |} ⇒ [ Alpha_context.Entrypoint.unparse_as_field_annot name ]
    end in
  Micheline.Prim loc_value name args annot

where "'unparse_comparable_ty_uncarbonated" :=
  (fun (loc : Set) ⇒ fun
    (loc_value : loc) (ty_value : Script_typed_ir.comparable_ty) ⇒
    unparse_ty_and_entrypoints_uncarbonated loc_value ty_value
      Script_typed_ir.no_entrypoints).

Definition unparse_comparable_ty_uncarbonated {loc : Set} :=
  'unparse_comparable_ty_uncarbonated loc.

Definition unparse_ty_uncarbonated {A : Set}
  (loc_value : A) (ty_value : Script_typed_ir.ty)
  : Alpha_context.Script.michelson_node A :=
  unparse_ty_and_entrypoints_uncarbonated loc_value ty_value
    Script_typed_ir.no_entrypoints.

Definition unparse_ty {A : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (ty_value : Script_typed_ir.ty)
  : M? (Alpha_context.Script.michelson_node A × Alpha_context.context) :=
  let? ctxt :=
    Alpha_context.Gas.consume ctxt (Unparse_costs.unparse_type ty_value) in
  return? ((unparse_ty_uncarbonated loc_value ty_value), ctxt).

Definition unparse_parameter_ty {A : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (ty_value : Script_typed_ir.ty)
  (entrypoints : Script_typed_ir.entrypoints)
  : M? (Alpha_context.Script.michelson_node A × Alpha_context.context) :=
  let? ctxt :=
    Alpha_context.Gas.consume ctxt (Unparse_costs.unparse_type ty_value) in
  return?
    ((unparse_ty_and_entrypoints_uncarbonated loc_value ty_value
      entrypoints.(Script_typed_ir.entrypoints.root)), ctxt).

Definition serialize_ty_for_error (ty_value : Script_typed_ir.ty)
  : Micheline.canonical Alpha_context.Script.prim :=
  Micheline.strip_locations (unparse_ty_uncarbonated tt ty_value).

Fixpoint unparse_stack_uncarbonated
  (function_parameter : Script_typed_ir.stack_ty)
  : list Alpha_context.Script.expr :=
  match function_parameter with
  | Script_typed_ir.Bot_tnil
  | Script_typed_ir.Item_t ty_value rest
    let uty := unparse_ty_uncarbonated tt ty_value in
    let urest := unparse_stack_uncarbonated rest in
    cons (Micheline.strip_locations uty) urest
  end.

Definition serialize_stack_for_error
  (ctxt : Alpha_context.context) (stack_ty : Script_typed_ir.stack_ty)
  : list Alpha_context.Script.expr :=
  match Alpha_context.Gas.level ctxt with
  | Alpha_context.Gas.Unaccountedunparse_stack_uncarbonated stack_ty
  | Alpha_context.Gas.Limited _nil
  end.

Definition unparse_unit {A B C : Set}
  (loc_value : A) (ctxt : B) (function_parameter : unit)
  : Pervasives.result (Micheline.node A Michelson_v1_primitives.prim × B) C :=
  let '_ := function_parameter in
  return?
    ((Micheline.Prim loc_value Michelson_v1_primitives.D_Unit nil nil), ctxt).

Definition unparse_int {A B C D : Set}
  (loc_value : A) (ctxt : B) (v_value : Script_int.num)
  : Pervasives.result (Micheline.node A C × B) D :=
  return? ((Micheline.Int loc_value (Script_int.to_zint v_value)), ctxt).

Definition unparse_nat {A B C D : Set}
  (loc_value : A) (ctxt : B) (v_value : Script_int.num)
  : Pervasives.result (Micheline.node A C × B) D :=
  return? ((Micheline.Int loc_value (Script_int.to_zint v_value)), ctxt).

Definition unparse_string {A B C D : Set}
  (loc_value : A) (ctxt : B) (s_value : Script_string.t)
  : Pervasives.result (Micheline.node A C × B) D :=
  return? ((Micheline.String loc_value (Script_string.to_string s_value)), ctxt).

Definition unparse_bytes {A B C D : Set}
  (loc_value : A) (ctxt : B) (s_value : bytes)
  : Pervasives.result (Micheline.node A C × B) D :=
  return? ((Micheline.Bytes loc_value s_value), ctxt).

Definition unparse_bool {A B C : Set}
  (loc_value : A) (ctxt : B) (b_value : bool)
  : Pervasives.result (Micheline.node A Michelson_v1_primitives.prim × B) C :=
  return?
    ((Micheline.Prim loc_value
      (if b_value then
        Michelson_v1_primitives.D_True
      else
        Michelson_v1_primitives.D_False) nil nil), ctxt).

Definition unparse_timestamp {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (t_value : Script_timestamp.t)
  : M? (Micheline.node A B × Alpha_context.context) :=
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    return? ((Micheline.Int loc_value (Script_timestamp.to_zint t_value)), ctxt)
  | Readable
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.timestamp_readable
      in
    match Script_timestamp.to_notation t_value with
    | None
      return?
        ((Micheline.Int loc_value (Script_timestamp.to_zint t_value)), ctxt)
    | Some s_valuereturn? ((Micheline.String loc_value s_value), ctxt)
    end
  end.

Definition unparse_address {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (function_parameter : Script_typed_ir.address)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let '{|
    Script_typed_ir.address.destination := destination;
      Script_typed_ir.address.entrypoint := entrypoint
      |} := function_parameter in
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.contract_optimized
      in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None
        (Data_encoding.tup2 Alpha_context.Destination.encoding
          Alpha_context.Entrypoint.value_encoding) (destination, entrypoint) in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.contract_readable
      in
    let notation :=
      Pervasives.op_caret (Alpha_context.Destination.to_b58check destination)
        (Alpha_context.Entrypoint.to_address_suffix entrypoint) in
    return? ((Micheline.String loc_value notation), ctxt)
  end.

Definition unparse_tx_rollup_l2_address {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (tx_address : Script_typed_ir.tx_rollup_l2_address)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let tx_address := Indexable.to_value tx_address in
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.contract_optimized
      in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None Tx_rollup_l2_address.encoding
        tx_address in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.contract_readable
      in
    let b58check := Tx_rollup_l2_address.to_b58check tx_address in
    return? ((Micheline.String loc_value b58check), ctxt)
  end.

Definition unparse_contract {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (typed_contract : Script_typed_ir.typed_contract)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let destination := Script_typed_ir.Typed_contract.destination typed_contract
    in
  let entrypoint := Script_typed_ir.Typed_contract.entrypoint typed_contract in
  let address :=
    {| Script_typed_ir.address.destination := destination;
      Script_typed_ir.address.entrypoint := entrypoint; |} in
  unparse_address loc_value ctxt mode address.

Definition unparse_signature {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (s_value : Script_typed_ir.Script_signature.t)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let s_value := Script_typed_ir.Script_signature.get s_value in
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt :=
      Alpha_context.Gas.consume ctxt Unparse_costs.signature_optimized in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None Signature.encoding s_value in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.signature_readable
      in
    return? ((Micheline.String loc_value (Signature.to_b58check s_value)), ctxt)
  end.

Definition unparse_mutez {A B C D : Set}
  (loc_value : A) (ctxt : B) (v_value : Alpha_context.Tez.tez)
  : Pervasives.result (Micheline.node A C × B) D :=
  return?
    ((Micheline.Int loc_value (Z.of_int64 (Alpha_context.Tez.to_mutez v_value))),
      ctxt).

Definition unparse_key {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (k_value : Signature.public_key)
  : M? (Micheline.node A B × Alpha_context.context) :=
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt :=
      Alpha_context.Gas.consume ctxt Unparse_costs.public_key_optimized in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None
        Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding) k_value in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable
    let? ctxt :=
      Alpha_context.Gas.consume ctxt Unparse_costs.public_key_readable in
    return?
      ((Micheline.String loc_value
        (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.to_b58check) k_value)),
        ctxt)
  end.

Definition unparse_key_hash {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (k_value : Signature.public_key_hash)
  : M? (Micheline.node A B × Alpha_context.context) :=
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.key_hash_optimized
      in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding) k_value
      in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.key_hash_readable
      in
    return?
      ((Micheline.String loc_value
        (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check)
          k_value)), ctxt)
  end.

Definition unparse_operation {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context)
  (function_parameter : Script_typed_ir.operation)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let '{|
    Script_typed_ir.operation.piop := piop;
      Script_typed_ir.operation.lazy_storage_diff := _
      |} := function_parameter in
  let iop := Apply_internal_results.packed_internal_operation_value piop in
  let bytes_value :=
    Data_encoding.Binary.to_bytes_exn None
      Apply_internal_results.internal_operation_encoding iop in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt (Unparse_costs.operation bytes_value) in
  return? ((Micheline.Bytes loc_value bytes_value), ctxt).

Definition unparse_chain_id {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (chain_id : Script_typed_ir.Script_chain_id.t)
  : M? (Micheline.node A B × Alpha_context.context) :=
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.chain_id_optimized
      in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None
        Script_typed_ir.Script_chain_id.encoding chain_id in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.chain_id_readable
      in
    return?
      ((Micheline.String loc_value
        (Script_typed_ir.Script_chain_id.to_b58check chain_id)), ctxt)
  end.

Definition unparse_bls12_381_g1 {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context)
  (x_value : Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.t))
  : M? (Micheline.node A B × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.bls12_381_g1 in
  let bytes_value :=
    Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.to_bytes)
      x_value in
  return? ((Micheline.Bytes loc_value bytes_value), ctxt).

Definition unparse_bls12_381_g2 {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context)
  (x_value : Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.t))
  : M? (Micheline.node A B × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.bls12_381_g2 in
  let bytes_value :=
    Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.to_bytes)
      x_value in
  return? ((Micheline.Bytes loc_value bytes_value), ctxt).

Definition unparse_bls12_381_fr {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context)
  (x_value : Script_typed_ir.Script_bls.Fr.t)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.bls12_381_fr in
  let bytes_value := Script_typed_ir.Script_bls.Fr.to_bytes x_value in
  return? ((Micheline.Bytes loc_value bytes_value), ctxt).

Definition unparse_with_data_encoding {A B C : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (s_value : B)
  (unparse_cost : Alpha_context.Gas.cost) (encoding : Data_encoding.encoding B)
  : M? (Micheline.node A C × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt unparse_cost in
  let bytes_value := Data_encoding.Binary.to_bytes_exn None encoding s_value in
  return? ((Micheline.Bytes loc_value bytes_value), ctxt).

Inductive comb_witness : Set :=
| Comb_Pair : comb_witness comb_witness
| Comb_Any : comb_witness.

Definition unparse_pair {A B C D E r G : Set}
  (loc_value : A)
  (unparse_l :
    B C
    Pervasives.result (Micheline.node A Michelson_v1_primitives.prim × D) E)
  (unparse_r :
    D r
    Pervasives.result (Micheline.node A Michelson_v1_primitives.prim × G) E)
  (ctxt : B) (mode : unparsing_mode) (r_comb_witness : comb_witness)
  (function_parameter : C × r)
  : Pervasives.result (Micheline.node A Michelson_v1_primitives.prim × G) E :=
  let '(l_value, r_value) := function_parameter in
  let? '(l_value, ctxt) := unparse_l ctxt l_value in
  let? '(r_value, ctxt) := unparse_r ctxt r_value in
  let res :=
    match (mode, r_comb_witness, r_value) with
    | (Optimized, Comb_Pair _, Micheline.Seq _ r_value)
      Micheline.Seq loc_value (cons l_value r_value)
    |
      (Optimized, Comb_Pair (Comb_Pair _),
        Micheline.Prim _ Michelson_v1_primitives.D_Pair
          (cons x2
            (cons
              (Micheline.Prim _ Michelson_v1_primitives.D_Pair
                (cons x3 (cons x4 [])) []) [])) [])
      Micheline.Seq loc_value [ l_value; x2; x3; x4 ]
    |
      (Readable, Comb_Pair _,
        Micheline.Prim _ Michelson_v1_primitives.D_Pair xs [])
      Micheline.Prim loc_value Michelson_v1_primitives.D_Pair (cons l_value xs)
        nil
    | _
      Micheline.Prim loc_value Michelson_v1_primitives.D_Pair
        [ l_value; r_value ] nil
    end in
  return? (res, ctxt).

Definition unparse_union {A B C D E F : Set}
  (loc_value : A)
  (unparse_l :
    B C
    Pervasives.result (Micheline.node A Michelson_v1_primitives.prim × D) E)
  (unparse_r :
    B F
    Pervasives.result (Micheline.node A Michelson_v1_primitives.prim × D) E)
  (ctxt : B) (function_parameter : Script_typed_ir.union C F)
  : Pervasives.result (Micheline.node A Michelson_v1_primitives.prim × D) E :=
  match function_parameter with
  | Script_typed_ir.L l_value
    let? '(l_value, ctxt) := unparse_l ctxt l_value in
    return?
      ((Micheline.Prim loc_value Michelson_v1_primitives.D_Left [ l_value ] nil),
        ctxt)
  | Script_typed_ir.R r_value
    let? '(r_value, ctxt) := unparse_r ctxt r_value in
    return?
      ((Micheline.Prim loc_value Michelson_v1_primitives.D_Right [ r_value ] nil),
        ctxt)
  end.

Definition unparse_option {A B C D : Set}
  (loc_value : A)
  (unparse_v :
    B C
    Pervasives.result (Micheline.node A Michelson_v1_primitives.prim × B) D)
  (ctxt : B) (function_parameter : option C)
  : Pervasives.result (Micheline.node A Michelson_v1_primitives.prim × B) D :=
  match function_parameter with
  | Some v_value
    let? '(v_value, ctxt) := unparse_v ctxt v_value in
    return?
      ((Micheline.Prim loc_value Michelson_v1_primitives.D_Some [ v_value ] nil),
        ctxt)
  | None
    return?
      ((Micheline.Prim loc_value Michelson_v1_primitives.D_None nil nil), ctxt)
  end.

Definition comb_witness2 (function_parameter : Script_typed_ir.ty)
  : comb_witness :=
  match function_parameter with
  | Script_typed_ir.Pair_t _ (Script_typed_ir.Pair_t _ _ _ _) _ _
    Comb_Pair (Comb_Pair Comb_Any)
  | Script_typed_ir.Pair_t _ _ _ _Comb_Pair Comb_Any
  | _Comb_Any
  end.

#[bypass_check(guard)]
Fixpoint unparse_comparable_data_rec {loc a : Set}
  (loc_value : loc) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (ty_value : Script_typed_ir.comparable_ty) (a_value : a) {struct ty_value}
  : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.unparse_data_cycle
    in
  match (ty_value, a_value) with
  | (Script_typed_ir.Unit_t, v_value)
    let v_value := cast unit v_value in
    unparse_unit loc_value ctxt v_value
  | (Script_typed_ir.Int_t, v_value)
    let v_value := cast Script_int.num v_value in
    unparse_int loc_value ctxt v_value
  | (Script_typed_ir.Nat_t, v_value)
    let v_value := cast Script_int.num v_value in
    unparse_nat loc_value ctxt v_value
  | (Script_typed_ir.String_t, s_value)
    let s_value := cast Script_string.t s_value in
    unparse_string loc_value ctxt s_value
  | (Script_typed_ir.Bytes_t, s_value)
    let s_value := cast bytes s_value in
    unparse_bytes loc_value ctxt s_value
  | (Script_typed_ir.Bool_t, b_value)
    let b_value := cast bool b_value in
    unparse_bool loc_value ctxt b_value
  | (Script_typed_ir.Timestamp_t, t_value)
    let t_value := cast Script_timestamp.t t_value in
    unparse_timestamp loc_value ctxt mode t_value
  | (Script_typed_ir.Address_t, address)
    let address := cast Script_typed_ir.address address in
    unparse_address loc_value ctxt mode address
  | (Script_typed_ir.Tx_rollup_l2_address_t, address)
    let address := cast Script_typed_ir.tx_rollup_l2_address address in
    unparse_tx_rollup_l2_address loc_value ctxt mode address
  | (Script_typed_ir.Signature_t, s_value)
    let s_value := cast Script_typed_ir.Script_signature.t s_value in
    unparse_signature loc_value ctxt mode s_value
  | (Script_typed_ir.Mutez_t, v_value)
    let v_value := cast Tez_repr.t v_value in
    unparse_mutez loc_value ctxt v_value
  | (Script_typed_ir.Key_t, k_value)
    let k_value := cast Alpha_context.public_key k_value in
    unparse_key loc_value ctxt mode k_value
  | (Script_typed_ir.Key_hash_t, k_value)
    let k_value := cast Alpha_context.public_key_hash k_value in
    unparse_key_hash loc_value ctxt mode k_value
  | (Script_typed_ir.Chain_id_t, chain_id)
    let chain_id := cast Script_typed_ir.Script_chain_id.t chain_id in
    unparse_chain_id loc_value ctxt mode chain_id
  | (Script_typed_ir.Pair_t tl tr _ Dependent_bool.YesYes, pair_value)
    let 'existT _ [__0, __1] [pair_value, tr, tl] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__0, __1]
          [__0 × __1 ** Script_typed_ir.ty ** Script_typed_ir.ty])
        [pair_value, tr, tl] in
    let r_witness := comb_witness2 tr in
    let unparse_l (ctxt : Alpha_context.context) (v_value : __0)
      : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
      unparse_comparable_data_rec loc_value ctxt mode tl v_value in
    let unparse_r (ctxt : Alpha_context.context) (v_value : __1)
      : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
      unparse_comparable_data_rec loc_value ctxt mode tr v_value in
    unparse_pair loc_value unparse_l unparse_r ctxt mode r_witness pair_value
  | (Script_typed_ir.Union_t tl tr _ Dependent_bool.YesYes, v_value)
    let 'existT _ [__2, __3] [v_value, tr, tl] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__2, __3]
          [Script_typed_ir.union __2 __3 ** Script_typed_ir.ty **
            Script_typed_ir.ty]) [v_value, tr, tl] in
    let unparse_l (ctxt : Alpha_context.context) (v_value : __2)
      : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
      unparse_comparable_data_rec loc_value ctxt mode tl v_value in
    let unparse_r (ctxt : Alpha_context.context) (v_value : __3)
      : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
      unparse_comparable_data_rec loc_value ctxt mode tr v_value in
    unparse_union loc_value unparse_l unparse_r ctxt v_value
  | (Script_typed_ir.Option_t t_value _ Dependent_bool.Yes, v_value)
    let 'existT _ __4 [v_value, t_value] :=
      cast_exists (Es := Set) (fun __4[option __4 ** Script_typed_ir.ty])
        [v_value, t_value] in
    let unparse_v (ctxt : Alpha_context.context) (v_value : __4)
      : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
      unparse_comparable_data_rec loc_value ctxt mode t_value v_value in
    unparse_option loc_value unparse_v ctxt v_value
  | _unreachable_gadt_branch
  end.

Definition account_for_future_serialization_cost {A : Set}
  (unparsed_data : Alpha_context.Script.michelson_node A)
  (ctxt : Alpha_context.context)
  : M? (Micheline.canonical Alpha_context.Script.prim × Alpha_context.context) :=
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.strip_locations_cost unparsed_data) in
  let unparsed_data := Micheline.strip_locations unparsed_data in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.micheline_serialization_cost unparsed_data) in
  return? (unparsed_data, ctxt).

Module MICHELSON_PARSER.
  Record signature : Set := {
    opened_ticket_type :
      Alpha_context.Script.location Script_typed_ir.comparable_ty
      M? Script_typed_ir.comparable_ty;
    parse_packable_ty_aux :
      Alpha_context.context int bool Alpha_context.Script.node
      M? (Script_typed_ir.ex_ty × Alpha_context.context);
    parse_data_aux :
       {a : Set},
      Script_ir_translator_config.elab_config int Alpha_context.context
      bool Script_typed_ir.ty Alpha_context.Script.node
      M? (a × Alpha_context.t);
  }.
End MICHELSON_PARSER.
Definition MICHELSON_PARSER := MICHELSON_PARSER.signature.

Module DATA_UNPARSER.
  Record signature : Set := {
    
[unparse_data_aux ctxt ~stack_depth unparsing_mode ty data] returns the Micheline representation of [data] of type [ty], consuming an appropriate amount of gas from [ctxt].
    unparse_data_aux :
       {a : Set},
      Alpha_context.context int unparsing_mode Script_typed_ir.ty
      a M? (Alpha_context.Script.expr × Alpha_context.context);
    
[unparse_items_aux ctxt ~stack_depth unparsing_mode kty vty assoc] returns the Micheline representation of [assoc] (being an association list) with keys of type [kty] and values of type [vty]. Gas is being consumed from [ctxt].
    unparse_items_aux :
       {k v : Set},
      Alpha_context.context int unparsing_mode
      Script_typed_ir.comparable_ty Script_typed_ir.ty list (k × v)
      M? (list Alpha_context.Script.expr × Alpha_context.context);
    
[unparse_code_aux ctxt ~stack_depth unparsing_mode code] returns [code] with [I_PUSH] instructions parsed and unparsed back to make sure that only forgeable values are being pushed. The gas is being consumed from [ctxt].
    unparse_code_aux :
      Alpha_context.context int unparsing_mode
      Alpha_context.Script.node
      M? (Alpha_context.Script.expr × Alpha_context.context);
  }.
End DATA_UNPARSER.
Definition DATA_UNPARSER := DATA_UNPARSER.signature.

Module Data_unparser.
  Class FArgs := {
    P : MICHELSON_PARSER;
  }.

  Reserved Notation "'unparse_items_rec".

  #[bypass_check(guard)]
  Fixpoint unparse_data_rec `{FArgs} {a : Set}
    (ctxt : Alpha_context.context) (stack_depth : int) (mode : unparsing_mode)
    (ty_value : Script_typed_ir.ty) (a_value : a) {struct ctxt}
    : M? (Alpha_context.Script.node × Alpha_context.context) :=
    let unparse_items_rec {k v} := 'unparse_items_rec k v in
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.unparse_data_cycle
      in
    let non_terminal_recursion {B : Set}
      (ctxt : Alpha_context.context) (mode : unparsing_mode)
      (ty_value : Script_typed_ir.ty) (a_value : B)
      : M? (Alpha_context.Script.node × Alpha_context.context) :=
      if stack_depth >i 10000 then
        Error_monad.fail
          (Build_extensible "Unparsing_too_many_recursive_calls" unit tt)
      else
        unparse_data_rec ctxt (stack_depth +i 1) mode ty_value a_value in
    let loc_value := Micheline.dummy_location in
    match (ty_value, a_value) with
    | (Script_typed_ir.Unit_t, v_value)
      let v_value := cast unit v_value in
      unparse_unit loc_value ctxt v_value
    | (Script_typed_ir.Int_t, v_value)
      let v_value := cast Script_int.num v_value in
      unparse_int loc_value ctxt v_value
    | (Script_typed_ir.Nat_t, v_value)
      let v_value := cast Script_int.num v_value in
      unparse_nat loc_value ctxt v_value
    | (Script_typed_ir.String_t, s_value)
      let s_value := cast Script_string.t s_value in
      unparse_string loc_value ctxt s_value
    | (Script_typed_ir.Bytes_t, s_value)
      let s_value := cast bytes s_value in
      unparse_bytes loc_value ctxt s_value
    | (Script_typed_ir.Bool_t, b_value)
      let b_value := cast bool b_value in
      unparse_bool loc_value ctxt b_value
    | (Script_typed_ir.Timestamp_t, t_value)
      let t_value := cast Script_timestamp.t t_value in
      unparse_timestamp loc_value ctxt mode t_value
    | (Script_typed_ir.Address_t, address)
      let address := cast Script_typed_ir.address address in
      unparse_address loc_value ctxt mode address
    | (Script_typed_ir.Tx_rollup_l2_address_t, address)
      let address := cast Script_typed_ir.tx_rollup_l2_address address in
      unparse_tx_rollup_l2_address loc_value ctxt mode address
    | (Script_typed_ir.Contract_t _ _, contract)
      let contract := cast Script_typed_ir.typed_contract contract in
      unparse_contract loc_value ctxt mode contract
    | (Script_typed_ir.Signature_t, s_value)
      let s_value := cast Script_typed_ir.signature s_value in
      unparse_signature loc_value ctxt mode s_value
    | (Script_typed_ir.Mutez_t, v_value)
      let v_value := cast Tez_repr.t v_value in
      unparse_mutez loc_value ctxt v_value
    | (Script_typed_ir.Key_t, k_value)
      let k_value := cast Alpha_context.public_key k_value in
      unparse_key loc_value ctxt mode k_value
    | (Script_typed_ir.Key_hash_t, k_value)
      let k_value := cast Alpha_context.public_key_hash k_value in
      unparse_key_hash loc_value ctxt mode k_value
    | (Script_typed_ir.Operation_t, operation)
      let operation := cast Script_typed_ir.operation operation in
      unparse_operation loc_value ctxt operation
    | (Script_typed_ir.Chain_id_t, chain_id)
      let chain_id := cast Script_typed_ir.Script_chain_id.t chain_id in
      unparse_chain_id loc_value ctxt mode chain_id
    | (Script_typed_ir.Bls12_381_g1_t, x_value)
      let x_value :=
        cast Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.t)
          x_value in
      unparse_bls12_381_g1 loc_value ctxt x_value
    | (Script_typed_ir.Bls12_381_g2_t, x_value)
      let x_value :=
        cast Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.t)
          x_value in
      unparse_bls12_381_g2 loc_value ctxt x_value
    | (Script_typed_ir.Bls12_381_fr_t, x_value)
      let x_value := cast Script_typed_ir.Script_bls.Fr.t x_value in
      unparse_bls12_381_fr loc_value ctxt x_value
    | (Script_typed_ir.Pair_t tl tr _ _, pair_value)
      let 'existT _ [__1, __2] [pair_value, tr, tl] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__1, __2]
            [__1 × __2 ** Script_typed_ir.ty ** Script_typed_ir.ty])
          [pair_value, tr, tl] in
      let r_witness := comb_witness2 tr in
      let unparse_l (ctxt : Alpha_context.context) (v_value : __1)
        : M? (Alpha_context.Script.node × Alpha_context.context) :=
        non_terminal_recursion ctxt mode tl v_value in
      let unparse_r (ctxt : Alpha_context.context) (v_value : __2)
        : M? (Alpha_context.Script.node × Alpha_context.context) :=
        non_terminal_recursion ctxt mode tr v_value in
      unparse_pair loc_value unparse_l unparse_r ctxt mode r_witness pair_value
    | (Script_typed_ir.Union_t tl tr _ _, v_value)
      let 'existT _ [__3, __4] [v_value, tr, tl] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__3, __4]
            [Script_typed_ir.union __3 __4 ** Script_typed_ir.ty **
              Script_typed_ir.ty]) [v_value, tr, tl] in
      let unparse_l (ctxt : Alpha_context.context) (v_value : __3)
        : M? (Alpha_context.Script.node × Alpha_context.context) :=
        non_terminal_recursion ctxt mode tl v_value in
      let unparse_r (ctxt : Alpha_context.context) (v_value : __4)
        : M? (Alpha_context.Script.node × Alpha_context.context) :=
        non_terminal_recursion ctxt mode tr v_value in
      unparse_union loc_value unparse_l unparse_r ctxt v_value
    | (Script_typed_ir.Option_t t_value _ _, v_value)
      let 'existT _ __5 [v_value, t_value] :=
        cast_exists (Es := Set) (fun __5[option __5 ** Script_typed_ir.ty])
          [v_value, t_value] in
      let unparse_v (ctxt : Alpha_context.context) (v_value : __5)
        : M? (Alpha_context.Script.node × Alpha_context.context) :=
        non_terminal_recursion ctxt mode t_value v_value in
      unparse_option loc_value unparse_v ctxt v_value
    | (Script_typed_ir.List_t t_value _, items)
      let 'existT _ __6 [items, t_value] :=
        cast_exists (Es := Set)
          (fun __6[Script_typed_ir.boxed_list __6 ** Script_typed_ir.ty])
          [items, t_value] in
      let? '(items, ctxt) :=
        List.fold_left_es
          (fun (function_parameter :
            list Alpha_context.Script.node × Alpha_context.context) ⇒
            let '(l_value, ctxt) := function_parameter in
            fun (element : __6) ⇒
              let? '(unparsed, ctxt) :=
                non_terminal_recursion ctxt mode t_value element in
              return? ((cons unparsed l_value), ctxt)) (nil, ctxt)
          items.(Script_typed_ir.boxed_list.elements) in
      return? ((Micheline.Seq loc_value (List.rev items)), ctxt)
    | (Script_typed_ir.Ticket_t t_value _, x_value)
      let 'existT _ __7 [x_value, t_value] :=
        cast_exists (Es := Set)
          (fun __7
            [Script_typed_ir.ticket __7 ** Script_typed_ir.comparable_ty])
          [x_value, t_value] in
      let '{|
        Script_typed_ir.ticket.ticketer := ticketer;
          Script_typed_ir.ticket.contents := contents;
          Script_typed_ir.ticket.amount := amount
          |} := x_value in
      let? t_value := P.(MICHELSON_PARSER.opened_ticket_type) loc_value t_value
        in
      let destination := Alpha_context.Destination.Contract ticketer in
      let addr :=
        {| Script_typed_ir.address.destination := destination;
          Script_typed_ir.address.entrypoint :=
            Alpha_context.Entrypoint.default; |} in
      unparse_data_rec ctxt stack_depth mode t_value (addr, (contents, amount))
    | (Script_typed_ir.Set_t t_value _, set)
      let 'existT _ __8 [set, t_value] :=
        cast_exists (Es := Set)
          (fun __8[Script_typed_ir.set __8 ** Script_typed_ir.comparable_ty])
          [set, t_value] in
      let? '(items, ctxt) :=
        List.fold_left_es
          (fun (function_parameter :
            list
              (Micheline.node Micheline.canonical_location
                Alpha_context.Script.prim) × Alpha_context.context) ⇒
            let '(l_value, ctxt) := function_parameter in
            fun (item : __8) ⇒
              let? '(item, ctxt) :=
                unparse_comparable_data_rec loc_value ctxt mode t_value item in
              return? ((cons item l_value), ctxt)) (nil, ctxt)
          (Script_set.fold
            (fun (e_value : __8) ⇒
              fun (acc_value : list __8) ⇒ cons e_value acc_value) set nil) in
      return? ((Micheline.Seq loc_value items), ctxt)
    | (Script_typed_ir.Map_t kt vt _, map)
      let 'existT _ [__9, __10] [map, vt, kt] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__9, __10]
            [Script_typed_ir.map __9 __10 ** Script_typed_ir.ty **
              Script_typed_ir.comparable_ty]) [map, vt, kt] in
      let items :=
        Script_map.fold
          (fun (k_value : __9) ⇒
            fun (v_value : __10) ⇒
              fun (acc_value : list (__9 × __10)) ⇒
                cons (k_value, v_value) acc_value) map nil in
      let? '(items, ctxt) :=
        unparse_items_rec ctxt (stack_depth +i 1) mode kt vt items in
      return? ((Micheline.Seq loc_value items), ctxt)
    | (Script_typed_ir.Big_map_t kt vt _, x_value)
      let 'existT _ [__11, __12] [x_value, vt, kt] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__11, __12]
            [Script_typed_ir.big_map ** Script_typed_ir.ty **
              Script_typed_ir.comparable_ty]) [x_value, vt, kt] in
      match
        (x_value,
          match x_value with
          |
            Script_typed_ir.Big_map {|
              Script_typed_ir.big_map.Big_map.id := Some id;
                Script_typed_ir.big_map.Big_map.diff := {|
                  Script_typed_ir.big_map_overlay.size := size_value
                    |}
                |} ⇒ size_value =i 0
          | _false
          end) with
      |
        (Script_typed_ir.Big_map {|
          Script_typed_ir.big_map.Big_map.id := Some id;
            Script_typed_ir.big_map.Big_map.diff := {|
              Script_typed_ir.big_map_overlay.size := size_value
                |}
            |}, true)
        let '[size_value, id] :=
          cast [int ** Alpha_context.Big_map.Id.t] [size_value, id] in
        return?
          ((Micheline.Int loc_value (Alpha_context.Big_map.Id.unparse_to_z id)),
            ctxt)
      |
        (Script_typed_ir.Big_map {|
          Script_typed_ir.big_map.Big_map.id := Some id;
            Script_typed_ir.big_map.Big_map.diff := {|
              Script_typed_ir.big_map_overlay.map := map
                |}
            |}, _)
        let '[map, id] :=
          cast
            [Script_typed_ir.Big_map_overlay.(Map.S.t) (__11 × option __12) **
              Alpha_context.Big_map.Id.t] [map, id] in
        let items :=
          Script_typed_ir.Big_map_overlay.(Map.S.fold)
            (fun (function_parameter : Script_expr_hash.t) ⇒
              let '_ := function_parameter in
              fun (function_parameter : __11 × option __12) ⇒
                let '(k_value, v_value) := function_parameter in
                fun (acc_value : list (__11 × option __12)) ⇒
                  cons (k_value, v_value) acc_value) map nil in
        let items :=
          List.sort
            (fun (function_parameter : __11 × option __12) ⇒
              let '(a_value, _) := function_parameter in
              fun (function_parameter : __11 × option __12) ⇒
                let '(b_value, _) := function_parameter in
                Script_comparable.compare_comparable kt b_value a_value) items
          in
        let? vt := Script_typed_ir.option_t loc_value vt in
        let? '(items, ctxt) :=
          unparse_items_rec ctxt (stack_depth +i 1) mode kt vt items in
        return?
          ((Micheline.Prim loc_value Michelson_v1_primitives.D_Pair
            [
              Micheline.Int loc_value (Alpha_context.Big_map.Id.unparse_to_z id);
              Micheline.Seq loc_value items
            ] nil), ctxt)
      |
        (Script_typed_ir.Big_map {|
          Script_typed_ir.big_map.Big_map.id := None;
            Script_typed_ir.big_map.Big_map.diff := {|
              Script_typed_ir.big_map_overlay.map := map
                |}
            |}, _)
        let map :=
          cast (Script_typed_ir.Big_map_overlay.(Map.S.t) (__11 × option __12))
            map in
        let items :=
          Script_typed_ir.Big_map_overlay.(Map.S.fold)
            (fun (function_parameter : Script_expr_hash.t) ⇒
              let '_ := function_parameter in
              fun (function_parameter : __11 × option __12) ⇒
                let '(k_value, v_value) := function_parameter in
                fun (acc_value : list (__11 × __12)) ⇒
                  match v_value with
                  | Noneacc_value
                  | Some v_valuecons (k_value, v_value) acc_value
                  end) map nil in
        let items :=
          List.sort
            (fun (function_parameter : __11 × __12) ⇒
              let '(a_value, _) := function_parameter in
              fun (function_parameter : __11 × __12) ⇒
                let '(b_value, _) := function_parameter in
                Script_comparable.compare_comparable kt b_value a_value) items
          in
        let? '(items, ctxt) :=
          unparse_items_rec ctxt (stack_depth +i 1) mode kt vt items in
        return? ((Micheline.Seq loc_value items), ctxt)
      end
    | (Script_typed_ir.Lambda_t _ _ _, x_value)
      let x_value := cast Script_typed_ir.lambda x_value in
      match x_value with
      | Script_typed_ir.Lam _ original_code
        unparse_code_rec ctxt (stack_depth +i 1) mode original_code
      | Script_typed_ir.LamRec _ original_code
        let? '(body, ctxt) :=
          unparse_code_rec ctxt (stack_depth +i 1) mode original_code in
        return?
          ((Micheline.Prim loc_value Michelson_v1_primitives.D_Lambda_rec
            [ body ] nil), ctxt)
      end
    | (Script_typed_ir.Sapling_transaction_t _, s_value)
      let s_value := cast Alpha_context.Sapling.transaction s_value in
      let? ctxt :=
        Alpha_context.Gas.consume ctxt
          (Unparse_costs.sapling_transaction s_value) in
      let bytes_value :=
        Data_encoding.Binary.to_bytes_exn None
          Alpha_context.Sapling.transaction_encoding s_value in
      return? ((Micheline.Bytes loc_value bytes_value), ctxt)
    | (Script_typed_ir.Sapling_transaction_deprecated_t _, s_value)
      let s_value := cast Sapling_repr.legacy_transaction s_value in
      let? ctxt :=
        Alpha_context.Gas.consume ctxt
          (Unparse_costs.sapling_transaction_deprecated s_value) in
      let bytes_value :=
        Data_encoding.Binary.to_bytes_exn None
          Alpha_context.Sapling.Legacy.transaction_encoding s_value in
      return? ((Micheline.Bytes loc_value bytes_value), ctxt)
    | (Script_typed_ir.Sapling_state_t _, x_value)
      let x_value := cast Alpha_context.Sapling.state x_value in
      let '{|
        Alpha_context.Sapling.state.id := id;
          Alpha_context.Sapling.state.diff := diff_value
          |} := x_value in
      let? ctxt :=
        Alpha_context.Gas.consume ctxt (Unparse_costs.sapling_diff diff_value)
        in
      return?
        (match diff_value with
        | {|
          Alpha_context.Sapling.diff.commitments_and_ciphertexts := [];
            Alpha_context.Sapling.diff.nullifiers := []
            |} ⇒
          match id with
          | NoneMicheline.Seq loc_value nil
          | Some id
            let id := Alpha_context.Sapling.Id.unparse_to_z id in
            Micheline.Int loc_value id
          end
        | diff_value
          let diff_bytes :=
            Data_encoding.Binary.to_bytes_exn None
              Alpha_context.Sapling.diff_encoding diff_value in
          let unparsed_diff {B : Set}
            : Micheline.node Micheline.canonical_location B :=
            Micheline.Bytes loc_value diff_bytes in
          match id with
          | Noneunparsed_diff
          | Some id
            let id := Alpha_context.Sapling.Id.unparse_to_z id in
            Micheline.Prim loc_value Michelson_v1_primitives.D_Pair
              [ Micheline.Int loc_value id; unparsed_diff ] nil
          end
        end, ctxt)
    | (Script_typed_ir.Chest_key_t, s_value)
      let s_value := cast Script_typed_ir.Script_timelock.chest_key s_value in
      unparse_with_data_encoding loc_value ctxt s_value
        Unparse_costs.chest_key_value
        Script_typed_ir.Script_timelock.chest_key_encoding
    | (Script_typed_ir.Chest_t, s_value)
      let s_value := cast Script_typed_ir.Script_timelock.chest s_value in
      unparse_with_data_encoding loc_value ctxt s_value
        (Unparse_costs.chest_value
          (Script_typed_ir.Script_timelock.get_plaintext_size s_value))
        Script_typed_ir.Script_timelock.chest_encoding
    | _unreachable_gadt_branch
    end
  
  with unparse_code_rec `{FArgs}
    (ctxt : Alpha_context.context) (stack_depth : int) (mode : unparsing_mode)
    (code : Alpha_context.Script.node) {struct ctxt}
    : M?
      (Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim
        × Alpha_context.context) :=
    let elab_conf := Script_ir_translator_config.make None None true tt in
    let? ctxt :=
      Alpha_context.Gas.consume ctxt Unparse_costs.unparse_instr_cycle in
    let non_terminal_recursion
      (ctxt : Alpha_context.context) (mode : unparsing_mode)
      (code : Alpha_context.Script.node)
      : M?
        (Micheline.node Micheline.canonical_location
          Michelson_v1_primitives.prim × Alpha_context.context) :=
      if stack_depth >i 10000 then
        Error_monad.fail
          (Build_extensible "Unparsing_too_many_recursive_calls" unit tt)
      else
        unparse_code_rec ctxt (stack_depth +i 1) mode code in
    match code with
    |
      Micheline.Prim loc_value Michelson_v1_primitives.I_PUSH
        (cons ty_value (cons data [])) annot
      let? '(Script_typed_ir.Ex_ty t_value, ctxt) :=
        P.(MICHELSON_PARSER.parse_packable_ty_aux) ctxt (stack_depth +i 1)
          elab_conf.(Script_ir_translator_config.elab_config.legacy) ty_value in
      let 'existT _ __Ex_ty_'a [ctxt, t_value] :=
        cast_exists (Es := Set)
          (fun __Ex_ty_'a[Alpha_context.context ** Script_typed_ir.ty])
          [ctxt, t_value] in
      let allow_forged := false in
      let? '(data, ctxt) :=
        P.(MICHELSON_PARSER.parse_data_aux) elab_conf (stack_depth +i 1) ctxt
          allow_forged t_value data in
      let? '(data, ctxt) :=
        unparse_data_rec ctxt (stack_depth +i 1) mode t_value
          (data : __Ex_ty_'a) in
      return?
        ((Micheline.Prim loc_value Michelson_v1_primitives.I_PUSH
          [ ty_value; data ] annot), ctxt)
    | Micheline.Seq loc_value items
      let? '(items, ctxt) :=
        List.fold_left_es
          (fun (function_parameter :
            list
              (Micheline.node Micheline.canonical_location
                Michelson_v1_primitives.prim) × Alpha_context.context) ⇒
            let '(l_value, ctxt) := function_parameter in
            fun (item : Alpha_context.Script.node) ⇒
              let? '(item, ctxt) := non_terminal_recursion ctxt mode item in
              return? ((cons item l_value), ctxt)) (nil, ctxt) items in
      return? ((Micheline.Seq loc_value (List.rev items)), ctxt)
    | Micheline.Prim loc_value prim items annot
      let? '(items, ctxt) :=
        List.fold_left_es
          (fun (function_parameter :
            list
              (Micheline.node Micheline.canonical_location
                Michelson_v1_primitives.prim) × Alpha_context.context) ⇒
            let '(l_value, ctxt) := function_parameter in
            fun (item : Alpha_context.Script.node) ⇒
              let? '(item, ctxt) := non_terminal_recursion ctxt mode item in
              return? ((cons item l_value), ctxt)) (nil, ctxt) items in
      return? ((Micheline.Prim loc_value prim (List.rev items) annot), ctxt)
    | (Micheline.Int _ _ | Micheline.String _ _ | Micheline.Bytes _ _) as atom
      ⇒ return? (atom, ctxt)
    end
  
  where "'unparse_items_rec" :=
    (fun (k v : Set) ⇒ fun
      (ctxt : Alpha_context.context) (stack_depth : int) (mode : unparsing_mode)
      (kt : Script_typed_ir.comparable_ty) (vt : Script_typed_ir.ty)
      (items : list (k × v)) ⇒
      List.fold_left_es
        (fun (function_parameter :
          list Alpha_context.Script.node × Alpha_context.context) ⇒
          let '(l_value, ctxt) := function_parameter in
          fun (function_parameter : k × v) ⇒
            let '(k_value, v_value) := function_parameter in
            let loc_value := Micheline.dummy_location in
            let? '(key_value, ctxt) :=
              unparse_comparable_data_rec loc_value ctxt mode kt k_value in
            let? '(value_value, ctxt) :=
              unparse_data_rec ctxt (stack_depth +i 1) mode vt v_value in
            return?
              ((cons
                (Micheline.Prim loc_value Michelson_v1_primitives.D_Elt
                  [ key_value; value_value ] nil) l_value), ctxt)) (nil, ctxt)
        items).

  Definition unparse_items_rec `{FArgs} {k v : Set} := 'unparse_items_rec k v.

  Definition unparse_data_aux `{FArgs} {A : Set}
    (ctxt : Alpha_context.context) (stack_depth : int) (mode : unparsing_mode)
    (ty_value : Script_typed_ir.ty) (v_value : A)
    : M? (Micheline.canonical Alpha_context.Script.prim × Alpha_context.context) :=
    let? '(unparsed_data, ctxt) :=
      unparse_data_rec ctxt stack_depth mode ty_value v_value in
    account_for_future_serialization_cost unparsed_data ctxt.

  Definition unparse_code_aux `{FArgs}
    (ctxt : Alpha_context.context) (stack_depth : int) (mode : unparsing_mode)
    (v_value : Alpha_context.Script.node)
    : M? (Micheline.canonical Alpha_context.Script.prim × Alpha_context.context) :=
    let? '(unparsed_data, ctxt) :=
      unparse_code_rec ctxt stack_depth mode v_value in
    account_for_future_serialization_cost unparsed_data ctxt.

  Definition unparse_items_aux `{FArgs} {A B : Set}
    (ctxt : Alpha_context.context) (stack_depth : int) (mode : unparsing_mode)
    (ty_value : Script_typed_ir.comparable_ty) (vty : Script_typed_ir.ty)
    (vs : list (A × B))
    : M?
      (list (Micheline.canonical Alpha_context.Script.prim) ×
        Alpha_context.context) :=
    let? '(unparsed_datas, ctxt) :=
      unparse_items_rec ctxt stack_depth mode ty_value vty vs in
    let? '(unparsed_datas, ctxt) :=
      List.fold_left_e
        (fun (function_parameter :
          list (Micheline.canonical Alpha_context.Script.prim) ×
            Alpha_context.context) ⇒
          let '(acc_value, ctxt) := function_parameter in
          fun (unparsed_data :
            Alpha_context.Script.michelson_node Alpha_context.Script.location)
            ⇒
            let? '(unparsed_data, ctxt) :=
              account_for_future_serialization_cost unparsed_data ctxt in
            return? ((cons unparsed_data acc_value), ctxt)) (nil, ctxt)
        unparsed_datas in
    return? ((List.rev unparsed_datas), ctxt).

  (* Data_unparser *)
  Definition functor `{FArgs} :=
    {|
      DATA_UNPARSER.unparse_data_aux _ := unparse_data_aux;
      DATA_UNPARSER.unparse_items_aux _ _ := unparse_items_aux;
      DATA_UNPARSER.unparse_code_aux := unparse_code_aux
    |}.
End Data_unparser.
Definition Data_unparser (P : MICHELSON_PARSER) : DATA_UNPARSER :=
  let '_ := Data_unparser.Build_FArgs P in
  Data_unparser.functor.

Definition unparse_comparable_data {A : Set}
  (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (ty_value : Script_typed_ir.comparable_ty) (v_value : A)
  : M? (Micheline.canonical Alpha_context.Script.prim × Alpha_context.context) :=
  let? '(unparsed_data, ctxt) :=
    unparse_comparable_data_rec tt ctxt mode ty_value v_value in
  account_for_future_serialization_cost unparsed_data ctxt.