🍬 Script_ir_unparser.v | Coq Tezos of OCaml 💫

    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 :
      ∀ {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 :
      Alpha_context.context → int → unparsing_mode →
      Alpha_context.Script.node →
      M ? (Alpha_context.Script.expr × Alpha_context.context );
    Internal_for_benchmarking : S_Internal_for_benchmarking;
  }.
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.tzfail
          (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_list.t __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_list.t.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
                  | None ⇒ acc_value
                  | Some v_value ⇒ cons (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
          | None ⇒ Micheline.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
          | None ⇒ unparsed_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.tzfail
          (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).

  Module Internal_for_benchmarking.
    Definition unparse_data `{FArgs} {A : Set}
      : Alpha_context.context → int → unparsing_mode → Script_typed_ir.ty →
      A → M ? (Alpha_context.Script.node × Alpha_context.context ) :=
      unparse_data_rec.

    Definition unparse_code `{FArgs}
      : Alpha_context.context → int → unparsing_mode →
      Alpha_context.Script.node →
      M ?
        (Micheline.node Micheline.canonical_location
          Michelson_v1_primitives.prim × Alpha_context.context ) :=
      unparse_code_rec.

    (* Internal_for_benchmarking *)
    Definition module `{FArgs} :=
      {|
        S_Internal_for_benchmarking.unparse_data _ := unparse_data;
        S_Internal_for_benchmarking.unparse_code := unparse_code
      |}.
  End Internal_for_benchmarking.
  Definition Internal_for_benchmarking `{FArgs} :=
    Internal_for_benchmarking.module.

  (* 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;
      DATA_UNPARSER.Internal_for_benchmarking := Internal_for_benchmarking
    |}.
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.