diff --git a/src/passes/09-typing/08-typer-common/errors.ml b/src/passes/09-typing/08-typer-common/errors.ml index b2a6bdf13..4e09f3285 100644 --- a/src/passes/09-typing/08-typer-common/errors.ml +++ b/src/passes/09-typing/08-typer-common/errors.ml @@ -1,6 +1,7 @@ open Trace open Simple_utils.Display + let stage = "typer" type typer_error = [ @@ -69,7 +70,28 @@ type typer_error = [ | `Typer_constant_decl_tracer of Ast_core.expression_variable * Ast_core.expr * Ast_typed.type_expression option * typer_error | `Typer_match_variant_tracer of Ast_core.matching_expr * typer_error | `Typer_unrecognized_type_operator of Ast_core.type_expression - |`Typer_expected_ascription of Ast_core.expression + | `Typer_expected_ascription of Ast_core.expression + | `Typer_different_kinds of Ast_typed.type_expression * Ast_typed.type_expression + | `Typer_different_constants of Ast_typed.type_constant * Ast_typed.type_constant + | `Typer_different_operators of Ast_typed.type_operator * Ast_typed.type_operator + | `Typer_operator_number_of_arguments of Ast_typed.type_operator * Ast_typed.type_operator * int * int + | `Typer_different_record_props of + Ast_typed.type_expression * Ast_typed.type_expression * Ast_typed.te_lmap * Ast_typed.te_lmap * string * string + | `Typer_different_kind_record_tuple of + Ast_typed.type_expression * Ast_typed.type_expression * Ast_typed.te_lmap * Ast_typed.te_lmap + | `Typer_different_size_records_tuples of + Ast_typed.type_expression * Ast_typed.type_expression * Ast_typed.te_lmap * Ast_typed.te_lmap + | `Typer_different_size_sums of + Ast_typed.type_expression * Ast_typed.type_expression + | `Typer_different_types of string * Ast_typed.type_expression * Ast_typed.type_expression * typer_error + | `Typer_different_literals of string * Ast_typed.literal * Ast_typed.literal + | `Typer_different_values of string * Ast_typed.expression * Ast_typed.expression + | `Typer_different_literals_because_different_types of string * Ast_typed.literal * Ast_typed.literal + | `Typer_different_values_because_different_types of string * Ast_typed.expression * Ast_typed.expression + | `Typer_uncomparable_literals of string * Ast_typed.literal * Ast_typed.literal + | `Typer_uncomparable_values of string * Ast_typed.expression * Ast_typed.expression + | `Typer_missing_key_in_record_value of string + | `Typer_compare_tracer of typer_error ] let michelson_comb_no_record (loc:Location.t) = `Typer_michelson_comb_no_record loc @@ -150,6 +172,23 @@ let constant_declaration_tracer (name: Ast_core.expression_variable) (ae:Ast_cor `Typer_constant_decl_tracer (name,ae,expected,err) let in_match_variant_tracer (ae:Ast_core.matching_expr) (err:typer_error) = `Typer_match_variant_tracer (ae,err) +let different_kinds a b = `Typer_different_kinds (a,b) +let different_constants a b = `Typer_different_constants (a,b) +let different_operators a b = `Typer_different_operators (a,b) +let different_operator_number_of_arguments opa opb lena lenb = `Typer_operator_number_of_arguments (opa, opb, lena, lenb) +let different_props_in_record a b ra rb ka kb = `Typer_different_record_props (a,b,ra,rb,ka,kb) +let different_kind_record_tuple a b ra rb = `Typer_different_kind_record_tuple (a,b,ra,rb) +let different_size_records_tuples a b ra rb = `Typer_different_size_records_tuples (a,b,ra,rb) +let different_size_sums a b = `Typer_different_size_sums (a,b) +let different_types name a b err = `Typer_different_types (name,a,b,err) +let different_literals name a b = `Typer_different_literals (name,a,b) +let different_values name a b = `Typer_different_values (name,a,b) +let different_literals_because_different_types name a b = `Typer_different_literals_because_different_types (name,a,b) +let different_values_because_different_types name a b = `Typer_different_values_because_different_types (name,a,b) +let error_uncomparable_literals name a b = `Typer_uncomparable_literals (name,a,b) +let error_uncomparable_values name a b = `Typer_uncomparable_values (name,a,b) +let missing_key_in_record_value k = `Typer_missing_key_in_record_value k +let compare_tracer err = `Typer_compare_tracer err let rec error_ppformat : display_format:string display_format -> Format.formatter -> typer_error -> unit = @@ -470,6 +509,75 @@ let rec error_ppformat : display_format:string display_format -> "@[%a@ expected ascription but got %a@]" Location.pp t.location Ast_core.PP.expression t + | `Typer_different_kinds (a,b) -> + Format.fprintf f + "@[ different kinds %a@ %a@]" + Ast_typed.PP.type_expression a + Ast_typed.PP.type_expression b + | `Typer_different_constants (a,b) -> + Format.fprintf f + "@[ different type constructors.@ \ + Expected these two constant type constructors to be the same, but they're different@ %a@ %a@]" + Ast_typed.PP.type_constant a + Ast_typed.PP.type_constant b + | `Typer_different_operators (a,b) -> + Format.fprintf f + "@[ different type constructors.@ \ + Expected these two n-ary type constructors to be the same, but they're different@ %a@ %a@]" + (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) a + (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) b + | `Typer_operator_number_of_arguments (opa, _opb, lena, lenb) -> + Format.fprintf f + "@[ different number of arguments to type constructors.@ \ + Expected these two n-ary type constructors to be the same, but they have different number\ + of arguments (both use the %s type constructor, but they have %d and %d arguments, respectively)@]" + (Ast_typed.Helpers.type_operator_name opa) lena lenb + | `Typer_different_record_props (_a,_b,ra,rb,_ka,_kb) -> + let names = if Ast_typed.Helpers.is_tuple_lmap ra &&Ast_typed.Helpers.is_tuple_lmap rb + then "tuples" else "records" in + Format.fprintf f + "@[ different keys in %s@]" + names + | `Typer_different_kind_record_tuple (_a,_b,ra,rb) -> + let name_a = if Ast_typed.Helpers.is_tuple_lmap ra then "tuple" else "record" in + let name_b = if Ast_typed.Helpers.is_tuple_lmap rb then "tuple" else "record" in + Format.fprintf f + "@[ different keys.@ Expected these two types to be the same, but they're different (one is a %s\ + and the other is a %s)@]" + name_a name_b + | `Typer_different_size_records_tuples (_a,_b,ra,rb) -> + let n = if Ast_typed.Helpers.is_tuple_lmap ra && Ast_typed.Helpers.is_tuple_lmap rb + then "tuples" else "records" in + Format.fprintf f + "@[ %s have different sizes.@ Expected these two types to be the same, but they're \ + different (both are %s, but with a different number of arguments)@]" + n n + | `Typer_different_size_sums (_a,_b) -> + Format.fprintf f + "@[ sum types have different sizes.@ Expected these two types to be the same, but they're \ + different" + | `Typer_different_types (name,_a,_b,err) -> + Format.fprintf f + "@[ %s are different.\ + Expected these two types to be the same, but they're different.@ %a@]" + name + (error_ppformat ~display_format) err + | `Typer_different_literals (name,_a,_b) -> + Format.fprintf f "@[ %s are different@]" name + | `Typer_different_values (name,_a,_b) -> + Format.fprintf f "@[ %s are different@]" name + | `Typer_different_literals_because_different_types (name,_a,_b) -> + Format.fprintf f "@[ Literals have different types: %s@]" name + | `Typer_different_values_because_different_types (name,_a,_b) -> + Format.fprintf f "@[ Values have different types: %s@]" name + | `Typer_uncomparable_literals (name,_a,_b) -> + Format.fprintf f "@[ %s are not comparable @]" name + | `Typer_uncomparable_values (name,_a,_b) -> + Format.fprintf f "@[ %s are not comparable @]" name + | `Typer_missing_key_in_record_value k -> + Format.fprintf f "@[ missing %s in one of the record @]" k + | `Typer_compare_tracer err -> + error_ppformat ~display_format f err ) let rec error_jsonformat : typer_error -> J.t = fun a -> @@ -1150,4 +1258,190 @@ let rec error_jsonformat : typer_error -> J.t = fun a -> ("location", location) ; ("value", value) ; ] in + json_error ~stage ~content + | `Typer_different_kinds (a,b) -> + let message = `String "different kinds" in + let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_different_constants (a,b) -> + let message = `String "different type constructors.\ + Expected these two constant type constructors to be the same, but they're different" in + let a = `String (Format.asprintf "%a" Ast_typed.PP.type_constant a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.type_constant b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_different_operators (a,b) -> + let message = `String "different type constructors.\ + Expected these two n-ary type constructors to be the same, but they're different" in + let a = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) a) in + let b = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_operator_number_of_arguments (opa, opb, lena, lenb) -> + let message = `String "different number of arguments to type constructors.\ + Expected these two n-ary type constructors to be the same, but they have different number\ + of arguments" in + let a = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) opa) in + let b = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) opb) in + let op = `String (Ast_typed.Helpers.type_operator_name opa) in + let len_a = `Int lena in + let len_b = `Int lenb in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ("op", op) ; + ("len_a", len_a) ; + ("len_b", len_b) ; + ] in + json_error ~stage ~content + | `Typer_different_record_props (a,b,ra,rb,ka,kb) -> + let names = if Ast_typed.Helpers.is_tuple_lmap ra &&Ast_typed.Helpers.is_tuple_lmap rb + then "tuples" else "records" in + let message = `String ("different keys in " ^ names) in + let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ("ka", `String ka) ; + ("kb", `String kb) ; + ] in + json_error ~stage ~content + | `Typer_different_kind_record_tuple (a,b,ra,rb) -> + let name_a = if Ast_typed.Helpers.is_tuple_lmap ra then "tuple" else "record" in + let name_b = if Ast_typed.Helpers.is_tuple_lmap rb then "tuple" else "record" in + let message = `String ("different keys. Expected these two types to be the same, but they're different (one is a " + ^ name_a ^ " and the other is a " ^ name_b ^ ")") in + let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_different_size_records_tuples (a,b,ra,rb) -> + let n = if Ast_typed.Helpers.is_tuple_lmap ra && Ast_typed.Helpers.is_tuple_lmap rb + then "tuples" else "records" in + let message = `String (n^ " have different sizes. Expected these two types to be the same, but they're \ + different (both are " ^ n ^ ", but with a different number of arguments)") in + let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_different_size_sums (a,b) -> + let message = `String (" sum types have different sizes. Expected these two types to be the same, but they're \ + different") in + let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_different_types (name,a,b,err) -> + let message = `String (name ^" are different.\ + Expected these two types to be the same, but they're different") in + let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ("children", error_jsonformat err) + ] in + json_error ~stage ~content + | `Typer_different_literals (name,a,b) -> + let message = `String (name ^ " are different") in + let a = `String (Format.asprintf "%a" Ast_typed.PP.literal a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.literal b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_different_values (name,a,b) -> + let message = `String (name ^ " are different") in + let a = `String (Format.asprintf "%a" Ast_typed.PP.expression a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.expression b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_different_literals_because_different_types (name,a,b) -> + let message = `String ("literals have different types: " ^ name) in + let a = `String (Format.asprintf "%a" Ast_typed.PP.literal a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.literal b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_different_values_because_different_types (name,a,b) -> + let message = `String ("values have different types: " ^ name) in + let a = `String (Format.asprintf "%a" Ast_typed.PP.expression a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.expression b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_uncomparable_literals (name,a,b) -> + let message = `String (name ^ " are not comparable") in + let a = `String (Format.asprintf "%a" Ast_typed.PP.literal a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.literal b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_uncomparable_values (name,a,b) -> + let message = `String (name ^ " are not comparable") in + let a = `String (Format.asprintf "%a" Ast_typed.PP.expression a) in + let b = `String (Format.asprintf "%a" Ast_typed.PP.expression b) in + let content = `Assoc [ + ("message", message) ; + ("a", a) ; + ("b", b) ; + ] in + json_error ~stage ~content + | `Typer_missing_key_in_record_value k -> + let message = `String "missing keys in one of the records" in + let content = `Assoc [ + ("message", message) ; + ("missing_key", `String k) ; + ] in + json_error ~stage ~content + | `Typer_compare_tracer err -> + let content = `Assoc [ + ("message", `String "not equal") ; + ("children", error_jsonformat err) + ] in json_error ~stage ~content \ No newline at end of file diff --git a/src/passes/09-typing/08-typer-new/compare.ml b/src/passes/09-typing/08-typer-new/compare.ml new file mode 100644 index 000000000..957b2c9c7 --- /dev/null +++ b/src/passes/09-typing/08-typer-new/compare.ml @@ -0,0 +1,165 @@ +open Ast_typed +open Trace +open Typer_common.Errors + +let rec assert_type_expression_eq (a, b: (type_expression * type_expression)) : (unit, typer_error) result = match (a.type_content, b.type_content) with + | T_constant ca, T_constant cb -> ( + Assert.assert_true (different_constants ca cb) (ca = cb) + ) + | T_constant _, _ -> fail @@ different_kinds a b + | T_operator opa, T_operator opb -> ( + let%bind (lsta, lstb) = match (opa, opb) with + | TC_option la, TC_option lb + | TC_list la, TC_list lb + | TC_contract la, TC_contract lb + | TC_set la, TC_set lb -> ok @@ ([la], [lb]) + | (TC_map {k=ka;v=va} | TC_map_or_big_map {k=ka;v=va}), (TC_map {k=kb;v=vb} | TC_map_or_big_map {k=kb;v=vb}) + | (TC_big_map {k=ka;v=va} | TC_map_or_big_map {k=ka;v=va}), (TC_big_map {k=kb;v=vb} | TC_map_or_big_map {k=kb;v=vb}) + -> ok @@ ([ka;va] ,[kb;vb]) + | (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ ), + (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ ) + -> fail @@ different_operators opa opb + in + if List.length lsta <> List.length lstb then + fail @@ different_operator_number_of_arguments opa opb (List.length lsta) (List.length lstb) + else + trace (different_types "arguments to type operators" a b) + @@ bind_list_iter (fun (a,b) -> assert_type_expression_eq (a,b) )(List.combine lsta lstb) + ) + | T_operator _, _ -> fail @@ different_kinds a b + | T_sum sa, T_sum sb -> ( + let sa' = CMap.to_kv_list sa in + let sb' = CMap.to_kv_list sb in + let aux ((ka, {ctor_type=va;_}), (kb, {ctor_type=vb;_})) = + let%bind _ = + Assert.assert_true (corner_case "different keys in sum types") + @@ (ka = kb) in + assert_type_expression_eq (va, vb) + in + let%bind _ = + Assert.assert_list_same_size (different_size_sums a b) + sa' sb' + in + trace (different_types "sum type" a b) @@ + bind_list_iter aux (List.combine sa' sb') + ) + | T_sum _, _ -> fail @@ different_kinds a b + | T_record ra, T_record rb + when Helpers.is_tuple_lmap ra <> Helpers.is_tuple_lmap rb -> ( + fail @@ different_kind_record_tuple a b ra rb + ) + | T_record ra, T_record rb -> ( + let sort_lmap r' = List.sort (fun (Label a,_) (Label b,_) -> String.compare a b) r' in + let ra' = sort_lmap @@ LMap.to_kv_list ra in + let rb' = sort_lmap @@ LMap.to_kv_list rb in + let aux ((ka, {field_type=va;_}), (kb, {field_type=vb;_})) = + let%bind _ = + trace (different_types "records" a b) @@ + let Label ka = ka in + let Label kb = kb in + Assert.assert_true (different_props_in_record a b ra rb ka kb) (ka = kb) in + assert_type_expression_eq (va, vb) + in + let%bind _ = + Assert.assert_list_same_size (different_size_records_tuples a b ra rb) ra' rb' in + trace (different_types "record type" a b) + @@ bind_list_iter aux (List.combine ra' rb') + + ) + | T_record _, _ -> fail @@ different_kinds a b + | T_arrow {type1;type2}, T_arrow {type1=type1';type2=type2'} -> + let%bind _ = assert_type_expression_eq (type1, type1') in + let%bind _ = assert_type_expression_eq (type2, type2') in + ok () + | T_arrow _, _ -> fail @@ different_kinds a b + | T_variable x, T_variable y -> let _ = (x = y) in failwith "TODO : we must check that the two types were bound at the same location (even if they have the same name), i.e. use something like De Bruijn indices or a propper graph encoding" + | T_variable _, _ -> fail @@ different_kinds a b + +(* No information about what made it fail *) +let type_expression_eq ab = Trace.to_bool @@ assert_type_expression_eq ab + +let assert_literal_eq (a, b : literal * literal) : (unit, typer_error) result = + match (a, b) with + | Literal_int a, Literal_int b when a = b -> ok () + | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b + | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b + | Literal_nat a, Literal_nat b when a = b -> ok () + | Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b + | Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b + | Literal_timestamp a, Literal_timestamp b when a = b -> ok () + | Literal_timestamp _, Literal_timestamp _ -> fail @@ different_literals "different timestamps" a b + | Literal_timestamp _, _ -> fail @@ different_literals_because_different_types "timestamp vs non-timestamp" a b + | Literal_mutez a, Literal_mutez b when a = b -> ok () + | Literal_mutez _, Literal_mutez _ -> fail @@ different_literals "different tezs" a b + | Literal_mutez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b + | Literal_string a, Literal_string b when a = b -> ok () + | Literal_string _, Literal_string _ -> fail @@ different_literals "different strings" a b + | Literal_string _, _ -> fail @@ different_literals_because_different_types "string vs non-string" a b + | Literal_bytes a, Literal_bytes b when a = b -> ok () + | Literal_bytes _, Literal_bytes _ -> fail @@ different_literals "different bytes" a b + | Literal_bytes _, _ -> fail @@ different_literals_because_different_types "bytes vs non-bytes" a b + | Literal_void, Literal_void -> ok () + | Literal_void, _ -> fail @@ different_literals_because_different_types "void vs non-void" a b + | Literal_unit, Literal_unit -> ok () + | Literal_unit, _ -> fail @@ different_literals_because_different_types "unit vs non-unit" a b + | Literal_address a, Literal_address b when a = b -> ok () + | Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b + | Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b + | Literal_signature a, Literal_signature b when a = b -> ok () + | Literal_signature _, Literal_signature _ -> fail @@ different_literals "different signature" a b + | Literal_signature _, _ -> fail @@ different_literals_because_different_types "signature vs non-signature" a b + | Literal_key a, Literal_key b when a = b -> ok () + | Literal_key _, Literal_key _ -> fail @@ different_literals "different key" a b + | Literal_key _, _ -> fail @@ different_literals_because_different_types "key vs non-key" a b + | Literal_key_hash a, Literal_key_hash b when a = b -> ok () + | Literal_key_hash _, Literal_key_hash _ -> fail @@ different_literals "different key_hash" a b + | Literal_key_hash _, _ -> fail @@ different_literals_because_different_types "key_hash vs non-key_hash" a b + | Literal_chain_id a, Literal_chain_id b when a = b -> ok () + | Literal_chain_id _, Literal_chain_id _ -> fail @@ different_literals "different chain_id" a b + | Literal_chain_id _, _ -> fail @@ different_literals_because_different_types "chain_id vs non-chain_id" a b + | Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b + | Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b + + +let rec assert_value_eq (a, b: (expression*expression)) : (unit, typer_error) result = + trace compare_tracer @@ + match (a.expression_content, b.expression_content) with + | E_literal a, E_literal b -> + assert_literal_eq (a, b) + | E_constant {cons_name=ca;arguments=lsta}, E_constant {cons_name=cb;arguments=lstb} when ca = cb -> ( + let%bind lst = + generic_try (corner_case "constants with different number of elements") + (fun () -> List.combine lsta lstb) in + let%bind _all = bind_list @@ List.map assert_value_eq lst in + ok () + ) + | E_constant _, E_constant _ -> + fail @@ different_values "constants" a b + | E_constant _, _ -> + fail @@ (corner_case "comparing constant with other stuff") + + | E_constructor {constructor=ca;element=a}, E_constructor {constructor=cb;element=b} when ca = cb -> ( + let%bind _eq = assert_value_eq (a, b) in + ok () + ) + | E_constructor _, E_constructor _ -> + fail @@ different_values "constructors" a b + | E_constructor _, _ -> + fail @@ different_values_because_different_types "constructor vs. non-constructor" a b + | E_record sma, E_record smb -> ( + let aux (Label k) a b = + match a, b with + | Some a, Some b -> Some (assert_value_eq (a, b)) + | _ -> Some (fail @@ missing_key_in_record_value k) + in + let%bind _all = Helpers.bind_lmap @@ LMap.merge aux sma smb in + ok () + ) + | E_record _, _ -> + fail @@ (different_values_because_different_types "record vs. non-record" a b) + + | (E_literal _, _) | (E_variable _, _) | (E_application _, _) + | (E_lambda _, _) | (E_let_in _, _) | (E_raw_code _, _) | (E_recursive _, _) + | (E_record_accessor _, _) | (E_record_update _,_) + | (E_matching _, _) + -> fail @@ error_uncomparable_values "can't compare sequences nor loops" a b diff --git a/src/passes/09-typing/08-typer-new/typer.ml b/src/passes/09-typing/08-typer-new/typer.ml index 6b690ceb5..72d986205 100644 --- a/src/passes/09-typing/08-typer-new/typer.ml +++ b/src/passes/09-typing/08-typer-new/typer.ml @@ -14,8 +14,7 @@ module Map = RedBlackTrees.PolyMap open Todo_use_fold_generator let assert_type_expression_eq ((tv',tv):O.type_expression * O.type_expression) : (unit,typer_error) result = - trace_option (assert_equal tv' tv) @@ - O.assert_type_expression_eq (tv' , tv) + Compare.assert_type_expression_eq (tv' , tv) (* Extract pairs of (name,type) in the declaration and add it to the environment @@ -67,8 +66,8 @@ and type_match : environment -> O'.typer_state -> O.type_expression -> I.matchin let%bind acc = match acc with | None -> ok (Some variant) | Some variant' -> - let%bind () = trace_option (not_matching variant variant') @@ - Ast_typed.assert_type_expression_eq (variant , variant') in + let%bind () = + assert_type_expression_eq (variant , variant') in ok (Some variant) in ok acc in diff --git a/vendors/ligo-utils/simple-utils/trace.ml b/vendors/ligo-utils/simple-utils/trace.ml index 19c0e42bd..ff825eb60 100644 --- a/vendors/ligo-utils/simple-utils/trace.ml +++ b/vendors/ligo-utils/simple-utils/trace.ml @@ -545,6 +545,9 @@ module Assert = struct let assert_list_empty err lst = assert_true err List.(length lst = 0) + + let assert_list_same_size err lsta lstb = + assert_true err List.(length lsta = length lstb) end