Compare commits
29 Commits
| Author | SHA1 | Date | |
|---|---|---|---|
| 9335db65d0 | |||
| 0bc9cfb957 | |||
| 89afa9ec8f | |||
| 5575d3cb17 | |||
| 1d6f24965b | |||
| bd726a8902 | |||
| 7277a968f8 | |||
| d8558df6a4 | |||
| 4d6b13bcf1 | |||
| cf7830e4f5 | |||
| 03e53f60cd | |||
| c0330be3b4 | |||
| 701a24553a | |||
| 54c8c50a58 | |||
| cdcc119c9e | |||
| 1aa476318f | |||
| 97db569b9b | |||
| 5c14fc3fe6 | |||
| 85c14c512b | |||
| 126a78455b | |||
| ffc63704fb | |||
| c4243fb1da | |||
| a64e9643fd | |||
| ed934019db | |||
| 0f5daafc29 | |||
| e050618d7a | |||
| 62a0ff2e4c | |||
| 7b8957b46a | |||
| e46226a693 |
@@ -16,14 +16,6 @@ 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).
|
||||
|
||||
+22
-76
@@ -354,29 +354,28 @@ namespace C =
|
||||
## Types
|
||||
Sophia has the following types:
|
||||
|
||||
| Type | Description | Example |
|
||||
|----------------------|---------------------------------------------------------------------------------------------|-------------------------------------------------------------------------------|
|
||||
| int | A 2-complement integer | ```-1``` |
|
||||
| char | A single character | ```'c'``` |
|
||||
| address | æternity address, 32 bytes | ```Call.origin``` ```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()``` |
|
||||
| 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()``` |
|
||||
|
||||
## Literals
|
||||
| Type | Constant/Literal example(s) |
|
||||
@@ -502,59 +501,6 @@ 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
|
||||
|
||||
@@ -812,8 +812,8 @@ Registers new oracle answering questions of type `'a` with answers of type `'b`.
|
||||
private key of the account, proving you have the private key of the oracle to be. If the
|
||||
address is the same as the contract `sign` is ignored and can be left out entirely.
|
||||
* The `qfee` is the minimum query fee to be paid by a user when asking a question of the oracle.
|
||||
* The `ttl` is the Time To Live for the oracle, either relative to the current
|
||||
height (`RelativeTTL(delta)`) or a fixed height (`FixedTTL(height)`).
|
||||
* The `ttl` is the Time To Live for the oracle in key blocks, either relative to the current
|
||||
key block height (`RelativeTTL(delta)`) or a fixed key block height (`FixedTTL(height)`).
|
||||
* The type `'a` is the type of the question to ask.
|
||||
* The type `'b` is the type of the oracle answers.
|
||||
|
||||
|
||||
@@ -29,11 +29,9 @@ namespace List =
|
||||
[] => abort("drop_last_unsafe: list empty")
|
||||
|
||||
|
||||
function
|
||||
contains : 'a is eq; ('a, list('a)) => bool
|
||||
contains(e, l) = switch(l)
|
||||
[] => false
|
||||
h::t => h == e || contains(e, t)
|
||||
function contains(e : 'a, l : list('a)) = 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.
|
||||
|
||||
@@ -30,9 +30,7 @@ namespace Option =
|
||||
None => abort(err)
|
||||
Some(x) => x
|
||||
|
||||
function
|
||||
contains : 'a is eq; ('a, option('a)) => bool
|
||||
contains(e, o) = o == Some(e)
|
||||
function contains(e : 'a, o : option('a)) = o == Some(e)
|
||||
|
||||
function on_elem(o : option('a), f : 'a => unit) : unit = match((), f, o)
|
||||
|
||||
|
||||
@@ -90,7 +90,6 @@ 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) =
|
||||
@@ -99,10 +98,10 @@ namespace String =
|
||||
|
||||
private function
|
||||
to_int_([], _, x, _) = Some(x)
|
||||
to_int_(i :: ints, value, x, b) =
|
||||
to_int_(i :: is, value, x, b) =
|
||||
switch(value(i))
|
||||
None => None
|
||||
Some(i) => to_int_(ints, value, x * b + i, b)
|
||||
Some(n) => to_int_(is, value, x * b + n, b)
|
||||
|
||||
private function ch_to_int_10(ch) =
|
||||
let c = Char.to_int(ch)
|
||||
|
||||
+5
-3
@@ -83,7 +83,7 @@ from_typed_ast(Type, TypedAst) ->
|
||||
string -> do_render_aci_json(JArray)
|
||||
end.
|
||||
|
||||
encode_contract(Contract = {Head, _, {con, _, Name}, _}) when ?IS_CONTRACT_HEAD(Head) ->
|
||||
encode_contract(Contract = {Head, _, {con, _, Name}, _, _}) when ?IS_CONTRACT_HEAD(Head) ->
|
||||
C0 = #{name => encode_name(Name)},
|
||||
|
||||
Tdefs0 = [ encode_typedef(T) || T <- sort_decls(contract_types(Contract)) ],
|
||||
@@ -341,10 +341,12 @@ stateful(false) -> "".
|
||||
|
||||
%% #contract{Ann, Con, [Declarations]}.
|
||||
|
||||
contract_funcs({C, _, _, Decls}) when ?IS_CONTRACT_HEAD(C); C == namespace ->
|
||||
contract_funcs({C, _, _, _, Decls}) when ?IS_CONTRACT_HEAD(C) ->
|
||||
[ D || D <- Decls, is_fun(D)].
|
||||
|
||||
contract_types({C, _, _, Decls}) when ?IS_CONTRACT_HEAD(C); C == namespace ->
|
||||
contract_types({namespace, _, _, Decls}) ->
|
||||
[ D || D <- Decls, is_type(D) ];
|
||||
contract_types({C, _, _, _, Decls}) when ?IS_CONTRACT_HEAD(C) ->
|
||||
[ D || D <- Decls, is_type(D) ].
|
||||
|
||||
is_fun({letfun, _, _, _, _, _}) -> true;
|
||||
|
||||
+243
-192
@@ -87,10 +87,7 @@
|
||||
-type byte_constraint() :: {is_bytes, utype()}
|
||||
| {add_bytes, aeso_syntax:ann(), concat | split, utype(), utype(), utype()}.
|
||||
|
||||
-type tvar_constraint() :: {is_eq, utype()}
|
||||
| {is_ord, utype()}.
|
||||
|
||||
-type constraint() :: named_argument_constraint() | field_constraint() | byte_constraint() | tvar_constraint().
|
||||
-type constraint() :: named_argument_constraint() | field_constraint() | byte_constraint().
|
||||
|
||||
-record(field_info,
|
||||
{ ann :: aeso_syntax:ann()
|
||||
@@ -116,6 +113,8 @@
|
||||
|
||||
-type type_constraints() :: none | bytes_concat | bytes_split | address_to_contract | bytecode_hash.
|
||||
|
||||
-type variance() :: invariant | covariant | contravariant | bivariant.
|
||||
|
||||
-type fun_info() :: {aeso_syntax:ann(), typesig() | type()}.
|
||||
-type type_info() :: {aeso_syntax:ann(), typedef()}.
|
||||
-type var_info() :: {aeso_syntax:ann(), utype()}.
|
||||
@@ -137,11 +136,13 @@
|
||||
, vars = [] :: [{name(), var_info()}]
|
||||
, typevars = unrestricted :: unrestricted | [name()]
|
||||
, fields = #{} :: #{ name() => [field_info()] } %% fields are global
|
||||
, contract_parents = #{} :: #{ name() => [name()] }
|
||||
, namespace = [] :: qname()
|
||||
, used_namespaces = [] :: used_namespaces()
|
||||
, in_pattern = false :: boolean()
|
||||
, in_guard = false :: boolean()
|
||||
, stateful = false :: boolean()
|
||||
, unify_throws = true :: boolean()
|
||||
, current_function = none :: none | aeso_syntax:id()
|
||||
, what = top :: top | namespace | contract | contract_interface
|
||||
}).
|
||||
@@ -283,7 +284,7 @@ contract_call_type({fun_t, Ann, [], Args, Ret}) ->
|
||||
Args, {if_t, Ann, Id("protected"), {app_t, Ann, {id, Ann, "option"}, [Ret]}, Ret}}.
|
||||
|
||||
-spec bind_contract(aeso_syntax:decl(), env()) -> env().
|
||||
bind_contract({Contract, Ann, Id, Contents}, Env)
|
||||
bind_contract({Contract, Ann, Id, _Impls, Contents}, Env)
|
||||
when ?IS_CONTRACT_HEAD(Contract) ->
|
||||
Key = name(Id),
|
||||
Sys = [{origin, system}],
|
||||
@@ -821,11 +822,13 @@ 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),
|
||||
ets_new(type_vars_variance, [set]),
|
||||
%% Set the variance for builtin types
|
||||
ets_insert(type_vars_variance, {"list", [covariant]}),
|
||||
ets_insert(type_vars_variance, {"option", [covariant]}),
|
||||
ets_insert(type_vars_variance, {"map", [covariant, covariant]}),
|
||||
ets_insert(type_vars_variance, {"oracle", [contravariant, covariant]}),
|
||||
ets_insert(type_vars_variance, {"oracle_query", [covariant, covariant]}),
|
||||
|
||||
when_warning(warn_unused_functions, fun() -> create_unused_functions() end),
|
||||
check_modifiers(Env, Contracts),
|
||||
@@ -854,9 +857,12 @@ infer(Contracts, Options) ->
|
||||
-spec infer1(env(), [aeso_syntax:decl()], [aeso_syntax:decl()], list(option())) ->
|
||||
{env(), [aeso_syntax:decl()]}.
|
||||
infer1(Env, [], Acc, _Options) -> {Env, lists:reverse(Acc)};
|
||||
infer1(Env, [{Contract, Ann, ConName, Code} | Rest], Acc, Options)
|
||||
infer1(Env0, [{Contract, Ann, ConName, Impls, Code} | Rest], Acc, Options)
|
||||
when ?IS_CONTRACT_HEAD(Contract) ->
|
||||
%% do type inference on each contract independently.
|
||||
Env = Env0#env{ contract_parents = maps:put(name(ConName),
|
||||
[name(Impl) || Impl <- Impls],
|
||||
Env0#env.contract_parents) },
|
||||
check_scope_name_clash(Env, contract, ConName),
|
||||
What = case Contract of
|
||||
contract_main -> contract;
|
||||
@@ -868,7 +874,8 @@ infer1(Env, [{Contract, Ann, ConName, Code} | Rest], Acc, Options)
|
||||
contract_interface -> ok
|
||||
end,
|
||||
{Env1, Code1} = infer_contract_top(push_scope(contract, ConName, Env), What, Code, Options),
|
||||
Contract1 = {Contract, Ann, ConName, Code1},
|
||||
Contract1 = {Contract, Ann, ConName, Impls, Code1},
|
||||
check_implemented_interfaces(Env1, Contract1, Acc),
|
||||
Env2 = pop_scope(Env1),
|
||||
Env3 = bind_contract(Contract1, Env2),
|
||||
infer1(Env3, Rest, [Contract1 | Acc], Options);
|
||||
@@ -888,17 +895,66 @@ infer1(Env, [{pragma, _, _} | Rest], Acc, Options) ->
|
||||
%% Pragmas are checked in check_modifiers
|
||||
infer1(Env, Rest, Acc, Options).
|
||||
|
||||
check_implemented_interfaces(Env, {_Contract, _Ann, ConName, Impls, Code}, DefinedContracts) ->
|
||||
create_type_errors(),
|
||||
AllInterfaces = [{name(IName), I} || I = {contract_interface, _, IName, _, _} <- DefinedContracts],
|
||||
ImplsNames = lists:map(fun name/1, Impls),
|
||||
|
||||
%% All implemented intrefaces should already be defined
|
||||
lists:foreach(fun(Impl) -> case proplists:get_value(name(Impl), AllInterfaces) of
|
||||
undefined -> type_error({referencing_undefined_interface, Impl});
|
||||
_ -> ok
|
||||
end
|
||||
end, Impls),
|
||||
|
||||
ImplementedInterfaces = [I || I <- [proplists:get_value(Name, AllInterfaces) || Name <- ImplsNames],
|
||||
I /= undefined],
|
||||
Funs = [ Fun || Fun <- Code,
|
||||
element(1, Fun) == letfun orelse element(1, Fun) == fun_decl ],
|
||||
check_implemented_interfaces1(Env, ImplementedInterfaces, ConName, Funs, AllInterfaces),
|
||||
destroy_and_report_type_errors(Env).
|
||||
|
||||
%% Recursively check that all directly and indirectly referenced interfaces are implemented
|
||||
check_implemented_interfaces1(_, [], _, _, _) ->
|
||||
ok;
|
||||
check_implemented_interfaces1(Env, [{contract_interface, _, IName, _, Decls} | Interfaces],
|
||||
ConId, Impls, AllInterfaces) ->
|
||||
Unmatched = match_impls(Env, Decls, ConId, name(IName), Impls),
|
||||
check_implemented_interfaces1(Env, Interfaces, ConId, Unmatched, AllInterfaces).
|
||||
|
||||
%% Match the functions of the contract with the interfaces functions, and return unmatched functions
|
||||
match_impls(_, [], _, _, Impls) ->
|
||||
Impls;
|
||||
match_impls(Env, [{fun_decl, _, {id, _, FunName}, FunType = {fun_t, _, _, ArgsTypes, RetDecl}} | Decls], ConId, IName, Impls) ->
|
||||
Match = fun({letfun, _, {id, _, FName}, Args, RetFun, _}) when FName == FunName ->
|
||||
length(ArgsTypes) == length(Args) andalso
|
||||
unify(Env#env{unify_throws = false}, RetDecl, RetFun, unknown) andalso
|
||||
lists:all(fun({T1, {typed, _, _, T2}}) -> unify(Env#env{unify_throws = false}, T1, T2, unknown) end,
|
||||
lists:zip(ArgsTypes, Args));
|
||||
({fun_decl, _, {id, _, FName}, FunT}) when FName == FunName ->
|
||||
unify(Env#env{unify_throws = false}, FunT, FunType, unknown);
|
||||
(_) -> false
|
||||
end,
|
||||
UnmatchedImpls = case lists:search(Match, Impls) of
|
||||
{value, V} ->
|
||||
lists:delete(V, Impls);
|
||||
false ->
|
||||
type_error({unimplemented_interface_function, ConId, IName, FunName}),
|
||||
Impls
|
||||
end,
|
||||
match_impls(Env, Decls, ConId, IName, UnmatchedImpls).
|
||||
|
||||
%% Asserts that the main contract is somehow defined.
|
||||
identify_main_contract(Contracts, Options) ->
|
||||
Children = [C || C = {contract_child, _, _, _} <- Contracts],
|
||||
Mains = [C || C = {contract_main, _, _, _} <- Contracts],
|
||||
Children = [C || C = {contract_child, _, _, _, _} <- Contracts],
|
||||
Mains = [C || C = {contract_main, _, _, _, _} <- Contracts],
|
||||
case Mains of
|
||||
[] -> case Children of
|
||||
[] -> type_error(
|
||||
{main_contract_undefined,
|
||||
[{file, File} || {src_file, File} <- Options]});
|
||||
[{contract_child, Ann, Con, Body}] ->
|
||||
(Contracts -- Children) ++ [{contract_main, Ann, Con, Body}];
|
||||
[{contract_child, Ann, Con, Impls, Body}] ->
|
||||
(Contracts -- Children) ++ [{contract_main, Ann, Con, Impls, Body}];
|
||||
[H|_] -> type_error({ambiguous_main_contract,
|
||||
aeso_syntax:get_ann(H)})
|
||||
end;
|
||||
@@ -1048,11 +1104,15 @@ check_typedef_sccs(Env, TypeMap, [{acyclic, Name} | SCCs], Acc) ->
|
||||
type_error({empty_record_definition, Ann, Name}),
|
||||
check_typedef_sccs(Env1, TypeMap, SCCs, Acc1);
|
||||
{record_t, Fields} ->
|
||||
ets_insert(type_vars_variance, {Env#env.namespace ++ qname(D),
|
||||
infer_type_vars_variance(Xs, Fields)}),
|
||||
%% check_type to get qualified name
|
||||
RecTy = check_type(Env1, app_t(Ann, D, Xs)),
|
||||
Env2 = check_fields(Env1, TypeMap, RecTy, Fields),
|
||||
check_typedef_sccs(Env2, TypeMap, SCCs, Acc1);
|
||||
{variant_t, Cons} ->
|
||||
ets_insert(type_vars_variance, {Env#env.namespace ++ qname(D),
|
||||
infer_type_vars_variance(Xs, Cons)}),
|
||||
Target = check_type(Env1, app_t(Ann, D, Xs)),
|
||||
ConType = fun([]) -> Target; (Args) -> {type_sig, Ann, none, [], Args, Target} end,
|
||||
ConTypes = [ begin
|
||||
@@ -1078,6 +1138,48 @@ check_typedef(Env, {variant_t, Cons}) ->
|
||||
{variant_t, [ {constr_t, Ann, Con, [ check_type(Env, Arg) || Arg <- Args ]}
|
||||
|| {constr_t, Ann, Con, Args} <- Cons ]}.
|
||||
|
||||
infer_type_vars_variance(TypeParams, Cons) ->
|
||||
% args from all type constructors
|
||||
FlatArgs = lists:flatten([Args || {constr_t, _, _, Args} <- Cons]) ++ [Type || {field_t, _, _, Type} <- Cons],
|
||||
|
||||
Vs = lists:flatten([infer_type_vars_variance(Arg) || Arg <- FlatArgs]),
|
||||
lists:map(fun({tvar, _, TVar}) ->
|
||||
S = sets:from_list([Variance || {TV, Variance} <- Vs, TV == TVar]),
|
||||
IsCovariant = sets:is_element(covariant, S),
|
||||
IsContravariant = sets:is_element(contravariant, S),
|
||||
case {IsCovariant, IsContravariant} of
|
||||
{true, true} -> invariant;
|
||||
{true, false} -> covariant;
|
||||
{false, true} -> contravariant;
|
||||
{false, false} -> bivariant
|
||||
end
|
||||
end, TypeParams).
|
||||
|
||||
-spec infer_type_vars_variance(utype()) -> [{name(), variance()}].
|
||||
infer_type_vars_variance(Types)
|
||||
when is_list(Types) ->
|
||||
lists:flatten([infer_type_vars_variance(T) || T <- Types]);
|
||||
infer_type_vars_variance({app_t, _, Type, Args}) ->
|
||||
Variances = case ets_lookup(type_vars_variance, qname(Type)) of
|
||||
[{_, Vs}] -> Vs;
|
||||
_ -> lists:duplicate(length(Args), covariant)
|
||||
end,
|
||||
TypeVarsVariance = [{TVar, Variance}
|
||||
|| {{tvar, _, TVar}, Variance} <- lists:zip(Args, Variances)],
|
||||
TypeVarsVariance;
|
||||
infer_type_vars_variance({tvar, _, TVar}) -> [{TVar, covariant}];
|
||||
infer_type_vars_variance({fun_t, _, [], Args, Res}) ->
|
||||
ArgsVariance = infer_type_vars_variance(Args),
|
||||
ResVariance = infer_type_vars_variance(Res),
|
||||
FlippedArgsVariance = lists:map(fun({TVar, Variance}) -> {TVar, opposite_variance(Variance)} end, ArgsVariance),
|
||||
FlippedArgsVariance ++ ResVariance;
|
||||
infer_type_vars_variance(_) -> [].
|
||||
|
||||
opposite_variance(invariant) -> invariant;
|
||||
opposite_variance(covariant) -> contravariant;
|
||||
opposite_variance(contravariant) -> covariant;
|
||||
opposite_variance(bivariant) -> bivariant.
|
||||
|
||||
check_usings(Env, []) ->
|
||||
Env;
|
||||
check_usings(Env = #env{ used_namespaces = UsedNamespaces }, [{using, Ann, Con, Alias, Parts} | Rest]) ->
|
||||
@@ -1123,7 +1225,7 @@ check_modifiers(Env, Contracts) ->
|
||||
check_modifiers_(Env, Contracts),
|
||||
destroy_and_report_type_errors(Env).
|
||||
|
||||
check_modifiers_(Env, [{Contract, _, Con, Decls} | Rest])
|
||||
check_modifiers_(Env, [{Contract, _, Con, _Impls, Decls} | Rest])
|
||||
when ?IS_CONTRACT_HEAD(Contract) ->
|
||||
IsInterface = Contract =:= contract_interface,
|
||||
check_modifiers1(contract, Decls),
|
||||
@@ -1186,14 +1288,6 @@ 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).
|
||||
@@ -1236,15 +1330,6 @@ 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}.
|
||||
@@ -1934,7 +2019,7 @@ infer_case(Env = #env{ namespace = NS, current_function = {id, _, Fun} }, Attrs,
|
||||
{guarded, Ann, NewGuards, NewBranch}
|
||||
end,
|
||||
NewGuardedBranches = lists:map(InferGuardedBranches, GuardedBranches),
|
||||
unify(Env, PatType, ExprType, {case_pat, Pattern, PatType, ExprType}),
|
||||
unify(Env, ExprType, PatType, {case_pat, Pattern, PatType, ExprType}),
|
||||
{'case', Attrs, NewPattern, NewGuardedBranches}.
|
||||
|
||||
%% NewStmts = infer_block(Env, Attrs, Stmts, BlockType)
|
||||
@@ -1969,16 +2054,10 @@ infer_infix({IntOp, As})
|
||||
Int = {id, As, "int"},
|
||||
{fun_t, As, [], [Int, Int], Int};
|
||||
infer_infix({RelOp, As})
|
||||
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 == '>';
|
||||
when RelOp == '=='; RelOp == '!=';
|
||||
RelOp == '<'; RelOp == '>';
|
||||
RelOp == '<='; RelOp == '=<'; RelOp == '>=' ->
|
||||
T = fresh_uvar(As),
|
||||
add_constraint({is_ord, T}),
|
||||
T = fresh_uvar(As), %% allow any type here, check in the backend that we have comparison for it
|
||||
Bool = {id, As, "bool"},
|
||||
{fun_t, As, [], [T, T], Bool};
|
||||
infer_infix({'..', As}) ->
|
||||
@@ -2049,7 +2128,7 @@ next_count() ->
|
||||
ets_tables() ->
|
||||
[options, type_vars, constraints, freshen_tvars, type_errors,
|
||||
defined_contracts, warnings, function_calls, all_functions,
|
||||
ord_constraint_types].
|
||||
type_vars_variance].
|
||||
|
||||
clean_up_ets() ->
|
||||
[ catch ets_delete(Tab) || Tab <- ets_tables() ],
|
||||
@@ -2211,16 +2290,11 @@ destroy_and_report_unsolved_constraints(Env) ->
|
||||
(#named_argument_constraint{}) -> true;
|
||||
(_) -> false
|
||||
end, OtherCs2),
|
||||
{BytesCs, OtherCs4} =
|
||||
{BytesCs, []} =
|
||||
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 ],
|
||||
@@ -2238,7 +2312,6 @@ 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().
|
||||
|
||||
@@ -2368,33 +2441,6 @@ 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;
|
||||
@@ -2622,9 +2668,11 @@ subst_tvars1(_Env, X) ->
|
||||
|
||||
%% Unification
|
||||
|
||||
unify(_, {id, _, "_"}, _, _When) -> true;
|
||||
unify(_, _, {id, _, "_"}, _When) -> true;
|
||||
unify(Env, A, B, When) ->
|
||||
unify(Env, A, B, When) -> unify0(Env, A, B, covariant, When).
|
||||
|
||||
unify0(_, {id, _, "_"}, _, _Variance, _When) -> true;
|
||||
unify0(_, _, {id, _, "_"}, _Variance, _When) -> true;
|
||||
unify0(Env, A, B, Variance, When) ->
|
||||
Options =
|
||||
case When of %% Improve source location for map_in_map_key errors
|
||||
{check_expr, E, _, _} -> [{ann, aeso_syntax:get_ann(E)}];
|
||||
@@ -2632,102 +2680,128 @@ unify(Env, A, B, When) ->
|
||||
end,
|
||||
A1 = dereference(unfold_types_in_type(Env, A, Options)),
|
||||
B1 = dereference(unfold_types_in_type(Env, B, Options)),
|
||||
unify1(Env, A1, B1, When).
|
||||
unify1(Env, A1, B1, Variance, When).
|
||||
|
||||
unify1(_Env, {uvar, _, R}, {uvar, _, R}, _When) ->
|
||||
unify1(_Env, {uvar, _, R}, {uvar, _, R}, _Variance, _When) ->
|
||||
true;
|
||||
unify1(_Env, {uvar, A, R}, T, When) ->
|
||||
unify1(Env, {uvar, A, R}, T, _Variance, When) ->
|
||||
case occurs_check(R, T) of
|
||||
true ->
|
||||
cannot_unify({uvar, A, R}, T, When),
|
||||
if
|
||||
Env#env.unify_throws ->
|
||||
cannot_unify({uvar, A, R}, T, none, When);
|
||||
true ->
|
||||
ok
|
||||
end,
|
||||
false;
|
||||
false ->
|
||||
ets_insert(type_vars, {R, T}),
|
||||
true
|
||||
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) ->
|
||||
unify1(Env, T, {uvar, A, R}, Variance, When) ->
|
||||
unify1(Env, {uvar, A, R}, T, Variance, When);
|
||||
unify1(_Env, {tvar, _, X}, {tvar, _, X}, _Variance, _When) -> true; %% Rigid type variables
|
||||
unify1(Env, [A|B], [C|D], [V|Variances], When) ->
|
||||
unify0(Env, A, C, V, When) andalso unify0(Env, B, D, Variances, When);
|
||||
unify1(Env, [A|B], [C|D], Variance, When) ->
|
||||
unify0(Env, A, C, Variance, When) andalso unify0(Env, B, D, Variance, When);
|
||||
unify1(_Env, X, X, _Variance, _When) ->
|
||||
true;
|
||||
unify1(_Env, {id, _, Name}, {id, _, Name}, _When) ->
|
||||
unify1(_Env, {id, _, Name}, {id, _, Name}, _Variance, _When) ->
|
||||
true;
|
||||
unify1(_Env, {con, _, Name}, {con, _, Name}, _When) ->
|
||||
unify1(Env, A = {con, _, NameA}, B = {con, _, NameB}, Variance, When) ->
|
||||
case is_subtype(Env, NameA, NameB, Variance) of
|
||||
true -> true;
|
||||
false ->
|
||||
if
|
||||
Env#env.unify_throws ->
|
||||
IsSubtype = is_subtype(Env, NameA, NameB, contravariant) orelse
|
||||
is_subtype(Env, NameA, NameB, covariant),
|
||||
Cxt = case IsSubtype of
|
||||
true -> Variance;
|
||||
false -> none
|
||||
end,
|
||||
cannot_unify(A, B, Cxt, When);
|
||||
true ->
|
||||
ok
|
||||
end,
|
||||
false
|
||||
end;
|
||||
unify1(_Env, {qid, _, Name}, {qid, _, Name}, _Variance, _When) ->
|
||||
true;
|
||||
unify1(_Env, {qid, _, Name}, {qid, _, Name}, _When) ->
|
||||
unify1(_Env, {qcon, _, Name}, {qcon, _, Name}, _Variance, _When) ->
|
||||
true;
|
||||
unify1(_Env, {qcon, _, Name}, {qcon, _, Name}, _When) ->
|
||||
unify1(_Env, {bytes_t, _, Len}, {bytes_t, _, Len}, _Variance, _When) ->
|
||||
true;
|
||||
unify1(_Env, {bytes_t, _, Len}, {bytes_t, _, Len}, _When) ->
|
||||
true;
|
||||
unify1(Env, {if_t, _, {id, _, Id}, Then1, Else1}, {if_t, _, {id, _, Id}, Then2, Else2}, When) ->
|
||||
unify(Env, Then1, Then2, When) andalso
|
||||
unify(Env, Else1, Else2, When);
|
||||
unify1(Env, {if_t, _, {id, _, Id}, Then1, Else1}, {if_t, _, {id, _, Id}, Then2, Else2}, Variance, When) ->
|
||||
unify0(Env, Then1, Then2, Variance, When) andalso
|
||||
unify0(Env, Else1, Else2, Variance, When);
|
||||
|
||||
unify1(_Env, {fun_t, _, _, _, _}, {fun_t, _, _, var_args, _}, When) ->
|
||||
unify1(_Env, {fun_t, _, _, _, _}, {fun_t, _, _, var_args, _}, _Variance, When) ->
|
||||
type_error({unify_varargs, When});
|
||||
unify1(_Env, {fun_t, _, _, var_args, _}, {fun_t, _, _, _, _}, When) ->
|
||||
unify1(_Env, {fun_t, _, _, var_args, _}, {fun_t, _, _, _, _}, _Variance, When) ->
|
||||
type_error({unify_varargs, When});
|
||||
unify1(Env, {fun_t, _, Named1, Args1, Result1}, {fun_t, _, Named2, Args2, Result2}, When)
|
||||
unify1(Env, {fun_t, _, Named1, Args1, Result1}, {fun_t, _, Named2, Args2, Result2}, Variance, When)
|
||||
when length(Args1) == length(Args2) ->
|
||||
unify(Env, Named1, Named2, When) andalso
|
||||
unify(Env, Args1, Args2, When) andalso unify(Env, Result1, Result2, When);
|
||||
unify1(Env, {app_t, _, {Tag, _, F}, Args1}, {app_t, _, {Tag, _, F}, Args2}, When)
|
||||
unify0(Env, Named1, Named2, opposite_variance(Variance), When) andalso
|
||||
unify0(Env, Args1, Args2, opposite_variance(Variance), When) andalso
|
||||
unify0(Env, Result1, Result2, Variance, When);
|
||||
unify1(Env, {app_t, _, {Tag, _, F}, Args1}, {app_t, _, {Tag, _, F}, Args2}, Variance, When)
|
||||
when length(Args1) == length(Args2), Tag == id orelse Tag == qid ->
|
||||
unify(Env, Args1, Args2, When);
|
||||
unify1(Env, {tuple_t, _, As}, {tuple_t, _, Bs}, When)
|
||||
Variances = case ets_lookup(type_vars_variance, F) of
|
||||
[{_, Vs}] ->
|
||||
case Variance of
|
||||
contravariant -> lists:map(fun opposite_variance/1, Vs);
|
||||
invariant -> invariant;
|
||||
_ -> Vs
|
||||
end;
|
||||
_ -> invariant
|
||||
end,
|
||||
unify1(Env, Args1, Args2, Variances, When);
|
||||
unify1(Env, {tuple_t, _, As}, {tuple_t, _, Bs}, Variance, When)
|
||||
when length(As) == length(Bs) ->
|
||||
unify(Env, As, 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);
|
||||
unify0(Env, As, Bs, Variance, When);
|
||||
unify1(Env, {named_arg_t, _, Id1, Type1, _}, {named_arg_t, _, Id2, Type2, _}, Variance, When) ->
|
||||
unify1(Env, Id1, Id2, Variance, {arg_name, Id1, Id2, When}),
|
||||
unify1(Env, Type1, Type2, Variance, 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.
|
||||
unify1(Env, {app_t, _, T, []}, B, When) ->
|
||||
unify(Env, T, B, When);
|
||||
unify1(Env, A, {app_t, _, T, []}, When) ->
|
||||
unify(Env, A, T, When);
|
||||
unify1(_Env, A, B, When) ->
|
||||
cannot_unify(A, B, When),
|
||||
unify1(Env, {app_t, _, T, []}, B, Variance, When) ->
|
||||
unify0(Env, T, B, Variance, When);
|
||||
unify1(Env, A, {app_t, _, T, []}, Variance, When) ->
|
||||
unify0(Env, A, T, Variance, When);
|
||||
unify1(Env, A, B, _Variance, When) ->
|
||||
if
|
||||
Env#env.unify_throws ->
|
||||
cannot_unify(A, B, none, When);
|
||||
true ->
|
||||
ok
|
||||
end,
|
||||
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.
|
||||
is_subtype(_Env, NameA, NameB, invariant) ->
|
||||
NameA == NameB;
|
||||
is_subtype(Env, NameA, NameB, covariant) ->
|
||||
is_subtype(Env, NameA, NameB);
|
||||
is_subtype(Env, NameA, NameB, contravariant) ->
|
||||
is_subtype(Env, NameB, NameA);
|
||||
is_subtype(Env, NameA, NameB, bivariant) ->
|
||||
is_subtype(Env, NameA, NameB) orelse is_subtype(Env, NameB, NameA).
|
||||
|
||||
is_subtype(Env, Child, Base) ->
|
||||
Parents = maps:get(Child, Env#env.contract_parents, []),
|
||||
if
|
||||
Child == Base ->
|
||||
true;
|
||||
Parents == [] ->
|
||||
false;
|
||||
true ->
|
||||
case lists:member(Base, Parents) of
|
||||
true -> true;
|
||||
false -> lists:any(fun(Parent) -> is_subtype(Env, Parent, Base) end, Parents)
|
||||
end
|
||||
end.
|
||||
|
||||
dereference(T = {uvar, _, R}) ->
|
||||
case ets_lookup(type_vars, R) of
|
||||
@@ -2756,7 +2830,6 @@ 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]);
|
||||
@@ -2873,8 +2946,7 @@ all_warnings() ->
|
||||
, warn_unused_functions
|
||||
, warn_shadowing
|
||||
, warn_division_by_zero
|
||||
, warn_negative_spend
|
||||
, warn_duplicated_constraints ].
|
||||
, warn_negative_spend ].
|
||||
|
||||
when_warning(Warn, Do) ->
|
||||
case lists:member(Warn, all_warnings()) of
|
||||
@@ -3011,23 +3083,10 @@ 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) ->
|
||||
type_error({cannot_unify, A, B, When}).
|
||||
cannot_unify(A, B, Cxt, When) ->
|
||||
type_error({cannot_unify, A, B, Cxt, When}).
|
||||
|
||||
type_error(Err) ->
|
||||
ets_insert(type_errors, Err).
|
||||
@@ -3096,8 +3155,12 @@ mk_error({fundecl_must_have_funtype, _Ann, Id, Type}) ->
|
||||
"Entrypoints and functions must have functional types"
|
||||
, [pp(Id), pp(instantiate(Type))]),
|
||||
mk_t_err(pos(Id), Msg);
|
||||
mk_error({cannot_unify, A, B, When}) ->
|
||||
Msg = io_lib:format("Cannot unify `~s` and `~s`",
|
||||
mk_error({cannot_unify, A, B, Cxt, When}) ->
|
||||
VarianceContext = case Cxt of
|
||||
none -> "";
|
||||
_ -> io_lib:format(" in a ~p context", [Cxt])
|
||||
end,
|
||||
Msg = io_lib:format("Cannot unify `~s` and `~s`" ++ VarianceContext,
|
||||
[pp(instantiate(A)), pp(instantiate(B))]),
|
||||
{Pos, Ctxt} = pp_when(When),
|
||||
mk_t_err(Pos, Msg, Ctxt);
|
||||
@@ -3228,7 +3291,7 @@ mk_error({namespace, _Pos, {con, Pos, Name}, _Def}) ->
|
||||
Msg = io_lib:format("Nested namespaces are not allowed. Namespace `~s` is not defined at top level.",
|
||||
[Name]),
|
||||
mk_t_err(pos(Pos), Msg);
|
||||
mk_error({Contract, _Pos, {con, Pos, Name}, _Def}) when ?IS_CONTRACT_HEAD(Contract) ->
|
||||
mk_error({Contract, _Pos, {con, Pos, Name}, _Impls, _Def}) when ?IS_CONTRACT_HEAD(Contract) ->
|
||||
Msg = io_lib:format("Nested contracts are not allowed. Contract `~s` is not defined at top level.",
|
||||
[Name]),
|
||||
mk_t_err(pos(Pos), Msg);
|
||||
@@ -3415,18 +3478,12 @@ 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({unimplemented_interface_function, ConId, InterfaceName, FunName}) ->
|
||||
Msg = io_lib:format("Unimplemented function `~s` from the interface `~s` in the contract `~s`", [FunName, InterfaceName, pp(ConId)]),
|
||||
mk_t_err(pos(ConId), Msg);
|
||||
mk_error({referencing_undefined_interface, InterfaceId}) ->
|
||||
Msg = io_lib:format("Trying to implement or extend an undefined interface `~s`", [pp(InterfaceId)]),
|
||||
mk_t_err(pos(InterfaceId), Msg);
|
||||
mk_error(Err) ->
|
||||
Msg = io_lib:format("Unknown error: ~p", [Err]),
|
||||
mk_t_err(pos(0, 0), Msg).
|
||||
@@ -3458,10 +3515,6 @@ 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).
|
||||
@@ -3686,8 +3739,6 @@ 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, _, []}) ->
|
||||
|
||||
@@ -75,6 +75,7 @@
|
||||
| {switch, fsplit()}
|
||||
| {set_state, state_reg(), fexpr()}
|
||||
| {get_state, state_reg()}
|
||||
| {loop, fexpr(), var_name(), fexpr()} | {continue, fexpr()} | {break, fexpr()}
|
||||
%% The following (unapplied top-level functions/builtins and
|
||||
%% lambdas) are generated by the fcode compiler, but translated
|
||||
%% to closures by the lambda lifter.
|
||||
@@ -326,7 +327,7 @@ get_option(Opt, Env, Default) ->
|
||||
%% -- Compilation ------------------------------------------------------------
|
||||
|
||||
-spec to_fcode(env(), aeso_syntax:ast()) -> {env(), fcode()}.
|
||||
to_fcode(Env, [{Contract, Attrs, Con = {con, _, Name}, Decls}|Rest])
|
||||
to_fcode(Env, [{Contract, Attrs, Con = {con, _, Name}, _Impls, Decls}|Rest])
|
||||
when ?IS_CONTRACT_HEAD(Contract) ->
|
||||
case Contract =:= contract_interface of
|
||||
false ->
|
||||
@@ -495,8 +496,6 @@ 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}) ->
|
||||
@@ -653,11 +652,22 @@ expr_to_fcode(Env, {record_t, FieldTypes}, {record, _Ann, Rec, Fields}) ->
|
||||
expr_to_fcode(Env, _Type, {list, _, Es}) ->
|
||||
lists:foldr(fun(E, L) -> {op, '::', [expr_to_fcode(Env, E), L]} end,
|
||||
nil, Es);
|
||||
|
||||
expr_to_fcode(Env, _Type, {app, _, {'..', _}, [A, B]}) ->
|
||||
{def_u, FromTo, _} = resolve_fun(Env, ["ListInternal", "from_to"]),
|
||||
{def, FromTo, [expr_to_fcode(Env, A), expr_to_fcode(Env, B)]};
|
||||
|
||||
AV = fresh_name(), % var to keep B
|
||||
WithA = fun(X) -> {'let', AV, expr_to_fcode(Env, A), X} end,
|
||||
St = fresh_name(), % loop state
|
||||
ItProj = {proj, {var, St}, 1},
|
||||
AcProj = {proj, {var, St}, 0},
|
||||
Init = {tuple, [nil, expr_to_fcode(Env, B)]},
|
||||
Loop = {loop, Init, St,
|
||||
make_if(
|
||||
{op, '>=', [ItProj, {var, AV}]},
|
||||
{continue, {tuple, [{op, '::', [ItProj, AcProj]},
|
||||
{op, '-', [ItProj, {lit, {int, 1}}]}
|
||||
]}},
|
||||
{break, AcProj}
|
||||
)},
|
||||
WithA(Loop);
|
||||
expr_to_fcode(Env, _Type, {list_comp, _, Yield, []}) ->
|
||||
{op, '::', [expr_to_fcode(Env, Yield), nil]};
|
||||
expr_to_fcode(Env, _Type, {list_comp, As, Yield, [{comprehension_bind, Pat = {typed, _, _, PatType}, BindExpr}|Rest]}) ->
|
||||
@@ -1340,6 +1350,9 @@ lambda_lift_expr(Layout, Expr) ->
|
||||
{proj, A, I} -> {proj, lambda_lift_expr(Layout, A), I};
|
||||
{set_proj, A, I, B} -> {set_proj, lambda_lift_expr(Layout, A), I, lambda_lift_expr(Layout, B)};
|
||||
{op, Op, As} -> {op, Op, lambda_lift_exprs(Layout, As)};
|
||||
{loop, Init, I, Body} -> {loop, lambda_lift_expr(Layout, Init), I, lambda_lift_expr(Layout, Body)};
|
||||
{break, E} -> {break, lambda_lift_expr(Layout, E)};
|
||||
{continue, E} -> {continue, lambda_lift_expr(Layout, E)};
|
||||
{'let', X, A, B} -> {'let', X, lambda_lift_expr(Layout, A), lambda_lift_expr(Layout, B)};
|
||||
{funcall, A, Bs} -> {funcall, lambda_lift_expr(Layout, A), lambda_lift_exprs(Layout, Bs)};
|
||||
{set_state, R, A} -> {set_state, R, lambda_lift_expr(Layout, A)};
|
||||
@@ -1655,6 +1668,9 @@ read_only({switch, Split}) -> read_only(Split);
|
||||
read_only({split, _, _, Cases}) -> read_only(Cases);
|
||||
read_only({nosplit, E}) -> read_only(E);
|
||||
read_only({'case', _, Split}) -> read_only(Split);
|
||||
read_only({loop, Init, _, Body}) -> read_only(Init) andalso read_only(Body);
|
||||
read_only({break, E}) -> read_only(E);
|
||||
read_only({continue, E}) -> read_only(E);
|
||||
read_only({'let', _, A, B}) -> read_only([A, B]);
|
||||
read_only({funcall, _, _}) -> false;
|
||||
read_only({closure, _, _}) -> internal_error(no_closures_here);
|
||||
@@ -1852,6 +1868,9 @@ free_vars(Expr) ->
|
||||
{proj, A, _} -> free_vars(A);
|
||||
{set_proj, A, _, B} -> free_vars([A, B]);
|
||||
{op, _, As} -> free_vars(As);
|
||||
{loop, Init, Var, Body} -> free_vars(Init) ++ (free_vars(Body) -- [Var]);
|
||||
{break, E} -> free_vars(E);
|
||||
{continue, E} -> free_vars(E);
|
||||
{'let', X, A, B} -> free_vars([A, {lam, [X], B}]);
|
||||
{funcall, A, Bs} -> free_vars([A | Bs]);
|
||||
{set_state, _, A} -> free_vars(A);
|
||||
@@ -1883,6 +1902,9 @@ used_defs(Expr) ->
|
||||
{proj, A, _} -> used_defs(A);
|
||||
{set_proj, A, _, B} -> used_defs([A, B]);
|
||||
{op, _, As} -> used_defs(As);
|
||||
{loop, I, _, B} -> used_defs(I) ++ used_defs(B);
|
||||
{break, E} -> used_defs(E);
|
||||
{continue, E} -> used_defs(E);
|
||||
{'let', _, A, B} -> used_defs([A, B]);
|
||||
{funcall, A, Bs} -> used_defs([A | Bs]);
|
||||
{set_state, _, A} -> used_defs(A);
|
||||
@@ -1919,6 +1941,9 @@ bottom_up(F, Env, Expr) ->
|
||||
{get_state, _} -> Expr;
|
||||
{closure, F, CEnv} -> {closure, F, bottom_up(F, Env, CEnv)};
|
||||
{switch, Split} -> {switch, bottom_up(F, Env, Split)};
|
||||
{loop, Init, Var, Body} -> {loop, bottom_up(F, Env, Init), Var, bottom_up(F, Env, Body)};
|
||||
{break, E} -> {break, bottom_up(F, Env, E)};
|
||||
{continue, E} -> {continue, bottom_up(F, Env, E)};
|
||||
{lam, Xs, B} -> {lam, Xs, bottom_up(F, Env, B)};
|
||||
{'let', X, E, Body} ->
|
||||
E1 = bottom_up(F, Env, E),
|
||||
@@ -1980,6 +2005,11 @@ rename(Ren, Expr) ->
|
||||
{lam, Xs, B} ->
|
||||
{Zs, Ren1} = rename_bindings(Ren, Xs),
|
||||
{lam, Zs, rename(Ren1, B)};
|
||||
{loop, Init, Var, Body} ->
|
||||
{Z, Ren1} = rename_binding(Ren, Var),
|
||||
{loop, rename(Ren, Init), Z, rename(Ren1, Body)};
|
||||
{break, E} -> {break, rename(Ren, E)};
|
||||
{continue, E} -> {continue, rename(Ren, E)};
|
||||
{'let', X, E, Body} ->
|
||||
{Z, Ren1} = rename_binding(Ren, X),
|
||||
{'let', Z, rename(Ren, E), rename(Ren1, Body)}
|
||||
@@ -2171,6 +2201,13 @@ pp_fexpr({tuple, Es}) ->
|
||||
pp_parens(pp_par(pp_punctuate(pp_text(","), [pp_fexpr(E) || E <- Es])));
|
||||
pp_fexpr({proj, E, I}) ->
|
||||
pp_beside([pp_fexpr(E), pp_text("."), pp_int(I)]);
|
||||
pp_fexpr({loop, Init, Var, Body}) ->
|
||||
pp_par(
|
||||
[ pp_beside([pp_text("loop"), pp_fexpr(Init), pp_text("as"), pp_text(Var)])
|
||||
, pp_fexpr(Body)
|
||||
]);
|
||||
pp_fexpr({break, E}) -> pp_beside([pp_text("break"), pp_fexpr(E)]);
|
||||
pp_fexpr({continue, E}) -> pp_beside([pp_text("continue"), pp_fexpr(E)]);
|
||||
pp_fexpr({lam, Xs, A}) ->
|
||||
pp_par([pp_fexpr({tuple, [{var, X} || X <- Xs]}), pp_text("=>"),
|
||||
prettypr:nest(2, pp_fexpr(A))]);
|
||||
|
||||
@@ -238,8 +238,8 @@ insert_init_function(Code, Options) ->
|
||||
|
||||
last_contract_indent(Decls) ->
|
||||
case lists:last(Decls) of
|
||||
{_, _, _, [Decl | _]} -> aeso_syntax:get_ann(col, Decl, 1) - 1;
|
||||
_ -> 0
|
||||
{_, _, _, _, [Decl | _]} -> aeso_syntax:get_ann(col, Decl, 1) - 1;
|
||||
_ -> 0
|
||||
end.
|
||||
|
||||
-spec to_sophia_value(string(), string(), ok | error | revert, binary()) ->
|
||||
@@ -338,7 +338,7 @@ decode_calldata(ContractString, FunName, Calldata, Options0) ->
|
||||
end.
|
||||
|
||||
-dialyzer({nowarn_function, get_decode_type/2}).
|
||||
get_decode_type(FunName, [{Contract, Ann, _, Defs}]) when ?IS_CONTRACT_HEAD(Contract) ->
|
||||
get_decode_type(FunName, [{Contract, Ann, _, _, Defs}]) when ?IS_CONTRACT_HEAD(Contract) ->
|
||||
GetType = fun({letfun, _, {id, _, Name}, Args, Ret, _}) when Name == FunName -> [{Args, Ret}];
|
||||
({fun_decl, _, {id, _, Name}, {fun_t, _, _, Args, Ret}}) when Name == FunName -> [{Args, Ret}];
|
||||
(_) -> [] end,
|
||||
|
||||
+66
-13
@@ -19,6 +19,7 @@
|
||||
|
||||
-type scode() :: [sinstr()].
|
||||
-type sinstr() :: {switch, arg(), stype(), [maybe_scode()], maybe_scode()} %% last arg is catch-all
|
||||
| {loop, scode(), var(), scode(), reference(), reference()}
|
||||
| switch_body
|
||||
| loop
|
||||
| tuple() | atom(). %% FATE instruction
|
||||
@@ -45,7 +46,7 @@
|
||||
-define(s(N), {store, N}).
|
||||
-define(void, {var, 9999}).
|
||||
|
||||
-record(env, { contract, vars = [], locals = [], current_function, tailpos = true, child_contracts = #{}, options = []}).
|
||||
-record(env, { contract, vars = [], locals = [], break_ref = none, cont_ref = none, loop_it = none, current_function, tailpos = true, child_contracts = #{}, options = []}).
|
||||
|
||||
%% -- Debugging --------------------------------------------------------------
|
||||
|
||||
@@ -159,6 +160,9 @@ init_env(ChildContracts, ContractName, FunNames, Name, Args, Options) ->
|
||||
next_var(#env{ vars = Vars }) ->
|
||||
1 + lists:max([-1 | [J || {_, {var, J}} <- Vars]]).
|
||||
|
||||
bind_loop(ContRef, BreakRef, It, Env) ->
|
||||
Env#env{break_ref = BreakRef, cont_ref = ContRef, loop_it = It}.
|
||||
|
||||
bind_var(Name, Var, Env = #env{ vars = Vars }) ->
|
||||
Env#env{ vars = [{Name, Var} | Vars] }.
|
||||
|
||||
@@ -368,7 +372,21 @@ to_scode1(Env, {set_state, Reg, Val}) ->
|
||||
|
||||
to_scode1(Env, {closure, Fun, FVs}) ->
|
||||
to_scode(Env, {tuple, [{lit, {string, make_function_id(Fun)}}, FVs]});
|
||||
|
||||
to_scode1(Env, {loop, Init, It, Expr}) ->
|
||||
ContRef = make_ref(),
|
||||
BreakRef = make_ref(),
|
||||
{ItV, Env1} = bind_local(It, Env),
|
||||
InitS = [to_scode(notail(Env), Init),
|
||||
{jump, ContRef}],
|
||||
ExprS = [aeb_fate_ops:store({var, ItV}, {stack, 0}),
|
||||
to_scode(bind_loop(ContRef, BreakRef, ItV, Env1), Expr),
|
||||
{jump, BreakRef}],
|
||||
[{loop, InitS, It, ExprS, ContRef, BreakRef}];
|
||||
to_scode1(Env = #env{cont_ref = ContRef}, {continue, Expr}) ->
|
||||
[to_scode1(notail(Env), Expr),
|
||||
{jump, ContRef}];
|
||||
to_scode1(Env, {break, Expr}) ->
|
||||
to_scode1(Env, Expr);
|
||||
to_scode1(Env, {switch, Case}) ->
|
||||
split_to_scode(Env, Case).
|
||||
|
||||
@@ -712,6 +730,8 @@ flatten(Code) -> lists:map(fun flatten_s/1, lists:flatten(Code)).
|
||||
|
||||
flatten_s({switch, Arg, Type, Alts, Catch}) ->
|
||||
{switch, Arg, Type, [flatten(Alt) || Alt <- Alts], flatten(Catch)};
|
||||
flatten_s({loop, Init, It, Body, BRef, CRef}) ->
|
||||
{loop, flatten(Init), It, flatten(Body), BRef, CRef};
|
||||
flatten_s(I) -> I.
|
||||
|
||||
-define(MAX_SIMPL_ITERATIONS, 10).
|
||||
@@ -808,6 +828,11 @@ ann_live1(LiveTop, {switch, Arg, Type, Alts, Def}, LiveOut) ->
|
||||
{Def1, LiveDef} = ann_live(LiveTop, Def, LiveOut),
|
||||
LiveIn = ordsets:union([Read, LiveDef | LiveAlts]),
|
||||
{{switch, Arg, Type, Alts1, Def1}, LiveIn};
|
||||
ann_live1(LiveTop, {loop, Init, It, Body, BRef, CRef}, LiveOut) ->
|
||||
{Init1, LiveInit} = ann_live(LiveTop, Init, LiveOut),
|
||||
{Body1, LiveBody} = ann_live(LiveTop, Body, LiveOut),
|
||||
LiveIn = ordsets:union([It, LiveInit, LiveBody]), % TODO not sure about this
|
||||
{{loop, Init1, It, Body1, BRef, CRef}, LiveIn};
|
||||
ann_live1(_LiveTop, I, LiveOut) ->
|
||||
#{ read := Reads0, write := W } = attributes(I),
|
||||
Reads = lists:filter(fun is_reg/1, Reads0),
|
||||
@@ -834,6 +859,7 @@ attributes(I) ->
|
||||
case I of
|
||||
loop -> Impure(pc, []);
|
||||
switch_body -> Pure(none, []);
|
||||
{jump, _} -> Impure(pc, []);
|
||||
'RETURN' -> Impure(pc, []);
|
||||
{'RETURNR', A} -> Impure(pc, A);
|
||||
{'CALL', A} -> Impure(?a, [A]);
|
||||
@@ -1023,6 +1049,7 @@ var_writes(I) ->
|
||||
-spec independent(sinstr_a(), sinstr_a()) -> boolean().
|
||||
%% independent({switch, _, _, _, _}, _) -> false; %% Commented due to Dialyzer whinging
|
||||
independent(_, {switch, _, _, _, _}) -> false;
|
||||
independent(_, {loop, _, _, _, _, _}) -> false;
|
||||
independent({i, _, I}, {i, _, J}) ->
|
||||
#{ write := WI, read := RI, pure := PureI } = attributes(I),
|
||||
#{ write := WJ, read := RJ, pure := PureJ } = attributes(J),
|
||||
@@ -1061,6 +1088,8 @@ live_in(R, {i, Ann, _}) -> live_in(R, Ann);
|
||||
live_in(R, [I = {i, _, _} | _]) -> live_in(R, I);
|
||||
live_in(R, [{switch, A, _, Alts, Def} | _]) ->
|
||||
R == A orelse lists:any(fun(Code) -> live_in(R, Code) end, [Def | Alts]);
|
||||
live_in(R, [{loop, Init, Var, Expr, _, _}]) ->
|
||||
live_in(Var, Init) orelse (R /= Var andalso live_in(R, Expr));
|
||||
live_in(_, missing) -> false;
|
||||
live_in(_, []) -> false.
|
||||
|
||||
@@ -1076,6 +1105,8 @@ simplify([I | Code], Options) ->
|
||||
|
||||
simpl_s({switch, Arg, Type, Alts, Def}, Options) ->
|
||||
{switch, Arg, Type, [simplify(A, Options) || A <- Alts], simplify(Def, Options)};
|
||||
simpl_s({loop, Init, Var, Expr, ContRef, BreakRef}, Options) ->
|
||||
{loop, simplify(Init, Options), Var, simplify(Expr, Options), ContRef, BreakRef};
|
||||
simpl_s(I, _) -> I.
|
||||
|
||||
%% Safe-guard against loops in the rewriting. Shouldn't happen so throw an
|
||||
@@ -1378,6 +1409,8 @@ does_abort({i, _, {'EXIT', _}}) -> true;
|
||||
does_abort(missing) -> true;
|
||||
does_abort({switch, _, _, Alts, Def}) ->
|
||||
lists:all(fun does_abort/1, [Def | Alts]);
|
||||
does_abort({loop, Init, _, Expr, _, _}) ->
|
||||
does_abort(Init) orelse does_abort(Expr);
|
||||
does_abort(_) -> false.
|
||||
|
||||
%% STORE R A, SWITCH R --> SWITCH A
|
||||
@@ -1505,6 +1538,8 @@ from_op_view(Op, R, As) -> list_to_tuple([Op, R | As]).
|
||||
(missing) -> missing.
|
||||
unannotate({switch, Arg, Type, Alts, Def}) ->
|
||||
[{switch, Arg, Type, [unannotate(A) || A <- Alts], unannotate(Def)}];
|
||||
unannotate({loop, Init, It, Body, BRef, CRef}) ->
|
||||
[{loop, unannotate(Init), It, unannotate(Body), BRef, CRef}];
|
||||
unannotate(missing) -> missing;
|
||||
unannotate(Code) when is_list(Code) ->
|
||||
lists:flatmap(fun unannotate/1, Code);
|
||||
@@ -1521,6 +1556,8 @@ desugar({'STORE', ?a, A}) -> [aeb_fate_ops:push(desugar_arg(A))];
|
||||
desugar({'STORE', R, ?a}) -> [aeb_fate_ops:pop(desugar_arg(R))];
|
||||
desugar({switch, Arg, Type, Alts, Def}) ->
|
||||
[{switch, desugar_arg(Arg), Type, [desugar(A) || A <- Alts], desugar(Def)}];
|
||||
desugar({loop, Init, Var, Expr, ContRef, BreakRef}) ->
|
||||
[{loop, desugar(Init), Var, desugar(Expr), ContRef, BreakRef}];
|
||||
desugar(missing) -> missing;
|
||||
desugar(Code) when is_list(Code) ->
|
||||
lists:flatmap(fun desugar/1, Code);
|
||||
@@ -1567,7 +1604,7 @@ bb(_Name, Code) ->
|
||||
-type bb() :: {bbref(), bcode()}.
|
||||
-type bcode() :: [binstr()].
|
||||
-type binstr() :: {jump, bbref()}
|
||||
| {jumpif, bbref()}
|
||||
| {jumpif, term(), bbref()}
|
||||
| tuple(). %% FATE instruction
|
||||
|
||||
-spec blocks(scode()) -> [bb()].
|
||||
@@ -1581,25 +1618,29 @@ blocks([], Acc) ->
|
||||
blocks([Blk | Blocks], Acc) ->
|
||||
block(Blk, [], Blocks, Acc).
|
||||
|
||||
fresh_block(C, Ca) ->
|
||||
R = make_ref(),
|
||||
{R, [#blk{ref = R, code = C, catchall = Ca}]}.
|
||||
|
||||
-spec block(#blk{}, bcode(), [#blk{}], [bb()]) -> [bb()].
|
||||
block(#blk{ref = Ref, code = []}, CodeAcc, Blocks, BlockAcc) ->
|
||||
blocks(Blocks, [{Ref, lists:reverse(CodeAcc)} | BlockAcc]);
|
||||
block(Blk = #blk{code = [{loop, Init, _, Expr, ContRef, BreakRef} | Code], catchall = Catchall}, Acc, Blocks, BlockAcc) ->
|
||||
LoopBlock = #blk{ref = ContRef, code = Expr, catchall = none},
|
||||
BreakBlock = #blk{ref = BreakRef, code = Code, catchall = Catchall},
|
||||
block(Blk#blk{code = Init}, Acc, [LoopBlock, BreakBlock | Blocks], BlockAcc);
|
||||
block(Blk = #blk{code = [switch_body | Code]}, Acc, Blocks, BlockAcc) ->
|
||||
%% Reached the body of a switch. Clear catchall ref.
|
||||
block(Blk#blk{code = Code, catchall = none}, Acc, Blocks, BlockAcc);
|
||||
block(Blk = #blk{code = [{switch, Arg, Type, Alts, Default} | Code],
|
||||
catchall = Catchall}, Acc, Blocks, BlockAcc) ->
|
||||
FreshBlk = fun(C, Ca) ->
|
||||
R = make_ref(),
|
||||
{R, [#blk{ref = R, code = C, catchall = Ca}]}
|
||||
end,
|
||||
{RestRef, RestBlk} = FreshBlk(Code, Catchall),
|
||||
{RestRef, RestBlk} = fresh_block(Code, Catchall),
|
||||
{DefRef, DefBlk} =
|
||||
case Default of
|
||||
missing when Catchall == none ->
|
||||
FreshBlk([aeb_fate_ops:abort(?i(<<"Incomplete patterns">>))], none);
|
||||
fresh_block([aeb_fate_ops:abort(?i(<<"Incomplete patterns">>))], none);
|
||||
missing -> {Catchall, []};
|
||||
_ -> FreshBlk(Default ++ [{jump, RestRef}], Catchall)
|
||||
_ -> fresh_block(Default ++ [{jump, RestRef}], Catchall)
|
||||
%% ^ fall-through to the outer catchall
|
||||
end,
|
||||
%% If we don't generate a switch, we need to pop the argument if on the stack.
|
||||
@@ -1611,7 +1652,7 @@ block(Blk = #blk{code = [{switch, Arg, Type, Alts, Default} | Code],
|
||||
{ThenRef, ThenBlk} =
|
||||
case TrueCode of
|
||||
missing -> {DefRef, []};
|
||||
_ -> FreshBlk(TrueCode ++ [{jump, RestRef}], DefRef)
|
||||
_ -> fresh_block(TrueCode ++ [{jump, RestRef}], DefRef)
|
||||
end,
|
||||
ElseCode =
|
||||
case FalseCode of
|
||||
@@ -1646,7 +1687,7 @@ block(Blk = #blk{code = [{switch, Arg, Type, Alts, Default} | Code],
|
||||
true -> {Blk#blk{code = Pop ++ [{jump, DefRef}]}, [], []};
|
||||
false ->
|
||||
MkBlk = fun(missing) -> {DefRef, []};
|
||||
(ACode) -> FreshBlk(ACode ++ [{jump, RestRef}], DefRef)
|
||||
(ACode) -> fresh_block(ACode ++ [{jump, RestRef}], DefRef)
|
||||
end,
|
||||
{AltRefs, AltBs} = lists:unzip(lists:map(MkBlk, Alts)),
|
||||
{Blk#blk{code = []}, [{switch, Arg, AltRefs}], lists:append(AltBs)}
|
||||
@@ -1662,7 +1703,7 @@ block(Blk = #blk{code = [I | Code]}, Acc, Blocks, BlockAcc) ->
|
||||
optimize_blocks(Blocks) ->
|
||||
%% We need to look at the last instruction a lot, so reverse all blocks.
|
||||
Rev = fun(Bs) -> [ {Ref, lists:reverse(Code)} || {Ref, Code} <- Bs ] end,
|
||||
RBlocks = Rev(Blocks),
|
||||
RBlocks = [{Ref, crop_jumps(Code)} || {Ref, Code} <- Blocks],
|
||||
RBlockMap = maps:from_list(RBlocks),
|
||||
RBlocks1 = reorder_blocks(RBlocks, []),
|
||||
RBlocks2 = [ {Ref, inline_block(RBlockMap, Ref, Code)} || {Ref, Code} <- RBlocks1 ],
|
||||
@@ -1744,6 +1785,18 @@ tweak_returns(['RETURN' | Code = [{'EXIT', _} | _]]) -> Code;
|
||||
tweak_returns(['RETURN' | Code = [loop | _]]) -> Code;
|
||||
tweak_returns(Code) -> Code.
|
||||
|
||||
%% -- Remove instructions that appear after jumps. Returns reversed code.
|
||||
%% This is useful for example when bb emitter adds continuation jumps
|
||||
%% for switch expressions, but some of the branches
|
||||
crop_jumps(Code) ->
|
||||
crop_jumps(Code, []).
|
||||
crop_jumps([], Acc) ->
|
||||
Acc;
|
||||
crop_jumps([I = {jump, _}|_], Acc) ->
|
||||
[I|Acc];
|
||||
crop_jumps([I|Code], Acc) ->
|
||||
crop_jumps(Code, [I|Acc]).
|
||||
|
||||
%% -- Split basic blocks at CALL instructions --
|
||||
%% Calls can only return to a new basic block. Also splits at JUMPIF instructions.
|
||||
|
||||
|
||||
+20
-19
@@ -96,17 +96,29 @@ decl() ->
|
||||
choice(
|
||||
%% Contract declaration
|
||||
[ ?RULE(token(main), keyword(contract),
|
||||
con(), tok('='), maybe_block(decl()), {contract_main, _2, _3, _5})
|
||||
con(), tok('='), maybe_block(decl()), {contract_main, _2, _3, [], _5})
|
||||
, ?RULE(token(main), keyword(contract),
|
||||
con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), {contract_main, _2, _3, _5, _7})
|
||||
, ?RULE(keyword(contract),
|
||||
con(), tok('='), maybe_block(decl()), {contract_child, _1, _2, _4})
|
||||
con(), tok('='), maybe_block(decl()), {contract_child, _1, _2, [], _4})
|
||||
, ?RULE(keyword(contract),
|
||||
con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), {contract_child, _1, _2, _4, _6})
|
||||
, ?RULE(keyword(contract), token(interface),
|
||||
con(), tok('='), maybe_block(decl()), {contract_interface, _1, _3, _5})
|
||||
con(), tok('='), maybe_block(decl()), {contract_interface, _1, _3, [], _5})
|
||||
, ?RULE(keyword(contract), token(interface),
|
||||
con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), {contract_interface, _1, _3, _5, _7})
|
||||
, ?RULE(token(payable), token(main), keyword(contract),
|
||||
con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_main, _3, _4, _6}))
|
||||
con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_main, _3, _4, [], _6}))
|
||||
, ?RULE(token(payable), token(main), keyword(contract),
|
||||
con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_main, _3, _4, _6, _8}))
|
||||
, ?RULE(token(payable), keyword(contract),
|
||||
con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_child, _2, _3, _5}))
|
||||
con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_child, _2, _3, [], _5}))
|
||||
, ?RULE(token(payable), keyword(contract),
|
||||
con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_child, _2, _3, _5, _7}))
|
||||
, ?RULE(token(payable), keyword(contract), token(interface),
|
||||
con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_interface, _2, _4, _6}))
|
||||
con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_interface, _2, _4, [], _6}))
|
||||
, ?RULE(token(payable), keyword(contract), token(interface),
|
||||
con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_interface, _2, _4, _6, _8}))
|
||||
|
||||
|
||||
, ?RULE(keyword(namespace), con(), tok('='), maybe_block(decl()), {namespace, _1, _2, _4})
|
||||
@@ -134,19 +146,9 @@ 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([fundecl(), fundef()]).
|
||||
choice([?RULE(id(), tok(':'), type(), {fun_decl, get_ann(_1), _1, _3}),
|
||||
fundef()]).
|
||||
|
||||
using() ->
|
||||
Alias = {keyword(as), con()},
|
||||
@@ -537,7 +539,6 @@ 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)).
|
||||
|
||||
+7
-5
@@ -151,12 +151,16 @@ decl(D, Options) ->
|
||||
with_options(Options, fun() -> decl(D) end).
|
||||
|
||||
-spec decl(aeso_syntax:decl()) -> doc().
|
||||
decl({Con, Attrs, C, Ds}) when ?IS_CONTRACT_HEAD(Con) ->
|
||||
decl({Con, Attrs, C, Is, Ds}) when ?IS_CONTRACT_HEAD(Con) ->
|
||||
Mod = fun({Mod, true}) when Mod == payable ->
|
||||
text(atom_to_list(Mod));
|
||||
(_) -> empty() end,
|
||||
ImplsList = case Is of
|
||||
[] -> [empty()];
|
||||
_ -> [text(":"), par(punctuate(text(","), lists:map(fun name/1, Is)), 0)]
|
||||
end,
|
||||
block(follow( hsep(lists:map(Mod, Attrs) ++ [contract_head(Con)])
|
||||
, hsep(name(C), text("="))), decls(Ds));
|
||||
, hsep([name(C)] ++ ImplsList ++ [text("=")])), decls(Ds));
|
||||
decl({namespace, _, C, Ds}) ->
|
||||
block(follow(text("namespace"), hsep(name(C), text("="))), decls(Ds));
|
||||
decl({pragma, _, Pragma}) -> pragma(Pragma);
|
||||
@@ -284,9 +288,7 @@ 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({constrained_t, _, Cs, T}) ->
|
||||
beside([name(T), text(" is "), tuple(lists:map(fun expr/1, Cs))]).
|
||||
type(T = {tvar, _, _}) -> name(T).
|
||||
|
||||
-spec args_type([aeso_syntax:type()]) -> doc().
|
||||
args_type(Args) ->
|
||||
|
||||
+1
-1
@@ -45,7 +45,7 @@ lexer() ->
|
||||
|
||||
Keywords = ["contract", "include", "let", "switch", "type", "record", "datatype", "if", "elif", "else", "function",
|
||||
"stateful", "payable", "true", "false", "mod", "public", "entrypoint", "private", "indexed", "namespace",
|
||||
"interface", "main", "using", "as", "for", "hiding", "is"
|
||||
"interface", "main", "using", "as", "for", "hiding"
|
||||
],
|
||||
KW = string:join(Keywords, "|"),
|
||||
|
||||
|
||||
+3
-6
@@ -38,9 +38,9 @@
|
||||
-type namespace_alias() :: none | con().
|
||||
-type namespace_parts() :: none | {for, [id()]} | {hiding, [id()]}.
|
||||
|
||||
-type decl() :: {contract_main, ann(), con(), [decl()]}
|
||||
| {contract_child, ann(), con(), [decl()]}
|
||||
| {contract_interface, ann(), con(), [decl()]}
|
||||
-type decl() :: {contract_main, ann(), con(), [con()], [decl()]}
|
||||
| {contract_child, ann(), con(), [con()], [decl()]}
|
||||
| {contract_interface, ann(), con(), [con()], [decl()]}
|
||||
| {namespace, ann(), con(), [decl()]}
|
||||
| {pragma, ann(), pragma()}
|
||||
| {type_decl, ann(), id(), [tvar()]} % Only for error msgs
|
||||
@@ -79,14 +79,11 @@
|
||||
|
||||
-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().
|
||||
|
||||
@@ -61,7 +61,6 @@ 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()
|
||||
|
||||
@@ -39,7 +39,7 @@ calldata_aci_test_() ->
|
||||
end} || {ContractName, Fun, Args} <- compilable_contracts()].
|
||||
|
||||
parse_args(Fun, Args) ->
|
||||
[{contract_main, _, _, [{letfun, _, _, _, _, [{guarded, _, [], {app, _, _, AST}}]}]}] =
|
||||
[{contract_main, _, _, _, [{letfun, _, _, _, _, [{guarded, _, [], {app, _, _, AST}}]}]}] =
|
||||
aeso_parser:string("main contract Temp = function foo() = " ++ Fun ++ "(" ++ string:join(Args, ", ") ++ ")"),
|
||||
strip_ann(AST).
|
||||
|
||||
|
||||
+191
-89
@@ -202,6 +202,12 @@ compilable_contracts() ->
|
||||
"assign_patterns",
|
||||
"patterns_guards",
|
||||
"pipe_operator",
|
||||
"polymorphism_contract_implements_interface",
|
||||
"polymorphism_contract_multi_interface",
|
||||
"polymorphism_contract_interface_extends_interface",
|
||||
"polymorphism_contract_interface_extensions",
|
||||
"polymorphism_contract_interface_same_decl_multi_interface",
|
||||
"polymorphism_contract_interface_same_name_same_type",
|
||||
"test" % Custom general-purpose test file. Keep it last on the list.
|
||||
].
|
||||
|
||||
@@ -265,9 +271,7 @@ warnings() ->
|
||||
"The function `called_unused_function2` is defined but never used.">>,
|
||||
<<?PosW(48, 5)
|
||||
"Unused return value.">>,
|
||||
<<?PosW(53, 44)
|
||||
"The constraint on the type variable `'a` is a duplication of the constraint at line 53, column 34">>,
|
||||
<<?PosW(65, 5)
|
||||
<<?PosW(60, 5)
|
||||
"The function `dec` is defined but never used.">>
|
||||
]).
|
||||
|
||||
@@ -566,7 +570,7 @@ failing_contracts() ->
|
||||
])
|
||||
, ?TYPE_ERROR(list_comp_bad_shadow,
|
||||
[<<?Pos(2, 53)
|
||||
"Cannot unify `int` and `string`\n"
|
||||
"Cannot unify `string` and `int`\n"
|
||||
"when checking the type of the pattern `x : int` against the expected type `string`">>
|
||||
])
|
||||
, ?TYPE_ERROR(map_as_map_key,
|
||||
@@ -807,88 +811,6 @@ 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.">>,
|
||||
@@ -918,11 +840,191 @@ failing_contracts() ->
|
||||
"The function `called_unused_function2` is defined but never used.">>,
|
||||
<<?Pos(48, 5)
|
||||
"Unused return value.">>,
|
||||
<<?Pos(53, 44)
|
||||
"The constraint on the type variable `'a` is a duplication of the constraint at line 53, column 34">>,
|
||||
<<?Pos(65, 5)
|
||||
<<?Pos(60, 5)
|
||||
"The function `dec` is defined but never used.">>
|
||||
])
|
||||
, ?TYPE_ERROR(polymorphism_contract_interface_recursive,
|
||||
[<<?Pos(1,24)
|
||||
"Trying to implement or extend an undefined interface `Z`">>
|
||||
])
|
||||
, ?TYPE_ERROR(polymorphism_contract_interface_same_name_different_type,
|
||||
[<<?Pos(4,20)
|
||||
"Unimplemented function `f` from the interface `I1` in the contract `I2`">>])
|
||||
, ?TYPE_ERROR(polymorphism_contract_missing_implementation,
|
||||
[<<?Pos(4,20)
|
||||
"Unimplemented function `f` from the interface `I1` in the contract `I2`">>
|
||||
])
|
||||
, ?TYPE_ERROR(polymorphism_contract_same_decl_multi_interface,
|
||||
[<<?Pos(7,10)
|
||||
"Unimplemented function `f` from the interface `J` in the contract `C`">>
|
||||
])
|
||||
, ?TYPE_ERROR(polymorphism_contract_undefined_interface,
|
||||
[<<?Pos(1,14)
|
||||
"Trying to implement or extend an undefined interface `I`">>
|
||||
])
|
||||
, ?TYPE_ERROR(polymorphism_contract_same_name_different_type_multi_interface,
|
||||
[<<?Pos(9,5)
|
||||
"Duplicate definitions of `f` at\n"
|
||||
" - line 8, column 5\n"
|
||||
" - line 9, column 5">>
|
||||
])
|
||||
, ?TYPE_ERROR(polymorphism_contract_interface_undefined_interface,
|
||||
[<<?Pos(1,24)
|
||||
"Trying to implement or extend an undefined interface `H`">>
|
||||
])
|
||||
, ?TYPE_ERROR(polymorphism_variance_switching,
|
||||
[<<?Pos(36,49)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the application of\n"
|
||||
" `g2 : (Cat) => Cat`\n"
|
||||
"to arguments\n"
|
||||
" `x : Animal`">>,
|
||||
<<?Pos(39,43)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the expression `g3(x) : Animal` against the expected type `Cat`">>,
|
||||
<<?Pos(48,55)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the application of\n"
|
||||
" `g5 : ((Animal) => Animal) => Cat`\n"
|
||||
"to arguments\n"
|
||||
" `x : (Cat) => Cat`">>,
|
||||
<<?Pos(52,44)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the expression `f6() : option(Animal)` against the expected type `option(Cat)`">>,
|
||||
<<?Pos(73,43)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the expression `some_animal : Animal` against the expected type `Cat`">>
|
||||
])
|
||||
, ?TYPE_ERROR(polymorphism_variance_switching_custom_types,
|
||||
[<<?Pos(56,39)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the expression `DT_CONTRA(f_c_to_u) : dt_contra(Cat)` against the expected type `dt_contra(Animal)`">>,
|
||||
<<?Pos(62,35)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the expression `DT_CO(f_u_to_a) : dt_co(Animal)` against the expected type `dt_co(Cat)`">>,
|
||||
<<?Pos(67,36)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the application of\n `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n `f_c_to_a : (Cat) => Animal`">>,
|
||||
<<?Pos(68,36)
|
||||
"Cannot unify `Cat` and `Animal` in a invariant context\n"
|
||||
"when checking the type of the expression `DT_INV(f_c_to_c) : dt_inv(Cat)` against the expected type `dt_inv(Animal)`">>,
|
||||
<<?Pos(69,36)
|
||||
"Cannot unify `Animal` and `Cat` in a invariant context\n"
|
||||
"when checking the type of the expression `DT_INV(f_a_to_a) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>,
|
||||
<<?Pos(70,36)
|
||||
"Cannot unify `Animal` and `Cat` in a invariant context\n"
|
||||
"when checking the type of the expression `DT_INV(f_a_to_c) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>,
|
||||
<<?Pos(71,36)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the application of\n `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n `f_c_to_a : (Cat) => Animal`">>,
|
||||
<<?Pos(80,40)
|
||||
"Cannot unify `Cat` and `Animal` in a invariant context\n"
|
||||
"when checking the type of the expression `DT_INV_SEP_A(f_c_to_u) : dt_inv_sep(Cat)` against the expected type `dt_inv_sep(Animal)`">>,
|
||||
<<?Pos(82,40)
|
||||
"Cannot unify `Cat` and `Animal` in a invariant context\n"
|
||||
"when checking the type of the expression `DT_INV_SEP_B(f_u_to_c) : dt_inv_sep(Cat)` against the expected type `dt_inv_sep(Animal)`">>,
|
||||
<<?Pos(83,40)
|
||||
"Cannot unify `Animal` and `Cat` in a invariant context\n"
|
||||
"when checking the type of the expression `DT_INV_SEP_A(f_a_to_u) : dt_inv_sep(Animal)` against the expected type `dt_inv_sep(Cat)`">>,
|
||||
<<?Pos(85,40)
|
||||
"Cannot unify `Animal` and `Cat` in a invariant context\n"
|
||||
"when checking the type of the expression `DT_INV_SEP_B(f_u_to_a) : dt_inv_sep(Animal)` against the expected type `dt_inv_sep(Cat)`">>,
|
||||
<<?Pos(90,42)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the expression `DT_CO_NEST_A(f_dt_contra_a_to_u) : dt_co_nest_a(Animal)` against the expected type `dt_co_nest_a(Cat)`">>,
|
||||
<<?Pos(94,46)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the expression `DT_CONTRA_NEST_A(f_dt_co_c_to_u) : dt_contra_nest_a(Cat)` against the expected type `dt_contra_nest_a(Animal)`">>,
|
||||
<<?Pos(99,46)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the expression `DT_CONTRA_NEST_B(f_u_to_dt_contra_c) : dt_contra_nest_b(Cat)` against the expected type `dt_contra_nest_b(Animal)`">>,
|
||||
<<?Pos(105,42)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the expression `DT_CO_NEST_B(f_u_to_dt_co_a) : dt_co_nest_b(Animal)` against the expected type `dt_co_nest_b(Cat)`">>,
|
||||
<<?Pos(110,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `vj3 : dt_co_twice(Cat)` against the expected type `dt_co_twice(Animal)`">>,
|
||||
<<?Pos(114,59)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
|
||||
<<?Pos(115,59)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) : dt_a_contra_b_contra(Cat, Animal)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
|
||||
<<?Pos(116,59)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
|
||||
<<?Pos(119,59)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) : dt_a_contra_b_contra(Cat, Animal)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>,
|
||||
<<?Pos(120,59)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>,
|
||||
<<?Pos(122,59)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>,
|
||||
<<?Pos(124,59)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>,
|
||||
<<?Pos(131,13)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the pattern `vl2 : dt_contra_twice(Animal)` against the expected type `dt_contra_twice(Cat)`">>
|
||||
])
|
||||
, ?TYPE_ERROR(polymorphism_variance_switching_records,
|
||||
[<<?Pos(27,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `r03 : rec_co(Cat)` against the expected type `Main.rec_co(Animal)`">>,
|
||||
<<?Pos(33,13)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the pattern `r06 : rec_contra(Animal)` against the expected type `Main.rec_contra(Cat)`">>,
|
||||
<<?Pos(40,13)
|
||||
"Cannot unify `Cat` and `Animal` in a invariant context\n"
|
||||
"when checking the type of the pattern `r10 : rec_inv(Animal)` against the expected type `Main.rec_inv(Cat)`">>,
|
||||
<<?Pos(41,13)
|
||||
"Cannot unify `Animal` and `Cat` in a invariant context\n"
|
||||
"when checking the type of the pattern `r11 : rec_inv(Cat)` against the expected type `Main.rec_inv(Animal)`">>])
|
||||
, ?TYPE_ERROR(polymorphism_variance_switching_oracles,
|
||||
[<<?Pos(15,13)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the pattern `o03 : oracle(Animal, Animal)` against the expected type `oracle(Cat, Animal)`">>,
|
||||
<<?Pos(16,13)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the pattern `o04 : oracle(Animal, Animal)` against the expected type `oracle(Cat, Cat)`">>,
|
||||
<<?Pos(17,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `o05 : oracle(Animal, Cat)` against the expected type `oracle(Animal, Animal)`">>,
|
||||
<<?Pos(19,13)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the pattern `o07 : oracle(Animal, Cat)` against the expected type `oracle(Cat, Animal)`">>,
|
||||
<<?Pos(20,13)
|
||||
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
|
||||
"when checking the type of the pattern `o08 : oracle(Animal, Cat)` against the expected type `oracle(Cat, Cat)`">>,
|
||||
<<?Pos(25,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `o13 : oracle(Cat, Cat)` against the expected type `oracle(Animal, Animal)`">>,
|
||||
<<?Pos(27,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `o15 : oracle(Cat, Cat)` against the expected type `oracle(Cat, Animal)`">>,
|
||||
<<?Pos(34,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `q05 : oracle_query(Animal, Cat)` against the expected type `oracle_query(Animal, Animal)`">>,
|
||||
<<?Pos(36,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `q07 : oracle_query(Animal, Cat)` against the expected type `oracle_query(Cat, Animal)`">>,
|
||||
<<?Pos(38,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `q09 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Animal, Animal)`">>,
|
||||
<<?Pos(39,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `q10 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Animal, Cat)`">>,
|
||||
<<?Pos(42,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `q13 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Animal)`">>,
|
||||
<<?Pos(43,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `q14 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Cat)`">>,
|
||||
<<?Pos(44,13)
|
||||
"Cannot unify `Animal` and `Cat` in a covariant context\n"
|
||||
"when checking the type of the pattern `q15 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Cat, Animal)`">>])
|
||||
].
|
||||
|
||||
-define(Path(File), "code_errors/" ??File).
|
||||
|
||||
@@ -15,7 +15,7 @@ simple_contracts_test_() ->
|
||||
Text = "main contract Identity =\n"
|
||||
" function id(x) = x\n",
|
||||
?assertMatch(
|
||||
[{contract_main, _, {con, _, "Identity"},
|
||||
[{contract_main, _, {con, _, "Identity"}, _,
|
||||
[{letfun, _, {id, _, "id"}, [{id, _, "x"}], {id, _, "_"},
|
||||
[{guarded, _, [], {id, _, "x"}}]}]}], parse_string(Text)),
|
||||
ok
|
||||
|
||||
@@ -1,169 +0,0 @@
|
||||
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
|
||||
|
||||
()
|
||||
@@ -0,0 +1,5 @@
|
||||
contract interface Strokable =
|
||||
entrypoint stroke : () => string
|
||||
|
||||
contract Cat : Strokable =
|
||||
entrypoint stroke() = "Cat stroke"
|
||||
@@ -0,0 +1,10 @@
|
||||
contract interface II =
|
||||
entrypoint f : () => unit
|
||||
|
||||
contract interface I : II =
|
||||
entrypoint f : () => unit
|
||||
entrypoint g : () => unit
|
||||
|
||||
contract C : I =
|
||||
entrypoint f() = ()
|
||||
entrypoint g() = ()
|
||||
@@ -0,0 +1,9 @@
|
||||
contract interface I0 =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract interface I1 : I0 =
|
||||
entrypoint f : () => int
|
||||
entrypoint something_else : () => int
|
||||
|
||||
main contract C =
|
||||
entrypoint f(x : I1) = x.f() // Here we should know that x has f
|
||||
@@ -0,0 +1,13 @@
|
||||
contract interface X : Z =
|
||||
entrypoint x : () => int
|
||||
|
||||
contract interface Y : X =
|
||||
entrypoint y : () => int
|
||||
|
||||
contract interface Z : Y =
|
||||
entrypoint z : () => int
|
||||
|
||||
contract C : Z =
|
||||
entrypoint x() = 1
|
||||
entrypoint y() = 1
|
||||
entrypoint z() = 1
|
||||
@@ -0,0 +1,8 @@
|
||||
contract interface I =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract interface II : I =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract C : II =
|
||||
entrypoint f() = 1
|
||||
@@ -0,0 +1,9 @@
|
||||
contract interface I1 =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract interface I2 : I1 =
|
||||
entrypoint f : () => char
|
||||
|
||||
contract C : I2 =
|
||||
entrypoint f() = 1
|
||||
entrypoint f() = 'c'
|
||||
@@ -0,0 +1,8 @@
|
||||
contract interface I1 =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract interface I2 : I1 =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract C : I2 =
|
||||
entrypoint f() = 1
|
||||
@@ -0,0 +1,5 @@
|
||||
contract interface I : H =
|
||||
entrypoint f : () => unit
|
||||
|
||||
contract C =
|
||||
entrypoint g() = ()
|
||||
@@ -0,0 +1,8 @@
|
||||
contract interface I1 =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract interface I2 : I1 =
|
||||
entrypoint g : () => int
|
||||
|
||||
contract C : I2 =
|
||||
entrypoint g() = 1
|
||||
@@ -0,0 +1,9 @@
|
||||
contract interface I =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract interface J =
|
||||
entrypoint g : () => char
|
||||
|
||||
contract C : I, J =
|
||||
entrypoint f() = 1
|
||||
entrypoint g() = 'c'
|
||||
@@ -0,0 +1,8 @@
|
||||
contract interface I =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract interface J =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract C : I, J =
|
||||
entrypoint f() = 1
|
||||
@@ -0,0 +1,9 @@
|
||||
contract interface I =
|
||||
entrypoint f : () => int
|
||||
|
||||
contract interface J =
|
||||
entrypoint f : () => char
|
||||
|
||||
contract C : I, J =
|
||||
entrypoint f() = 1
|
||||
entrypoint f() = 'c'
|
||||
@@ -0,0 +1,2 @@
|
||||
contract C : I =
|
||||
entrypoint f() = ()
|
||||
@@ -0,0 +1,75 @@
|
||||
contract interface Creature =
|
||||
entrypoint is_alive : () => bool
|
||||
|
||||
contract interface Animal : Creature =
|
||||
entrypoint is_alive : () => bool
|
||||
entrypoint sound : () => string
|
||||
|
||||
contract Cat : Animal =
|
||||
entrypoint sound() = "meow"
|
||||
entrypoint is_alive() = true
|
||||
|
||||
main contract Main =
|
||||
entrypoint init() = ()
|
||||
|
||||
stateful function g0(_ : Creature) : Cat = Chain.create()
|
||||
stateful function f0(x : Cat) : Creature = g0(x)
|
||||
stateful function h0() =
|
||||
let a : Animal = (Chain.create() : Cat)
|
||||
let c : Creature = (Chain.create() : Cat)
|
||||
let c1 : Creature = a
|
||||
()
|
||||
|
||||
stateful function g1(x : Animal) : Cat = Chain.create()
|
||||
stateful function f1(x : Cat) : Animal = g1(x)
|
||||
|
||||
stateful function g11(x : list(Animal)) : list(Cat) = [Chain.create()]
|
||||
stateful function f11(x : list(Cat)) : list(Animal) = g11(x)
|
||||
|
||||
stateful function g12(x : Animal * Animal) : Cat * Cat = (Chain.create(), Chain.create())
|
||||
stateful function f12(x : Cat * Cat) : Animal * Animal = g12(x)
|
||||
|
||||
stateful function g13() : map(Cat, Cat) = { [Chain.create()] = Chain.create() }
|
||||
stateful function f13() : map(Animal, Animal) = g13()
|
||||
|
||||
stateful function g2(x : Cat) : Cat = Chain.create()
|
||||
stateful function f2(x : Animal) : Animal = g2(x) // fail
|
||||
|
||||
stateful function g3(x : Cat) : Animal = f1(x)
|
||||
stateful function f3(x : Cat) : Cat = g3(x) // fail
|
||||
|
||||
stateful function g4(x : (Cat => Animal)) : Cat = Chain.create()
|
||||
stateful function f4(x : (Animal => Cat)) : Animal = g4(x)
|
||||
|
||||
stateful function g44(x : list(list(Cat) => list(Animal))) : Cat = Chain.create()
|
||||
stateful function f44(x : list(list(Animal) => list(Cat))) : Animal = g44(x)
|
||||
|
||||
stateful function g5(x : (Animal => Animal)) : Cat = Chain.create()
|
||||
stateful function f5(x : (Cat => Cat)) : Animal = g5(x) // fail
|
||||
|
||||
stateful function g6() : option(Cat) = Some(Chain.create())
|
||||
stateful function f6() : option(Animal) = g6()
|
||||
stateful function h6() : option(Cat) = f6() // fail
|
||||
|
||||
type cat_type = Cat
|
||||
type animal_type = Animal
|
||||
type cat_cat_map = map(cat_type, cat_type)
|
||||
type animal_animal_map = map(animal_type, animal_type)
|
||||
|
||||
stateful function g71(x : animal_type) : cat_type = Chain.create()
|
||||
stateful function f71(x : cat_type) : animal_type = g1(x)
|
||||
|
||||
stateful function g72() : cat_cat_map = { [Chain.create()] = Chain.create() }
|
||||
stateful function f72() : animal_animal_map = g13()
|
||||
|
||||
stateful function g73() =
|
||||
let some_cat : Cat = Chain.create()
|
||||
let some_animal : Animal = some_cat
|
||||
|
||||
let some_cat_cat_map : map(Cat, Cat) = g13()
|
||||
let some_animal_animal_map : map(Animal, Animal) = some_cat_cat_map
|
||||
|
||||
let x : Animal = some_animal_animal_map[some_cat] // success
|
||||
let y : Cat = some_cat_cat_map[some_animal] // fail
|
||||
|
||||
()
|
||||
@@ -0,0 +1,135 @@
|
||||
contract interface Animal =
|
||||
entrypoint sound : () => string
|
||||
|
||||
contract Cat : Animal =
|
||||
entrypoint sound() = "meow"
|
||||
|
||||
main contract Main =
|
||||
datatype dt_contra('a) = DT_CONTRA('a => unit)
|
||||
datatype dt_co('a) = DT_CO(unit => 'a)
|
||||
datatype dt_inv('a) = DT_INV('a => 'a)
|
||||
datatype dt_biv('a) = DT_BIV(unit => unit)
|
||||
datatype dt_inv_sep('a) = DT_INV_SEP_A('a => unit) | DT_INV_SEP_B(unit => 'a)
|
||||
datatype dt_co_nest_a('a) = DT_CO_NEST_A(dt_contra('a) => unit)
|
||||
datatype dt_contra_nest_a('a) = DT_CONTRA_NEST_A(dt_co('a) => unit)
|
||||
datatype dt_contra_nest_b('a) = DT_CONTRA_NEST_B(unit => dt_contra('a))
|
||||
datatype dt_co_nest_b('a) = DT_CO_NEST_B(unit => dt_co('a))
|
||||
datatype dt_co_twice('a) = DT_CO_TWICE(('a => unit) => 'a)
|
||||
datatype dt_contra_twice('a) = DT_CONTRA_TWICE('a => 'a => unit)
|
||||
datatype dt_a_contra_b_contra('a, 'b) = DT_A_CONTRA_B_CONTRA('a => 'b => unit)
|
||||
|
||||
function f_a_to_a_to_u(_ : Animal) : (Animal => unit) = f_a_to_u
|
||||
function f_a_to_c_to_u(_ : Animal) : (Cat => unit) = f_c_to_u
|
||||
function f_c_to_a_to_u(_ : Cat) : (Animal => unit) = f_a_to_u
|
||||
function f_c_to_c_to_u(_ : Cat) : (Cat => unit) = f_c_to_u
|
||||
|
||||
function f_u_to_u(_ : unit) : unit = ()
|
||||
function f_a_to_u(_ : Animal) : unit = ()
|
||||
function f_c_to_u(_ : Cat) : unit = ()
|
||||
|
||||
function f_dt_contra_a_to_u(_ : dt_contra(Animal)) : unit = ()
|
||||
function f_dt_contra_c_to_u(_ : dt_contra(Cat)) : unit = ()
|
||||
function f_dt_co_a_to_u(_ : dt_co(Animal)) : unit = ()
|
||||
function f_dt_co_c_to_u(_ : dt_co(Cat)) : unit = ()
|
||||
function f_u_to_dt_contra_a(_ : unit) : dt_contra(Animal) = DT_CONTRA(f_a_to_u)
|
||||
function f_u_to_dt_contra_c(_ : unit) : dt_contra(Cat) = DT_CONTRA(f_c_to_u)
|
||||
|
||||
stateful function f_c() : Cat = Chain.create()
|
||||
stateful function f_a() : Animal = f_c()
|
||||
|
||||
stateful function f_u_to_a(_ : unit) : Animal = f_a()
|
||||
stateful function f_u_to_c(_ : unit) : Cat = f_c()
|
||||
stateful function f_a_to_a(_ : Animal) : Animal = f_a()
|
||||
stateful function f_a_to_c(_ : Animal) : Cat = f_c()
|
||||
stateful function f_c_to_a(_ : Cat) : Animal = f_a()
|
||||
stateful function f_c_to_c(_ : Cat) : Cat = f_c()
|
||||
|
||||
stateful function f_a_to_u_to_c(_ : (Animal => unit)) : Cat = f_c()
|
||||
stateful function f_c_to_u_to_a(_ : (Cat => unit)) : Animal = f_a()
|
||||
stateful function f_c_to_u_to_c(_ : (Cat => unit)) : Cat = f_c()
|
||||
|
||||
stateful function f_u_to_dt_co_a(_ : unit) : dt_co(Animal) = DT_CO(f_u_to_a)
|
||||
stateful function f_u_to_dt_co_c(_ : unit) : dt_co(Cat) = DT_CO(f_u_to_c)
|
||||
|
||||
stateful entrypoint init() =
|
||||
let va1 : dt_contra(Animal) = DT_CONTRA(f_a_to_u) // success
|
||||
let va2 : dt_contra(Animal) = DT_CONTRA(f_c_to_u) // fail
|
||||
let va3 : dt_contra(Cat) = DT_CONTRA(f_a_to_u) // success
|
||||
let va4 : dt_contra(Cat) = DT_CONTRA(f_c_to_u) // success
|
||||
|
||||
let vb1 : dt_co(Animal) = DT_CO(f_u_to_a) // success
|
||||
let vb2 : dt_co(Animal) = DT_CO(f_u_to_c) // success
|
||||
let vb3 : dt_co(Cat) = DT_CO(f_u_to_a) // fail
|
||||
let vb4 : dt_co(Cat) = DT_CO(f_u_to_c) // success
|
||||
|
||||
let vc1 : dt_inv(Animal) = DT_INV(f_a_to_a) // success
|
||||
let vc2 : dt_inv(Animal) = DT_INV(f_a_to_c) // success
|
||||
let vc3 : dt_inv(Animal) = DT_INV(f_c_to_a) // fail
|
||||
let vc4 : dt_inv(Animal) = DT_INV(f_c_to_c) // fail
|
||||
let vc5 : dt_inv(Cat) = DT_INV(f_a_to_a) // fail
|
||||
let vc6 : dt_inv(Cat) = DT_INV(f_a_to_c) // fail
|
||||
let vc7 : dt_inv(Cat) = DT_INV(f_c_to_a) // fail
|
||||
let vc8 : dt_inv(Cat) = DT_INV(f_c_to_c) // success
|
||||
|
||||
let vd1 : dt_biv(Animal) = DT_BIV(f_u_to_u) : dt_biv(Animal) // success
|
||||
let vd2 : dt_biv(Animal) = DT_BIV(f_u_to_u) : dt_biv(Cat) // success
|
||||
let vd3 : dt_biv(Cat) = DT_BIV(f_u_to_u) : dt_biv(Animal) // success
|
||||
let vd4 : dt_biv(Cat) = DT_BIV(f_u_to_u) : dt_biv(Cat) // success
|
||||
|
||||
let ve1 : dt_inv_sep(Animal) = DT_INV_SEP_A(f_a_to_u) // success
|
||||
let ve2 : dt_inv_sep(Animal) = DT_INV_SEP_A(f_c_to_u) // fail
|
||||
let ve3 : dt_inv_sep(Animal) = DT_INV_SEP_B(f_u_to_a) // success
|
||||
let ve4 : dt_inv_sep(Animal) = DT_INV_SEP_B(f_u_to_c) // fail
|
||||
let ve5 : dt_inv_sep(Cat) = DT_INV_SEP_A(f_a_to_u) // fail
|
||||
let ve6 : dt_inv_sep(Cat) = DT_INV_SEP_A(f_c_to_u) // success
|
||||
let ve7 : dt_inv_sep(Cat) = DT_INV_SEP_B(f_u_to_a) // fail
|
||||
let ve8 : dt_inv_sep(Cat) = DT_INV_SEP_B(f_u_to_c) // success
|
||||
|
||||
let vf1 : dt_co_nest_a(Animal) = DT_CO_NEST_A(f_dt_contra_a_to_u) // success
|
||||
let vf2 : dt_co_nest_a(Animal) = DT_CO_NEST_A(f_dt_contra_c_to_u) // success
|
||||
let vf3 : dt_co_nest_a(Cat) = DT_CO_NEST_A(f_dt_contra_a_to_u) // fail
|
||||
let vf4 : dt_co_nest_a(Cat) = DT_CO_NEST_A(f_dt_contra_c_to_u) // success
|
||||
|
||||
let vg1 : dt_contra_nest_a(Animal) = DT_CONTRA_NEST_A(f_dt_co_a_to_u) // success
|
||||
let vg2 : dt_contra_nest_a(Animal) = DT_CONTRA_NEST_A(f_dt_co_c_to_u) // fail
|
||||
let vg3 : dt_contra_nest_a(Cat) = DT_CONTRA_NEST_A(f_dt_co_a_to_u) // success
|
||||
let vg4 : dt_contra_nest_a(Cat) = DT_CONTRA_NEST_A(f_dt_co_c_to_u) // success
|
||||
|
||||
let vh1 : dt_contra_nest_b(Animal) = DT_CONTRA_NEST_B(f_u_to_dt_contra_a) // success
|
||||
let vh2 : dt_contra_nest_b(Animal) = DT_CONTRA_NEST_B(f_u_to_dt_contra_c) // fail
|
||||
let vh3 : dt_contra_nest_b(Cat) = DT_CONTRA_NEST_B(f_u_to_dt_contra_a) // success
|
||||
let vh4 : dt_contra_nest_b(Cat) = DT_CONTRA_NEST_B(f_u_to_dt_contra_c) // success
|
||||
|
||||
let vi1 : dt_co_nest_b(Animal) = DT_CO_NEST_B(f_u_to_dt_co_a) // success
|
||||
let vi2 : dt_co_nest_b(Animal) = DT_CO_NEST_B(f_u_to_dt_co_c) // success
|
||||
let vi3 : dt_co_nest_b(Cat) = DT_CO_NEST_B(f_u_to_dt_co_a) // fail
|
||||
let vi4 : dt_co_nest_b(Cat) = DT_CO_NEST_B(f_u_to_dt_co_c) // success
|
||||
|
||||
let vj1 : dt_co_twice(Animal) = DT_CO_TWICE(f_a_to_u_to_c : (Animal => unit) => Animal) : dt_co_twice(Animal) // success
|
||||
let vj2 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_c : (Cat => unit) => Cat ) : dt_co_twice(Cat) // success
|
||||
let vj3 : dt_co_twice(Cat) = DT_CO_TWICE(f_c_to_u_to_a : (Animal => unit) => Animal) : dt_co_twice(Animal) // fail
|
||||
let vj4 : dt_co_twice(Cat) = DT_CO_TWICE(f_c_to_u_to_c : (Cat => unit) => Cat ) : dt_co_twice(Cat) // success
|
||||
|
||||
let vk01 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u) // success
|
||||
let vk02 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) // fail
|
||||
let vk03 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) // fail
|
||||
let vk04 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) // fail
|
||||
let vk05 : dt_a_contra_b_contra(Animal, Cat) = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u) // success
|
||||
let vk06 : dt_a_contra_b_contra(Animal, Cat) = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) // success
|
||||
let vk07 : dt_a_contra_b_contra(Animal, Cat) = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) // fail
|
||||
let vk08 : dt_a_contra_b_contra(Animal, Cat) = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) // fail
|
||||
let vk09 : dt_a_contra_b_contra(Cat, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u) // success
|
||||
let vk10 : dt_a_contra_b_contra(Cat, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) // fail
|
||||
let vk11 : dt_a_contra_b_contra(Cat, Animal) = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) // success
|
||||
let vk12 : dt_a_contra_b_contra(Cat, Animal) = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) // fail
|
||||
let vk13 : dt_a_contra_b_contra(Cat, Cat) = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u) // success
|
||||
let vk14 : dt_a_contra_b_contra(Cat, Cat) = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) // success
|
||||
let vk15 : dt_a_contra_b_contra(Cat, Cat) = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) // success
|
||||
let vk16 : dt_a_contra_b_contra(Cat, Cat) = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) // success
|
||||
|
||||
let vl1 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_a_to_u : Animal => Animal => unit) : dt_contra_twice(Animal) // success
|
||||
let vl2 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_c_to_u : Cat => Cat => unit) : dt_contra_twice(Cat) // fail
|
||||
let vl3 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_a_to_a_to_u : Animal => Animal => unit) : dt_contra_twice(Animal) // success
|
||||
let vl4 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_c_to_a_to_u : Cat => Cat => unit) : dt_contra_twice(Cat) // success
|
||||
|
||||
()
|
||||
@@ -0,0 +1,47 @@
|
||||
contract interface Animal =
|
||||
entrypoint sound : () => string
|
||||
|
||||
contract Cat : Animal =
|
||||
entrypoint sound() = "meow"
|
||||
|
||||
main contract Main =
|
||||
entrypoint oracle() = ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5
|
||||
|
||||
entrypoint query() = oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY
|
||||
|
||||
entrypoint init() =
|
||||
let o01 : oracle(Animal, Animal) = oracle() : oracle(Animal, Animal) // success
|
||||
let o02 : oracle(Animal, Animal) = oracle() : oracle(Animal, Cat) // success
|
||||
let o03 : oracle(Animal, Animal) = oracle() : oracle(Cat, Animal) // fail
|
||||
let o04 : oracle(Animal, Animal) = oracle() : oracle(Cat, Cat) // fail
|
||||
let o05 : oracle(Animal, Cat) = oracle() : oracle(Animal, Animal) // fail
|
||||
let o06 : oracle(Animal, Cat) = oracle() : oracle(Animal, Cat) // success
|
||||
let o07 : oracle(Animal, Cat) = oracle() : oracle(Cat, Animal) // fail
|
||||
let o08 : oracle(Animal, Cat) = oracle() : oracle(Cat, Cat) // fail
|
||||
let o09 : oracle(Cat, Animal) = oracle() : oracle(Animal, Animal) // success
|
||||
let o10 : oracle(Cat, Animal) = oracle() : oracle(Animal, Cat) // success
|
||||
let o11 : oracle(Cat, Animal) = oracle() : oracle(Cat, Animal) // success
|
||||
let o12 : oracle(Cat, Animal) = oracle() : oracle(Cat, Cat) // success
|
||||
let o13 : oracle(Cat, Cat) = oracle() : oracle(Animal, Animal) // fail
|
||||
let o14 : oracle(Cat, Cat) = oracle() : oracle(Animal, Cat) // success
|
||||
let o15 : oracle(Cat, Cat) = oracle() : oracle(Cat, Animal) // fail
|
||||
let o16 : oracle(Cat, Cat) = oracle() : oracle(Cat, Cat) // success
|
||||
|
||||
let q01 : oracle_query(Animal, Animal) = query() : oracle_query(Animal, Animal) // success
|
||||
let q02 : oracle_query(Animal, Animal) = query() : oracle_query(Animal, Cat) // success
|
||||
let q03 : oracle_query(Animal, Animal) = query() : oracle_query(Cat, Animal) // success
|
||||
let q04 : oracle_query(Animal, Animal) = query() : oracle_query(Cat, Cat) // success
|
||||
let q05 : oracle_query(Animal, Cat) = query() : oracle_query(Animal, Animal) // fail
|
||||
let q06 : oracle_query(Animal, Cat) = query() : oracle_query(Animal, Cat) // success
|
||||
let q07 : oracle_query(Animal, Cat) = query() : oracle_query(Cat, Animal) // fail
|
||||
let q08 : oracle_query(Animal, Cat) = query() : oracle_query(Cat, Cat) // success
|
||||
let q09 : oracle_query(Cat, Animal) = query() : oracle_query(Animal, Animal) // fail
|
||||
let q10 : oracle_query(Cat, Animal) = query() : oracle_query(Animal, Cat) // fail
|
||||
let q11 : oracle_query(Cat, Animal) = query() : oracle_query(Cat, Animal) // success
|
||||
let q12 : oracle_query(Cat, Animal) = query() : oracle_query(Cat, Cat) // success
|
||||
let q13 : oracle_query(Cat, Cat) = query() : oracle_query(Animal, Animal) // fail
|
||||
let q14 : oracle_query(Cat, Cat) = query() : oracle_query(Animal, Cat) // fail
|
||||
let q15 : oracle_query(Cat, Cat) = query() : oracle_query(Cat, Animal) // fail
|
||||
let q16 : oracle_query(Cat, Cat) = query() : oracle_query(Cat, Cat) // success
|
||||
|
||||
()
|
||||
@@ -0,0 +1,51 @@
|
||||
contract interface Animal =
|
||||
entrypoint sound : () => string
|
||||
|
||||
contract Cat : Animal =
|
||||
entrypoint sound() = "meow"
|
||||
|
||||
main contract Main =
|
||||
record rec_co('a) = { x : 'a ,
|
||||
y : () => 'a }
|
||||
record rec_contra('a) = { x : 'a => unit }
|
||||
record rec_inv('a) = { x : 'a => unit,
|
||||
y : () => 'a }
|
||||
record rec_biv('a) = { x : int }
|
||||
|
||||
stateful entrypoint new_cat() : Cat = Chain.create()
|
||||
stateful entrypoint new_animal() : Animal = new_cat()
|
||||
stateful entrypoint animal_to_unit(_ : Animal) : unit = ()
|
||||
stateful entrypoint cat_to_unit(_ : Cat) : unit = ()
|
||||
stateful entrypoint unit_to_animal() : Animal = new_animal()
|
||||
stateful entrypoint unit_to_cat() : Cat = new_cat()
|
||||
|
||||
stateful entrypoint init() =
|
||||
let ra : rec_co(Animal) = { x = new_animal(), y = unit_to_animal }
|
||||
let rc : rec_co(Cat) = { x = new_cat(), y = unit_to_cat }
|
||||
let r01 : rec_co(Animal) = ra // success
|
||||
let r02 : rec_co(Animal) = rc // success
|
||||
let r03 : rec_co(Cat) = ra // fail
|
||||
let r04 : rec_co(Cat) = rc // sucess
|
||||
|
||||
let ratu : rec_contra(Animal) = { x = animal_to_unit }
|
||||
let rctu : rec_contra(Cat) = { x = cat_to_unit }
|
||||
let r05 : rec_contra(Animal) = ratu // success
|
||||
let r06 : rec_contra(Animal) = rctu // fail
|
||||
let r07 : rec_contra(Cat) = ratu // success
|
||||
let r08 : rec_contra(Cat) = rctu // success
|
||||
|
||||
let rxaya : rec_inv(Animal) = { x = animal_to_unit, y = unit_to_animal }
|
||||
let rxcyc : rec_inv(Cat) = { x = cat_to_unit, y = unit_to_cat }
|
||||
let r09 : rec_inv(Animal) = rxaya // success
|
||||
let r10 : rec_inv(Animal) = rxcyc // fail
|
||||
let r11 : rec_inv(Cat) = rxaya // fail
|
||||
let r12 : rec_inv(Cat) = rxcyc // success
|
||||
|
||||
let rba : rec_biv(Animal) = { x = 1 }
|
||||
let rbc : rec_biv(Cat) = { x = 1 }
|
||||
let r13 : rec_biv(Animal) = rba // success
|
||||
let r14 : rec_biv(Animal) = rbc // success
|
||||
let r15 : rec_biv(Cat) = rba // success
|
||||
let r16 : rec_biv(Cat) = rbc // success
|
||||
|
||||
()
|
||||
+12
-4
@@ -1,4 +1,12 @@
|
||||
contract ShareTwo =
|
||||
record state = {s1 : int, s2 : int}
|
||||
entrypoint init() = {s1 = 0, s2 = 0}
|
||||
stateful entrypoint buy() = ()
|
||||
// This is a custom test file if you need to run a compiler without
|
||||
// changing aeso_compiler_tests.erl
|
||||
|
||||
include "List.aes"
|
||||
|
||||
contract IntegerHolder =
|
||||
type state = int
|
||||
entrypoint init(x) = x
|
||||
entrypoint get() = state
|
||||
|
||||
main contract Test =
|
||||
stateful entrypoint f(c) = Chain.clone(ref=c, 123)
|
||||
|
||||
@@ -48,11 +48,6 @@ 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()
|
||||
|
||||
|
||||
Reference in New Issue
Block a user