diff --git a/CHANGELOG.md b/CHANGELOG.md index 218866c..f0bdfef 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). diff --git a/docs/sophia_features.md b/docs/sophia_features.md index aa9e229..12ca2ff 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -354,28 +354,29 @@ namespace C = ## Types Sophia has the following types: -| Type | Description | Example | -|----------------------|---------------------------------------------------------------------------------------------|--------------------------------------------------------------| -| int | A 2-complement integer | ```-1``` | -| 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) | @@ -501,6 +502,59 @@ function Guards cannot be stateful even when used inside a stateful function. +## Comparable types + +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: + +``` +function f() = + f == f // type error +``` + +The rules apply as follows: + +- 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. + +In all other cases the types are not comparable. + +### Type constraints + +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: + +``` + +function eq(x : 'a, y : 'a) = x == y // Type error, 'a is not comparable + +function + eq : 'a is eq ; ('a, 'a) => bool + eq(x, y) = x == y // Compiles + +function eq(x, y) = x == y // Compiles as the constraints are inferred +``` + +Currently only two constraints are allowed: `eq` for equality and `ord` for +inequality. Declaring a type as `ord` automatically implies `eq`. + ## Lists A Sophia list is a dynamically sized, homogenous, immutable, singly 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 33f813b..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) = @@ -98,10 +99,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_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 72c9372..977935e 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() @@ -818,6 +821,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"}, {"address"} ], + 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 +1186,14 @@ check_modifiers1(What, Decl) when element(1, Decl) == letfun; element(1, Decl) = ok; check_modifiers1(_, _) -> ok. +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 +1236,15 @@ 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) ], + [ 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}, _) -> type_error({new_tuple_syntax, Ann, Ts}), {tuple_t, Ann, Ts}. @@ -1398,7 +1424,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 +1969,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 +2048,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 +2211,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 +2238,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 +2368,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; @@ -2581,7 +2647,16 @@ 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) -> unify(Env, A, C, When) andalso unify(Env, B, D, When); unify1(_Env, X, X, _When) -> @@ -2617,6 +2692,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 +2707,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 +2756,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 +2873,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 +3011,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 +3415,18 @@ 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({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). @@ -3330,6 +3458,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 +3686,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_parser.erl b/src/aeso_parser.erl index 51b81f6..c32d944 100644 --- a/src/aeso_parser.erl +++ b/src/aeso_parser.erl @@ -134,9 +134,19 @@ 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), id(), {constraint, get_ann(_1), _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 +537,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_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/src/aeso_scan.erl b/src/aeso_scan.erl index 4587efa..c7de2eb 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" ], KW = string:join(Keywords, "|"), diff --git a/src/aeso_syntax.erl b/src/aeso_syntax.erl index 1e01153..c92f0f6 100644 --- a/src/aeso_syntax.erl +++ b/src/aeso_syntax.erl @@ -79,11 +79,14 @@ -type constructor_t() :: {constr_t, ann(), con(), [type()]}. +-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(), [tvar_constraint()], type()} | id() | qid() | con() | qcon() %% contracts | tvar(). diff --git a/src/aeso_syntax_utils.erl b/src/aeso_syntax_utils.erl index e50f2d4..5a0d416 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() diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl index 6fccd21..56d1c42 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,88 @@ 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">>, + <>, + < 'a` are not comparable by inequality">>, + < 'b` are not comparable by equality">> + ]) , ?TYPE_ERROR(warnings, [<>, @@ -834,7 +918,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..b87fce7 --- /dev/null +++ b/test/contracts/comparable_typevar_constraints.aes @@ -0,0 +1,169 @@ +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 + + 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 + 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 + + 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 + + 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(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(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 : (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 + + 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(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(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(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(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(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 + + 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() = + 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 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()