diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index dbbb1f8d7f252250ea829589f5a55e9e9c10ae38..c8dbb9166664ce5e8d0eb6cd7d12023dcdc2d623 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml @@ -382,7 +382,7 @@ end) let* (Ex_ty right) = m_type ~size:rsize in match pair_t (-1) left right with | Error _ -> assert false - | Ok res_ty -> return @@ Ex_ty res_ty) + | Ok (Ty_ex_c res_ty) -> return @@ Ex_ty res_ty) | `TLambda -> ( let* (lsize, rsize) = pick_split (size - 1) in let* (Ex_ty domain) = m_type ~size:lsize in @@ -396,7 +396,7 @@ end) let* (Ex_ty right) = m_type ~size:rsize in match union_t (-1) left right with | Error _ -> assert false - | Ok res_ty -> return @@ Ex_ty res_ty) + | Ok (Ty_ex_c res_ty) -> return @@ Ex_ty res_ty) | `TOption -> ( let* (Ex_ty t) = m_type ~size:(size - 1) in match option_t (-1) t with @@ -556,18 +556,18 @@ end) | Bool_t -> Base_samplers.uniform_bool | Address_t -> address | Tx_rollup_l2_address_t -> tx_rollup_l2_address - | Pair_t (left_t, right_t, _) -> + | Pair_t (left_t, right_t, _, _) -> M.( let* left_v = value left_t in let* right_v = value right_t in return (left_v, right_v)) - | Union_t (left_t, right_t, _) -> + | Union_t (left_t, right_t, _, _) -> fun rng_state -> if Base_samplers.uniform_bool rng_state then L (value left_t rng_state) else R (value right_t rng_state) | Lambda_t (arg_ty, ret_ty, _) -> generate_lambda arg_ty ret_ty - | Option_t (ty, _) -> + | Option_t (ty, _, _) -> fun rng_state -> if Base_samplers.uniform_bool rng_state then None else Some (value ty rng_state) diff --git a/src/proto_alpha/lib_benchmark/test/test_distribution.ml b/src/proto_alpha/lib_benchmark/test/test_distribution.ml index 9253c16d3902639361b083b9a0bf9f228ab7ddf4..2dee94ce5adba393a239b3261e688bc659cb21ac 100644 --- a/src/proto_alpha/lib_benchmark/test/test_distribution.ml +++ b/src/proto_alpha/lib_benchmark/test/test_distribution.ml @@ -71,13 +71,13 @@ let rec tnames_of_type : | Script_typed_ir.Address_t -> `TAddress :: acc | Script_typed_ir.Tx_rollup_l2_address_t -> `TTx_rollup_l2_address :: acc | Script_typed_ir.Bool_t -> `TBool :: acc - | Script_typed_ir.Pair_t (lty, rty, _) -> + | Script_typed_ir.Pair_t (lty, rty, _, _) -> tnames_of_type lty (tnames_of_type rty (`TPair :: acc)) - | Script_typed_ir.Union_t (lty, rty, _) -> + | Script_typed_ir.Union_t (lty, rty, _, _) -> tnames_of_type lty (tnames_of_type rty (`TUnion :: acc)) | Script_typed_ir.Lambda_t (dom, range, _) -> tnames_of_type dom (tnames_of_type range (`TLambda :: acc)) - | Script_typed_ir.Option_t (ty, _) -> tnames_of_type ty (`TOption :: acc) + | Script_typed_ir.Option_t (ty, _, _) -> tnames_of_type ty (`TOption :: acc) | Script_typed_ir.List_t (ty, _) -> tnames_of_type ty (`TList :: acc) | Script_typed_ir.Set_t (ty, _) -> tnames_of_comparable_type ty (`TSet :: acc) | Script_typed_ir.Map_t (kty, vty, _) -> diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml index 53d3028f379ab983a27d248b883596e6eb1bb6dd..1a91337abea3e293973554bdb3edd53887ed9e73 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml @@ -850,7 +850,7 @@ module Registration_section = struct else match comb_acc with | Ex_value {value; ty} -> - let ty = pair unit ty in + let (Ty_ex_c ty) = pair unit ty in make_comb (comb_width - 1) (Ex_value {value = ((), value); ty}) let () = @@ -2178,7 +2178,7 @@ module Registration_section = struct let () = let lambda = let open Script_typed_ir in - let pair_list_operation_unit = pair (list operation) unit in + let (Ty_ex_c pair_list_operation_unit) = pair (list operation) unit in let descr = { kloc = 0; @@ -2462,8 +2462,10 @@ module Registration_section = struct let kinstr = let spl_state = sapling_state memo_size in let spl_tx = sapling_transaction memo_size in - let pair_int_spl_state = pair int spl_state in - let pair_bytes_pair_int_spl_state = pair bytes pair_int_spl_state in + let (Ty_ex_c pair_int_spl_state) = pair int spl_state in + let (Ty_ex_c pair_bytes_pair_int_spl_state) = + pair bytes pair_int_spl_state + in ISapling_verify_update ( kinfo (spl_tx @$ spl_state @$ bot), halt (option pair_bytes_pair_int_spl_state @$ bot) ) @@ -2668,7 +2670,7 @@ module Registration_section = struct () let () = - let pair_bls12_381_g1_g2 = pair bls12_381_g1 bls12_381_g2 in + let (Ty_ex_c pair_bls12_381_g1_g2) = pair bls12_381_g1 bls12_381_g2 in simple_benchmark ~name:Interpreter_workload.N_IPairing_check_bls12_381 ~kinstr: @@ -2697,7 +2699,9 @@ module Registration_section = struct let split_ticket_instr = let ticket_unit = ticket unit_cmp in - let pair_ticket_unit_ticket_unit = pair ticket_unit ticket_unit in + let (Ty_ex_c pair_ticket_unit_ticket_unit) = + pair ticket_unit ticket_unit + in ISplit_ticket ( kinfo (ticket_unit @$ cpair nat nat @$ bot), halt (option pair_ticket_unit_ticket_unit @$ bot) ) @@ -2745,7 +2749,7 @@ module Registration_section = struct let join_tickets_instr = let ticket_str = ticket string_cmp in - let pair_ticket_str_ticket_str = pair ticket_str ticket_str in + let (Ty_ex_c pair_ticket_str_ticket_str) = pair ticket_str ticket_str in IJoin_tickets ( kinfo (pair_ticket_str_ticket_str @$ bot), string_cmp, diff --git a/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml b/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml index f8fcd1d897fe0eb423b33dc0e2390950e070bb1a..019736f39f94b73e09bcc141d6d17398de619447 100644 --- a/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml +++ b/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml @@ -98,7 +98,7 @@ let pair k1 k2 = (* (will become) comparable pair type constructor *) let cpair k1 k2 = - match pair_t (-1) k1 k2 with Error _ -> assert false | Ok t -> t + match pair_t (-1) k1 k2 with Error _ -> assert false | Ok (Ty_ex_c t) -> t (* union type constructor*) let union k1 k2 = @@ -106,7 +106,7 @@ let union k1 k2 = (* (will become) comparable union type constructor *) let cunion k1 k2 = - match union_t (-1) k1 k2 with Error _ -> assert false | Ok t -> t + match union_t (-1) k1 k2 with Error _ -> assert false | Ok (Ty_ex_c t) -> t let lambda x y = match lambda_t (-1) x y with Error _ -> assert false | Ok t -> t diff --git a/src/proto_alpha/lib_benchmarks_proto/ticket_benchmarks.ml b/src/proto_alpha/lib_benchmarks_proto/ticket_benchmarks.ml index 421e96959a11c667cded5a9ab54c6bfa6fe011ca..23fadf09a62aeeb324876d7915df7701a877366d 100644 --- a/src/proto_alpha/lib_benchmarks_proto/ticket_benchmarks.ml +++ b/src/proto_alpha/lib_benchmarks_proto/ticket_benchmarks.ml @@ -188,8 +188,10 @@ let rec dummy_type_generator ~rng_state size = if size <= 1 then ticket_or_int else match (ticket_or_int, dummy_type_generator ~rng_state (size - 3)) with - | (Ex_ty l, Ex_ty r) -> - Ex_ty (match pair_t (-1) l r with Error _ -> assert false | Ok t -> t) + | (Ex_ty l, Ex_ty r) -> ( + match pair_t (-1) l r with + | Error _ -> assert false + | Ok (Ty_ex_c t) -> Ex_ty t) (** A benchmark for {!Ticket_costs.Constants.cost_has_tickets_of_ty}. *) module Has_tickets_type_benchmark : Benchmark.S = struct diff --git a/src/proto_alpha/lib_benchmarks_proto/translator_benchmarks.ml b/src/proto_alpha/lib_benchmarks_proto/translator_benchmarks.ml index a967e3a0b1ee648eda5252007031fe6045b2d342..e24350e3e51b242a6e35961cfa4b60dc8b34bd0b 100644 --- a/src/proto_alpha/lib_benchmarks_proto/translator_benchmarks.ml +++ b/src/proto_alpha/lib_benchmarks_proto/translator_benchmarks.ml @@ -637,9 +637,11 @@ let rec dummy_type_generator size = if size <= 1 then Ex_ty unit_t else match dummy_type_generator (size - 2) with - | Ex_ty r -> + | Ex_ty r -> ( let l = unit_t in - Ex_ty (match pair_t (-1) l r with Error _ -> assert false | Ok t -> t) + match pair_t (-1) l r with + | Error _ -> assert false + | Ok (Ty_ex_c t) -> Ex_ty t) (* A dummy comparable type generator, sampling linear terms of a given size. *) let rec dummy_comparable_type_generator size = diff --git a/src/proto_alpha/lib_plugin/plugin.ml b/src/proto_alpha/lib_plugin/plugin.ml index 8667af203ee0839f56770830d2ced4e8134c4fa9..8e0fe2cf24e54d8d3daaca4d9f29b684833fcf85 100644 --- a/src/proto_alpha/lib_plugin/plugin.ml +++ b/src/proto_alpha/lib_plugin/plugin.ml @@ -2043,12 +2043,12 @@ module RPC = struct | Contract_t (ut, _meta) -> let t = unparse_ty ~loc ut in return (T_contract, [t], []) - | Pair_t (utl, utr, _meta) -> + | Pair_t (utl, utr, _meta, _) -> let annot = [] in let tl = unparse_ty ~loc utl in let tr = unparse_ty ~loc utr in return (T_pair, [tl; tr], annot) - | Union_t (utl, utr, _meta) -> + | Union_t (utl, utr, _meta, _) -> let annot = [] in let tl = unparse_ty ~loc utl in let tr = unparse_ty ~loc utr in @@ -2057,7 +2057,7 @@ module RPC = struct let ta = unparse_ty ~loc uta in let tr = unparse_ty ~loc utr in return (T_lambda, [ta; tr], []) - | Option_t (ut, _meta) -> + | Option_t (ut, _meta, _) -> let annot = [] in let ut = unparse_ty ~loc ut in return (T_option, [ut], annot) diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index a066cc50351c5d1e858a568c607fe474e9996f2d..44bf5999956a9b9548339525fe2cd3aa28c9f521 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -1084,7 +1084,8 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = kinstr; }, _script_view ) -> ( - pair_t kloc input_ty storage_type >>?= fun pair_ty -> + pair_t kloc input_ty storage_type + >>?= fun (Ty_ex_c pair_ty) -> let io_ty = let open Gas_monad.Syntax in let* out_eq = diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml index 2bd9dbf35d27aa8a6217598aeb3252a7598ea5eb..3a0e161d00c7722a548291d58656e747183a27b3 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml @@ -469,7 +469,7 @@ let apply ctxt gas capture_ty capture lam = let loc = Micheline.dummy_location in unparse_ty ~loc ctxt capture_ty >>?= fun (ty_expr, ctxt) -> match full_arg_ty with - | Pair_t (capture_ty, arg_ty, _) -> + | Pair_t (capture_ty, arg_ty, _, _) -> let arg_stack_ty = Item_t (arg_ty, Bot_t) in let full_descr = { @@ -532,7 +532,7 @@ let transfer (ctxt, sc) gas amount location parameters_ty parameters destination | Tx_rollup _ -> ( let open Micheline in match tp with - | Pair_t (Ticket_t (tp, _), _, _) -> + | Pair_t (Ticket_t (tp, _), _, _, _) -> Script_ir_translator.unparse_comparable_ty ~loc:dummy_location ctxt diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 38df9c7a993cc4ccfc002614a03208f2fd23c148..a4ffaa7a2d8d10c1894f7b981461602a04f6b267 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -178,10 +178,10 @@ let rec ty_of_comparable_ty : type a. a comparable_ty -> a ty = function | Tx_rollup_l2_address_key -> Tx_rollup_l2_address_t | Chain_id_key -> Chain_id_t | Pair_key (l, r, meta) -> - Pair_t (ty_of_comparable_ty l, ty_of_comparable_ty r, meta) + Pair_t (ty_of_comparable_ty l, ty_of_comparable_ty r, meta, ()) | Union_key (l, r, meta) -> - Union_t (ty_of_comparable_ty l, ty_of_comparable_ty r, meta) - | Option_key (t, meta) -> Option_t (ty_of_comparable_ty t, meta) + Union_t (ty_of_comparable_ty l, ty_of_comparable_ty r, meta, ()) + | Option_key (t, meta) -> Option_t (ty_of_comparable_ty t, meta, ()) let rec unparse_comparable_ty_uncarbonated : type a loc. loc:loc -> a comparable_ty -> loc Script.michelson_node = @@ -248,7 +248,7 @@ let rec unparse_ty_entrypoints_uncarbonated : | Contract_t (ut, _meta) -> let t = unparse_ty_entrypoints_uncarbonated ~loc ut no_entrypoints in (T_contract, [t]) - | Pair_t (utl, utr, _meta) -> ( + | Pair_t (utl, utr, _meta, _) -> ( let tl = unparse_ty_entrypoints_uncarbonated ~loc utl no_entrypoints in let tr = unparse_ty_entrypoints_uncarbonated ~loc utr no_entrypoints in (* Fold [pair a1 (pair ... (pair an-1 an))] into [pair a1 ... an] *) @@ -257,7 +257,7 @@ let rec unparse_ty_entrypoints_uncarbonated : match tr with | Prim (_, T_pair, ts, []) -> (T_pair, tl :: ts) | _ -> (T_pair, [tl; tr])) - | Union_t (utl, utr, _meta) -> + | Union_t (utl, utr, _meta, _) -> let (entrypoints_l, entrypoints_r) = match nested_entrypoints with | Entrypoints_None -> (no_entrypoints, no_entrypoints) @@ -270,7 +270,7 @@ let rec unparse_ty_entrypoints_uncarbonated : let ta = unparse_ty_entrypoints_uncarbonated ~loc uta no_entrypoints in let tr = unparse_ty_entrypoints_uncarbonated ~loc utr no_entrypoints in (T_lambda, [ta; tr]) - | Option_t (ut, _meta) -> + | Option_t (ut, _meta, _) -> let ut = unparse_ty_entrypoints_uncarbonated ~loc ut no_entrypoints in (T_option, [ut]) | List_t (ut, _meta) -> @@ -352,15 +352,15 @@ let[@coq_axiom_with_reason "gadt"] rec comparable_ty_of_ty : | Address_t -> ok (Address_key, ctxt) | Tx_rollup_l2_address_t -> ok (Tx_rollup_l2_address_key, ctxt) | Chain_id_t -> ok (Chain_id_key, ctxt) - | Pair_t (l, r, pname) -> + | Pair_t (l, r, pname, _) -> comparable_ty_of_ty ctxt loc l >>? fun (lty, ctxt) -> comparable_ty_of_ty ctxt loc r >|? fun (rty, ctxt) -> (Pair_key (lty, rty, pname), ctxt) - | Union_t (l, r, meta) -> + | Union_t (l, r, meta, _) -> comparable_ty_of_ty ctxt loc l >>? fun (lty, ctxt) -> comparable_ty_of_ty ctxt loc r >|? fun (rty, ctxt) -> (Union_key (lty, rty, meta), ctxt) - | Option_t (tt, meta) -> + | Option_t (tt, meta, _) -> comparable_ty_of_ty ctxt loc tt >|? fun (ty, ctxt) -> (Option_key (ty, meta), ctxt) | Lambda_t _ | List_t _ | Ticket_t _ | Set_t _ | Map_t _ | Big_map_t _ @@ -706,10 +706,10 @@ let check_dupable_ty ctxt loc ty = | Chest_t -> return_unit | Chest_key_t -> return_unit | Ticket_t _ -> fail @@ Unexpected_ticket loc - | Pair_t (ty_a, ty_b, _) -> + | Pair_t (ty_a, ty_b, _, _) -> let* () = aux loc ty_a in aux loc ty_b - | Union_t (ty_a, ty_b, _) -> + | Union_t (ty_a, ty_b, _, _) -> let* () = aux loc ty_a in aux loc ty_b | Lambda_t (_, _, _) -> @@ -722,7 +722,7 @@ let check_dupable_ty ctxt loc ty = Hence non-dupable should imply non-packable. *) return_unit - | Option_t (ty, _) -> aux loc ty + | Option_t (ty, _, _) -> aux loc ty | List_t (ty, _) -> aux loc ty | Set_t (key_ty, _) -> let () = check_dupable_comparable_ty key_ty in @@ -951,13 +951,13 @@ let ty_eq : let+ Eq = comparable_ty_eq ~error_details ea eb in (Eq : (ta ty, tb ty) eq) | (Ticket_t _, _) -> not_equal () - | (Pair_t (tal, tar, meta1), Pair_t (tbl, tbr, meta2)) -> + | (Pair_t (tal, tar, meta1, _), Pair_t (tbl, tbr, meta2, _)) -> let* () = type_metadata_eq meta1 meta2 in let* Eq = help tal tbl in let+ Eq = help tar tbr in (Eq : (ta ty, tb ty) eq) | (Pair_t _, _) -> not_equal () - | (Union_t (tal, tar, meta1), Union_t (tbl, tbr, meta2)) -> + | (Union_t (tal, tar, meta1, _), Union_t (tbl, tbr, meta2, _)) -> let* () = type_metadata_eq meta1 meta2 in let* Eq = help tal tbl in let+ Eq = help tar tbr in @@ -974,7 +974,7 @@ let ty_eq : let+ Eq = help tal tbl in (Eq : (ta ty, tb ty) eq) | (Contract_t _, _) -> not_equal () - | (Option_t (tva, meta1), Option_t (tvb, meta2)) -> + | (Option_t (tva, meta1, _), Option_t (tvb, meta2, _)) -> let* () = type_metadata_eq meta1 meta2 in let+ Eq = help tva tvb in (Eq : (ta ty, tb ty) eq) @@ -1362,7 +1362,7 @@ let[@coq_axiom_with_reason "complex mutually recursive definition"] rec parse_ty utr >>? fun (Ex_ty tr, ctxt) -> check_type_annot loc annot >>? fun () -> - pair_t loc tl tr >|? fun ty -> return ctxt ty + pair_t loc tl tr >|? fun (Ty_ex_c ty) -> return ctxt ty | Prim (loc, T_or, [utl; utr], annot) -> ( (match ret with | Don't_parse_entrypoints -> @@ -1397,7 +1397,7 @@ let[@coq_axiom_with_reason "complex mutually recursive definition"] rec parse_ty | Don't_parse_entrypoints -> let (Ex_ty tl) = parsed_l in let (Ex_ty tr) = parsed_r in - union_t loc tl tr >|? fun ty -> ((Ex_ty ty : ret), ctxt) + union_t loc tl tr >|? fun (Ty_ex_c ty) -> ((Ex_ty ty : ret), ctxt) | Parse_entrypoints -> let (Ex_parameter_ty_and_entrypoints {arg_type = tl; entrypoints = left}) = @@ -1407,7 +1407,7 @@ let[@coq_axiom_with_reason "complex mutually recursive definition"] rec parse_ty {arg_type = tr; entrypoints = right}) = parsed_r in - union_t loc tl tr >|? fun arg_type -> + union_t loc tl tr >|? fun (Ty_ex_c arg_type) -> let entrypoints = {name; nested = Entrypoints_Union {left; right}} in @@ -1721,8 +1721,8 @@ let parse_storage_ty : remaining_storage >>? fun (Ex_ty remaining_storage, ctxt) -> check_composed_type_annot loc storage_annot >>? fun () -> - pair_t loc big_map_ty remaining_storage >|? fun ty -> (Ex_ty ty, ctxt) - ) + pair_t loc big_map_ty remaining_storage >|? fun (Ty_ex_c ty) -> + (Ex_ty ty, ctxt)) | _ -> (parse_normal_storage_ty [@tailcall]) ctxt ~stack_depth ~legacy node let check_packable ~legacy loc root = @@ -1753,9 +1753,9 @@ let check_packable ~legacy loc root = | Bls12_381_g1_t -> Result.return_unit | Bls12_381_g2_t -> Result.return_unit | Bls12_381_fr_t -> Result.return_unit - | Pair_t (l_ty, r_ty, _) -> check l_ty >>? fun () -> check r_ty - | Union_t (l_ty, r_ty, _) -> check l_ty >>? fun () -> check r_ty - | Option_t (v_ty, _) -> check v_ty + | Pair_t (l_ty, r_ty, _, _) -> check l_ty >>? fun () -> check r_ty + | Union_t (l_ty, r_ty, _, _) -> check l_ty >>? fun () -> check r_ty + | Option_t (v_ty, _, _) -> check v_ty | List_t (elt_ty, _) -> check elt_ty | Map_t (_, elt_ty, _) -> check elt_ty | Contract_t (_, _) when legacy -> Result.return_unit @@ -1885,9 +1885,9 @@ let rec make_comb_get_proof_argument : fun n ty -> match (n, ty) with | (0, value_ty) -> Some (Comb_get_proof_argument (Comb_get_zero, value_ty)) - | (1, Pair_t (hd_ty, _, _annot)) -> + | (1, Pair_t (hd_ty, _, _annot, _)) -> Some (Comb_get_proof_argument (Comb_get_one, hd_ty)) - | (n, Pair_t (_, tl_ty, _annot)) -> + | (n, Pair_t (_, tl_ty, _annot, _)) -> make_comb_get_proof_argument (n - 2) tl_ty |> Option.map @@ fun (Comb_get_proof_argument (comb_get_left_witness, ty')) -> @@ -1906,13 +1906,13 @@ let rec make_comb_set_proof_argument : fun ctxt stack_ty loc n value_ty ty -> match (n, ty) with | (0, _) -> ok @@ Comb_set_proof_argument (Comb_set_zero, value_ty) - | (1, Pair_t (_hd_ty, tl_ty, _)) -> - pair_t loc value_ty tl_ty >|? fun after_ty -> + | (1, Pair_t (_hd_ty, tl_ty, _, _)) -> + pair_t loc value_ty tl_ty >|? fun (Ty_ex_c after_ty) -> Comb_set_proof_argument (Comb_set_one, after_ty) - | (n, Pair_t (hd_ty, tl_ty, _)) -> + | (n, Pair_t (hd_ty, tl_ty, _, _)) -> make_comb_set_proof_argument ctxt stack_ty loc (n - 2) value_ty tl_ty >>? fun (Comb_set_proof_argument (comb_set_left_witness, tl_ty')) -> - pair_t loc hd_ty tl_ty' >|? fun after_ty -> + pair_t loc hd_ty tl_ty' >|? fun (Ty_ex_c after_ty) -> Comb_set_proof_argument (Comb_set_plus_two comb_set_left_witness, after_ty) | _ -> let whole_stack = serialize_stack_for_error ctxt stack_ty in @@ -1934,7 +1934,8 @@ let find_entrypoint (type full error_trace) match (ty, entrypoints) with | (_, {name = Some name; _}) when Entrypoint.(name = entrypoint) -> return (Ex_ty_cstr (ty, fun e -> e)) - | (Union_t (tl, tr, _), {nested = Entrypoints_Union {left; right}; _}) -> ( + | (Union_t (tl, tr, _, _), {nested = Entrypoints_Union {left; right}; _}) + -> ( Gas_monad.bind_recover (find_entrypoint tl left entrypoint) @@ function | Ok (Ex_ty_cstr (t, f)) -> return (Ex_ty_cstr (t, fun e -> L (f e))) | Error () -> @@ -2004,7 +2005,7 @@ let well_formed_entrypoints (type full) (full : full ty) entrypoints = (prim list option * Entrypoint.Set.t) tzresult = fun t entrypoints path reachable acc -> match (t, entrypoints) with - | (Union_t (tl, tr, _), {nested = Entrypoints_Union {left; right}; _}) -> + | (Union_t (tl, tr, _, _), {nested = Entrypoints_Union {left; right}; _}) -> merge (D_Left :: path) tl left reachable acc >>? fun (acc, l_reachable) -> merge (D_Right :: path) tr right reachable acc @@ -2679,7 +2680,7 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : ~entrypoint:address.entrypoint >|=? fun (ctxt, _) -> (Typed_contract {arg_ty; address}, ctxt) ) (* Pairs *) - | (Pair_t (tl, tr, _), expr) -> + | (Pair_t (tl, tr, _, _), expr) -> let r_witness = comb_witness1 tr in let parse_l ctxt v = non_terminal_recursion ?type_logger ctxt ~legacy tl v @@ -2689,7 +2690,7 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : in traced @@ parse_pair parse_l parse_r ctxt ~legacy r_witness expr (* Unions *) - | (Union_t (tl, tr, _), expr) -> + | (Union_t (tl, tr, _, _), expr) -> let parse_l ctxt v = non_terminal_recursion ?type_logger ctxt ~legacy tl v in @@ -2712,7 +2713,7 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : | (Lambda_t _, expr) -> traced_fail (Invalid_kind (location expr, [Seq_kind], kind expr)) (* Options *) - | (Option_t (t, _), expr) -> + | (Option_t (t, _, _), expr) -> let parse_v ctxt v = non_terminal_recursion ?type_logger ctxt ~legacy t v in @@ -2962,7 +2963,7 @@ and parse_view_returning : (Some "return of view", strip_locations output_ty, output_ty_loc)) (parse_view_output_ty ctxt ~stack_depth:0 ~legacy output_ty) >>?= fun (Ex_ty output_ty', ctxt) -> - pair_t input_ty_loc input_ty' storage_type >>?= fun pair_ty -> + pair_t input_ty_loc input_ty' storage_type >>?= fun (Ty_ex_c pair_ty) -> parse_instr ?type_logger ~stack_depth:0 @@ -3264,7 +3265,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : option_t loc t >>?= fun ty -> let stack_ty = Item_t (ty, stack) in typed ctxt loc cons_none stack_ty - | (Prim (loc, I_MAP, [body], annot), Item_t (Option_t (t, _), rest)) -> ( + | (Prim (loc, I_MAP, [body], annot), Item_t (Option_t (t, _, _), rest)) -> ( check_kind [Seq_kind] body >>?= fun () -> check_var_type_annot loc annot >>?= fun () -> non_terminal_recursion @@ -3298,7 +3299,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : error (Invalid_map_body (loc, aft)) | Failed _ -> error (Invalid_map_block_fail loc)) | ( Prim (loc, I_IF_NONE, [bt; bf], annot), - (Item_t (Option_t (t, _), rest) as bef) ) -> + (Item_t (Option_t (t, _, _), rest) as bef) ) -> check_kind [Seq_kind] bt >>?= fun () -> check_kind [Seq_kind] bf >>?= fun () -> error_unexpected_annot loc annot >>?= fun () -> @@ -3326,7 +3327,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : (* pairs *) | (Prim (loc, I_PAIR, [], annot), Item_t (a, Item_t (b, rest))) -> check_constr_annot loc annot >>?= fun () -> - pair_t loc a b >>?= fun ty -> + pair_t loc a b >>?= fun (Ty_ex_c ty) -> let stack_ty = Item_t (ty, rest) in let cons_pair = {apply = (fun kinfo k -> ICons_pair (kinfo, k))} in typed ctxt loc cons_pair stack_ty @@ -3343,7 +3344,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : make_proof_argument (n - 1) tl_ty >>? fun (Comb_proof_argument (comb_witness, Item_t (b_ty, tl_ty'))) -> - pair_t loc a_ty b_ty >|? fun pair_t -> + pair_t loc a_ty b_ty >|? fun (Ty_ex_c pair_t) -> Comb_proof_argument (Comb_succ comb_witness, Item_t (pair_t, tl_ty')) | _ -> let whole_stack = serialize_stack_for_error ctxt stack_ty in @@ -3365,7 +3366,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : fun n stack_ty -> match (n, stack_ty) with | (1, stack) -> ok @@ Uncomb_proof_argument (Uncomb_one, stack) - | (n, Item_t (Pair_t (a_ty, b_ty, _), tl_ty)) -> + | (n, Item_t (Pair_t (a_ty, b_ty, _, _), tl_ty)) -> make_proof_argument (n - 1) (Item_t (b_ty, tl_ty)) >|? fun (Uncomb_proof_argument (uncomb_witness, after_ty)) -> Uncomb_proof_argument @@ -3408,15 +3409,15 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : {apply = (fun kinfo k -> IComb_set (kinfo, n, witness, k))} in typed ctxt loc comb_set after_stack_ty - | (Prim (loc, I_UNPAIR, [], annot), Item_t (Pair_t (a, b, _), rest)) -> + | (Prim (loc, I_UNPAIR, [], annot), Item_t (Pair_t (a, b, _, _), rest)) -> check_unpair_annot loc annot >>?= fun () -> let unpair = {apply = (fun kinfo k -> IUnpair (kinfo, k))} in typed ctxt loc unpair (Item_t (a, Item_t (b, rest))) - | (Prim (loc, I_CAR, [], annot), Item_t (Pair_t (a, _, _), rest)) -> + | (Prim (loc, I_CAR, [], annot), Item_t (Pair_t (a, _, _, _), rest)) -> check_destr_annot loc annot >>?= fun () -> let car = {apply = (fun kinfo k -> ICar (kinfo, k))} in typed ctxt loc car (Item_t (a, rest)) - | (Prim (loc, I_CDR, [], annot), Item_t (Pair_t (_, b, _), rest)) -> + | (Prim (loc, I_CDR, [], annot), Item_t (Pair_t (_, b, _, _), rest)) -> check_destr_annot loc annot >>?= fun () -> let cdr = {apply = (fun kinfo k -> ICdr (kinfo, k))} in typed ctxt loc cdr (Item_t (b, rest)) @@ -3426,7 +3427,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : >>?= fun (Ex_ty tr, ctxt) -> check_constr_annot loc annot >>?= fun () -> let cons_left = {apply = (fun kinfo k -> ICons_left (kinfo, k))} in - union_t loc tl tr >>?= fun ty -> + union_t loc tl tr >>?= fun (Ty_ex_c ty) -> let stack_ty = Item_t (ty, rest) in typed ctxt loc cons_left stack_ty | (Prim (loc, I_RIGHT, [tl], annot), Item_t (tr, rest)) -> @@ -3434,11 +3435,11 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : >>?= fun (Ex_ty tl, ctxt) -> check_constr_annot loc annot >>?= fun () -> let cons_right = {apply = (fun kinfo k -> ICons_right (kinfo, k))} in - union_t loc tl tr >>?= fun ty -> + union_t loc tl tr >>?= fun (Ty_ex_c ty) -> let stack_ty = Item_t (ty, rest) in typed ctxt loc cons_right stack_ty | ( Prim (loc, I_IF_LEFT, [bt; bf], annot), - (Item_t (Union_t (tl, tr, _), rest) as bef) ) -> + (Item_t (Union_t (tl, tr, _, _), rest) as bef) ) -> check_kind [Seq_kind] bt >>?= fun () -> check_kind [Seq_kind] bf >>?= fun () -> error_unexpected_annot loc annot >>?= fun () -> @@ -3671,7 +3672,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : let k = ty_of_comparable_ty ck in check_kind [Seq_kind] body >>?= fun () -> check_var_type_annot loc annot >>?= fun () -> - pair_t loc k elt >>?= fun ty -> + pair_t loc k elt >>?= fun (Ty_ex_c ty) -> non_terminal_recursion ?type_logger tc_context @@ -3713,7 +3714,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : check_kind [Seq_kind] body >>?= fun () -> error_unexpected_annot loc annot >>?= fun () -> let key = ty_of_comparable_ty comp_elt in - pair_t loc key element_ty >>?= fun ty -> + pair_t loc key element_ty >>?= fun (Ty_ex_c ty) -> non_terminal_recursion ?type_logger tc_context @@ -3766,8 +3767,9 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : typed ctxt loc instr (Item_t (ty, rest)) | ( Prim (loc, I_UPDATE, [], annot), Item_t - (vk, Item_t (Option_t (vv, _), (Item_t (Map_t (ck, v, _), _) as stack))) - ) -> + ( vk, + Item_t (Option_t (vv, _, _), (Item_t (Map_t (ck, v, _), _) as stack)) + ) ) -> let k = ty_of_comparable_ty ck in check_item_ty ctxt vk k loc I_UPDATE 1 3 >>?= fun (Eq, ctxt) -> check_item_ty ctxt vv v loc I_UPDATE 2 3 >>?= fun (Eq, ctxt) -> @@ -3776,8 +3778,9 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : (typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t) | ( Prim (loc, I_GET_AND_UPDATE, [], annot), Item_t - (vk, (Item_t (Option_t (vv, _), Item_t (Map_t (ck, v, _), _)) as stack)) - ) -> + ( vk, + (Item_t (Option_t (vv, _, _), Item_t (Map_t (ck, v, _), _)) as stack) + ) ) -> let k = ty_of_comparable_ty ck in check_item_ty ctxt vk k loc I_GET_AND_UPDATE 1 3 >>?= fun (Eq, ctxt) -> check_item_ty ctxt vv v loc I_GET_AND_UPDATE 2 3 >>?= fun (Eq, ctxt) -> @@ -3822,7 +3825,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : Item_t ( set_key, Item_t - ( Option_t (set_value, _), + ( Option_t (set_value, _, _), (Item_t (Big_map_t (map_key, map_value, _), _) as stack) ) ) ) -> let k = ty_of_comparable_ty map_key in check_item_ty ctxt set_key k loc I_UPDATE 1 3 >>?= fun (Eq, ctxt) -> @@ -3834,8 +3837,8 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : | ( Prim (loc, I_GET_AND_UPDATE, [], annot), Item_t ( vk, - (Item_t (Option_t (vv, _), Item_t (Big_map_t (ck, v, _), _)) as stack) - ) ) -> + (Item_t (Option_t (vv, _, _), Item_t (Big_map_t (ck, v, _), _)) as + stack) ) ) -> let k = ty_of_comparable_ty ck in check_item_ty ctxt vk k loc I_GET_AND_UPDATE 1 3 >>?= fun (Eq, ctxt) -> check_item_ty ctxt vv v loc I_GET_AND_UPDATE 2 3 >>?= fun (Eq, ctxt) -> @@ -3868,7 +3871,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : apply = (fun kinfo k -> ISapling_verify_update_deprecated (kinfo, k)); } in - pair_t loc int_t state_ty >>?= fun pair_ty -> + pair_t loc int_t state_ty >>?= fun (Ty_ex_c pair_ty) -> option_t loc pair_ty >>?= fun ty -> let stack = Item_t (ty, rest) in typed ctxt loc instr stack @@ -3885,8 +3888,8 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : let instr = {apply = (fun kinfo k -> ISapling_verify_update (kinfo, k))} in - pair_t loc int_t state_ty >>?= fun pair_ty -> - pair_t loc bytes_t pair_ty >>?= fun pair_ty -> + pair_t loc int_t state_ty >>?= fun (Ty_ex_c pair_ty) -> + pair_t loc bytes_t pair_ty >>?= fun (Ty_ex_c pair_ty) -> option_t loc pair_ty >>?= fun ty -> let stack = Item_t (ty, rest) in typed ctxt loc instr stack @@ -3983,7 +3986,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : in typed_no_lwt ctxt loc instr rest) | ( Prim (loc, I_LOOP_LEFT, [body], annot), - (Item_t (Union_t (tl, tr, _), rest) as stack) ) -> ( + (Item_t (Union_t (tl, tr, _, _), rest) as stack) ) -> ( check_kind [Seq_kind] body >>?= fun () -> check_var_annot loc annot >>?= fun () -> non_terminal_recursion @@ -4063,8 +4066,8 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : | ( Prim (loc, I_APPLY, [], annot), Item_t ( capture, - Item_t (Lambda_t (Pair_t (capture_ty, arg_ty, _), ret, _), rest) ) ) - -> + Item_t (Lambda_t (Pair_t (capture_ty, arg_ty, _, _), ret, _), rest) ) + ) -> check_packable ~legacy:false loc capture_ty >>?= fun () -> check_item_ty ctxt capture capture_ty loc I_APPLY 1 2 >>?= fun (Eq, ctxt) -> @@ -4557,7 +4560,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : let stack = Item_t (operation_t, rest) in (typed ctxt loc instr stack : ((a, s) judgement * context) tzresult Lwt.t) | ( Prim (loc, (I_SET_DELEGATE as prim), [], annot), - Item_t (Option_t (Key_hash_t, _), rest) ) -> + Item_t (Option_t (Key_hash_t, _, _), rest) ) -> Tc_context.check_not_in_view loc ~legacy tc_context prim >>?= fun () -> check_var_annot loc annot >>?= fun () -> let instr = {apply = (fun kinfo k -> ISet_delegate (kinfo, k))} in @@ -4571,8 +4574,9 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : let stack = Item_t (contract_unit_t, rest) in typed ctxt loc instr stack | ( Prim (loc, (I_CREATE_CONTRACT as prim), [(Seq _ as code)], annot), - Item_t (Option_t (Key_hash_t, _), Item_t (Mutez_t, Item_t (ginit, rest))) - ) -> + Item_t + (Option_t (Key_hash_t, _, _), Item_t (Mutez_t, Item_t (ginit, rest))) ) + -> Tc_context.check_not_in_view ~legacy loc tc_context prim >>?= fun () -> check_two_var_annot loc annot >>?= fun () -> let canonical_code = Micheline.strip_locations code in @@ -4595,8 +4599,9 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : ~legacy storage_type) >>?= fun (Ex_ty storage_type, ctxt) -> - pair_t loc arg_type storage_type >>?= fun arg_type_full -> - pair_t loc list_operation_t storage_type >>?= fun ret_type_full -> + pair_t loc arg_type storage_type >>?= fun (Ty_ex_c arg_type_full) -> + pair_t loc list_operation_t storage_type + >>?= fun (Ty_ex_c ret_type_full) -> trace (Ill_typed_contract (canonical_code, [])) (parse_returning @@ -4830,7 +4835,8 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : let instr = {apply = (fun kinfo k -> INeg_bls12_381_fr (kinfo, k))} in typed ctxt loc instr stack | ( Prim (loc, I_PAIRING_CHECK, [], annot), - Item_t (List_t (Pair_t (Bls12_381_g1_t, Bls12_381_g2_t, _), _), rest) ) -> + Item_t (List_t (Pair_t (Bls12_381_g1_t, Bls12_381_g2_t, _, _), _), rest) + ) -> check_var_annot loc annot >>?= fun () -> let instr = {apply = (fun kinfo k -> IPairing_check_bls12_381 (kinfo, k))} @@ -4856,11 +4862,11 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : typed ctxt loc instr stack | ( Prim (loc, I_SPLIT_TICKET, [], annot), Item_t - ((Ticket_t (t, _) as ticket_t), Item_t (Pair_t (Nat_t, Nat_t, _), rest)) - ) -> + ( (Ticket_t (t, _) as ticket_t), + Item_t (Pair_t (Nat_t, Nat_t, _, _), rest) ) ) -> check_var_annot loc annot >>?= fun () -> let () = check_dupable_comparable_ty t in - pair_t loc ticket_t ticket_t >>?= fun pair_tickets_ty -> + pair_t loc ticket_t ticket_t >>?= fun (Ty_ex_c pair_tickets_ty) -> option_t loc pair_tickets_ty >>?= fun res_ty -> let instr = {apply = (fun kinfo k -> ISplit_ticket (kinfo, k))} in let stack = Item_t (res_ty, rest) in @@ -4870,6 +4876,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : ( Pair_t ( (Ticket_t (contents_ty_a, _) as ty_a), Ticket_t (contents_ty_b, _), + _, _ ), rest ) ) -> check_var_annot loc annot >>?= fun () -> @@ -5158,7 +5165,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra (* /!\ This pattern matching needs to remain in sync with [parse_contract] and [parse_tx_rollup_deposit_parameters]. *) match arg with - | Pair_t (Ticket_t (_, _), Tx_rollup_l2_address_t, _) -> + | Pair_t (Ticket_t (_, _), Tx_rollup_l2_address_t, _, _) -> let address = {destination; entrypoint} in return (ctxt, Typed_contract {arg_ty = arg; address}) | _ -> @@ -5367,7 +5374,7 @@ let parse_contract_for_script : [parse_contract_for_script] and [parse_tx_rollup_deposit_parameters]. *) match arg with - | Pair_t (Ticket_t (_, _), Tx_rollup_l2_address_t, _) + | Pair_t (Ticket_t (_, _), Tx_rollup_l2_address_t, _, _) when Entrypoint.( entrypoint = Alpha_context.Tx_rollup.deposit_entrypoint) -> ( Tx_rollup_state.find ctxt tx_rollup >|=? function @@ -5421,9 +5428,10 @@ let parse_code : (Ill_formed_type (Some "storage", code, storage_type_loc)) (parse_storage_ty ctxt ~stack_depth:0 ~legacy storage_type) >>?= fun (Ex_ty storage_type, ctxt) -> - pair_t storage_type_loc arg_type storage_type >>?= fun arg_type_full -> + pair_t storage_type_loc arg_type storage_type + >>?= fun (Ty_ex_c arg_type_full) -> pair_t storage_type_loc list_operation_t storage_type - >>?= fun ret_type_full -> + >>?= fun (Ty_ex_c ret_type_full) -> trace (Ill_typed_contract (code, [])) (parse_returning @@ -5517,9 +5525,10 @@ let typecheck_code : (Ill_formed_type (Some "storage", code, storage_type_loc)) (parse_storage_ty ctxt ~stack_depth:0 ~legacy storage_type) >>?= fun (Ex_ty storage_type, ctxt) -> - pair_t storage_type_loc arg_type storage_type >>?= fun arg_type_full -> + pair_t storage_type_loc arg_type storage_type + >>?= fun (Ty_ex_c arg_type_full) -> pair_t storage_type_loc list_operation_t storage_type - >>?= fun ret_type_full -> + >>?= fun (Ty_ex_c ret_type_full) -> let type_logger loc ~stack_ty_before ~stack_ty_after = type_map := (loc, (stack_ty_before, stack_ty_after)) :: !type_map in @@ -5583,7 +5592,7 @@ let list_entrypoints ctxt (type full) (full : full ty) tzresult = fun t entrypoints path reachable acc -> match (t, entrypoints) with - | (Union_t (tl, tr, _), {nested = Entrypoints_Union {left; right}; _}) -> + | (Union_t (tl, tr, _, _), {nested = Entrypoints_Union {left; right}; _}) -> merge (D_Left :: path) tl left reachable acc >>? fun (acc, l_reachable) -> merge (D_Right :: path) tr right reachable acc @@ -5607,7 +5616,7 @@ let list_entrypoints ctxt (type full) (full : full ty) let comb_witness2 : type t. t ty -> (t, unit -> unit -> unit) comb_witness = function - | Pair_t (_, Pair_t _, _) -> Comb_Pair (Comb_Pair Comb_Any) + | Pair_t (_, Pair_t _, _, _) -> Comb_Pair (Comb_Pair Comb_Any) | Pair_t _ -> Comb_Pair Comb_Any | _ -> Comb_Any @@ -5651,16 +5660,16 @@ let[@coq_axiom_with_reason "gadt"] rec unparse_data : | (Bls12_381_g1_t, x) -> Lwt.return @@ unparse_bls12_381_g1 ~loc ctxt x | (Bls12_381_g2_t, x) -> Lwt.return @@ unparse_bls12_381_g2 ~loc ctxt x | (Bls12_381_fr_t, x) -> Lwt.return @@ unparse_bls12_381_fr ~loc ctxt x - | (Pair_t (tl, tr, _), pair) -> + | (Pair_t (tl, tr, _, _), pair) -> let r_witness = comb_witness2 tr in let unparse_l ctxt v = non_terminal_recursion ctxt mode tl v in let unparse_r ctxt v = non_terminal_recursion ctxt mode tr v in unparse_pair ~loc unparse_l unparse_r ctxt mode r_witness pair - | (Union_t (tl, tr, _), v) -> + | (Union_t (tl, tr, _, _), v) -> let unparse_l ctxt v = non_terminal_recursion ctxt mode tl v in let unparse_r ctxt v = non_terminal_recursion ctxt mode tr v in unparse_union ~loc unparse_l unparse_r ctxt v - | (Option_t (t, _), v) -> + | (Option_t (t, _, _), v) -> let unparse_v ctxt v = non_terminal_recursion ctxt mode t v in unparse_option ~loc unparse_v ctxt v | (List_t (t, _), items) -> @@ -6149,9 +6158,9 @@ let rec has_lazy_storage : type t. t ty -> t has_lazy_storage = | Ticket_t _ -> False_f | Chest_key_t -> False_f | Chest_t -> False_f - | Pair_t (l, r, _) -> aux2 (fun l r -> Pair_f (l, r)) l r - | Union_t (l, r, _) -> aux2 (fun l r -> Union_f (l, r)) l r - | Option_t (t, _) -> aux1 (fun h -> Option_f h) t + | Pair_t (l, r, _, _) -> aux2 (fun l r -> Pair_f (l, r)) l r + | Union_t (l, r, _, _) -> aux2 (fun l r -> Union_f (l, r)) l r + | Option_t (t, _, _) -> aux1 (fun h -> Option_f h) t | List_t (t, _) -> aux1 (fun h -> List_f h) t | Map_t (_, t, _) -> aux1 (fun h -> Map_f h) t @@ -6204,19 +6213,19 @@ let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_updates ctxt mode let diff = Lazy_storage.make Sapling_state id diff in let ids_to_copy = Lazy_storage.IdSet.add Sapling_state id ids_to_copy in (ctxt, sapling_state, ids_to_copy, diff :: acc) - | (Pair_f (hl, hr), Pair_t (tyl, tyr, _), (xl, xr)) -> + | (Pair_f (hl, hr), Pair_t (tyl, tyr, _, _), (xl, xr)) -> aux ctxt mode ~temporary ids_to_copy acc tyl xl ~has_lazy_storage:hl >>=? fun (ctxt, xl, ids_to_copy, acc) -> aux ctxt mode ~temporary ids_to_copy acc tyr xr ~has_lazy_storage:hr >|=? fun (ctxt, xr, ids_to_copy, acc) -> (ctxt, (xl, xr), ids_to_copy, acc) - | (Union_f (has_lazy_storage, _), Union_t (ty, _, _), L x) -> + | (Union_f (has_lazy_storage, _), Union_t (ty, _, _, _), L x) -> aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage >|=? fun (ctxt, x, ids_to_copy, acc) -> (ctxt, L x, ids_to_copy, acc) - | (Union_f (_, has_lazy_storage), Union_t (_, ty, _), R x) -> + | (Union_f (_, has_lazy_storage), Union_t (_, ty, _, _), R x) -> aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage >|=? fun (ctxt, x, ids_to_copy, acc) -> (ctxt, R x, ids_to_copy, acc) - | (Option_f has_lazy_storage, Option_t (ty, _), Some x) -> + | (Option_f has_lazy_storage, Option_t (ty, _, _), Some x) -> aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage >|=? fun (ctxt, x, ids_to_copy, acc) -> (ctxt, Some x, ids_to_copy, acc) | (List_f has_lazy_storage, List_t (ty, _), l) -> @@ -6259,7 +6268,7 @@ let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_updates ctxt mode and type value = M.value), ids_to_copy, acc ) - | (_, Option_t (_, _), None) -> return (ctxt, None, ids_to_copy, acc) + | (_, Option_t (_, _, _), None) -> return (ctxt, None, ids_to_copy, acc) in let has_lazy_storage = has_lazy_storage ty in aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage @@ -6298,19 +6307,19 @@ let[@coq_axiom_with_reason "gadt"] rec fold_lazy_storage : ok (Fold_lazy_storage.Ok init, ctxt) | (Sapling_state_f, Sapling_state_t _, {id = None; _}) -> ok (Fold_lazy_storage.Ok init, ctxt) - | (Pair_f (hl, hr), Pair_t (tyl, tyr, _), (xl, xr)) -> ( + | (Pair_f (hl, hr), Pair_t (tyl, tyr, _, _), (xl, xr)) -> ( fold_lazy_storage ~f ~init ctxt tyl xl ~has_lazy_storage:hl >>? fun (init, ctxt) -> match init with | Fold_lazy_storage.Ok init -> fold_lazy_storage ~f ~init ctxt tyr xr ~has_lazy_storage:hr | Fold_lazy_storage.Error -> ok (init, ctxt)) - | (Union_f (has_lazy_storage, _), Union_t (ty, _, _), L x) -> + | (Union_f (has_lazy_storage, _), Union_t (ty, _, _, _), L x) -> fold_lazy_storage ~f ~init ctxt ty x ~has_lazy_storage - | (Union_f (_, has_lazy_storage), Union_t (_, ty, _), R x) -> + | (Union_f (_, has_lazy_storage), Union_t (_, ty, _, _), R x) -> fold_lazy_storage ~f ~init ctxt ty x ~has_lazy_storage - | (_, Option_t (_, _), None) -> ok (Fold_lazy_storage.Ok init, ctxt) - | (Option_f has_lazy_storage, Option_t (ty, _), Some x) -> + | (_, Option_t (_, _, _), None) -> ok (Fold_lazy_storage.Ok init, ctxt) + | (Option_f has_lazy_storage, Option_t (ty, _, _), Some x) -> fold_lazy_storage ~f ~init ctxt ty x ~has_lazy_storage | (List_f has_lazy_storage, List_t (ty, _), l) -> List.fold_left_e diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 38aeb1b605f2c1de83c3c0705a415c5de5f79316..ed6a521f498abec5142ff081cb002d10d73c8dc8 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -1223,6 +1223,8 @@ and logger = { get_log : unit -> execution_trace option tzresult Lwt.t; } +and to_be_replaced = unit + (* ---- Auxiliary types -----------------------------------------------------*) and 'ty ty = | Unit_t : unit ty @@ -1238,12 +1240,16 @@ and 'ty ty = | Address_t : address ty | Tx_rollup_l2_address_t : tx_rollup_l2_address ty | Bool_t : bool ty - | Pair_t : 'a ty * 'b ty * ('a, 'b) pair ty_metadata -> ('a, 'b) pair ty - | Union_t : 'a ty * 'b ty * ('a, 'b) union ty_metadata -> ('a, 'b) union ty + | Pair_t : + 'a ty * 'b ty * ('a, 'b) pair ty_metadata * to_be_replaced + -> ('a, 'b) pair ty + | Union_t : + 'a ty * 'b ty * ('a, 'b) union ty_metadata * to_be_replaced + -> ('a, 'b) union ty | Lambda_t : 'arg ty * 'ret ty * ('arg, 'ret) lambda ty_metadata -> ('arg, 'ret) lambda ty - | Option_t : 'v ty * 'v option ty_metadata -> 'v option ty + | Option_t : 'v ty * 'v option ty_metadata * to_be_replaced -> 'v option ty | List_t : 'v ty * 'v boxed_list ty_metadata -> 'v boxed_list ty | Set_t : 'v comparable_ty * 'v set ty_metadata -> 'v set ty | Map_t : @@ -1765,9 +1771,9 @@ let ty_metadata : type a. a ty -> a ty_metadata = function | Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t | Tx_rollup_l2_address_t -> meta_basic - | Pair_t (_, _, meta) -> meta - | Union_t (_, _, meta) -> meta - | Option_t (_, meta) -> meta + | Pair_t (_, _, meta, _) -> meta + | Union_t (_, _, meta, _) -> meta + | Option_t (_, meta, _) -> meta | Lambda_t (_, _, meta) -> meta | List_t (_, meta) -> meta | Set_t (_, meta) -> meta @@ -1793,6 +1799,8 @@ let ty_size t = (ty_metadata t).size let comparable_ty_size t = (comparable_ty_metadata t).size +type 'v ty_ex_c = Ty_ex_c : 'v ty -> 'v ty_ex_c [@@ocaml.unboxed] + let unit_t = Unit_t let unit_key = Unit_key @@ -1847,7 +1855,7 @@ let tx_rollup_l2_address_key = Tx_rollup_l2_address_key let pair_t loc l r = Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size -> - Pair_t (l, r, {size}) + Ty_ex_c (Pair_t (l, r, {size}, ())) let pair_key loc l r = Type_size.compound2 loc (comparable_ty_size l) (comparable_ty_size r) @@ -1857,9 +1865,9 @@ let pair_3_key loc l m r = pair_key loc m r >>? fun r -> pair_key loc l r let union_t loc l r = Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size -> - Union_t (l, r, {size}) + Ty_ex_c (Union_t (l, r, {size}, ())) -let union_bytes_bool_t = Union_t (bytes_t, bool_t, {size = Type_size.three}) +let union_bytes_bool_t = Union_t (bytes_t, bool_t, {size = Type_size.three}, ()) let union_key loc l r = Type_size.compound2 loc (comparable_ty_size l) (comparable_ty_size r) @@ -1870,32 +1878,39 @@ let lambda_t loc l r = Lambda_t (l, r, {size}) let option_t loc t = - Type_size.compound1 loc (ty_size t) >|? fun size -> Option_t (t, {size}) + Type_size.compound1 loc (ty_size t) >|? fun size -> Option_t (t, {size}, ()) -let option_mutez_t = Option_t (mutez_t, {size = Type_size.two}) +let option_mutez_t = Option_t (mutez_t, {size = Type_size.two}, ()) -let option_string_t = Option_t (string_t, {size = Type_size.two}) +let option_string_t = Option_t (string_t, {size = Type_size.two}, ()) -let option_bytes_t = Option_t (bytes_t, {size = Type_size.two}) +let option_bytes_t = Option_t (bytes_t, {size = Type_size.two}, ()) -let option_nat_t = Option_t (nat_t, {size = Type_size.two}) +let option_nat_t = Option_t (nat_t, {size = Type_size.two}, ()) let option_pair_nat_nat_t = Option_t - (Pair_t (nat_t, nat_t, {size = Type_size.three}), {size = Type_size.four}) + ( Pair_t (nat_t, nat_t, {size = Type_size.three}, ()), + {size = Type_size.four}, + () ) let option_pair_nat_mutez_t = Option_t - (Pair_t (nat_t, mutez_t, {size = Type_size.three}), {size = Type_size.four}) + ( Pair_t (nat_t, mutez_t, {size = Type_size.three}, ()), + {size = Type_size.four}, + () ) let option_pair_mutez_mutez_t = Option_t - ( Pair_t (mutez_t, mutez_t, {size = Type_size.three}), - {size = Type_size.four} ) + ( Pair_t (mutez_t, mutez_t, {size = Type_size.three}, ()), + {size = Type_size.four}, + () ) let option_pair_int_nat_t = Option_t - (Pair_t (int_t, nat_t, {size = Type_size.three}), {size = Type_size.four}) + ( Pair_t (int_t, nat_t, {size = Type_size.three}, ()), + {size = Type_size.four}, + () ) let option_key loc t = Type_size.compound1 loc (comparable_ty_size t) >|? fun size -> @@ -2186,12 +2201,13 @@ let (ty_traverse, comparable_ty_traverse) = (continue [@ocaml.tailcall]) accu | Ticket_t (cty, _) -> aux f accu cty continue | Chest_key_t | Chest_t -> (continue [@ocaml.tailcall]) accu - | Pair_t (ty1, ty2, _) -> (next2' [@ocaml.tailcall]) f accu ty1 ty2 continue - | Union_t (ty1, ty2, _) -> + | Pair_t (ty1, ty2, _, _) -> + (next2' [@ocaml.tailcall]) f accu ty1 ty2 continue + | Union_t (ty1, ty2, _, _) -> (next2' [@ocaml.tailcall]) f accu ty1 ty2 continue | Lambda_t (ty1, ty2, _) -> (next2' [@ocaml.tailcall]) f accu ty1 ty2 continue - | Option_t (ty1, _) -> (next' [@ocaml.tailcall]) f accu ty1 continue + | Option_t (ty1, _, _) -> (next' [@ocaml.tailcall]) f accu ty1 continue | List_t (ty1, _) -> (next' [@ocaml.tailcall]) f accu ty1 continue | Set_t (cty, _) -> (aux [@ocaml.tailcall]) f accu cty @@ continue | Map_t (cty, ty1, _) -> @@ -2265,12 +2281,13 @@ let value_traverse (type t) (ty : (t ty, t comparable_ty) union) (x : t) init f | Bls12_381_g2_t | Bls12_381_fr_t | Chest_key_t | Chest_t | Lambda_t (_, _, _) -> (return [@ocaml.tailcall]) () - | Pair_t (ty1, ty2, _) -> (next2 [@ocaml.tailcall]) ty1 ty2 (fst x) (snd x) - | Union_t (ty1, ty2, _) -> ( + | Pair_t (ty1, ty2, _, _) -> + (next2 [@ocaml.tailcall]) ty1 ty2 (fst x) (snd x) + | Union_t (ty1, ty2, _, _) -> ( match x with | L l -> (next [@ocaml.tailcall]) ty1 l | R r -> (next [@ocaml.tailcall]) ty2 r) - | Option_t (ty, _) -> ( + | Option_t (ty, _, _) -> ( match x with | None -> return () | Some v -> (next [@ocaml.tailcall]) ty v) @@ -2343,5 +2360,5 @@ let value_traverse (type t) (ty : (t ty, t comparable_ty) union) (x : t) init f | R cty -> aux' init cty x (fun accu -> accu) [@@coq_axiom_with_reason "local mutually recursive definition not handled"] -let stack_top_ty : type a b s. (a, b * s) stack_ty -> a ty = function - | Item_t (ty, _) -> ty +let stack_top_ty : type a b s. (a, b * s) stack_ty -> a ty_ex_c = function + | Item_t (ty, _) -> Ty_ex_c ty diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index d7e8496272e2148f6927a05e5babb3b971d9898e..b6ee0aca6e268ce12be51447cc34f34a77d54e6b 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -1327,6 +1327,8 @@ and logger = { produced. *) } +and to_be_replaced = unit + (* ---- Auxiliary types -----------------------------------------------------*) and 'ty ty = | Unit_t : unit ty @@ -1342,12 +1344,16 @@ and 'ty ty = | Address_t : address ty | Tx_rollup_l2_address_t : tx_rollup_l2_address ty | Bool_t : bool ty - | Pair_t : 'a ty * 'b ty * ('a, 'b) pair ty_metadata -> ('a, 'b) pair ty - | Union_t : 'a ty * 'b ty * ('a, 'b) union ty_metadata -> ('a, 'b) union ty + | Pair_t : + 'a ty * 'b ty * ('a, 'b) pair ty_metadata * to_be_replaced + -> ('a, 'b) pair ty + | Union_t : + 'a ty * 'b ty * ('a, 'b) union ty_metadata * to_be_replaced + -> ('a, 'b) union ty | Lambda_t : 'arg ty * 'ret ty * ('arg, 'ret) lambda ty_metadata -> ('arg, 'ret) lambda ty - | Option_t : 'v ty * 'v option ty_metadata -> 'v option ty + | Option_t : 'v ty * 'v option ty_metadata * to_be_replaced -> 'v option ty | List_t : 'v ty * 'v boxed_list ty_metadata -> 'v boxed_list ty | Set_t : 'v comparable_ty * 'v set ty_metadata -> 'v set ty | Map_t : @@ -1540,6 +1546,8 @@ val ty_size : 'a ty -> 'a Type_size.t val comparable_ty_size : 'a comparable_ty -> 'a Type_size.t +type 'v ty_ex_c = Ty_ex_c : 'v ty -> 'v ty_ex_c [@@ocaml.unboxed] + val unit_key : unit comparable_ty val never_key : never comparable_ty @@ -1618,9 +1626,10 @@ val tx_rollup_l2_address_t : tx_rollup_l2_address ty val bool_t : bool ty -val pair_t : Script.location -> 'a ty -> 'b ty -> ('a, 'b) pair ty tzresult +val pair_t : Script.location -> 'a ty -> 'b ty -> ('a, 'b) pair ty_ex_c tzresult -val union_t : Script.location -> 'a ty -> 'b ty -> ('a, 'b) union ty tzresult +val union_t : + Script.location -> 'a ty -> 'b ty -> ('a, 'b) union ty_ex_c tzresult val union_bytes_bool_t : (Bytes.t, bool) union ty @@ -1736,4 +1745,4 @@ type 'a value_traverse = { val value_traverse : ('t ty, 't comparable_ty) union -> 't -> 'r -> 'r value_traverse -> 'r -val stack_top_ty : ('a, 'b * 's) stack_ty -> 'a ty +val stack_top_ty : ('a, 'b * 's) stack_ty -> 'a ty_ex_c diff --git a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml index bcc08ee53010d7e222159d5125dd19e025a21bb5..8ffaabc9a1c630effae51fca259f56903ad04ee3 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml @@ -90,13 +90,14 @@ let ty_traverse_f = | Bls12_381_fr_t -> ret_succ_adding accu base_basic | Chest_key_t -> ret_succ_adding accu base_basic | Chest_t -> ret_succ_adding accu base_basic - | Pair_t (_ty1, _ty2, a) -> - ret_succ_adding accu @@ (base_compound a +! (word_size *? 2)) - | Union_t (_ty1, _ty2, a) -> - ret_succ_adding accu @@ (base_compound a +! (word_size *? 2)) + | Pair_t (_ty1, _ty2, a, _) -> + ret_succ_adding accu @@ (base_compound a +! (word_size *? 3)) + | Union_t (_ty1, _ty2, a, _) -> + ret_succ_adding accu @@ (base_compound a +! (word_size *? 3)) | Lambda_t (_ty1, _ty2, a) -> ret_succ_adding accu @@ (base_compound a +! (word_size *? 2)) - | Option_t (_ty, a) -> ret_succ_adding accu @@ (base_compound a +! word_size) + | Option_t (_ty, a, _) -> + ret_succ_adding accu @@ (base_compound a +! (word_size *? 2)) | List_t (_ty, a) -> ret_succ_adding accu @@ (base_compound a +! word_size) | Set_t (_cty, a) -> ret_succ_adding accu @@ (base_compound a +! word_size) | Map_t (_cty, _ty, a) -> @@ -285,11 +286,11 @@ let rec value_size : | Tx_rollup_l2_address_t -> ret_succ_adding accu (tx_rollup_l2_address_size x) | Bool_t -> ret_succ accu - | Pair_t (_, _, _) -> ret_succ_adding accu h2w - | Union_t (_, _, _) -> ret_succ_adding accu h1w + | Pair_t (_, _, _, _) -> ret_succ_adding accu h2w + | Union_t (_, _, _, _) -> ret_succ_adding accu h1w | Lambda_t (_, _, _) -> (lambda_size [@ocaml.tailcall]) ~count_lambda_nodes (ret_succ accu) x - | Option_t (_, _) -> ret_succ_adding accu (option_size (fun _ -> !!0) x) + | Option_t (_, _, _) -> ret_succ_adding accu (option_size (fun _ -> !!0) x) | List_t (_, _) -> ret_succ_adding accu (h2w +! (h2w *? x.length)) | Set_t (_, _) -> let module M = (val Script_set.get x) in @@ -433,11 +434,8 @@ and kinstr_size : | ISwap (kinfo, _) -> ret_succ_adding accu (base kinfo) | IConst (kinfo, x, k) -> let accu = ret_succ_adding accu (base kinfo +! word_size) in - (value_size [@ocaml.tailcall]) - ~count_lambda_nodes - accu - (L (stack_top_ty (kinfo_of_kinstr k).kstack_ty)) - x + let (Ty_ex_c top_ty) = stack_top_ty (kinfo_of_kinstr k).kstack_ty in + (value_size [@ocaml.tailcall]) ~count_lambda_nodes accu (L top_ty) x | ICons_pair (kinfo, _) -> ret_succ_adding accu (base kinfo) | ICar (kinfo, _) -> ret_succ_adding accu (base kinfo) | ICdr (kinfo, _) -> ret_succ_adding accu (base kinfo) diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_sapling.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_sapling.ml index 541355261875356968970babd043891771c49c89..4e9918de5dbb1e9db4201588c37e33f431446adb 100644 --- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_sapling.ml +++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_sapling.ml @@ -1049,7 +1049,7 @@ module Interpreter_tests = struct let open Script_typed_ir in let state_ty = sapling_state_t ~memo_size in pair_t (-1) state_ty state_ty) - >>??= fun tytype -> + >>??= fun (Ty_ex_c tytype) -> Script_ir_translator.parse_storage ctx_without_gas ~legacy:true diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_cache.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_cache.ml index 1f72c33d996e1812a4039633b0f934fa11115dee..60247caa3586c57a6f4535cf2db2d057ada070f6 100644 --- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_cache.ml +++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_cache.ml @@ -46,7 +46,7 @@ let err x = Exn (Script_cache_test_error x) model. It has been computed by a manual run of the test. *) -let liquidity_baking_contract_size = 266738 +let liquidity_baking_contract_size = 267304 let liquidity_baking_contract = Contract.of_b58check "KT1TxqZ8QtKvLu3V3JH7Gx58n7Co8pgtpQU5" |> function @@ -120,7 +120,7 @@ let add_some_contracts k src block baker = model. It has been computed by a manual run of the test. *) -let int_store_contract_size = 891 +let int_store_contract_size = 916 (* diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_ticket_accounting.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_ticket_accounting.ml index 86c5c4002d72b6c21b58fc5dee2443d46dda7c8d..9a70b37d20281192a4d2368be4117b6630a023c6 100644 --- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_ticket_accounting.ml +++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_ticket_accounting.ml @@ -785,7 +785,7 @@ let test_diffs_args_storage_and_lazy_diffs () = let*? int_ticket_big_map_ty = big_map_type ~key_type:int_key ~value_type:ticket_string_type in - let*? list_big_map_pair_type = + let*? (Ty_ex_c list_big_map_pair_type) = Environment.wrap_tzresult @@ pair_t (-1) ticket_string_list_type int_ticket_big_map_ty in diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml index c63cd71ce4f11c459c39b7dd3459f3a5cd44cf69..90f03f0606f7181790e09f6efe1d74d7ab2b6d98 100644 --- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml +++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml @@ -197,54 +197,56 @@ let test_parse_comb_type () = let pair_ty ty1 ty2 = pair_t (-1) ty1 ty2 in let pair_prim2 a b = pair_prim [a; b] in let pair_nat_nat_prim = pair_prim2 nat_prim nat_prim in - pair_ty nat_ty nat_ty >>??= fun pair_nat_nat_ty -> + pair_ty nat_ty nat_ty >>??= fun (Ty_ex_c pair_nat_nat_ty) -> test_context () >>=? fun ctxt -> (* pair nat nat *) test_parse_ty ctxt pair_nat_nat_prim pair_nat_nat_ty >>?= fun ctxt -> (* pair (pair nat nat) nat *) - pair_ty pair_nat_nat_ty nat_ty >>??= fun pair_pair_nat_nat_nat_ty -> + pair_ty pair_nat_nat_ty nat_ty >>??= fun (Ty_ex_c pair_pair_nat_nat_nat_ty) -> test_parse_ty ctxt (pair_prim2 pair_nat_nat_prim nat_prim) pair_pair_nat_nat_nat_ty >>?= fun ctxt -> (* pair nat (pair nat nat) *) - pair_ty nat_ty pair_nat_nat_ty >>??= fun pair_nat_pair_nat_nat_ty -> + pair_ty nat_ty pair_nat_nat_ty >>??= fun (Ty_ex_c pair_nat_pair_nat_nat_ty) -> test_parse_ty ctxt (pair_prim2 nat_prim pair_nat_nat_prim) pair_nat_pair_nat_nat_ty >>?= fun ctxt -> (* pair nat nat nat *) - pair_ty nat_ty pair_nat_nat_ty >>??= fun pair_nat_nat_nat_ty -> + pair_ty nat_ty pair_nat_nat_ty >>??= fun (Ty_ex_c pair_nat_nat_nat_ty) -> test_parse_ty ctxt (pair_prim [nat_prim; nat_prim; nat_prim]) pair_nat_nat_nat_ty >>?= fun ctxt -> (* pair (nat %a) nat *) - pair_t (-1) nat_ty nat_ty >>??= fun pair_nat_a_nat_ty -> + pair_t (-1) nat_ty nat_ty >>??= fun (Ty_ex_c pair_nat_a_nat_ty) -> test_parse_ty ctxt (pair_prim2 nat_prim_a nat_prim) pair_nat_a_nat_ty >>?= fun ctxt -> (* pair nat (nat %b) *) - pair_t (-1) nat_ty nat_ty >>??= fun pair_nat_nat_b_ty -> + pair_t (-1) nat_ty nat_ty >>??= fun (Ty_ex_c pair_nat_nat_b_ty) -> test_parse_ty ctxt (pair_prim2 nat_prim nat_prim_b) pair_nat_nat_b_ty >>?= fun ctxt -> (* pair (nat %a) (nat %b) *) - pair_t (-1) nat_ty nat_ty >>??= fun pair_nat_a_nat_b_ty -> + pair_t (-1) nat_ty nat_ty >>??= fun (Ty_ex_c pair_nat_a_nat_b_ty) -> test_parse_ty ctxt (pair_prim2 nat_prim_a nat_prim_b) pair_nat_a_nat_b_ty >>?= fun ctxt -> (* pair (nat %a) (nat %b) (nat %c) *) - pair_t (-1) nat_ty nat_ty >>??= fun pair_nat_b_nat_c_ty -> - pair_t (-1) nat_ty pair_nat_b_nat_c_ty >>??= fun pair_nat_a_nat_b_nat_c_ty -> + pair_t (-1) nat_ty nat_ty >>??= fun (Ty_ex_c pair_nat_b_nat_c_ty) -> + pair_t (-1) nat_ty pair_nat_b_nat_c_ty + >>??= fun (Ty_ex_c pair_nat_a_nat_b_nat_c_ty) -> test_parse_ty ctxt (pair_prim [nat_prim_a; nat_prim_b; nat_prim_c]) pair_nat_a_nat_b_nat_c_ty >>?= fun ctxt -> (* pair (nat %a) (pair %b nat nat) *) - pair_t (-1) nat_ty nat_ty >>??= fun pair_b_nat_nat_ty -> - pair_t (-1) nat_ty pair_b_nat_nat_ty >>??= fun pair_nat_a_pair_b_nat_nat_ty -> + pair_t (-1) nat_ty nat_ty >>??= fun (Ty_ex_c pair_b_nat_nat_ty) -> + pair_t (-1) nat_ty pair_b_nat_nat_ty + >>??= fun (Ty_ex_c pair_nat_a_pair_b_nat_nat_ty) -> test_parse_ty ctxt (pair_prim2 nat_prim_a (Prim (-1, T_pair, [nat_prim; nat_prim], ["%b"]))) @@ -266,13 +268,13 @@ let test_unparse_comb_type () = let pair_ty ty1 ty2 = pair_t (-1) ty1 ty2 in let pair_prim2 a b = pair_prim [a; b] in let pair_nat_nat_prim = pair_prim2 nat_prim nat_prim in - pair_ty nat_ty nat_ty >>??= fun pair_nat_nat_ty -> + pair_ty nat_ty nat_ty >>??= fun (Ty_ex_c pair_nat_nat_ty) -> test_context () >>=? fun ctxt -> (* pair nat nat *) test_unparse_ty __LOC__ ctxt pair_nat_nat_prim pair_nat_nat_ty >>?= fun ctxt -> (* pair (pair nat nat) nat *) - pair_ty pair_nat_nat_ty nat_ty >>??= fun pair_pair_nat_nat_nat_ty -> + pair_ty pair_nat_nat_ty nat_ty >>??= fun (Ty_ex_c pair_pair_nat_nat_nat_ty) -> test_unparse_ty __LOC__ ctxt @@ -280,7 +282,7 @@ let test_unparse_comb_type () = pair_pair_nat_nat_nat_ty >>?= fun ctxt -> (* pair nat nat nat *) - pair_ty nat_ty pair_nat_nat_ty >>??= fun pair_nat_nat_nat_ty -> + pair_ty nat_ty pair_nat_nat_ty >>??= fun (Ty_ex_c pair_nat_nat_nat_ty) -> test_unparse_ty __LOC__ ctxt @@ -373,7 +375,7 @@ let test_parse_comb_data () = let nat_ty = nat_t in let pair_prim l = Prim (-1, D_Pair, l, []) in let pair_ty ty1 ty2 = pair_t (-1) ty1 ty2 in - pair_ty nat_ty nat_ty >>??= fun pair_nat_nat_ty -> + pair_ty nat_ty nat_ty >>??= fun (Ty_ex_c pair_nat_nat_ty) -> let pair_prim2 a b = pair_prim [a; b] in let pair_z_z_prim = pair_prim2 z_prim z_prim in list_t (-1) nat_ty >>??= fun list_nat_ty -> @@ -391,7 +393,7 @@ let test_parse_comb_data () = (z, z) >>=? fun ctxt -> (* Pair (Pair 0 0) 0 *) - pair_ty pair_nat_nat_ty nat_ty >>??= fun pair_pair_nat_nat_nat_ty -> + pair_ty pair_nat_nat_ty nat_ty >>??= fun (Ty_ex_c pair_pair_nat_nat_nat_ty) -> test_parse_data __LOC__ ctxt @@ -400,7 +402,7 @@ let test_parse_comb_data () = ((z, z), z) >>=? fun ctxt -> (* Pair 0 (Pair 0 0) *) - pair_ty nat_ty pair_nat_nat_ty >>??= fun pair_nat_pair_nat_nat_ty -> + pair_ty nat_ty pair_nat_nat_ty >>??= fun (Ty_ex_c pair_nat_pair_nat_nat_ty) -> test_parse_data __LOC__ ctxt @@ -425,7 +427,7 @@ let test_parse_comb_data () = (z, (z, z)) >>=? fun ctxt -> (* Should fail: {0} against pair nat (list nat) *) - pair_ty nat_ty list_nat_ty >>??= fun pair_nat_list_nat_ty -> + pair_ty nat_ty list_nat_ty >>??= fun (Ty_ex_c pair_nat_list_nat_ty) -> test_parse_data_fails __LOC__ ctxt @@ -461,7 +463,8 @@ let test_parse_comb_data () = && Big_map_overlay.bindings big_map1.diff.map = Big_map_overlay.bindings big_map2.diff.map in - pair_ty nat_ty big_map_nat_nat_ty >>??= fun pair_nat_big_map_nat_nat_ty -> + pair_ty nat_ty big_map_nat_nat_ty + >>??= fun (Ty_ex_c pair_nat_big_map_nat_nat_ty) -> test_parse_data ~equal __LOC__ @@ -523,7 +526,7 @@ let test_unparse_comb_data () = let nat_ty = nat_t in let pair_prim l = Prim (-1, D_Pair, l, []) in let pair_ty ty1 ty2 = pair_t (-1) ty1 ty2 in - pair_ty nat_ty nat_ty >>??= fun pair_nat_nat_ty -> + pair_ty nat_ty nat_ty >>??= fun (Ty_ex_c pair_nat_nat_ty) -> let pair_prim2 a b = pair_prim [a; b] in let pair_z_z_prim = pair_prim2 z_prim z_prim in test_context () >>=? fun ctxt -> @@ -537,7 +540,7 @@ let test_unparse_comb_data () = ~expected_optimized:pair_z_z_prim >>=? fun ctxt -> (* Pair (Pair 0 0) 0 *) - pair_ty pair_nat_nat_ty nat_ty >>??= fun pair_pair_nat_nat_nat_ty -> + pair_ty pair_nat_nat_ty nat_ty >>??= fun (Ty_ex_c pair_pair_nat_nat_nat_ty) -> test_unparse_data __LOC__ ctxt @@ -547,7 +550,7 @@ let test_unparse_comb_data () = ~expected_optimized:(pair_prim2 pair_z_z_prim z_prim) >>=? fun ctxt -> (* Readable: Pair 0 0 0; Optimized: Pair 0 (Pair 0 0) *) - pair_ty nat_ty pair_nat_nat_ty >>??= fun pair_nat_pair_nat_nat_ty -> + pair_ty nat_ty pair_nat_nat_ty >>??= fun (Ty_ex_c pair_nat_pair_nat_nat_ty) -> test_unparse_data __LOC__ ctxt @@ -558,7 +561,7 @@ let test_unparse_comb_data () = >>=? fun ctxt -> (* Readable: Pair 0 0 0 0; Optimized: {0; 0; 0; 0} *) pair_ty nat_ty pair_nat_pair_nat_nat_ty - >>??= fun pair_nat_pair_nat_pair_nat_nat_ty -> + >>??= fun (Ty_ex_c pair_nat_pair_nat_pair_nat_nat_ty) -> test_unparse_data __LOC__ ctxt @@ -631,16 +634,16 @@ let test_optimal_comb () = in let pair_ty ty1 ty2 = pair_t (-1) ty1 ty2 in test_context () >>=? fun ctxt -> - pair_ty leaf_ty leaf_ty >>??= fun comb2_ty -> + pair_ty leaf_ty leaf_ty >>??= fun (Ty_ex_c comb2_ty) -> let comb2_v = (leaf_v, leaf_v) in check_optimal_comb __LOC__ ctxt comb2_ty comb2_v 2 >>=? fun ctxt -> - pair_ty leaf_ty comb2_ty >>??= fun comb3_ty -> + pair_ty leaf_ty comb2_ty >>??= fun (Ty_ex_c comb3_ty) -> let comb3_v = (leaf_v, comb2_v) in check_optimal_comb __LOC__ ctxt comb3_ty comb3_v 3 >>=? fun ctxt -> - pair_ty leaf_ty comb3_ty >>??= fun comb4_ty -> + pair_ty leaf_ty comb3_ty >>??= fun (Ty_ex_c comb4_ty) -> let comb4_v = (leaf_v, comb3_v) in check_optimal_comb __LOC__ ctxt comb4_ty comb4_v 4 >>=? fun ctxt -> - pair_ty leaf_ty comb4_ty >>??= fun comb5_ty -> + pair_ty leaf_ty comb4_ty >>??= fun (Ty_ex_c comb5_ty) -> let comb5_v = (leaf_v, comb4_v) in check_optimal_comb __LOC__ ctxt comb5_ty comb5_v 5 >>=? fun _ctxt -> return_unit diff --git a/src/proto_alpha/lib_protocol/ticket_scanner.ml b/src/proto_alpha/lib_protocol/ticket_scanner.ml index e533549b8c244d86e21887011c00cc4140547331..2130c276718fc1b83e4e243956cf5da65da050c1 100644 --- a/src/proto_alpha/lib_protocol/ticket_scanner.ml +++ b/src/proto_alpha/lib_protocol/ticket_scanner.ml @@ -163,13 +163,13 @@ module Ticket_inspection = struct | Address_t -> (k [@ocaml.tailcall]) False_ht | Tx_rollup_l2_address_t -> (k [@ocaml.tailcall]) False_ht | Bool_t -> (k [@ocaml.tailcall]) False_ht - | Pair_t (ty1, ty2, _) -> + | Pair_t (ty1, ty2, _, _) -> (has_tickets_of_pair [@ocaml.tailcall]) ty1 ty2 ~pair:(fun ht1 ht2 -> Pair_ht (ht1, ht2)) k - | Union_t (ty1, ty2, _) -> + | Union_t (ty1, ty2, _, _) -> (has_tickets_of_pair [@ocaml.tailcall]) ty1 ty2 @@ -179,7 +179,7 @@ module Ticket_inspection = struct (* As of H, closures cannot contain tickets because APPLY requires a packable type and tickets are not packable. *) (k [@ocaml.tailcall]) False_ht - | Option_t (ty, _) -> + | Option_t (ty, _, _) -> (has_tickets_of_ty [@ocaml.tailcall]) ty (fun ht -> let opt_hty = map_has_tickets (fun ht -> Option_ht ht) ht in (k [@ocaml.tailcall]) opt_hty) @@ -322,7 +322,7 @@ module Ticket_collection = struct consume_gas_steps ctxt ~num_steps:1 >>?= fun ctxt -> match (hty, ty) with | (False_ht, _) -> (k [@ocaml.tailcall]) ctxt acc - | (Pair_ht (hty1, hty2), Pair_t (ty1, ty2, _)) -> + | (Pair_ht (hty1, hty2), Pair_t (ty1, ty2, _, _)) -> let (l, r) = x in (tickets_of_value [@ocaml.tailcall]) ~include_lazy @@ -340,7 +340,7 @@ module Ticket_collection = struct r acc k) - | (Union_ht (htyl, htyr), Union_t (tyl, tyr, _)) -> ( + | (Union_ht (htyl, htyr), Union_t (tyl, tyr, _, _)) -> ( match x with | L v -> (tickets_of_value [@ocaml.tailcall]) @@ -360,7 +360,7 @@ module Ticket_collection = struct v acc k) - | (Option_ht el_hty, Option_t (el_ty, _)) -> ( + | (Option_ht el_hty, Option_t (el_ty, _, _)) -> ( match x with | Some x -> (tickets_of_value [@ocaml.tailcall])