From 69713036d0aad9cdce4013b99c5528d167e59b7e Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Mon, 13 Jun 2022 21:37:00 +0400 Subject: [PATCH] Add constraints to typechecker, fix old tests, add new ones --- priv/stdlib/List.aes | 8 +- priv/stdlib/Option.aes | 4 +- priv/stdlib/String.aes | 1 + src/aeso_ast_infer_types.erl | 133 ++++++++++++++- src/aeso_ast_to_fcode.erl | 2 + src/aeso_pretty.erl | 4 +- test/aeso_compiler_tests.erl | 84 +++++++++- .../comparable_typevar_constraints.aes | 156 ++++++++++++++++++ test/contracts/warnings.aes | 5 + 9 files changed, 383 insertions(+), 14 deletions(-) create mode 100644 test/contracts/comparable_typevar_constraints.aes diff --git a/priv/stdlib/List.aes b/priv/stdlib/List.aes index e0201d0..53b4841 100644 --- a/priv/stdlib/List.aes +++ b/priv/stdlib/List.aes @@ -29,9 +29,11 @@ namespace List = [] => abort("drop_last_unsafe: list empty") - function contains(e : 'a, l : list('a)) = switch(l) - [] => false - h::t => h == e || contains(e, t) + function + contains : 'a is eq; ('a, list('a)) => bool + contains(e, l) = switch(l) + [] => false + h::t => h == e || contains(e, t) /** Finds first element of `l` fulfilling predicate `p` as `Some` or `None` * if no such element exists. diff --git a/priv/stdlib/Option.aes b/priv/stdlib/Option.aes index 651a2d5..4009b7e 100644 --- a/priv/stdlib/Option.aes +++ b/priv/stdlib/Option.aes @@ -30,7 +30,9 @@ namespace Option = None => abort(err) Some(x) => x - function contains(e : 'a, o : option('a)) = o == Some(e) + function + contains : 'a is eq; ('a, option('a)) => bool + contains(e, o) = o == Some(e) function on_elem(o : option('a), f : 'a => unit) : unit = match((), f, o) diff --git a/priv/stdlib/String.aes b/priv/stdlib/String.aes index 99d5c0e..8046b78 100644 --- a/priv/stdlib/String.aes +++ b/priv/stdlib/String.aes @@ -90,6 +90,7 @@ namespace String = Some(ix) private function + is_prefix : (list(char), list(char)) => option(list(char)) is_prefix([], ys) = Some(ys) is_prefix(_, []) = None is_prefix(x :: xs, y :: ys) = diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 72c9372..8f00714 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -818,6 +818,12 @@ infer(Contracts, Options) -> ets_new(defined_contracts, [bag]), ets_new(type_vars, [set]), ets_new(warnings, [bag]), + + %% Set the constraints for the builtin types + ets_new(ord_constraint_types, [set]), + OrdTypes = [ {"int"}, {"bool"}, {"bits"}, {"char"}, {"string"}, {"list"}, {"option"} ], + ets_insert(ord_constraint_types, OrdTypes), + when_warning(warn_unused_functions, fun() -> create_unused_functions() end), check_modifiers(Env, Contracts), create_type_errors(), @@ -1177,6 +1183,15 @@ check_modifiers1(What, Decl) when element(1, Decl) == letfun; element(1, Decl) = ok; check_modifiers1(_, _) -> ok. +-spec extract_typevars(utype()) -> [aeso_syntax:tvar()]. +extract_typevars(Type) -> + case Type of + TVar = {tvar, _, _} -> [TVar]; + Tup when is_tuple(Tup) -> extract_typevars(tuple_to_list(Tup)); + [H | T] -> extract_typevars(H) ++ extract_typevars(T); + _ -> [] + end. + -spec check_type(env(), aeso_syntax:type()) -> aeso_syntax:type(). check_type(Env, T) -> check_type(Env, T, 0). @@ -1219,6 +1234,13 @@ check_type(Env, Type = {fun_t, Ann, NamedArgs, Args, Ret}, Arity) -> check_type(_Env, Type = {uvar, _, _}, Arity) -> ensure_base_type(Type, Arity), Type; +check_type(Env, {constrained_t, Ann, Constraints, Type}, Arity) -> + when_warning(warn_duplicated_constraints, fun() -> warn_duplicated_constraints(Constraints) end), + TVars = [ Name || {tvar, _, Name} <- extract_typevars(Type) ], + [ type_error({unused_constraint, C}) || C = {constraint, _, {tvar, _, Name}, _} <- Constraints, + not lists:member(Name, TVars) ], + + {constrained_t, Ann, Constraints, check_type(Env, Type, Arity)}; check_type(_Env, {args_t, Ann, Ts}, _) -> type_error({new_tuple_syntax, Ann, Ts}), {tuple_t, Ann, Ts}. @@ -1398,7 +1420,7 @@ infer_letfun(Env = #env{ namespace = Namespace }, LetFun = {letfun, Ann, Fun, _, {{Name, Sig}, Clause} = infer_letfun1(Env, LetFun), {{Name, Sig}, desugar_clauses(Ann, Fun, Sig, [Clause])}. -infer_letfun1(Env0 = #env{ namespace = NS }, {letfun, Attrib, Fun = {id, NameAttrib, Name}, Args, What, GuardedBodies}) -> +infer_letfun1(Env0 = #env{ namespace = NS }, {letfun, Attrib, Fun = {id, NameAttrib, Name}, Args, What, GuardedBodies}) -> Env = Env0#env{ stateful = aeso_syntax:get_ann(stateful, Attrib, false), current_function = Fun }, {NewEnv, {typed, _, {tuple, _, TypedArgs}, {tuple_t, _, ArgTypes}}} = infer_pattern(Env, {tuple, [{origin, system} | NameAttrib], Args}), @@ -1943,10 +1965,16 @@ infer_infix({IntOp, As}) Int = {id, As, "int"}, {fun_t, As, [], [Int, Int], Int}; infer_infix({RelOp, As}) - when RelOp == '=='; RelOp == '!='; - RelOp == '<'; RelOp == '>'; + when RelOp == '=='; RelOp == '!=' -> + T = fresh_uvar(As), + add_constraint({is_eq, T}), + Bool = {id, As, "bool"}, + {fun_t, As, [], [T, T], Bool}; +infer_infix({RelOp, As}) + when RelOp == '<'; RelOp == '>'; RelOp == '<='; RelOp == '=<'; RelOp == '>=' -> - T = fresh_uvar(As), %% allow any type here, check in the backend that we have comparison for it + T = fresh_uvar(As), + add_constraint({is_ord, T}), Bool = {id, As, "bool"}, {fun_t, As, [], [T, T], Bool}; infer_infix({'..', As}) -> @@ -2016,7 +2044,8 @@ next_count() -> ets_tables() -> [options, type_vars, constraints, freshen_tvars, type_errors, - defined_contracts, warnings, function_calls, all_functions]. + defined_contracts, warnings, function_calls, all_functions, + ord_constraint_types]. clean_up_ets() -> [ catch ets_delete(Tab) || Tab <- ets_tables() ], @@ -2178,11 +2207,16 @@ destroy_and_report_unsolved_constraints(Env) -> (#named_argument_constraint{}) -> true; (_) -> false end, OtherCs2), - {BytesCs, []} = + {BytesCs, OtherCs4} = lists:partition(fun({is_bytes, _}) -> true; ({add_bytes, _, _, _, _, _}) -> true; (_) -> false end, OtherCs3), + {TVarsCs, []} = + lists:partition(fun({is_eq, _}) -> true; + ({is_ord, _}) -> true; + (_) -> false + end, OtherCs4), Unsolved = [ S || S <- [ solve_constraint(Env, dereference_deep(C)) || C <- NamedArgCs ], S == unsolved ], @@ -2200,6 +2234,7 @@ destroy_and_report_unsolved_constraints(Env) -> check_record_create_constraints(Env, CreateCs), check_is_contract_constraints(Env, ContractCs), check_bytes_constraints(Env, BytesCs), + check_tvars_constraints(Env, TVarsCs), destroy_constraints(). @@ -2329,6 +2364,33 @@ check_bytes_constraint(Env, {add_bytes, Ann, Fun, A0, B0, C0}) -> _ -> type_error({unsolved_bytes_constraint, Ann, Fun, A, B, C}) end. +%% -- Typevars constraints -- + +check_tvars_constraints(Env, Constraints) -> + [ check_tvars_constraint(Env, C) || C <- Constraints ]. + +check_tvars_constraint(Env, {is_eq, Type = {uvar, Ann, _}}) -> + Type1 = unfold_types_in_type(Env, instantiate(Type)), + type_is_eq(Type1) orelse type_error({type_not_eq, Ann, Type1}); +check_tvars_constraint(Env, {is_ord, Type = {uvar, Ann, _}}) -> + Type1 = unfold_types_in_type(Env, instantiate(Type)), + type_is_ord(Type1) orelse type_error({type_not_ord, Ann, Type1}). + +type_is_ord({app_t, _, Id, Ts}) -> type_is_ord(Id) andalso lists:all(fun type_is_ord/1, Ts); +type_is_ord({tuple_t, _, Ts}) -> lists:all(fun type_is_ord/1, Ts); +type_is_ord({bytes_t, _, _}) -> true; +type_is_ord({constrained_t, _, Constraints, {tvar, _, _}}) -> lists:keyfind("ord", 3, Constraints) =/= false; +type_is_ord({id, _, Id}) -> ets_lookup(ord_constraint_types, Id) =/= []; +type_is_ord(_) -> false. + +type_is_eq({app_t, _, Id, Ts}) -> type_is_eq(Id) andalso lists:all(fun type_is_eq/1, Ts); +type_is_eq({con, _, _}) -> true; +type_is_eq({qcon, _, _}) -> true; +type_is_eq({id, _, _}) -> true; +type_is_eq({qid, _, _}) -> true; +type_is_eq({constrained_t, _, Constraints, {tvar, _, _}}) -> lists:keyfind("eq", 3, Constraints) =/= false; +type_is_eq(T) -> type_is_ord(T). + %% -- Field constraints -- check_record_create_constraints(_, []) -> ok; @@ -2582,6 +2644,7 @@ unify1(_Env, {uvar, A, R}, T, When) -> unify1(Env, T, {uvar, A, R}, When) -> unify1(Env, {uvar, A, R}, T, When); unify1(_Env, {tvar, _, X}, {tvar, _, X}, _When) -> true; %% Rigid type variables +unify1(_Env, {constrained_t, _, Cs, {tvar, _, X}}, {constrained_t, _, Cs, {tvar, _, X}}, _When) -> true; unify1(Env, [A|B], [C|D], When) -> unify(Env, A, C, When) andalso unify(Env, B, D, When); unify1(_Env, X, X, _When) -> @@ -2617,6 +2680,10 @@ unify1(Env, {tuple_t, _, As}, {tuple_t, _, Bs}, When) unify1(Env, {named_arg_t, _, Id1, Type1, _}, {named_arg_t, _, Id2, Type2, _}, When) -> unify1(Env, Id1, Id2, {arg_name, Id1, Id2, When}), unify1(Env, Type1, Type2, When); +unify1(Env, {constrained_t, _, Constraints, Type1 = {fun_t, _, _, _, _}}, Type2, When) -> + unify1(Env, constrain_tvars(Type1, Constraints), Type2, When); +unify1(Env, Type1, {constrained_t, _, Constraints, Type2 = {fun_t, _, _, _, _}}, When) -> + unify1(Env, Type1, constrain_tvars(Type2, Constraints), When); %% The grammar is a bit inconsistent about whether types without %% arguments are represented as applications to an empty list of %% parameters or not. We therefore allow them to unify. @@ -2628,6 +2695,28 @@ unify1(_Env, A, B, When) -> cannot_unify(A, B, When), false. +%% Propagate the constraints to their corresponding type vars +-spec constrain_tvars(utype() | [utype()], [constraint()]) -> utype(). +constrain_tvars(Types, Constraints) + when is_list(Types) -> + [ constrain_tvars(Type, Constraints) || Type <- Types ]; +constrain_tvars({fun_t, Ann, NamedArgs, ArgsT, RetT}, Constraints) -> + ConstrainedArgsT = constrain_tvars(ArgsT, Constraints), + ConstrainedRetT = constrain_tvars(RetT, Constraints), + {fun_t, Ann, NamedArgs, ConstrainedArgsT, ConstrainedRetT}; +constrain_tvars({app_t, Ann, AppT, ArgsT}, Constraints) -> + ConstrainedAppT = constrain_tvars(AppT, Constraints), + ConstrainedArgsT = constrain_tvars(ArgsT, Constraints), + {app_t, Ann, ConstrainedAppT, ConstrainedArgsT}; +constrain_tvars({tuple_t, Ann, ElemsT}, Constraints) -> + ConstrainedElemsT = constrain_tvars(ElemsT, Constraints), + {tuple_t, Ann, ConstrainedElemsT}; +constrain_tvars(TVar = {tvar, Ann, NameT}, Constraints) -> + TVarConstraints = [ C || {constraint, _, {tvar, _, NameC}, C} <- Constraints, NameT == NameC ], + {constrained_t, Ann, TVarConstraints, TVar}; +constrain_tvars(Type, _) -> + Type. + dereference(T = {uvar, _, R}) -> case ets_lookup(type_vars, R) of [] -> @@ -2655,6 +2744,7 @@ occurs_check1(_, {con, _, _}) -> false; occurs_check1(_, {qid, _, _}) -> false; occurs_check1(_, {qcon, _, _}) -> false; occurs_check1(_, {tvar, _, _}) -> false; +occurs_check1(_, {constrained_t, _, _, _}) -> false; occurs_check1(_, {bytes_t, _, _}) -> false; occurs_check1(R, {fun_t, _, Named, Args, Res}) -> occurs_check(R, [Res, Named | Args]); @@ -2771,7 +2861,8 @@ all_warnings() -> , warn_unused_functions , warn_shadowing , warn_division_by_zero - , warn_negative_spend ]. + , warn_negative_spend + , warn_duplicated_constraints ]. when_warning(Warn, Do) -> case lists:member(Warn, all_warnings()) of @@ -2908,6 +2999,19 @@ warn_potential_negative_spend(Ann, Fun, Args) -> _ -> ok end. +%% Warnings (Duplicated tvar constraints) + +warn_duplicated_constraints(Constraints) -> + warn_duplicated_constraints([], Constraints). + +warn_duplicated_constraints(_, []) -> ok; +warn_duplicated_constraints(UniqueConstraints, [Constraint = {constraint, _, {tvar, _, Name1}, {id, _, Constr1}}| Rest]) -> + case [ C || C = {constraint, _, {tvar, _, Name2}, {id, _, Constr2}} <- UniqueConstraints, + Name1 == Name2 andalso Constr1 == Constr2 ] of + [] -> warn_duplicated_constraints([Constraint | UniqueConstraints], Rest); + [Unique] -> ets_insert(warnings, {duplicated_constraint, Constraint, Unique}) + end. + %% Save unification failures for error messages. cannot_unify(A, B, When) -> @@ -3299,6 +3403,15 @@ mk_error({unknown_warning, Warning}) -> mk_error({empty_record_definition, Ann, Name}) -> Msg = io_lib:format("Empty record definitions are not allowed. Cannot define the record `~s`", [Name]), mk_t_err(pos(Ann), Msg); +mk_error({type_not_eq, Ann, Type}) -> + Msg = io_lib:format("Values of type `~s` are not comparable by equality", [pp_type("", Type)]), + mk_t_err(pos(Ann), Msg); +mk_error({type_not_ord, Ann, Type}) -> + Msg = io_lib:format("Values of type `~s` are not comparable by inequality", [pp_type("", Type)]), + mk_t_err(pos(Ann), Msg); +mk_error({unused_constraint, {constraint, Ann, {tvar, _, Name}, _}}) -> + Msg = io_lib:format("The type variable `~s` is constrained but never used", [Name]), + mk_t_err(pos(Ann), Msg); mk_error(Err) -> Msg = io_lib:format("Unknown error: ~p", [Err]), mk_t_err(pos(0, 0), Msg). @@ -3330,6 +3443,10 @@ mk_warning({division_by_zero, Ann}) -> mk_warning({negative_spend, Ann}) -> Msg = io_lib:format("Negative spend.", []), aeso_warnings:new(pos(Ann), Msg); +mk_warning({duplicated_constraint, {constraint, Ann, {tvar, _, Name}, _}, {constraint, AnnFirst, _, _}}) -> + Msg = io_lib:format("The constraint on the type variable `~s` is a duplication of the constraint at ~s", + [Name, pp_loc(AnnFirst)]), + aeso_warnings:new(pos(Ann), Msg); mk_warning(Warn) -> Msg = io_lib:format("Unknown warning: ~p", [Warn]), aeso_warnings:new(Msg). @@ -3554,6 +3671,8 @@ pp({uvar, _, Ref}) -> ["?u" | integer_to_list(erlang:phash2(Ref, 16384)) ]; pp({tvar, _, Name}) -> Name; +pp(T = {constrained_t, _, _, {tvar, _, _}}) -> + prettypr:format(aeso_pretty:type(T)); pp({if_t, _, Id, Then, Else}) -> ["if(", pp([Id, Then, Else]), ")"]; pp({tuple_t, _, []}) -> diff --git a/src/aeso_ast_to_fcode.erl b/src/aeso_ast_to_fcode.erl index 25802e0..c8e9989 100644 --- a/src/aeso_ast_to_fcode.erl +++ b/src/aeso_ast_to_fcode.erl @@ -495,6 +495,8 @@ type_to_fcode(_Env, _Sub, {tvar, Ann, "void"}) -> fcode_error({found_void, Ann}); type_to_fcode(_Env, Sub, {tvar, _, X}) -> maps:get(X, Sub, {tvar, X}); +type_to_fcode(Env, Sub, {constrained_t, _, _, TVar = {tvar, _, _}}) -> + type_to_fcode(Env, Sub, TVar); type_to_fcode(_Env, _Sub, {fun_t, Ann, _, var_args, _}) -> fcode_error({var_args_not_set, {id, Ann, "a very suspicious function"}}); type_to_fcode(Env, Sub, {fun_t, _, Named, Args, Res}) -> diff --git a/src/aeso_pretty.erl b/src/aeso_pretty.erl index 0ee05f2..72fedae 100644 --- a/src/aeso_pretty.erl +++ b/src/aeso_pretty.erl @@ -284,7 +284,9 @@ type(T = {id, _, _}) -> name(T); type(T = {qid, _, _}) -> name(T); type(T = {con, _, _}) -> name(T); type(T = {qcon, _, _}) -> name(T); -type(T = {tvar, _, _}) -> name(T). +type(T = {tvar, _, _}) -> name(T); +type({constrained_t, _, Cs, T}) -> + beside([name(T), text(" is "), tuple(lists:map(fun expr/1, Cs))]). -spec args_type([aeso_syntax:type()]) -> doc(). args_type(Args) -> diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl index 6fccd21..397d583 100644 --- a/test/aeso_compiler_tests.erl +++ b/test/aeso_compiler_tests.erl @@ -265,7 +265,9 @@ warnings() -> "The function `called_unused_function2` is defined but never used.">>, <>, - <>, + <> ]). @@ -805,6 +807,82 @@ failing_contracts() -> "to arguments\n" " `1 : int`">> ]) + , ?TYPE_ERROR(comparable_typevar_constraints, + [<>, + <>, + <>, + <>, + <>, + < bool` are not comparable by inequality">>, + < bool` are not comparable by equality">>, + <>, + <>, + <>, + <>, + < bool)` are not comparable by inequality">>, + < bool)` are not comparable by equality">>, + < bool)` are not comparable by inequality">>, + < bool)` are not comparable by equality">>, + < bool * int)` are not comparable by inequality">>, + < bool * int)` are not comparable by equality">>, + <>, + <>, + <>, + <>, + <>, + <>, + <>, + <>, + <>, + <>, + < bool, (int, char) => bool)` are not comparable by inequality">>, + < bool, (int, char) => bool)` are not comparable by equality">>, + < bool, (int, char) => bool)` are not comparable by inequality">>, + < bool, (int, char) => bool)` are not comparable by equality">>, + < bool, (int, char) => bool)` are not comparable by inequality">>, + < bool, (int, char) => bool)` are not comparable by equality">>, + < bool)` are not comparable by inequality">>, + < bool)` are not comparable by equality">>, + < bool)` are not comparable by inequality">>, + < bool)` are not comparable by equality">> + ]) , ?TYPE_ERROR(warnings, [<>, @@ -834,7 +912,9 @@ failing_contracts() -> "The function `called_unused_function2` is defined but never used.">>, <>, - <>, + <> ]) ]. diff --git a/test/contracts/comparable_typevar_constraints.aes b/test/contracts/comparable_typevar_constraints.aes new file mode 100644 index 0000000..1e8cc84 --- /dev/null +++ b/test/contracts/comparable_typevar_constraints.aes @@ -0,0 +1,156 @@ +contract A = entrypoint init() = () + +main contract C = + datatype custom_datatype('a) = CD('a) + + record custom_record('a) = { f : 'a } + + // pass + function + passing_ord: 'a is ord ; ('a, 'a) => bool + passing_ord(x, y) = x >= y + + // pass + function + passing_eq: 'a is eq ; ('a, 'a) => bool + passing_eq(x, y) = x == y + + // fail because eq is not specified for 'a + function + fail_no_eq : ('a, 'a) => bool + fail_no_eq(x, y) = x == y + + // fail because 'b is not used + function + fail_unused_tvar: 'a is eq, 'b is eq ; ('a, 'a) => bool + fail_unused_tvar(x, y) = x == y + + // Ord types + + function bool_ord(x : bool, y : bool) = x >= y // pass + function bool_eq (x : bool, y : bool) = x == y // pass + + function int_ord(x : int, y : int) = x >= y // pass + function int_eq (x : int, y : int) = x == y // pass + + function char_ord(x : char, y : char) = x >= y // pass + function char_eq (x : char, y : char) = x == y // pass + + function bits_ord(x : bits, y : bits) = x >= y // pass + function bits_eq (x : bits, y : bits) = x == y // pass + + function bytes_ord(x : bytes(16), y : bytes(16)) = x >= y // pass + function bytes_eq (x : bytes(16), y : bytes(16)) = x == y // pass + + function string_ord(x : string, y : string) = x >= y // pass + function string_eq (x : string, y : string) = x == y // pass + + function hash_ord(x : hash, y : hash) = x >= y // pass + function hash_eq (x : hash, y : hash) = x == y // pass + + function signature_ord(x : signature, y : signature) = x >= y // pass + function signature_eq (x : signature, y : signature) = x == y // pass + + // Eq types + + function address_ord(x : address, y : address) = x >= y // fail + function address_eq (x : address, y : address) = x == y // pass + + function event_ord(x : Chain.ttl, y : Chain.ttl) = x >= y // fail + function event_eq (x : Chain.ttl, y : Chain.ttl) = x == y // pass + + function contract_ord(x : A, y : A) = x >= y // fail + function contract_eq (x : A, y : A) = x == y // pass + + // Noncomparable types + + type lam = (int, char) => bool + + function lambda_ord(x : lam, y : lam) = x >= y // fail + function lambda_eq (x : lam, y : lam) = x == y // fail + + // Ord composite types of ord + + function list_of_ord_ord(x : list(int), y : list(int)) = x >= y // pass + function list_of_ord_eq (x : list(int), y : list(int)) = x == y // pass + + function option_of_ord_ord(x : option(int), y : option(int)) = x >= y // pass + function option_of_ord_eq (x : option(int), y : option(int)) = x == y // pass + + function tuple_of_ord_ord(x : (int * bool), y : (int * bool)) = x >= y // pass + function tuple_of_ord_eq (x : (int * bool), y : (int * bool)) = x == y // pass + + // Ord composite types of eq + + function list_of_eq_ord(x : list(address), y : list(address)) = x >= y // fail + function list_of_eq_eq (x : list(address), y : list(address)) = x == y // pass + + function option_of_eq_ord(x : option(address), y : option(address)) = x >= y // fail + function option_of_eq_eq (x : option(address), y : option(address)) = x == y // pass + + function tuple_of_eq_ord(x : (address * int), y : (address * int)) = x >= y // fail + function tuple_of_eq_eq (x : (address * int), y : (address * int)) = x == y // pass + + // Ord composite types of nomcomparable + + function list_of_noncomp_ord(x : list(lam), y : list(lam)) = x >= y // fail + function list_of_noncomp_eq (x : list(lam), y : list(lam)) = x == y // fail + + function option_of_noncomp_ord(x : option(lam), y : option(lam)) = x >= y // fail + function option_of_noncomp_eq (x : option(lam), y : option(lam)) = x == y // fail + + function tuple_of_noncomp_ord(x : (lam * int), y : (lam * int)) = x >= y // fail + function tuple_of_noncomp_eq (x : (lam * int), y : (lam * int)) = x == y // fail + + // Eq composite types of ord + + function map_of_ord_ord(x : map(int, int), y : map(int, int)) = x >= y // fail + function map_of_ord_eq (x : map(int, int), y : map(int, int)) = x == y // pass + + function oracle_of_ord_ord(x : oracle(int, int), y : oracle(int, int)) = x >= y // fail + function oracle_of_ord_eq (x : oracle(int, int), y : oracle(int, int)) = x == y // pass + + function oracle_query_of_ord_ord(x : oracle_query(int, int), y : oracle_query(int, int)) = x >= y // fail + function oracle_query_of_ord_eq (x : oracle_query(int, int), y : oracle_query(int, int)) = x == y // pass + + function datatype_of_ord_ord(x : custom_datatype(int), y : custom_datatype(int)) = x >= y // fail + function datatype_of_ord_eq (x : custom_datatype(int), y : custom_datatype(int)) = x == y // pass + + function record_of_ord_ord(x : custom_record(int), y : custom_record(int)) = x >= y // fail + function record_of_ord_eq (x : custom_record(int), y : custom_record(int)) = x == y // pass + + // Eq composite types of eq + + function map_of_eq_ord(x : map(address, address), y : map(address, address)) = x >= y // fail + function map_of_eq_eq (x : map(address, address), y : map(address, address)) = x == y // pass + + function oracle_of_eq_ord(x : oracle(address, address), y : oracle(address, address)) = x >= y // fail + function oracle_of_eq_eq (x : oracle(address, address), y : oracle(address, address)) = x == y // pass + + function oracle_query_of_eq_ord(x : oracle_query(address, address), y : oracle_query(address, address)) = x >= y // fail + function oracle_query_of_eq_eq (x : oracle_query(address, address), y : oracle_query(address, address)) = x == y // pass + + function datatype_of_eq_ord(x : custom_datatype(address), y : custom_datatype(address)) = x >= y // fail + function datatype_of_eq_eq (x : custom_datatype(address), y : custom_datatype(address)) = x == y // pass + + function record_of_eq_ord(x : custom_record(address), y : custom_record(address)) = x >= y // fail + function record_of_eq_eq (x : custom_record(address), y : custom_record(address)) = x == y // pass + + // Eq composite types of nomcomparable + + function map_of_noncomp_ord(x : map(lam, lam), y : map(lam, lam)) = x >= y // fail + function map_of_noncomp_eq (x : map(lam, lam), y : map(lam, lam)) = x == y // fail + + function oracle_of_noncomp_ord(x : oracle(lam, lam), y : oracle(lam, lam)) = x >= y // fail + function oracle_of_noncomp_eq (x : oracle(lam, lam), y : oracle(lam, lam)) = x == y // fail + + function oracle_query_of_noncomp_ord(x : oracle_query(lam, lam), y : oracle_query(lam, lam)) = x >= y // fail + function oracle_query_of_noncomp_eq (x : oracle_query(lam, lam), y : oracle_query(lam, lam)) = x == y // fail + + function datatype_of_noncomp_ord(x : custom_datatype(lam), y : custom_datatype(lam)) = x >= y // fail + function datatype_of_noncomp_eq (x : custom_datatype(lam), y : custom_datatype(lam)) = x == y // pass + + function record_of_nomcomp_ord(x : custom_record(lam), y : custom_record(lam)) = x >= y // fail + function record_of_nomcomp_eq (x : custom_record(lam), y : custom_record(lam)) = x == y // pass + + entrypoint init() = () \ No newline at end of file diff --git a/test/contracts/warnings.aes b/test/contracts/warnings.aes index 5aa05ce..f3f36ad 100644 --- a/test/contracts/warnings.aes +++ b/test/contracts/warnings.aes @@ -48,6 +48,11 @@ contract Warnings = rv() 2 + // Duplicated constraint on 'a + entrypoint + duplicated_tvar_constraint : 'a is eq, 'a is eq ; ('a, 'a) => bool + duplicated_tvar_constraint (x, y) = x == y + namespace FunctionsAsArgs = function f() = g()