diff --git a/docs/protocols/alpha.rst b/docs/protocols/alpha.rst index c6a15a2d78d8d4b214dd8e1ff02bb9f80fa453a6..ee76af25f06e944e9904e1a9519a502feba73b39 100644 --- a/docs/protocols/alpha.rst +++ b/docs/protocols/alpha.rst @@ -94,8 +94,8 @@ Michelson - Type annotations are ignored and not propagated. (MR :gl:`!4141`) -- Field annotations are ignored and not propagated on comparable types and on - regular pairs (MR :gl:`!4175`) +- Field annotations are ignored and not propagated. + (MR :gl:`!4175`, :gl:`!4311`, :gl:`!4259`) - Annotating the parameter toplevel constructor to designate the root entrypoint is now forbidden. Put the annotation on the parameter type instead. diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index 9e34f20503f54d097f8f9b40d6f210cb1dee702c..7e27e332c6ec2c63862ac21a48b8f81e2549ec84 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* (lsize, rsize) = pick_split (size - 1) in let* (Ex_ty left) = m_type ~size:lsize in let* (Ex_ty right) = m_type ~size:rsize in - match union_t (-1) (left, None) (right, None) with + match union_t (-1) left right with | Error _ -> assert false | Ok res_ty -> return @@ Ex_ty res_ty) | `TOption -> ( @@ -539,7 +539,7 @@ end) 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) diff --git a/src/proto_alpha/lib_benchmark/test/test_distribution.ml b/src/proto_alpha/lib_benchmark/test/test_distribution.ml index 2591f85de4c67fa22bd789af561b48438adfe681..980c7e351baf7b870cae5ccbb899cc57a758c9fc 100644 --- a/src/proto_alpha/lib_benchmark/test/test_distribution.ml +++ b/src/proto_alpha/lib_benchmark/test/test_distribution.ml @@ -70,7 +70,7 @@ let rec tnames_of_type : | Script_typed_ir.Bool_t _ -> `TBool :: acc | 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)) diff --git a/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml b/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml index 826529558b370368fbe5876fac49634e26c23cb1..0e659cc97c91f52514d1680aa606280f7180da2d 100644 --- a/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml +++ b/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml @@ -98,9 +98,7 @@ let pair k1 k2 = (* union type constructor*) let union k1 k2 = - match union_t (-1) (k1, None) (k2, None) with - | Error _ -> assert false - | Ok t -> t + match union_t (-1) k1 k2 with Error _ -> assert false | Ok 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_client/michelson_v1_emacs.ml b/src/proto_alpha/lib_client/michelson_v1_emacs.ml index c7e7010770a6784bbb43b931f18e211298a399cd..66a970b5e6e190bd51a259f54f5dbdfcc5507650 100644 --- a/src/proto_alpha/lib_client/michelson_v1_emacs.ml +++ b/src/proto_alpha/lib_client/michelson_v1_emacs.ml @@ -103,8 +103,7 @@ let print_type_map ppf (parsed, type_map) = let first_error_location errs = let rec find = function | [] -> 0 - | ( Inconsistent_type_annotations (loc, _, _) - | Unexpected_annotation loc + | ( Unexpected_annotation loc | Ill_formed_type (_, _, loc) | Invalid_arity (loc, _, _, _) | Invalid_seq_arity (loc, _, _) diff --git a/src/proto_alpha/lib_client/michelson_v1_error_reporter.ml b/src/proto_alpha/lib_client/michelson_v1_error_reporter.ml index 8eb1e753855f4f14d6ef536936569f6190b6d19d..e74e64be2b3bb2566f2d11f5b9a18bee8280b9ee 100644 --- a/src/proto_alpha/lib_client/michelson_v1_error_reporter.ml +++ b/src/proto_alpha/lib_client/michelson_v1_error_reporter.ml @@ -79,7 +79,6 @@ let collect_error_locations errs = | Environment.Ecoproto_error ( Invalid_arity (loc, _, _, _) | Invalid_seq_arity (loc, _, _) - | Inconsistent_type_annotations (loc, _, _) | Unexpected_annotation loc | Ungrouped_annotations loc | Type_too_large (loc, _) @@ -618,26 +617,6 @@ let report_errors ~details ~show_source ?parsed ppf errs = "@[ A view name, \"%s\", exceeds the maximum length of 31 \ characters." name - | Inconsistent_annotations (annot1, annot2) -> - Format.fprintf - ppf - "@[The two annotations do not match:@,\ - - @[%s@]@,\ - - @[%s@]@]" - annot1 - annot2 - | Inconsistent_type_annotations (loc, ty1, ty2) -> - Format.fprintf - ppf - "@[%athe two types contain incompatible annotations:@,\ - - @[%a@]@,\ - - @[%a@]@]" - print_loc - loc - print_ty - ty1 - print_ty - ty2 | Inconsistent_type_sizes (size1, size2) -> Format.fprintf ppf diff --git a/src/proto_alpha/lib_plugin/plugin.ml b/src/proto_alpha/lib_plugin/plugin.ml index 113c2f259cdee3a7330df690f2d95a06ab82e0f6..466f1039432dc7fb990ff79246182922375d88db 100644 --- a/src/proto_alpha/lib_plugin/plugin.ml +++ b/src/proto_alpha/lib_plugin/plugin.ml @@ -2001,7 +2001,7 @@ module RPC = struct let tl = unparse_ty ~loc utl in let tr = unparse_ty ~loc utr in return (T_pair, [tl; tr], annot) - | Union_t ((utl, _l_field), (utr, _r_field), _meta) -> + | Union_t (utl, utr, _meta) -> let annot = [] in let tl = unparse_ty ~loc utl in let tr = unparse_ty ~loc utr in diff --git a/src/proto_alpha/lib_protocol/script_ir_annot.ml b/src/proto_alpha/lib_protocol/script_ir_annot.ml index 2f06b7c5ebc7b722775322505847d9485ce6b44d..dc0210d23fe54f8adfc301b942efe07162519325 100644 --- a/src/proto_alpha/lib_protocol/script_ir_annot.ml +++ b/src/proto_alpha/lib_protocol/script_ir_annot.ml @@ -39,31 +39,6 @@ module FOR_TESTS = struct Field_annot (Non_empty_string.of_string_exn s) end -let field_annot_opt_to_entrypoint_strict ~loc = function - | None -> Ok Entrypoint.default - | Some (Field_annot a) -> Entrypoint.of_annot_strict ~loc a - -let merge_field_annot : - type error_trace. - legacy:bool -> - error_details:error_trace error_details -> - field_annot option -> - field_annot option -> - (field_annot option, error_trace) result = - fun ~legacy ~error_details annot1 annot2 -> - match (annot1, annot2) with - | (None, None) | (Some _, None) | (None, Some _) -> Result.return_none - | (Some (Field_annot a1), Some (Field_annot a2)) -> - if legacy || Non_empty_string.(a1 = a2) then ok annot1 - else - Error - (match error_details with - | Fast -> Inconsistent_types_fast - | Informative -> - trace_of_error - @@ Inconsistent_annotations - ("%" ^ (a1 :> string), "%" ^ (a2 :> string))) - let error_unexpected_annot loc annot = match annot with | [] -> Result.return_unit @@ -224,6 +199,14 @@ let extract_field_annot : >|? fun field_annot -> (Prim (loc, prim, args, annot), field_annot) | expr -> ok (expr, None) +let has_field_annot node = + extract_field_annot node >|? function + | (_node, Some _) -> true + | (_node, None) -> false + +let remove_field_annot node = + extract_field_annot node >|? fun (node, _a) -> node + let extract_entrypoint_annot : Script.node -> (Script.node * Entrypoint.t option) tzresult = fun node -> @@ -239,23 +222,13 @@ let check_var_annot : Script.location -> string list -> unit tzresult = error_unexpected_annot loc fields >>? fun () -> get_one_annot loc vars >|? fun (_a : var_annot option) -> () -let ignore_special f = - match f with - | Some (Field_annot fa) when Non_empty_string.(fa = at) -> ok None - | _ -> ok f - -let parse_constr_annot : - Script.location -> - string list -> - (field_annot option * field_annot option) tzresult = +let check_constr_annot : Script.location -> string list -> unit tzresult = fun loc annot -> parse_annots ~allow_special_field:true loc annot >>? classify_annot loc >>? fun (vars, types, fields) -> get_one_annot loc vars >>? fun (_v : var_annot option) -> get_one_annot loc types >>? fun (_t : type_annot option) -> - get_two_annot loc fields >>? fun (f1, f2) -> - ignore_special f1 >>? fun f1 -> - ignore_special f2 >|? fun f2 -> (f1, f2) + get_two_annot loc fields >|? fun (_f1, _f2) -> () let check_two_var_annot : Script.location -> string list -> unit tzresult = fun loc annot -> @@ -288,6 +261,16 @@ let parse_entrypoint_annot : get_one_annot loc fields >>? fun f -> get_one_annot loc vars >|? fun (_v : var_annot option) -> f +let parse_entrypoint_annot_strict loc annot = + parse_entrypoint_annot loc annot >>? function + | None -> Ok Entrypoint.default + | Some (Field_annot a) -> Entrypoint.of_annot_strict ~loc a + +let parse_entrypoint_annot_lax loc annot = + parse_entrypoint_annot loc annot >>? function + | None -> Ok Entrypoint.default + | Some (Field_annot annot) -> Entrypoint.of_annot_lax annot + let check_var_type_annot : Script.location -> string list -> unit tzresult = fun loc annot -> parse_annots loc annot >>? classify_annot loc >>? fun (vars, types, fields) -> diff --git a/src/proto_alpha/lib_protocol/script_ir_annot.mli b/src/proto_alpha/lib_protocol/script_ir_annot.mli index 664673928c0e2ac9f627159596487ee808199b4c..d97233de873fb31fb2ac6527b99e11aa95d42c97 100644 --- a/src/proto_alpha/lib_protocol/script_ir_annot.mli +++ b/src/proto_alpha/lib_protocol/script_ir_annot.mli @@ -32,23 +32,6 @@ module FOR_TESTS : sig val unsafe_field_annot_of_string : string -> field_annot end -(** Converts a field annot option to an entrypoint. - An error is returned if the field annot is too long or is "default". - [None] is converted to [Some default]. -*) -val field_annot_opt_to_entrypoint_strict : - loc:Script.location -> field_annot option -> Entrypoint.t tzresult - -(** Merge field annotations. - @return an error {!Inconsistent_type_annotations} if they are both present - and different, unless [legacy] *) -val merge_field_annot : - legacy:bool -> - error_details:'error_trace Script_tc_errors.error_details -> - field_annot option -> - field_annot option -> - (field_annot option, 'error_trace) result - (** @return an error {!Unexpected_annotation} in the monad the list is not empty. *) val error_unexpected_annot : Script.location -> 'a list -> unit tzresult @@ -70,9 +53,11 @@ val is_field_annot : Script.location -> string -> bool tzresult [:ty_name %field1 %field2] in any order. *) val check_composed_type_annot : Script.location -> string list -> unit tzresult -(** Extract and remove a field annotation from a node *) -val extract_field_annot : - Script.node -> (Script.node * field_annot option) tzresult +(** Checks whether a node has a field annotation. *) +val has_field_annot : Script.node -> bool tzresult + +(** Removes a field annotation from a node. *) +val remove_field_annot : Script.node -> Script.node tzresult (** Extract and remove a field annotation as an entrypoint from a node *) val extract_entrypoint_annot : @@ -85,10 +70,7 @@ val check_var_annot : Script.location -> string list -> unit tzresult val is_allowed_char : char -> bool -val parse_constr_annot : - Script.location -> - string list -> - (field_annot option * field_annot option) tzresult +val check_constr_annot : Script.location -> string list -> unit tzresult val check_two_var_annot : Script.location -> string list -> unit tzresult @@ -96,7 +78,16 @@ val check_destr_annot : Script.location -> string list -> unit tzresult val check_unpair_annot : Script.location -> string list -> unit tzresult -val parse_entrypoint_annot : - Script.location -> string list -> field_annot option tzresult +(** Parses a field annotation and converts it to an entrypoint. + An error is returned if the annotation is too long or is "default". + An empty annotation is converted to "default". *) +val parse_entrypoint_annot_strict : + Script.location -> string list -> Entrypoint.t tzresult + +(** Parse a field annotation and convert it to an entrypoint. + An error is returned if the field annot is too long. + An empty annotation is converted to "default". *) +val parse_entrypoint_annot_lax : + Script.location -> string list -> Entrypoint.t tzresult val check_var_type_annot : Script.location -> string list -> unit tzresult diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 1a5438b1631a77a318286e5cad4c007136e2ca42..af68507530ccc937c0af2c3e8b0754f5408ffd9c 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -175,8 +175,7 @@ let rec ty_of_comparable_ty : type a. a comparable_ty -> a ty = function | Pair_key (l, r, tname) -> Pair_t (ty_of_comparable_ty l, ty_of_comparable_ty r, tname) | Union_key (l, r, tname) -> - Union_t - ((ty_of_comparable_ty l, None), (ty_of_comparable_ty r, None), tname) + Union_t (ty_of_comparable_ty l, ty_of_comparable_ty r, tname) | Option_key (t, tname) -> Option_t (ty_of_comparable_ty t, tname) let rec unparse_comparable_ty_uncarbonated : @@ -251,7 +250,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, _l_field), (utr, _r_field), _meta) -> + | Union_t (utl, utr, _meta) -> let (entrypoints_l, entrypoints_r) = match nested_entrypoints with | Entrypoints_None -> (no_entrypoints, no_entrypoints) @@ -357,7 +356,7 @@ let[@coq_axiom_with_reason "gadt"] rec comparable_ty_of_ty : 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, _al), (r, _ar), tname) -> + | Union_t (l, r, tname) -> comparable_ty_of_ty ctxt loc l >>? fun (lty, ctxt) -> comparable_ty_of_ty ctxt loc r >|? fun (rty, ctxt) -> (Union_key (lty, rty, tname), ctxt) @@ -683,8 +682,7 @@ let check_dupable_ty ctxt loc ty = | Chest_key_t _ -> return_unit | Ticket_t _ -> of_result (error (Unexpected_ticket loc)) | Pair_t (ty_a, ty_b, _) -> aux loc ty_a >>$ fun () -> aux loc ty_b - | Union_t ((ty_a, _), (ty_b, _), _) -> - aux loc ty_a >>$ fun () -> aux loc ty_b + | Union_t (ty_a, ty_b, _) -> aux loc ty_a >>$ fun () -> aux loc ty_b | Lambda_t (_, _, _) -> (* Lambda are dupable as long as: @@ -876,9 +874,6 @@ let merge_types : let ty2 = serialize_ty_for_error ty2 in Inconsistent_types (Some loc, ty1, ty2)) in - let merge_field_annot ~legacy tn1 tn2 = - of_result (merge_field_annot ~legacy ~error_details tn1 tn2) - in let merge_memo_sizes ms1 ms2 = of_result (merge_memo_sizes ~error_details ms1 ms2) in @@ -957,15 +952,11 @@ let merge_types : help tal tbl >>$ fun (Eq, left_ty) -> help tar tbr >|$ fun (Eq, right_ty) -> ((Eq : (ta ty, tb ty) eq), Pair_t (left_ty, right_ty, tname)) - | ( Union_t ((tal, tal_annot), (tar, tar_annot), tn1), - Union_t ((tbl, tbl_annot), (tbr, tbr_annot), tn2) ) -> + | (Union_t (tal, tar, tn1), Union_t (tbl, tbr, tn2)) -> merge_type_metadata tn1 tn2 >>$ fun tname -> - merge_field_annot ~legacy tal_annot tbl_annot >>$ fun left_annot -> - merge_field_annot ~legacy tar_annot tbr_annot >>$ fun right_annot -> help tal tbl >>$ fun (Eq, left_ty) -> help tar tbr >|$ fun (Eq, right_ty) -> - ( (Eq : (ta ty, tb ty) eq), - Union_t ((left_ty, left_annot), (right_ty, right_annot), tname) ) + ((Eq : (ta ty, tb ty) eq), Union_t (left_ty, right_ty, tname)) | (Lambda_t (tal, tar, tn1), Lambda_t (tbl, tbr, tn2)) -> merge_type_metadata tn1 tn2 >>$ fun tname -> help tal tbl >>$ fun (Eq, left_ty) -> @@ -1188,13 +1179,13 @@ let[@coq_struct "ty"] rec parse_comparable_ty : error (Invalid_arity (loc, prim, 0, List.length l)) | Prim (loc, T_pair, left :: right, annot) -> check_type_annot loc annot >>? fun () -> - extract_field_annot left >>? fun (left, _left_annot) -> + remove_field_annot left >>? fun left -> (match right with - | [right] -> extract_field_annot right + | [right] -> remove_field_annot right | right -> (* Unfold [pair t1 ... tn] as [pair t1 (... (pair tn-1 tn))] *) - ok (Prim (loc, T_pair, right, []), None)) - >>? fun (right, _right_annot) -> + ok (Prim (loc, T_pair, right, []))) + >>? fun right -> parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt right >>? fun (Ex_comparable_ty right, ctxt) -> parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt left @@ -1202,8 +1193,8 @@ let[@coq_struct "ty"] rec parse_comparable_ty : pair_key loc left right >|? fun ty -> (Ex_comparable_ty ty, ctxt) | Prim (loc, T_or, [left; right], annot) -> check_type_annot loc annot >>? fun () -> - extract_field_annot left >>? fun (left, _left_annot) -> - extract_field_annot right >>? fun (right, _right_annot) -> + remove_field_annot left >>? fun left -> + remove_field_annot right >>? fun right -> parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt right >>? fun (Ex_comparable_ty right, ctxt) -> parse_comparable_ty ~stack_depth:(stack_depth + 1) ctxt left @@ -1366,7 +1357,7 @@ let[@coq_axiom_with_reason "complex mutually recursive definition"] rec parse_ty contract_t loc tl >|? fun ty -> return ctxt ty else error (Unexpected_contract loc) | Prim (loc, T_pair, utl :: utr, annot) -> - extract_field_annot utl >>? fun (utl, _left_field) -> + remove_field_annot utl >>? fun utl -> parse_ty ctxt ~stack_depth:(stack_depth + 1) @@ -1379,11 +1370,11 @@ let[@coq_axiom_with_reason "complex mutually recursive definition"] rec parse_ty utl >>? fun (Ex_ty tl, ctxt) -> (match utr with - | [utr] -> extract_field_annot utr + | [utr] -> remove_field_annot utr | utr -> (* Unfold [pair t1 ... tn] as [pair t1 (... (pair tn-1 tn))] *) - ok (Prim (loc, T_pair, utr, []), None)) - >>? fun (utr, _right_field) -> + ok (Prim (loc, T_pair, utr, []))) + >>? fun utr -> parse_ty ctxt ~stack_depth:(stack_depth + 1) @@ -1400,8 +1391,8 @@ let[@coq_axiom_with_reason "complex mutually recursive definition"] rec parse_ty | Prim (loc, T_or, [utl; utr], annot) -> ( (match ret with | Don't_parse_entrypoints -> - extract_field_annot utl >>? fun (utl, _left_constr) -> - extract_field_annot utr >|? fun (utr, _right_constr) -> (utl, utr) + remove_field_annot utl >>? fun utl -> + remove_field_annot utr >|? fun utr -> (utl, utr) | Parse_entrypoints -> ok (utl, utr)) >>? fun (utl, utr) -> parse_ty @@ -1431,8 +1422,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, None) (tr, None) >|? fun ty -> - ((Ex_ty ty : ret), ctxt) + union_t loc tl tr >|? fun ty -> ((Ex_ty ty : ret), ctxt) | Parse_entrypoints -> let (Ex_parameter_ty_and_entrypoints {arg_type = tl; entrypoints = left}) = @@ -1442,7 +1432,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, None) (tr, None) >|? fun arg_type -> + union_t loc tl tr >|? fun arg_type -> let entrypoints = {name; nested = Entrypoints_Union {left; right}} in @@ -1457,7 +1447,7 @@ let[@coq_axiom_with_reason "complex mutually recursive definition"] rec parse_ty | Prim (loc, T_option, [ut], annot) -> (if legacy then (* legacy semantics with (broken) field annotations *) - extract_field_annot ut >>? fun (ut, _some_constr) -> + remove_field_annot ut >>? fun ut -> check_composed_type_annot loc annot >>? fun () -> ok ut else check_type_annot loc annot >>? fun () -> ok ut) >>? fun ut -> @@ -1780,7 +1770,7 @@ let check_packable ~legacy loc root = | 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 + | 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 @@ -1886,8 +1876,7 @@ let find_entrypoint (type full error_trace) match (ty, entrypoints) with | (_, {name = Some name; _}) when Entrypoint.(name = entrypoint) -> return ((fun e -> e), Ex_ty ty) - | ( Union_t ((tl, _al), (tr, _ar), _), - {nested = Entrypoints_Union {left; right}; _} ) -> ( + | (Union_t (tl, tr, _), {nested = Entrypoints_Union {left; right}; _}) -> ( find_entrypoint tl left entrypoint >??$ function | Ok (f, t) -> return ((fun e -> Prim (loc, D_Left, [f e], [])), t) | Error () -> @@ -1953,8 +1942,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, _al), (tr, _ar), _), - {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 @@ -2575,7 +2563,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 @@ -3198,7 +3186,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : Lwt.return @@ merge_branches ~legacy ctxt loc btr bfr {branch} (* pairs *) | (Prim (loc, I_PAIR, [], annot), Item_t (a, Item_t (b, rest))) -> - parse_constr_annot loc annot >>?= fun (_l_field, _r_field) -> + check_constr_annot loc annot >>?= fun () -> pair_t loc a b >>?= fun ty -> let stack_ty = Item_t (ty, rest) in let cons_pair = {apply = (fun kinfo k -> ICons_pair (kinfo, k))} in @@ -3334,21 +3322,21 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : | (Prim (loc, I_LEFT, [tr], annot), Item_t (tl, rest)) -> parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy tr >>?= fun (Ex_ty tr, ctxt) -> - parse_constr_annot loc annot >>?= fun (l_field, r_field) -> + check_constr_annot loc annot >>?= fun () -> let cons_left = {apply = (fun kinfo k -> ICons_left (kinfo, k))} in - union_t loc (tl, l_field) (tr, r_field) >>?= fun ty -> + union_t loc tl tr >>?= fun 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)) -> parse_any_ty ctxt ~stack_depth:(stack_depth + 1) ~legacy tl >>?= fun (Ex_ty tl, ctxt) -> - parse_constr_annot loc annot >>?= fun (l_field, r_field) -> + check_constr_annot loc annot >>?= fun () -> let cons_right = {apply = (fun kinfo k -> ICons_right (kinfo, k))} in - union_t loc (tl, l_field) (tr, r_field) >>?= fun ty -> + union_t loc tl tr >>?= fun 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, _l_field), (tr, _r_field), _), 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 () -> @@ -3889,7 +3877,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, _l_field), (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 @@ -4480,9 +4468,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : >>?= fun (Ex_ty t, ctxt) -> contract_t loc t >>?= fun contract_ty -> option_t loc contract_ty >>?= fun res_ty -> - parse_entrypoint_annot loc annot >>?= fun entrypoint -> - Script_ir_annot.field_annot_opt_to_entrypoint_strict ~loc entrypoint - >>?= fun entrypoint -> + parse_entrypoint_annot_strict loc annot >>?= fun entrypoint -> let instr = {apply = (fun kinfo k -> IContract (kinfo, t, entrypoint, k))} in @@ -4637,11 +4623,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : typed ctxt loc instr stack | (Prim (loc, (I_SELF as prim), [], annot), stack) -> Lwt.return - ( parse_entrypoint_annot loc annot >>? fun entrypoint -> - (match entrypoint with - | None -> Ok Entrypoint.default - | Some (Field_annot annot) -> Entrypoint.of_annot_lax annot) - >>? fun entrypoint -> + ( parse_entrypoint_annot_lax loc annot >>? fun entrypoint -> let open Tc_context in match tc_context.callsite with | _ when is_in_lambda tc_context -> @@ -5208,10 +5190,9 @@ and parse_toplevel : In the latter case we move it to the parameter type. *) - Script_ir_annot.extract_field_annot p >>? fun (_p, root_name) -> - match root_name with - | Some _ -> ok (p, pannot) - | None -> ( + Script_ir_annot.has_field_annot p >>? function + | true -> ok (p, pannot) + | false -> ( match pannot with | [single] when legacy @@ -5516,8 +5497,7 @@ let list_entrypoints ctxt (type full) (full : full ty) tzresult = fun t entrypoints path reachable acc -> match (t, entrypoints) with - | ( Union_t ((tl, _al), (tr, _ar), _), - {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 @@ -5589,7 +5569,7 @@ let[@coq_axiom_with_reason "gadt"] rec unparse_data : 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 @@ -6066,7 +6046,7 @@ let rec has_lazy_storage : type t. t ty -> t has_lazy_storage = | 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 + | 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 @@ -6124,10 +6104,10 @@ let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_updates ctxt mode 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) -> @@ -6221,9 +6201,9 @@ let[@coq_axiom_with_reason "gadt"] rec fold_lazy_storage : | 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) -> diff --git a/src/proto_alpha/lib_protocol/script_tc_errors.ml b/src/proto_alpha/lib_protocol/script_tc_errors.ml index b75572cae9c4b109e8226dfde73ea89211cd7939..ae5e3260b50c56ba7fca5cc3ab7bc37d06473dda 100644 --- a/src/proto_alpha/lib_protocol/script_tc_errors.ml +++ b/src/proto_alpha/lib_protocol/script_tc_errors.ml @@ -112,13 +112,6 @@ type error += Bad_stack_length type error += Bad_stack_item of int -type error += Inconsistent_annotations of string * string - -type error += - | Inconsistent_type_annotations : - Script.location * Script.expr * Script.expr - -> error - type error += Unexpected_annotation of Script.location type error += Ungrouped_annotations of Script.location diff --git a/src/proto_alpha/lib_protocol/script_tc_errors_registration.ml b/src/proto_alpha/lib_protocol/script_tc_errors_registration.ml index 26e5b3a9e4226368244153a2d48c0b1400352e4f..6f3eade19076627c375bffa75144340f840e91bb 100644 --- a/src/proto_alpha/lib_protocol/script_tc_errors_registration.ml +++ b/src/proto_alpha/lib_protocol/script_tc_errors_registration.ml @@ -365,31 +365,6 @@ let () = (function | Bad_stack (loc, name, s, sty) -> Some (loc, (name, s, sty)) | _ -> None) (fun (loc, (name, s, sty)) -> Bad_stack (loc, name, s, sty)) ; - (* Inconsistent annotations *) - register_error_kind - `Permanent - ~id:"michelson_v1.inconsistent_annotations" - ~title:"Annotations inconsistent between branches" - ~description:"The annotations on two types could not be merged" - (obj2 (req "annot1" string) (req "annot2" string)) - (function - | Inconsistent_annotations (annot1, annot2) -> Some (annot1, annot2) - | _ -> None) - (fun (annot1, annot2) -> Inconsistent_annotations (annot1, annot2)) ; - (* Inconsistent type annotations *) - register_error_kind - `Permanent - ~id:"michelson_v1.inconsistent_type_annotations" - ~title:"Types contain inconsistent annotations" - ~description:"The two types contain annotations that do not match" - (located - (obj2 - (req "type1" Script.expr_encoding) - (req "type2" Script.expr_encoding))) - (function - | Inconsistent_type_annotations (loc, ty1, ty2) -> Some (loc, (ty1, ty2)) - | _ -> None) - (fun (loc, (ty1, ty2)) -> Inconsistent_type_annotations (loc, ty1, ty2)) ; (* Unexpected annotation *) register_error_kind `Permanent diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 9ba4d5199aa1d98844474b1cc1b4f88da4db58e7..6945bbe3f2dc37c4fa35873e6cb9788427834d31 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -27,7 +27,6 @@ open Alpha_context open Script_int -open Script_ir_annot (* @@ -1304,11 +1303,7 @@ and 'ty ty = | Address_t : address ty_metadata -> address ty | Bool_t : bool ty_metadata -> bool ty | Pair_t : 'a ty * 'b ty * ('a, 'b) pair ty_metadata -> ('a, 'b) pair ty - | Union_t : - ('a ty * field_annot option) - * ('b ty * field_annot option) - * ('a, 'b) union ty_metadata - -> ('a, 'b) union ty + | Union_t : 'a ty * 'b ty * ('a, 'b) union ty_metadata -> ('a, 'b) union ty | Lambda_t : 'arg ty * 'ret ty * ('arg, 'ret) lambda ty_metadata -> ('arg, 'ret) lambda ty @@ -1846,12 +1841,11 @@ let pair_t loc l r = Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size -> Pair_t (l, r, {size}) -let union_t loc (l, fannot_l) (r, fannot_r) = +let union_t loc l r = Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size -> - Union_t ((l, fannot_l), (r, fannot_r), {size}) + Union_t (l, r, {size}) -let union_bytes_bool_t = - Union_t ((bytes_t, None), (bool_t, None), {size = Type_size.three}) +let union_bytes_bool_t = Union_t (bytes_t, bool_t, {size = Type_size.three}) let lambda_t loc l r = Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size -> @@ -2166,7 +2160,7 @@ let (ty_traverse, comparable_ty_traverse) = | 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, _), _) -> + | Union_t (ty1, ty2, _) -> (next2' [@ocaml.tailcall]) f accu ty1 ty2 continue | Lambda_t (ty1, ty2, _) -> (next2' [@ocaml.tailcall]) f accu ty1 ty2 continue @@ -2247,7 +2241,7 @@ let value_traverse (type t) (ty : (t ty, t comparable_ty) union) (x : t) init f | Lambda_t (_, _, _) -> (return [@ocaml.tailcall]) () | Pair_t (ty1, ty2, _) -> (next2 [@ocaml.tailcall]) ty1 ty2 (fst x) (snd x) - | Union_t ((ty1, _), (ty2, _), _) -> ( + | Union_t (ty1, ty2, _) -> ( match x with | L l -> (next [@ocaml.tailcall]) ty1 l | R r -> (next [@ocaml.tailcall]) ty2 r) diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 60f5fc11df21987c936907629fde23377fab3413..38ad03b265889c622aac19e3db1af251ebf0f9ac 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -27,7 +27,6 @@ open Alpha_context open Script_int -open Script_ir_annot type step_constants = { source : Contract.t; @@ -1392,11 +1391,7 @@ and 'ty ty = | Address_t : address ty_metadata -> address ty | Bool_t : bool ty_metadata -> bool ty | Pair_t : 'a ty * 'b ty * ('a, 'b) pair ty_metadata -> ('a, 'b) pair ty - | Union_t : - ('a ty * field_annot option) - * ('b ty * field_annot option) - * ('a, 'b) union ty_metadata - -> ('a, 'b) union ty + | Union_t : 'a ty * 'b ty * ('a, 'b) union ty_metadata -> ('a, 'b) union ty | Lambda_t : 'arg ty * 'ret ty * ('arg, 'ret) lambda ty_metadata -> ('arg, 'ret) lambda ty @@ -1578,11 +1573,7 @@ val bool_t : bool ty val pair_t : Script.location -> 'a ty -> 'b ty -> ('a, 'b) pair ty tzresult -val union_t : - Script.location -> - 'a ty * field_annot option -> - 'b ty * field_annot option -> - ('a, 'b) union ty tzresult +val union_t : Script.location -> 'a ty -> 'b ty -> ('a, 'b) union ty tzresult val union_bytes_bool_t : (Bytes.t, bool) union ty 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 6622dc7ae308ac2f50ce693512282a43cb18f478..86503c7908a1591c4776e9fde36727161bd284bb 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml @@ -89,8 +89,8 @@ let (comparable_ty_size, ty_size) = | Chest_t a -> ret_succ_adding accu @@ base_basic a | Pair_t (_ty1, _ty2, a) -> ret_succ_adding accu @@ (base_compound a +! (word_size *? 2)) - | Union_t ((_ty1, _fa1), (_ty2, _fa2), a) -> - ret_succ_adding accu @@ (base_compound a +! hh6w) + | Union_t (_ty1, _ty2, a) -> + ret_succ_adding accu @@ (base_compound a +! (word_size *? 2)) | 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) 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 0a3aa188953c1705e328a8432fd5c2c85d1a5966..82229eb5c1dcf52d9409440e203f80dd7f8b86a4 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 = 269853 +let liquidity_baking_contract_size = 269476 let liquidity_baking_contract = Contract.of_b58check "KT1TxqZ8QtKvLu3V3JH7Gx58n7Co8pgtpQU5" |> function diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml index 18407d30e6565f91fde0ad1a20ac8e7d5c1453fa..bfafbac9c33149d8de26f5413af1070a9fcd9a4c 100644 --- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml @@ -357,7 +357,7 @@ module Tests = struct let check_lambda_size_stats () = check_stats "lambda_size" - ~expected_mean:(1., 0.25) + ~expected_mean:(1., 0.3) ~expected_stddev:(0., 0.1) ~expected_ratios:(1., 0.4) end diff --git a/src/proto_alpha/lib_protocol/ticket_scanner.ml b/src/proto_alpha/lib_protocol/ticket_scanner.ml index e50eee3be5433519f2eeb86b323218ed79bfcceb..bcb497f1f26379da204030a9f85d4db4cde2db5b 100644 --- a/src/proto_alpha/lib_protocol/ticket_scanner.ml +++ b/src/proto_alpha/lib_protocol/ticket_scanner.ml @@ -167,7 +167,7 @@ module Ticket_inspection = struct 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 @@ -336,7 +336,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])