Add comparable typevar constraints #881
@ -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 sum(l : list(int)) : int = foldl((+), 0, l)
|
||||||
function logical_and(x, y) = (&&)(x, y)
|
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
|
### Changed
|
||||||
- Error messages have been restructured (less newlines) to provide more unified errors. Also `pp_oneline/1` has been added.
|
- 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).
|
- Ban empty record definitions (e.g. `record r = {}` would give an error).
|
||||||
|
@ -354,28 +354,29 @@ namespace C =
|
|||||||
## Types
|
## Types
|
||||||
Sophia has the following types:
|
Sophia has the following types:
|
||||||
|
|
||||||
| Type | Description | Example |
|
| Type | Description | Example |
|
||||||
|----------------------|---------------------------------------------------------------------------------------------|--------------------------------------------------------------|
|
|----------------------|---------------------------------------------------------------------------------------------|-------------------------------------------------------------------------------|
|
||||||
| int | A 2-complement integer | ```-1``` |
|
| int | A 2-complement integer | ```-1``` |
|
||||||
| address | æternity address, 32 bytes | ```Call.origin``` |
|
| char | A single character | ```'c'``` |
|
||||||
| bool | A Boolean | ```true``` |
|
| address | æternity address, 32 bytes | ```Call.origin``` ```ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt``` |
|
||||||
| bits | A bit field | ```Bits.none``` |
|
| bool | A Boolean | ```true``` |
|
||||||
| bytes(n) | A byte array with `n` bytes | ```#fedcba9876543210``` |
|
| bits | A bit field | ```Bits.none``` |
|
||||||
| string | An array of bytes | ```"Foo"``` |
|
| bytes(n) | A byte array with `n` bytes | ```#fedcba9876543210``` |
|
||||||
| list | A homogeneous immutable singly linked list. | ```[1, 2, 3]``` |
|
| string | An array of bytes | ```"Foo"``` |
|
||||||
| ('a, 'b) => 'c | A function. Parentheses can be skipped if there is only one argument | ```(x : int, y : int) => x + y``` |
|
| list | A homogeneous immutable singly linked list. | ```[1, 2, 3]``` |
|
||||||
| tuple | An ordered heterogeneous array | ```(42, "Foo", true)``` |
|
| ('a, 'b) => 'c | A function. Parentheses can be skipped if there is only one argument | ```(x : int, y : int) => x + y``` |
|
||||||
| record | An immutable key value store with fixed key names and typed values | ``` record balance = { owner: address, value: int } ``` |
|
| tuple | An ordered heterogeneous array | ```(42, "Foo", true)``` |
|
||||||
| map | An immutable key value store with dynamic mapping of keys of one type to values of one type | ```type accounts = map(string, address)``` |
|
| record | An immutable key value store with fixed key names and typed values | ``` record balance = { owner: address, value: int } ``` |
|
||||||
| option('a) | An optional value either None or Some('a) | ```Some(42)``` |
|
| map | An immutable key value store with dynamic mapping of keys of one type to values of one type | ```type accounts = map(string, address)``` |
|
||||||
| state | A user defined type holding the contract state | ```record state = { owner: address, magic_key: bytes(4) }``` |
|
| option('a) | An optional value either None or Some('a) | ```Some(42)``` |
|
||||||
| event | An append only list of blockchain events (or log entries) | ```datatype event = EventX(indexed int, string)``` |
|
| state | A user defined type holding the contract state | ```record state = { owner: address, magic_key: bytes(4) }``` |
|
||||||
| hash | A 32-byte hash - equivalent to `bytes(32)` | |
|
| event | An append only list of blockchain events (or log entries) | ```datatype event = EventX(indexed int, string)``` |
|
||||||
| signature | A signature - equivalent to `bytes(64)` | |
|
| hash | A 32-byte hash - equivalent to `bytes(32)` | |
|
||||||
| Chain.ttl | Time-to-live (fixed height or relative to current block) | ```FixedTTL(1050)``` ```RelativeTTL(50)``` |
|
| signature | A signature - equivalent to `bytes(64)` | |
|
||||||
| oracle('a, 'b) | And oracle answering questions of type 'a with answers of type 'b | ```Oracle.register(acct, qfee, ttl)``` |
|
| Chain.ttl | Time-to-live (fixed height or relative to current block) | ```FixedTTL(1050)``` ```RelativeTTL(50)``` |
|
||||||
| oracle_query('a, 'b) | A specific oracle query | ```Oracle.query(o, q, qfee, qttl, rttl)``` |
|
| oracle('a, 'b) | And oracle answering questions of type 'a with answers of type 'b | ```Oracle.register(acct, qfee, ttl)``` |
|
||||||
| contract | A user defined, typed, contract address | ```function call_remote(r : RemoteContract) = r.fun()``` |
|
| 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
|
## Literals
|
||||||
| Type | Constant/Literal example(s) |
|
| Type | Constant/Literal example(s) |
|
||||||
@ -501,6 +502,59 @@ function
|
|||||||
|
|
||||||
Guards cannot be stateful even when used inside a stateful 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
|
## Lists
|
||||||
|
|
||||||
A Sophia list is a dynamically sized, homogenous, immutable, singly
|
A Sophia list is a dynamically sized, homogenous, immutable, singly
|
||||||
|
@ -29,9 +29,11 @@ namespace List =
|
|||||||
[] => abort("drop_last_unsafe: list empty")
|
[] => abort("drop_last_unsafe: list empty")
|
||||||
|
|
||||||
|
|
||||||
function contains(e : 'a, l : list('a)) = switch(l)
|
function
|
||||||
[] => false
|
contains : 'a is eq; ('a, list('a)) => bool
|
||||||
h::t => h == e || contains(e, t)
|
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`
|
/** Finds first element of `l` fulfilling predicate `p` as `Some` or `None`
|
||||||
* if no such element exists.
|
* if no such element exists.
|
||||||
|
@ -30,7 +30,9 @@ namespace Option =
|
|||||||
None => abort(err)
|
None => abort(err)
|
||||||
Some(x) => x
|
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)
|
function on_elem(o : option('a), f : 'a => unit) : unit = match((), f, o)
|
||||||
|
|
||||||
|
@ -90,6 +90,7 @@ namespace String =
|
|||||||
Some(ix)
|
Some(ix)
|
||||||
|
|
||||||
private function
|
private function
|
||||||
|
is_prefix : (list(char), list(char)) => option(list(char))
|
||||||
is_prefix([], ys) = Some(ys)
|
is_prefix([], ys) = Some(ys)
|
||||||
is_prefix(_, []) = None
|
is_prefix(_, []) = None
|
||||||
is_prefix(x :: xs, y :: ys) =
|
is_prefix(x :: xs, y :: ys) =
|
||||||
@ -98,10 +99,10 @@ namespace String =
|
|||||||
|
|
||||||
private function
|
private function
|
||||||
to_int_([], _, x, _) = Some(x)
|
to_int_([], _, x, _) = Some(x)
|
||||||
to_int_(i :: is, value, x, b) =
|
to_int_(i :: ints, value, x, b) =
|
||||||
switch(value(i))
|
switch(value(i))
|
||||||
None => None
|
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) =
|
private function ch_to_int_10(ch) =
|
||||||
let c = Char.to_int(ch)
|
let c = Char.to_int(ch)
|
||||||
|
@ -87,7 +87,10 @@
|
|||||||
-type byte_constraint() :: {is_bytes, utype()}
|
-type byte_constraint() :: {is_bytes, utype()}
|
||||||
| {add_bytes, aeso_syntax:ann(), concat | split, utype(), utype(), 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,
|
-record(field_info,
|
||||||
{ ann :: aeso_syntax:ann()
|
{ ann :: aeso_syntax:ann()
|
||||||
@ -818,6 +821,12 @@ infer(Contracts, Options) ->
|
|||||||
ets_new(defined_contracts, [bag]),
|
ets_new(defined_contracts, [bag]),
|
||||||
ets_new(type_vars, [set]),
|
ets_new(type_vars, [set]),
|
||||||
ets_new(warnings, [bag]),
|
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),
|
when_warning(warn_unused_functions, fun() -> create_unused_functions() end),
|
||||||
check_modifiers(Env, Contracts),
|
check_modifiers(Env, Contracts),
|
||||||
create_type_errors(),
|
create_type_errors(),
|
||||||
@ -1177,6 +1186,14 @@ check_modifiers1(What, Decl) when element(1, Decl) == letfun; element(1, Decl) =
|
|||||||
ok;
|
ok;
|
||||||
check_modifiers1(_, _) -> 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().
|
-spec check_type(env(), aeso_syntax:type()) -> aeso_syntax:type().
|
||||||
check_type(Env, T) ->
|
check_type(Env, T) ->
|
||||||
check_type(Env, T, 0).
|
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) ->
|
check_type(_Env, Type = {uvar, _, _}, Arity) ->
|
||||||
ensure_base_type(Type, Arity),
|
ensure_base_type(Type, Arity),
|
||||||
Type;
|
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}, _) ->
|
check_type(_Env, {args_t, Ann, Ts}, _) ->
|
||||||
type_error({new_tuple_syntax, Ann, Ts}),
|
type_error({new_tuple_syntax, Ann, Ts}),
|
||||||
{tuple_t, 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}, Clause} = infer_letfun1(Env, LetFun),
|
||||||
{{Name, Sig}, desugar_clauses(Ann, Fun, Sig, [Clause])}.
|
{{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),
|
Env = Env0#env{ stateful = aeso_syntax:get_ann(stateful, Attrib, false),
|
||||||
current_function = Fun },
|
current_function = Fun },
|
||||||
{NewEnv, {typed, _, {tuple, _, TypedArgs}, {tuple_t, _, ArgTypes}}} = infer_pattern(Env, {tuple, [{origin, system} | NameAttrib], Args}),
|
{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"},
|
Int = {id, As, "int"},
|
||||||
{fun_t, As, [], [Int, Int], Int};
|
{fun_t, As, [], [Int, Int], Int};
|
||||||
infer_infix({RelOp, As})
|
infer_infix({RelOp, As})
|
||||||
when RelOp == '=='; RelOp == '!=';
|
when RelOp == '=='; RelOp == '!=' ->
|
||||||
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 == '>=' ->
|
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"},
|
Bool = {id, As, "bool"},
|
||||||
{fun_t, As, [], [T, T], Bool};
|
{fun_t, As, [], [T, T], Bool};
|
||||||
infer_infix({'..', As}) ->
|
infer_infix({'..', As}) ->
|
||||||
@ -2016,7 +2048,8 @@ next_count() ->
|
|||||||
|
|
||||||
ets_tables() ->
|
ets_tables() ->
|
||||||
[options, type_vars, constraints, freshen_tvars, type_errors,
|
[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() ->
|
clean_up_ets() ->
|
||||||
[ catch ets_delete(Tab) || Tab <- ets_tables() ],
|
[ catch ets_delete(Tab) || Tab <- ets_tables() ],
|
||||||
@ -2178,11 +2211,16 @@ destroy_and_report_unsolved_constraints(Env) ->
|
|||||||
(#named_argument_constraint{}) -> true;
|
(#named_argument_constraint{}) -> true;
|
||||||
(_) -> false
|
(_) -> false
|
||||||
end, OtherCs2),
|
end, OtherCs2),
|
||||||
{BytesCs, []} =
|
{BytesCs, OtherCs4} =
|
||||||
lists:partition(fun({is_bytes, _}) -> true;
|
lists:partition(fun({is_bytes, _}) -> true;
|
||||||
({add_bytes, _, _, _, _, _}) -> true;
|
({add_bytes, _, _, _, _, _}) -> true;
|
||||||
(_) -> false
|
(_) -> false
|
||||||
end, OtherCs3),
|
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 ],
|
Unsolved = [ S || S <- [ solve_constraint(Env, dereference_deep(C)) || C <- NamedArgCs ],
|
||||||
S == unsolved ],
|
S == unsolved ],
|
||||||
@ -2200,6 +2238,7 @@ destroy_and_report_unsolved_constraints(Env) ->
|
|||||||
check_record_create_constraints(Env, CreateCs),
|
check_record_create_constraints(Env, CreateCs),
|
||||||
check_is_contract_constraints(Env, ContractCs),
|
check_is_contract_constraints(Env, ContractCs),
|
||||||
check_bytes_constraints(Env, BytesCs),
|
check_bytes_constraints(Env, BytesCs),
|
||||||
|
check_tvars_constraints(Env, TVarsCs),
|
||||||
|
|
||||||
destroy_constraints().
|
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})
|
_ -> type_error({unsolved_bytes_constraint, Ann, Fun, A, B, C})
|
||||||
end.
|
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 --
|
%% -- Field constraints --
|
||||||
|
|
||||||
check_record_create_constraints(_, []) -> ok;
|
check_record_create_constraints(_, []) -> ok;
|
||||||
@ -2581,7 +2647,16 @@ unify1(_Env, {uvar, A, R}, T, When) ->
|
|||||||
end;
|
end;
|
||||||
unify1(Env, T, {uvar, A, R}, When) ->
|
unify1(Env, T, {uvar, A, R}, When) ->
|
||||||
unify1(Env, {uvar, A, R}, T, 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, {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) ->
|
unify1(Env, [A|B], [C|D], When) ->
|
||||||
unify(Env, A, C, When) andalso unify(Env, B, D, When);
|
unify(Env, A, C, When) andalso unify(Env, B, D, When);
|
||||||
unify1(_Env, X, X, _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, {named_arg_t, _, Id1, Type1, _}, {named_arg_t, _, Id2, Type2, _}, When) ->
|
||||||
unify1(Env, Id1, Id2, {arg_name, Id1, Id2, When}),
|
unify1(Env, Id1, Id2, {arg_name, Id1, Id2, When}),
|
||||||
unify1(Env, Type1, Type2, 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
|
%% The grammar is a bit inconsistent about whether types without
|
||||||
%% arguments are represented as applications to an empty list of
|
%% arguments are represented as applications to an empty list of
|
||||||
%% parameters or not. We therefore allow them to unify.
|
%% parameters or not. We therefore allow them to unify.
|
||||||
@ -2628,6 +2707,28 @@ unify1(_Env, A, B, When) ->
|
|||||||
cannot_unify(A, B, When),
|
cannot_unify(A, B, When),
|
||||||
false.
|
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}) ->
|
dereference(T = {uvar, _, R}) ->
|
||||||
case ets_lookup(type_vars, R) of
|
case ets_lookup(type_vars, R) of
|
||||||
[] ->
|
[] ->
|
||||||
@ -2655,6 +2756,7 @@ occurs_check1(_, {con, _, _}) -> false;
|
|||||||
occurs_check1(_, {qid, _, _}) -> false;
|
occurs_check1(_, {qid, _, _}) -> false;
|
||||||
occurs_check1(_, {qcon, _, _}) -> false;
|
occurs_check1(_, {qcon, _, _}) -> false;
|
||||||
occurs_check1(_, {tvar, _, _}) -> false;
|
occurs_check1(_, {tvar, _, _}) -> false;
|
||||||
|
occurs_check1(_, {constrained_t, _, _, _}) -> false;
|
||||||
occurs_check1(_, {bytes_t, _, _}) -> false;
|
occurs_check1(_, {bytes_t, _, _}) -> false;
|
||||||
occurs_check1(R, {fun_t, _, Named, Args, Res}) ->
|
occurs_check1(R, {fun_t, _, Named, Args, Res}) ->
|
||||||
occurs_check(R, [Res, Named | Args]);
|
occurs_check(R, [Res, Named | Args]);
|
||||||
@ -2771,7 +2873,8 @@ all_warnings() ->
|
|||||||
, warn_unused_functions
|
, warn_unused_functions
|
||||||
, warn_shadowing
|
, warn_shadowing
|
||||||
, warn_division_by_zero
|
, warn_division_by_zero
|
||||||
, warn_negative_spend ].
|
, warn_negative_spend
|
||||||
|
, warn_duplicated_constraints ].
|
||||||
|
|
||||||
when_warning(Warn, Do) ->
|
when_warning(Warn, Do) ->
|
||||||
case lists:member(Warn, all_warnings()) of
|
case lists:member(Warn, all_warnings()) of
|
||||||
@ -2908,6 +3011,19 @@ warn_potential_negative_spend(Ann, Fun, Args) ->
|
|||||||
_ -> ok
|
_ -> ok
|
||||||
end.
|
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.
|
%% Save unification failures for error messages.
|
||||||
|
|
||||||
cannot_unify(A, B, When) ->
|
cannot_unify(A, B, When) ->
|
||||||
@ -3299,6 +3415,18 @@ mk_error({unknown_warning, Warning}) ->
|
|||||||
mk_error({empty_record_definition, Ann, Name}) ->
|
mk_error({empty_record_definition, Ann, Name}) ->
|
||||||
Msg = io_lib:format("Empty record definitions are not allowed. Cannot define the record `~s`", [Name]),
|
Msg = io_lib:format("Empty record definitions are not allowed. Cannot define the record `~s`", [Name]),
|
||||||
mk_t_err(pos(Ann), Msg);
|
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) ->
|
mk_error(Err) ->
|
||||||
Msg = io_lib:format("Unknown error: ~p", [Err]),
|
Msg = io_lib:format("Unknown error: ~p", [Err]),
|
||||||
mk_t_err(pos(0, 0), Msg).
|
mk_t_err(pos(0, 0), Msg).
|
||||||
@ -3330,6 +3458,10 @@ mk_warning({division_by_zero, Ann}) ->
|
|||||||
mk_warning({negative_spend, Ann}) ->
|
mk_warning({negative_spend, Ann}) ->
|
||||||
Msg = io_lib:format("Negative spend.", []),
|
Msg = io_lib:format("Negative spend.", []),
|
||||||
aeso_warnings:new(pos(Ann), Msg);
|
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) ->
|
mk_warning(Warn) ->
|
||||||
Msg = io_lib:format("Unknown warning: ~p", [Warn]),
|
Msg = io_lib:format("Unknown warning: ~p", [Warn]),
|
||||||
aeso_warnings:new(Msg).
|
aeso_warnings:new(Msg).
|
||||||
@ -3554,6 +3686,8 @@ pp({uvar, _, Ref}) ->
|
|||||||
["?u" | integer_to_list(erlang:phash2(Ref, 16384)) ];
|
["?u" | integer_to_list(erlang:phash2(Ref, 16384)) ];
|
||||||
pp({tvar, _, Name}) ->
|
pp({tvar, _, Name}) ->
|
||||||
Name;
|
Name;
|
||||||
|
pp(T = {constrained_t, _, _, {tvar, _, _}}) ->
|
||||||
|
prettypr:format(aeso_pretty:type(T));
|
||||||
pp({if_t, _, Id, Then, Else}) ->
|
pp({if_t, _, Id, Then, Else}) ->
|
||||||
["if(", pp([Id, Then, Else]), ")"];
|
["if(", pp([Id, Then, Else]), ")"];
|
||||||
pp({tuple_t, _, []}) ->
|
pp({tuple_t, _, []}) ->
|
||||||
|
@ -495,6 +495,8 @@ type_to_fcode(_Env, _Sub, {tvar, Ann, "void"}) ->
|
|||||||
fcode_error({found_void, Ann});
|
fcode_error({found_void, Ann});
|
||||||
type_to_fcode(_Env, Sub, {tvar, _, X}) ->
|
type_to_fcode(_Env, Sub, {tvar, _, X}) ->
|
||||||
maps:get(X, 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, _}) ->
|
type_to_fcode(_Env, _Sub, {fun_t, Ann, _, var_args, _}) ->
|
||||||
fcode_error({var_args_not_set, {id, Ann, "a very suspicious function"}});
|
fcode_error({var_args_not_set, {id, Ann, "a very suspicious function"}});
|
||||||
type_to_fcode(Env, Sub, {fun_t, _, Named, Args, Res}) ->
|
type_to_fcode(Env, Sub, {fun_t, _, Named, Args, Res}) ->
|
||||||
|
@ -134,9 +134,19 @@ fun_block(Mods, Kind, [Decl]) ->
|
|||||||
fun_block(Mods, Kind, Decls) ->
|
fun_block(Mods, Kind, Decls) ->
|
||||||
{block, get_ann(Kind), [ add_modifiers(Mods, Kind, Decl) || Decl <- 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() ->
|
fundef_or_decl() ->
|
||||||
choice([?RULE(id(), tok(':'), type(), {fun_decl, get_ann(_1), _1, _3}),
|
choice([fundecl(), fundef()]).
|
||||||
fundef()]).
|
|
||||||
|
|
||||||
using() ->
|
using() ->
|
||||||
Alias = {keyword(as), con()},
|
Alias = {keyword(as), con()},
|
||||||
@ -527,6 +537,7 @@ parens(P) -> between(tok('('), P, tok(')')).
|
|||||||
braces(P) -> between(tok('{'), P, tok('}')).
|
braces(P) -> between(tok('{'), P, tok('}')).
|
||||||
brackets(P) -> between(tok('['), P, tok(']')).
|
brackets(P) -> between(tok('['), P, tok(']')).
|
||||||
comma_sep(P) -> sep(P, tok(',')).
|
comma_sep(P) -> sep(P, tok(',')).
|
||||||
|
comma_sep1(P) -> sep1(P, tok(',')).
|
||||||
|
|
||||||
paren_list(P) -> parens(comma_sep(P)).
|
paren_list(P) -> parens(comma_sep(P)).
|
||||||
brace_list(P) -> braces(comma_sep(P)).
|
brace_list(P) -> braces(comma_sep(P)).
|
||||||
|
@ -284,7 +284,9 @@ type(T = {id, _, _}) -> name(T);
|
|||||||
type(T = {qid, _, _}) -> name(T);
|
type(T = {qid, _, _}) -> name(T);
|
||||||
type(T = {con, _, _}) -> name(T);
|
type(T = {con, _, _}) -> name(T);
|
||||||
type(T = {qcon, _, _}) -> 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().
|
-spec args_type([aeso_syntax:type()]) -> doc().
|
||||||
args_type(Args) ->
|
args_type(Args) ->
|
||||||
|
@ -45,7 +45,7 @@ lexer() ->
|
|||||||
|
|
||||||
Keywords = ["contract", "include", "let", "switch", "type", "record", "datatype", "if", "elif", "else", "function",
|
Keywords = ["contract", "include", "let", "switch", "type", "record", "datatype", "if", "elif", "else", "function",
|
||||||
"stateful", "payable", "true", "false", "mod", "public", "entrypoint", "private", "indexed", "namespace",
|
"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, "|"),
|
KW = string:join(Keywords, "|"),
|
||||||
|
|
||||||
|
@ -79,11 +79,14 @@
|
|||||||
|
|
||||||
-type constructor_t() :: {constr_t, ann(), con(), [type()]}.
|
-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()}
|
-type type() :: {fun_t, ann(), [named_arg_t()], [type()], type()}
|
||||||
| {app_t, ann(), type(), [type()]}
|
| {app_t, ann(), type(), [type()]}
|
||||||
| {tuple_t, ann(), [type()]}
|
| {tuple_t, ann(), [type()]}
|
||||||
| {args_t, ann(), [type()]} %% old tuple syntax, old for error messages
|
| {args_t, ann(), [type()]} %% old tuple syntax, old for error messages
|
||||||
| {bytes_t, ann(), integer() | any}
|
| {bytes_t, ann(), integer() | any}
|
||||||
|
| {constrained_t, ann(), [tvar_constraint()], type()}
|
||||||
| id() | qid()
|
| id() | qid()
|
||||||
| con() | qcon() %% contracts
|
| con() | qcon() %% contracts
|
||||||
| tvar().
|
| tvar().
|
||||||
|
@ -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]);
|
{fun_t, _, Named, Args, Ret} -> Type([Named, Args, Ret]);
|
||||||
{app_t, _, T, Ts} -> Type([T | Ts]);
|
{app_t, _, T, Ts} -> Type([T | Ts]);
|
||||||
{tuple_t, _, Ts} -> Type(Ts);
|
{tuple_t, _, Ts} -> Type(Ts);
|
||||||
|
{constrained_t, _, _, T} -> Type(T);
|
||||||
%% named_arg_t()
|
%% named_arg_t()
|
||||||
{named_arg_t, _, _, T, E} -> Plus(Type(T), Expr(E));
|
{named_arg_t, _, _, T, E} -> Plus(Type(T), Expr(E));
|
||||||
%% expr()
|
%% expr()
|
||||||
|
@ -265,7 +265,9 @@ warnings() ->
|
|||||||
"The function `called_unused_function2` is defined but never used.">>,
|
"The function `called_unused_function2` is defined but never used.">>,
|
||||||
<<?PosW(48, 5)
|
<<?PosW(48, 5)
|
||||||
"Unused return value.">>,
|
"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.">>
|
"The function `dec` is defined but never used.">>
|
||||||
]).
|
]).
|
||||||
|
|
||||||
@ -805,6 +807,88 @@ failing_contracts() ->
|
|||||||
"to arguments\n"
|
"to arguments\n"
|
||||||
" `1 : int`">>
|
" `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,
|
, ?TYPE_ERROR(warnings,
|
||||||
[<<?Pos(0, 0)
|
[<<?Pos(0, 0)
|
||||||
"The file `Triple.aes` is included but not used.">>,
|
"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.">>,
|
"The function `called_unused_function2` is defined but never used.">>,
|
||||||
<<?Pos(48, 5)
|
<<?Pos(48, 5)
|
||||||
"Unused return value.">>,
|
"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.">>
|
"The function `dec` is defined but never used.">>
|
||||||
])
|
])
|
||||||
].
|
].
|
||||||
|
169
test/contracts/comparable_typevar_constraints.aes
Normal file
169
test/contracts/comparable_typevar_constraints.aes
Normal 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
|
||||||
|
|
||||||
|
()
|
@ -48,6 +48,11 @@ contract Warnings =
|
|||||||
rv()
|
rv()
|
||||||
2
|
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 =
|
namespace FunctionsAsArgs =
|
||||||
function f() = g()
|
function f() = g()
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user