QPQ-AG/sophia
10
0
Fork 0
Code Issues 41 Pull Requests 5 Actions Packages Projects Releases 16 Wiki Activity

Add comparable typevar constraints #881

Open
ghallak wants to merge 15 commits from ghallak/229 into master
pull from: ghallak/229
merge into: QPQ-AG:master
Conversation 18 Commits 15 Files Changed 15 +522 -42
15 changed files with 522 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
CHANGELOG.md
View File

@ -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).

98
docs/sophia_features.md
View File

@ -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

8
priv/stdlib/List.aes
View File

@ -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.

4
priv/stdlib/Option.aes
View File

@ -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)

5
priv/stdlib/String.aes
View File

@ -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)

150
src/aeso_ast_infer_types.erl
View File

@ -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, _, []}) ->

2
src/aeso_ast_to_fcode.erl
View File

@ -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}) ->

15
src/aeso_parser.erl
View File

@ -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)).

4
src/aeso_pretty.erl
View File

@ -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) ->

2
src/aeso_scan.erl
View File

@ -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, "|"),

3
src/aeso_syntax.erl
View File

@ -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().

1
src/aeso_syntax_utils.erl
View File

@ -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()

90
test/aeso_compiler_tests.erl
View File

@ -265,7 +265,9 @@ warnings() ->
"The function `called_unused_function2` is defined but never used.">>,
<<?PosW(48, 5)
"Unused return value.">>,
<<?PosW(60, 5)
<<?PosW(53, 44)
"The constraint on the type variable `'a` is a duplication of the constraint at line 53, column 34">>,
<<?PosW(65, 5)
"The function `dec` is defined but never used.">>
]).
@ -805,6 +807,88 @@ failing_contracts() ->
"to arguments\n"
" `1 : int`">>
])
, ?TYPE_ERROR(comparable_typevar_constraints,
[<<?Pos(21,30)
"Values of type `'a` are not comparable by equality">>,
<<?Pos(25,38)
"The type variable `'b` is constrained but never used">>,
<<?Pos(29,41)
"Unknown constraint `foo` used on the type variable `'a`">>,
<<?Pos(63,58)
"Values of type `Chain.ttl` are not comparable by inequality">>,
<<?Pos(66,45)
"Values of type `A` are not comparable by inequality">>,
<<?Pos(73,47)
"Values of type `(int, char) => bool` are not comparable by inequality">>,
<<?Pos(74,47)
"Values of type `(int, char) => bool` are not comparable by equality">>,
<<?Pos(89,59)
"Values of type `list(A)` are not comparable by inequality">>,
<<?Pos(92,65)
"Values of type `option(A)` are not comparable by inequality">>,
<<?Pos(95,64)
"Values of type `(A * int)` are not comparable by inequality">>,
<<?Pos(96,64)
"Values of type `(A * int)` are not comparable by equality">>,
<<?Pos(100,68)
"Values of type `list((int, char) => bool)` are not comparable by inequality">>,
<<?Pos(101,68)
"Values of type `list((int, char) => bool)` are not comparable by equality">>,
<<?Pos(103,74)
"Values of type `option((int, char) => bool)` are not comparable by inequality">>,
<<?Pos(104,74)
"Values of type `option((int, char) => bool)` are not comparable by equality">>,
<<?Pos(106,73)
"Values of type `((int, char) => bool * int)` are not comparable by inequality">>,
<<?Pos(107,73)
"Values of type `((int, char) => bool * int)` are not comparable by equality">>,
<<?Pos(111,71)
"Values of type `map(int, int)` are not comparable by inequality">>,
<<?Pos(114,80)
"Values of type `oracle(int, int)` are not comparable by inequality">>,
<<?Pos(117,98)
"Values of type `oracle_query(int, int)` are not comparable by inequality">>,
<<?Pos(120,90)
"Values of type `custom_datatype(int)` are not comparable by inequality">>,
<<?Pos(123,84)
"Values of type `custom_record(int)` are not comparable by inequality">>,
<<?Pos(128,62)
"Values of type `map(A, A)` are not comparable by inequality">>,
<<?Pos(131,71)
"Values of type `oracle(A, A)` are not comparable by inequality">>,
<<?Pos(134,89)
"Values of type `oracle_query(A, A)` are not comparable by inequality">>,
<<?Pos(137,85)
"Values of type `custom_datatype(A)` are not comparable by inequality">>,
<<?Pos(140,79)
"Values of type `custom_record(A)` are not comparable by inequality">>,
<<?Pos(145,75)
"Values of type `map((int, char) => bool, (int, char) => bool)` are not comparable by inequality">>,
<<?Pos(146,75)
"Values of type `map((int, char) => bool, (int, char) => bool)` are not comparable by equality">>,
<<?Pos(148,84)
"Values of type `oracle((int, char) => bool, (int, char) => bool)` are not comparable by inequality">>,
<<?Pos(149,84)
"Values of type `oracle((int, char) => bool, (int, char) => bool)` are not comparable by equality">>,
<<?Pos(151,102)
"Values of type `oracle_query((int, char) => bool, (int, char) => bool)` are not comparable by inequality">>,
<<?Pos(152,102)
"Values of type `oracle_query((int, char) => bool, (int, char) => bool)` are not comparable by equality">>,
<<?Pos(154,94)
"Values of type `custom_datatype((int, char) => bool)` are not comparable by inequality">>,
<<?Pos(155,94)
"Values of type `custom_datatype((int, char) => bool)` are not comparable by equality">>,
<<?Pos(157,88)
"Values of type `custom_record((int, char) => bool)` are not comparable by inequality">>,
<<?Pos(158,88)
"Values of type `custom_record((int, char) => bool)` are not comparable by equality">>,
<<?Pos(162,35)
"Values of type `map(int, int)` are not comparable by inequality">>,
<<?Pos(163,35)
"Values of type `('a) => 'a` are not comparable by inequality">>,
<<?Pos(167,34)
"Values of type `('b) => 'b` are not comparable by equality">>
])
, ?TYPE_ERROR(warnings,
[<<?Pos(0, 0)
"The file `Triple.aes` is included but not used.">>,
@ -834,7 +918,9 @@ failing_contracts() ->
"The function `called_unused_function2` is defined but never used.">>,
<<?Pos(48, 5)
"Unused return value.">>,
<<?Pos(60, 5)
<<?Pos(53, 44)
"The constraint on the type variable `'a` is a duplication of the constraint at line 53, column 34">>,
<<?Pos(65, 5)
"The function `dec` is defined but never used.">>
])
].

169
test/contracts/comparable_typevar_constraints.aes Normal file
View File

@ -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
()

5
test/contracts/warnings.aes
View File

@ -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()