From 3f177d363f1322d449d312c84168c1b0782f1089 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sat, 11 Jun 2022 17:26:13 +0400 Subject: [PATCH 01/15] Add constraints to the syntax and parser --- src/aeso_parser.erl | 16 ++++++++++++++-- src/aeso_scan.erl | 2 +- src/aeso_syntax.erl | 4 ++++ 3 files changed, 19 insertions(+), 3 deletions(-) diff --git a/src/aeso_parser.erl b/src/aeso_parser.erl index 51b81f6d..b0f0bced 100644 --- a/src/aeso_parser.erl +++ b/src/aeso_parser.erl @@ -134,9 +134,20 @@ fun_block(Mods, Kind, [Decl]) -> fun_block(Mods, Kind, Decls) -> {block, get_ann(Kind), [ add_modifiers(Mods, Kind, Decl) || Decl <- Decls ]}. +typevar_constraint() -> + ?RULE(tvar(), keyword(is), choice([tok(eq), tok(ord)]), + {constraint, element(2, _1), element(3, _1), element(1, _3)}). + +typevars_constraints() -> + ?RULE(comma_sep1(typevar_constraint()), tok(';'), _1). + +fundecl() -> + choice([?RULE(id(), tok(':'), typevars_constraints(), type(), + {fun_decl, get_ann(_1), _1, {constrained_t, get_ann(_1), _3, _4}}), + ?RULE(id(), tok(':'), type(), {fun_decl, get_ann(_1), _1, _3})]). + fundef_or_decl() -> - choice([?RULE(id(), tok(':'), type(), {fun_decl, get_ann(_1), _1, _3}), - fundef()]). + choice([fundecl(), fundef()]). using() -> Alias = {keyword(as), con()}, @@ -527,6 +538,7 @@ parens(P) -> between(tok('('), P, tok(')')). braces(P) -> between(tok('{'), P, tok('}')). brackets(P) -> between(tok('['), P, tok(']')). comma_sep(P) -> sep(P, tok(',')). +comma_sep1(P) -> sep1(P, tok(',')). paren_list(P) -> parens(comma_sep(P)). brace_list(P) -> braces(comma_sep(P)). diff --git a/src/aeso_scan.erl b/src/aeso_scan.erl index 4587efab..11900b19 100644 --- a/src/aeso_scan.erl +++ b/src/aeso_scan.erl @@ -45,7 +45,7 @@ lexer() -> Keywords = ["contract", "include", "let", "switch", "type", "record", "datatype", "if", "elif", "else", "function", "stateful", "payable", "true", "false", "mod", "public", "entrypoint", "private", "indexed", "namespace", - "interface", "main", "using", "as", "for", "hiding" + "interface", "main", "using", "as", "for", "hiding", "is", "eq", "ord" ], KW = string:join(Keywords, "|"), diff --git a/src/aeso_syntax.erl b/src/aeso_syntax.erl index 1e01153c..6461dac1 100644 --- a/src/aeso_syntax.erl +++ b/src/aeso_syntax.erl @@ -79,11 +79,15 @@ -type constructor_t() :: {constr_t, ann(), con(), [type()]}. +-type tvar_constraint() :: eq | ord. +-type constraint() :: {constraint, ann(), name(), tvar_constraint()}. + -type type() :: {fun_t, ann(), [named_arg_t()], [type()], type()} | {app_t, ann(), type(), [type()]} | {tuple_t, ann(), [type()]} | {args_t, ann(), [type()]} %% old tuple syntax, old for error messages | {bytes_t, ann(), integer() | any} + | {constrained_t, ann(), [constraint()], type()} | id() | qid() | con() | qcon() %% contracts | tvar(). From f56eeb0b2bc5d210c891f3681c4d7a5f751d8133 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sat, 11 Jun 2022 21:52:23 +0400 Subject: [PATCH 02/15] Use id() for constraints instead of keywords --- priv/stdlib/String.aes | 4 ++-- src/aeso_parser.erl | 3 +-- src/aeso_scan.erl | 2 +- src/aeso_syntax.erl | 5 ++--- 4 files changed, 6 insertions(+), 8 deletions(-) diff --git a/priv/stdlib/String.aes b/priv/stdlib/String.aes index 33f813b2..99d5c0e7 100644 --- a/priv/stdlib/String.aes +++ b/priv/stdlib/String.aes @@ -98,10 +98,10 @@ namespace String = private function to_int_([], _, x, _) = Some(x) - to_int_(i :: is, value, x, b) = + to_int_(i :: ints, value, x, b) = switch(value(i)) None => None - Some(n) => to_int_(is, value, x * b + n, b) + Some(i) => to_int_(ints, value, x * b + i, b) private function ch_to_int_10(ch) = let c = Char.to_int(ch) diff --git a/src/aeso_parser.erl b/src/aeso_parser.erl index b0f0bced..c32d9443 100644 --- a/src/aeso_parser.erl +++ b/src/aeso_parser.erl @@ -135,8 +135,7 @@ fun_block(Mods, Kind, Decls) -> {block, get_ann(Kind), [ add_modifiers(Mods, Kind, Decl) || Decl <- Decls ]}. typevar_constraint() -> - ?RULE(tvar(), keyword(is), choice([tok(eq), tok(ord)]), - {constraint, element(2, _1), element(3, _1), element(1, _3)}). + ?RULE(tvar(), keyword(is), id(), {constraint, get_ann(_1), _1, _3}). typevars_constraints() -> ?RULE(comma_sep1(typevar_constraint()), tok(';'), _1). diff --git a/src/aeso_scan.erl b/src/aeso_scan.erl index 11900b19..c7de2eb2 100644 --- a/src/aeso_scan.erl +++ b/src/aeso_scan.erl @@ -45,7 +45,7 @@ lexer() -> Keywords = ["contract", "include", "let", "switch", "type", "record", "datatype", "if", "elif", "else", "function", "stateful", "payable", "true", "false", "mod", "public", "entrypoint", "private", "indexed", "namespace", - "interface", "main", "using", "as", "for", "hiding", "is", "eq", "ord" + "interface", "main", "using", "as", "for", "hiding", "is" ], KW = string:join(Keywords, "|"), diff --git a/src/aeso_syntax.erl b/src/aeso_syntax.erl index 6461dac1..c92f0f6a 100644 --- a/src/aeso_syntax.erl +++ b/src/aeso_syntax.erl @@ -79,15 +79,14 @@ -type constructor_t() :: {constr_t, ann(), con(), [type()]}. --type tvar_constraint() :: eq | ord. --type constraint() :: {constraint, ann(), name(), tvar_constraint()}. +-type tvar_constraint() :: {constraint, ann(), tvar(), id()}. -type type() :: {fun_t, ann(), [named_arg_t()], [type()], type()} | {app_t, ann(), type(), [type()]} | {tuple_t, ann(), [type()]} | {args_t, ann(), [type()]} %% old tuple syntax, old for error messages | {bytes_t, ann(), integer() | any} - | {constrained_t, ann(), [constraint()], type()} + | {constrained_t, ann(), [tvar_constraint()], type()} | id() | qid() | con() | qcon() %% contracts | tvar(). From 69713036d0aad9cdce4013b99c5528d167e59b7e Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Mon, 13 Jun 2022 21:37:00 +0400 Subject: [PATCH 03/15] 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 e0201d03..53b48412 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 651a2d59..4009b7e1 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 99d5c0e7..8046b78c 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 72c93727..8f007147 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 25802e04..c8e9989c 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 0ee05f20..72fedaea 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 6fccd211..397d5837 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 00000000..1e8cc842 --- /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 5aa05cef..f3f36ad3 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() From 6c17e57a7c9cb3d4a44e397f93844c4be8650c25 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Tue, 14 Jun 2022 11:58:40 +0400 Subject: [PATCH 04/15] Fix dialyzer warnings --- src/aeso_ast_infer_types.erl | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 8f007147..0a7fa392 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -87,7 +87,10 @@ -type byte_constraint() :: {is_bytes, utype()} | {add_bytes, aeso_syntax:ann(), concat | split, utype(), utype(), utype()}. --type constraint() :: named_argument_constraint() | field_constraint() | byte_constraint(). +-type tvar_constraint() :: {is_eq, utype()} + | {is_ord, utype()}. + +-type constraint() :: named_argument_constraint() | field_constraint() | byte_constraint() | tvar_constraint(). -record(field_info, { ann :: aeso_syntax:ann() @@ -1183,7 +1186,6 @@ 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]; From fc08fe09a5b305296a5c52dde92957a61ff62ca4 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Tue, 14 Jun 2022 13:27:00 +0400 Subject: [PATCH 05/15] Add tests for calling constrained functions --- src/aeso_ast_infer_types.erl | 8 ++++++++ test/aeso_compiler_tests.erl | 8 +++++++- test/contracts/comparable_typevar_constraints.aes | 11 ++++++++++- 3 files changed, 25 insertions(+), 2 deletions(-) diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 0a7fa392..d52144b3 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -2645,6 +2645,14 @@ unify1(_Env, {uvar, A, R}, T, When) -> end; unify1(Env, T, {uvar, A, R}, When) -> unify1(Env, {uvar, A, R}, T, When); +unify1(Env, {constrained_t, _, Cs, UVar = {uvar, _, _}}, Type2, When) -> + [ add_constraint({is_ord, UVar}) || {id, _, "ord"} <- Cs ], + [ add_constraint({is_eq, UVar}) || {id, _, "eq"} <- Cs ], + unify1(Env, UVar, Type2, When); +unify1(Env, Type1, UVar = {constrained_t, _, Cs, {uvar, _, _}}, When) -> + [ add_constraint({is_ord, UVar}) || {id, _, "ord"} <- Cs ], + [ add_constraint({is_eq, UVar}) || {id, _, "eq"} <- Cs ], + unify1(Env, Type1, UVar, 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) -> diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl index 397d5837..a84eeaf8 100644 --- a/test/aeso_compiler_tests.erl +++ b/test/aeso_compiler_tests.erl @@ -881,7 +881,13 @@ failing_contracts() -> < bool)` are not comparable by inequality">>, < bool)` are not comparable by equality">> + "Values of type `custom_record((int, char) => bool)` are not comparable by equality">>, + <>, + < 'a` are not comparable by inequality">>, + < 'b` are not comparable by equality">> ]) , ?TYPE_ERROR(warnings, [<= 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 + entrypoint init() = + let passing_ord_ord = passing_ord([1], [2]) // pass + let passing_ord_eq = passing_ord({[1] = 2}, {[2] = 3}) // fail + let passing_ord_noncomp = passing_ord((x) => x, (x) => x) // fail + + let passing_eq_ord = passing_eq([1], [2]) // pass + let passing_eq_eq = passing_eq({[1] = 2}, {[2] = 3}) // pass + let passing_eq_noncomp = passing_eq((x) => x, (x) => x) // fail + + () \ No newline at end of file From 2d17ce3ee2029292b8cb2505f23dd9a2c5a1e72c Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Tue, 14 Jun 2022 14:55:50 +0400 Subject: [PATCH 06/15] Add test for unknown tvar constraints --- src/aeso_ast_infer_types.erl | 5 ++ test/aeso_compiler_tests.erl | 80 ++++++++++--------- .../comparable_typevar_constraints.aes | 10 ++- 3 files changed, 53 insertions(+), 42 deletions(-) diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index d52144b3..94a9542b 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -1241,6 +1241,8 @@ check_type(Env, {constrained_t, Ann, Constraints, Type}, Arity) -> TVars = [ Name || {tvar, _, Name} <- extract_typevars(Type) ], [ type_error({unused_constraint, C}) || C = {constraint, _, {tvar, _, Name}, _} <- Constraints, not lists:member(Name, TVars) ], + [ type_error({unknown_tvar_constraint, C}) || C = {constraint, _, _, {id, _, Name}} <- Constraints, + not lists:member(Name, ["eq", "ord"]) ], {constrained_t, Ann, Constraints, check_type(Env, Type, Arity)}; check_type(_Env, {args_t, Ann, Ts}, _) -> @@ -3422,6 +3424,9 @@ mk_error({type_not_ord, Ann, Type}) -> 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({unknown_tvar_constraint, {constraint, _, {tvar, _, TVar}, {id, Ann, C}}}) -> + Msg = io_lib:format("Unknown constraint `~s` used on the type variable `~s`", [C, TVar]), + mk_t_err(pos(Ann), Msg); mk_error(Err) -> Msg = io_lib:format("Unknown error: ~p", [Err]), mk_t_err(pos(0, 0), Msg). diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl index a84eeaf8..7d630eca 100644 --- a/test/aeso_compiler_tests.erl +++ b/test/aeso_compiler_tests.erl @@ -810,83 +810,85 @@ failing_contracts() -> , ?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">>, - <>, - < 'a` are not comparable by inequality">>, - < 'b` are not comparable by equality">> ]) , ?TYPE_ERROR(warnings, diff --git a/test/contracts/comparable_typevar_constraints.aes b/test/contracts/comparable_typevar_constraints.aes index 11e98fb5..852ab5ac 100644 --- a/test/contracts/comparable_typevar_constraints.aes +++ b/test/contracts/comparable_typevar_constraints.aes @@ -7,12 +7,12 @@ main contract C = // pass function - passing_ord: 'a is ord ; ('a, 'a) => bool + 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 : 'a is eq ; ('a, 'a) => bool passing_eq(x, y) = x == y // fail because eq is not specified for 'a @@ -22,9 +22,13 @@ main contract C = // fail because 'b is not used function - fail_unused_tvar: 'a is eq, 'b is eq ; ('a, 'a) => bool + fail_unused_tvar : 'a is eq, 'b is eq ; ('a, 'a) => bool fail_unused_tvar(x, y) = x == y + function + fail_unknown_constraint : 'a is foo ; ('a) => 'a + fail_unknown_constraint(x) = x + // Ord types function bool_ord(x : bool, y : bool) = x >= y // pass From 8e6c6d81ad25495f6b3b2529c244c885b3b5dbbe Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Tue, 14 Jun 2022 18:20:47 +0400 Subject: [PATCH 07/15] Add char type to the docs --- docs/sophia_features.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index aa9e2293..bcd1f861 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -357,7 +357,8 @@ Sophia has the following types: | Type | Description | Example | |----------------------|---------------------------------------------------------------------------------------------|--------------------------------------------------------------| | int | A 2-complement integer | ```-1``` | -| address | æternity address, 32 bytes | ```Call.origin``` | +| char | A single character | ```'c'``` | +| address | æternity address, 32 bytes | ```Call.origin``` | | bool | A Boolean | ```true``` | | bits | A bit field | ```Bits.none``` | | bytes(n) | A byte array with `n` bytes | ```#fedcba9876543210``` | From 75f27111484d7dee17cda006d9f0cd27c1757dd4 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Tue, 14 Jun 2022 19:04:20 +0400 Subject: [PATCH 08/15] Update CHANGELOG --- CHANGELOG.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 218866c1..f0bdfef5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 function sum(l : list(int)) : int = foldl((+), 0, l) function logical_and(x, y) = (&&)(x, y) ``` +- Add comparable typevar constraints (`ord` and `eq`) + ``` + lt : 'a is ord ; ('a, 'a) => bool + lt(x, y) = x < y + + is_eq : 'a is eq ; ('a, 'a) => bool + is_eq(x, y) = x == y + ``` ### Changed - Error messages have been restructured (less newlines) to provide more unified errors. Also `pp_oneline/1` has been added. - Ban empty record definitions (e.g. `record r = {}` would give an error). From 46ac9bfa8260d6a3eeb67519be1644083859a3fb Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Tue, 14 Jun 2022 22:19:35 +0400 Subject: [PATCH 09/15] Update the docs --- docs/sophia_features.md | 61 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index bcd1f861..c98ceb8a 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -502,6 +502,67 @@ function Guards cannot be stateful even when used inside a stateful function. +## Constrainted type variables + +Comparing types by equality (using `==` and `!=`) or by inequality +(using `<`, `>`, `<=`, `=<`, and `>=`) only makes sense by some types. +For example, it is possible to compare two `int`s by inequality +(e.g. `1 < 2`), but it would not make sense to compare two instances of +a contract by inequality. + +``` +contract C = ... +contract Main = + function f(x : C, y : c) = x > y // this is wrong +``` + +This is solved in Sophia by adding type variable constraints +(`ord` and `eq`) to limit what can be passed to the binary comparison +operators. + +The type of the equality comparison operators is `'a is eq ; ('a, 'a) => bool` +and of the inequality comparison operators is `'a is ord ; ('a, 'a) => bool` +which means that these operators can only accept types that are comparable by +equality or by inequality respectively. + +The builtin types `bool`, `int`, `char`, `bits`, `bytes`, `string`, `hash`, +and `signature` are comparable by inequality (and equality) while the types +`address`, `event` are only comparable by equality. + +The composite types `list`, `option`, and `tuple` are comparable by inequality +if and only if their type argmuments are comparable by inequality. + +The composite types `map`, `oracle`, and `oracle_query` are comparable by +equality if and only if their type arguments are comparable by equality. + +All user-defined records and datatypes are comparable by equality if their +type arguments are also comparable by equality. In addition to that, all +user-defined contracts are comparable by equality. + +Anonymous functions (or lambda functions) are not comparable neither by +equality nor by inequality. + +All types that are comparable by inequality are also comparable by equality. +In other words, if a type has `ord` constraint, that implies that it also +have `eq` constraint. + +The type variable constraints can be specified in the type signature of any +function. + +``` +// Comparison with < is only allowed because 'a has the constraint ord +lt : 'a is ord ; ('a, 'a) => bool +lt(x, y) = x < y + +// Multiple constraints can be specified +ord_and_eq : 'a is ord, 'b is eq ; ('a, 'a, 'b, 'b) => bool +ord_and_eq(x, y, p, q) = x > y && p == q +``` + +If the constraints are not mentioned, the type variable is assumed to +have no constraints, and calling any equality or inequality operation +on it will cause an error. + ## Lists A Sophia list is a dynamically sized, homogenous, immutable, singly From ea98fc97bbe2f8860850c1d812dd11b4b3ff8aa4 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sun, 19 Jun 2022 19:18:10 +0400 Subject: [PATCH 10/15] Add an example of address type to the docs --- docs/sophia_features.md | 46 ++++++++++++++++++++--------------------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index c98ceb8a..e4f3087e 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -354,29 +354,29 @@ namespace C = ## Types Sophia has the following types: -| Type | Description | Example | -|----------------------|---------------------------------------------------------------------------------------------|--------------------------------------------------------------| -| int | A 2-complement integer | ```-1``` | -| char | A single character | ```'c'``` | -| address | æternity address, 32 bytes | ```Call.origin``` | -| bool | A Boolean | ```true``` | -| bits | A bit field | ```Bits.none``` | -| bytes(n) | A byte array with `n` bytes | ```#fedcba9876543210``` | -| string | An array of bytes | ```"Foo"``` | -| list | A homogeneous immutable singly linked list. | ```[1, 2, 3]``` | -| ('a, 'b) => 'c | A function. Parentheses can be skipped if there is only one argument | ```(x : int, y : int) => x + y``` | -| tuple | An ordered heterogeneous array | ```(42, "Foo", true)``` | -| record | An immutable key value store with fixed key names and typed values | ``` record balance = { owner: address, value: int } ``` | -| map | An immutable key value store with dynamic mapping of keys of one type to values of one type | ```type accounts = map(string, address)``` | -| option('a) | An optional value either None or Some('a) | ```Some(42)``` | -| state | A user defined type holding the contract state | ```record state = { owner: address, magic_key: bytes(4) }``` | -| event | An append only list of blockchain events (or log entries) | ```datatype event = EventX(indexed int, string)``` | -| hash | A 32-byte hash - equivalent to `bytes(32)` | | -| signature | A signature - equivalent to `bytes(64)` | | -| Chain.ttl | Time-to-live (fixed height or relative to current block) | ```FixedTTL(1050)``` ```RelativeTTL(50)``` | -| oracle('a, 'b) | And oracle answering questions of type 'a with answers of type 'b | ```Oracle.register(acct, qfee, ttl)``` | -| oracle_query('a, 'b) | A specific oracle query | ```Oracle.query(o, q, qfee, qttl, rttl)``` | -| contract | A user defined, typed, contract address | ```function call_remote(r : RemoteContract) = r.fun()``` | +| Type | Description | Example | +|----------------------|---------------------------------------------------------------------------------------------|-------------------------------------------------------------------------------| +| int | A 2-complement integer | ```-1``` | +| char | A single character | ```'c'``` | +| address | æternity address, 32 bytes | ```Call.origin``` ```ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt``` | +| bool | A Boolean | ```true``` | +| bits | A bit field | ```Bits.none``` | +| bytes(n) | A byte array with `n` bytes | ```#fedcba9876543210``` | +| string | An array of bytes | ```"Foo"``` | +| list | A homogeneous immutable singly linked list. | ```[1, 2, 3]``` | +| ('a, 'b) => 'c | A function. Parentheses can be skipped if there is only one argument | ```(x : int, y : int) => x + y``` | +| tuple | An ordered heterogeneous array | ```(42, "Foo", true)``` | +| record | An immutable key value store with fixed key names and typed values | ``` record balance = { owner: address, value: int } ``` | +| map | An immutable key value store with dynamic mapping of keys of one type to values of one type | ```type accounts = map(string, address)``` | +| option('a) | An optional value either None or Some('a) | ```Some(42)``` | +| state | A user defined type holding the contract state | ```record state = { owner: address, magic_key: bytes(4) }``` | +| event | An append only list of blockchain events (or log entries) | ```datatype event = EventX(indexed int, string)``` | +| hash | A 32-byte hash - equivalent to `bytes(32)` | | +| signature | A signature - equivalent to `bytes(64)` | | +| Chain.ttl | Time-to-live (fixed height or relative to current block) | ```FixedTTL(1050)``` ```RelativeTTL(50)``` | +| oracle('a, 'b) | And oracle answering questions of type 'a with answers of type 'b | ```Oracle.register(acct, qfee, ttl)``` | +| oracle_query('a, 'b) | A specific oracle query | ```Oracle.query(o, q, qfee, qttl, rttl)``` | +| contract | A user defined, typed, contract address | ```function call_remote(r : RemoteContract) = r.fun()``` | ## Literals | Type | Constant/Literal example(s) | From 9d296f04cb23d387fc0d6e3c47962ef166800591 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sun, 19 Jun 2022 19:19:15 +0400 Subject: [PATCH 11/15] Formatting fix --- src/aeso_ast_infer_types.erl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 94a9542b..86484040 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -2217,9 +2217,9 @@ destroy_and_report_unsolved_constraints(Env) -> (_) -> false end, OtherCs3), {TVarsCs, []} = - lists:partition(fun({is_eq, _}) -> true; + lists:partition(fun({is_eq, _}) -> true; ({is_ord, _}) -> true; - (_) -> false + (_) -> false end, OtherCs4), Unsolved = [ S || S <- [ solve_constraint(Env, dereference_deep(C)) || C <- NamedArgCs ], From fc2875965e302c75a1c02e9655beeb0c524aecee Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sun, 19 Jun 2022 20:54:58 +0400 Subject: [PATCH 12/15] Make address comparable by inequality --- src/aeso_ast_infer_types.erl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 86484040..977935e2 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -824,7 +824,7 @@ infer(Contracts, Options) -> %% Set the constraints for the builtin types ets_new(ord_constraint_types, [set]), - OrdTypes = [ {"int"}, {"bool"}, {"bits"}, {"char"}, {"string"}, {"list"}, {"option"} ], + OrdTypes = [ {"int"}, {"bool"}, {"bits"}, {"char"}, {"string"}, {"list"}, {"option"}, {"address"} ], ets_insert(ord_constraint_types, OrdTypes), when_warning(warn_unused_functions, fun() -> create_unused_functions() end), From 4562a7166cfe7ddac65a940508a8266a0e7034f8 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sun, 19 Jun 2022 21:07:41 +0400 Subject: [PATCH 13/15] Fix the tests after changing address to ord --- test/aeso_compiler_tests.erl | 38 +++++++++---------- .../comparable_typevar_constraints.aes | 38 +++++++++---------- 2 files changed, 37 insertions(+), 39 deletions(-) diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl index 7d630eca..56d1c420 100644 --- a/test/aeso_compiler_tests.erl +++ b/test/aeso_compiler_tests.erl @@ -814,8 +814,6 @@ failing_contracts() -> "The type variable `'b` is constrained but never used">>, <>, - <>, <>, < "Values of type `(int, char) => bool` are not comparable by inequality">>, < bool` are not comparable by equality">>, - <>, - <>, - <>, - <>, + <>, + <>, + <>, + <>, < bool)` are not comparable by inequality">>, < "Values of type `custom_datatype(int)` are not comparable by inequality">>, <>, - <>, - <>, - <>, - <>, - <>, + <>, + <>, + <>, + <>, + <>, < bool, (int, char) => bool)` are not comparable by inequality">>, <= 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_ord(x : address, y : address) = x >= y // pass function address_eq (x : address, y : address) = x == y // pass + // Eq types + function event_ord(x : Chain.ttl, y : Chain.ttl) = x >= y // fail function event_eq (x : Chain.ttl, y : Chain.ttl) = x == y // pass @@ -86,14 +86,14 @@ main contract C = // 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 list_of_eq_ord(x : list(A), y : list(A)) = x >= y // fail + function list_of_eq_eq (x : list(A), y : list(A)) = 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 option_of_eq_ord(x : option(A), y : option(A)) = x >= y // fail + function option_of_eq_eq (x : option(A), y : option(A)) = 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 + function tuple_of_eq_ord(x : (A * int), y : (A * int)) = x >= y // fail + function tuple_of_eq_eq (x : (A * int), y : (A * int)) = x == y // pass // Ord composite types of nomcomparable @@ -125,20 +125,20 @@ main contract C = // 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 map_of_eq_ord(x : map(A, A), y : map(A, A)) = x >= y // fail + function map_of_eq_eq (x : map(A, A), y : map(A, A)) = 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_of_eq_ord(x : oracle(A, A), y : oracle(A, A)) = x >= y // fail + function oracle_of_eq_eq (x : oracle(A, A), y : oracle(A, A)) = 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 oracle_query_of_eq_ord(x : oracle_query(A, A), y : oracle_query(A, A)) = x >= y // fail + function oracle_query_of_eq_eq (x : oracle_query(A, A), y : oracle_query(A, A)) = 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 datatype_of_eq_ord(x : custom_datatype(A), y : custom_datatype(A)) = x >= y // fail + function datatype_of_eq_eq (x : custom_datatype(A), y : custom_datatype(A)) = 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 + function record_of_eq_ord(x : custom_record(A), y : custom_record(A)) = x >= y // fail + function record_of_eq_eq (x : custom_record(A), y : custom_record(A)) = x == y // pass // Eq composite types of nomcomparable From e8da0a7cfe1563b8f127a220ebe109adb685bbdd Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sun, 19 Jun 2022 21:44:47 +0400 Subject: [PATCH 14/15] Update docs/sophia_features.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Radosław Rowicki <35342116+radrow@users.noreply.github.com> --- docs/sophia_features.md | 82 +++++++++++++++++++---------------------- 1 file changed, 37 insertions(+), 45 deletions(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index e4f3087e..12ca2ff4 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -502,66 +502,58 @@ function Guards cannot be stateful even when used inside a stateful function. -## Constrainted type variables +## Comparable types -Comparing types by equality (using `==` and `!=`) or by inequality -(using `<`, `>`, `<=`, `=<`, and `>=`) only makes sense by some types. -For example, it is possible to compare two `int`s by inequality -(e.g. `1 < 2`), but it would not make sense to compare two instances of -a contract by inequality. +Only certain types are allowed to be compared by equality (`==`, `!=`) and +inequality (`<`, `>`, `=<`, `>=`). For instance, while it is legal to compare +integers, comparing functions would lead to an error: ``` -contract C = ... -contract Main = - function f(x : C, y : c) = x > y // this is wrong +function f() = + f == f // type error ``` -This is solved in Sophia by adding type variable constraints -(`ord` and `eq`) to limit what can be passed to the binary comparison -operators. +The rules apply as follows: -The type of the equality comparison operators is `'a is eq ; ('a, 'a) => bool` -and of the inequality comparison operators is `'a is ord ; ('a, 'a) => bool` -which means that these operators can only accept types that are comparable by -equality or by inequality respectively. +- All types that are comparable by inequality are also comparable by equality. +- The builtin types `bool`, `int`, `char`, `bits`, `bytes`, `string`, `unit`, + `hash`, `address` and `signature` are comparable by inequality (and thus by + equality). +- The composite types `list`, `option`, and tuples are comparable by + equality/inequality if their type parameters are comparable by + equality/inequality. +- The composite types `map`, `oracle`, and `oracle_query` are comparable by + equality if their type parameters are comparable by equality. +- User-defined records and datatypes are comparable by equality if their type + parameters are comparable by equality. +- Smart contracts are comparable by equality. +- User-declared type variables are comparable according to the [type + constraints](#type-constraints) given in the function signature. -The builtin types `bool`, `int`, `char`, `bits`, `bytes`, `string`, `hash`, -and `signature` are comparable by inequality (and equality) while the types -`address`, `event` are only comparable by equality. +In all other cases the types are not comparable. -The composite types `list`, `option`, and `tuple` are comparable by inequality -if and only if their type argmuments are comparable by inequality. +### Type constraints -The composite types `map`, `oracle`, and `oracle_query` are comparable by -equality if and only if their type arguments are comparable by equality. +Polymorphic types are not declared as comparable by default. If the user +specifies the type signature for a function, they need to manually declare type +constraints in order to allow the variables to be compared. This can only be +done if the type declaration is separated from the function definition. The +constraints have to be prepended to the type declaration and separated with a +semicolon: -All user-defined records and datatypes are comparable by equality if their -type arguments are also comparable by equality. In addition to that, all -user-defined contracts are comparable by equality. - -Anonymous functions (or lambda functions) are not comparable neither by -equality nor by inequality. - -All types that are comparable by inequality are also comparable by equality. -In other words, if a type has `ord` constraint, that implies that it also -have `eq` constraint. +``` -The type variable constraints can be specified in the type signature of any -function. +function eq(x : 'a, y : 'a) = x == y // Type error, 'a is not comparable -``` -// Comparison with < is only allowed because 'a has the constraint ord -lt : 'a is ord ; ('a, 'a) => bool -lt(x, y) = x < y +function + eq : 'a is eq ; ('a, 'a) => bool + eq(x, y) = x == y // Compiles -// Multiple constraints can be specified -ord_and_eq : 'a is ord, 'b is eq ; ('a, 'a, 'b, 'b) => bool -ord_and_eq(x, y, p, q) = x > y && p == q +function eq(x, y) = x == y // Compiles as the constraints are inferred ``` -If the constraints are not mentioned, the type variable is assumed to -have no constraints, and calling any equality or inequality operation -on it will cause an error. +Currently only two constraints are allowed: `eq` for equality and `ord` for +inequality. Declaring a type as `ord` automatically implies `eq`. ## Lists From 21cc6f2b3e49417487252d4ecde78270bf7b2528 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Mon, 20 Jun 2022 10:23:39 +0400 Subject: [PATCH 15/15] Add constrained_t to fold --- src/aeso_syntax_utils.erl | 1 + 1 file changed, 1 insertion(+) diff --git a/src/aeso_syntax_utils.erl b/src/aeso_syntax_utils.erl index e50f2d48..5a0d4164 100644 --- a/src/aeso_syntax_utils.erl +++ b/src/aeso_syntax_utils.erl @@ -61,6 +61,7 @@ fold(Alg = #alg{zero = Zero, plus = Plus, scoped = Scoped}, Fun, K, X) -> {fun_t, _, Named, Args, Ret} -> Type([Named, Args, Ret]); {app_t, _, T, Ts} -> Type([T | Ts]); {tuple_t, _, Ts} -> Type(Ts); + {constrained_t, _, _, T} -> Type(T); %% named_arg_t() {named_arg_t, _, _, T, E} -> Plus(Type(T), Expr(E)); %% expr()