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

Merge pull request #137 from aeternity/polymorpism-checks

Browse Source 
Polymorphism checks
This commit is contained in:
Ulf Norell 2019-08-30 15:48:34 +02:00 committed by GitHub
commit 41e59506ba
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 107 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
rebar.config
View File

@ -2,7 +2,7 @@
{erl_opts, [debug_info]}.
{deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {ref,"10cc127"}}}
{deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {ref,"e7f2be7"}}}
, {getopt, "1.0.1"}
, {eblake2, "1.0.0"}
, {jsx, {git, "https://github.com/talentdeficit/jsx.git",

2
rebar.lock
View File

@ -1,7 +1,7 @@
{"1.1.0",
[{<<"aebytecode">>,
{git,"https://github.com/aeternity/aebytecode.git",
{ref,"10cc1278831ad7e90138533466ceef4bcafd74a9"}},
{ref,"e7f2be7ce878b1e22bad287f3342f32579e98599"}},
0},
{<<"aeserialization">>,
{git,"https://github.com/aeternity/aeserialization.git",

2
src/aeso_ast_infer_types.erl
View File

@ -1327,7 +1327,7 @@ infer_block(Env, _, [E], BlockType) ->
[check_expr(Env, E, BlockType)];
infer_block(Env, Attrs, [Def={letfun, Ann, _, _, _, _}|Rest], BlockType) ->
{{Name, TypeSig}, LetFun} = infer_letfun(Env, Def),
FunT = freshen_type(Ann, typesig_to_fun_t(TypeSig)),
FunT = typesig_to_fun_t(TypeSig),
NewE = bind_var({id, Ann, Name}, FunT, Env),
[LetFun|infer_block(NewE, Attrs, Rest, BlockType)];
infer_block(Env, _, [{letval, Attrs, Pattern, Type, E}|Rest], BlockType) ->

49
src/aeso_ast_to_fcode.erl
View File

@ -282,10 +282,13 @@ decl_to_fcode(Env = #{ functions := Funs }, {letfun, Ann, {id, _, Name}, Args, R
Attrs = get_attributes(Ann),
FName = lookup_fun(Env, qname(Env, Name)),
FArgs = args_to_fcode(Env, Args),
FRet = type_to_fcode(Env, Ret),
FBody = expr_to_fcode(Env#{ vars => [X || {X, _} <- FArgs] }, Body),
[ ensure_first_order_entrypoint(Ann, FArgs, FRet)
|| aeso_syntax:get_ann(entrypoint, Ann, false) ],
Def = #{ attrs => Attrs,
args => FArgs,
return => type_to_fcode(Env, Ret),
return => FRet,
body => FBody },
NewFuns = Funs#{ FName => Def },
Env#{ functions := NewFuns }.
@ -510,7 +513,7 @@ expr_to_fcode(Env, _Type, {app, _Ann, {Op, _}, [A]}) when is_atom(Op) ->
end;
%% Function calls
expr_to_fcode(Env, Type, {app, _Ann, Fun = {typed, _, _, {fun_t, _, NamedArgsT, _, _}}, Args}) ->
expr_to_fcode(Env, Type, {app, _, Fun = {typed, _, _, {fun_t, _, NamedArgsT, _, _}}, Args}) ->
Args1 = get_named_args(NamedArgsT, Args),
FArgs = [expr_to_fcode(Env, Arg) || Arg <- Args1],
case expr_to_fcode(Env, Fun) of
@ -524,11 +527,13 @@ expr_to_fcode(Env, Type, {app, _Ann, Fun = {typed, _, _, {fun_t, _, NamedArgsT,
%% Get the type of the oracle from the args or the expression itself
OType = get_oracle_type(B, Type, Args1),
{oracle, QType, RType} = type_to_fcode(Env, OType),
validate_oracle_type(aeso_syntax:get_ann(Fun), QType, RType),
TypeArgs = [{lit, {typerep, QType}}, {lit, {typerep, RType}}],
builtin_to_fcode(B, FArgs ++ TypeArgs);
{builtin_u, B, _} when B =:= aens_resolve ->
%% Get the type we are assuming the name resolves to
AensType = type_to_fcode(Env, Type),
validate_aens_resolve_type(aeso_syntax:get_ann(Fun), AensType),
TypeArgs = [{lit, {typerep, AensType}}],
builtin_to_fcode(B, FArgs ++ TypeArgs);
{builtin_u, B, _Ar} -> builtin_to_fcode(B, FArgs);
@ -604,6 +609,46 @@ get_oracle_type(oracle_check, _Type, [{typed, _, _Expr, OType}]) ->
get_oracle_type(oracle_check_query, _Type, [{typed, _, _Expr, OType} | _]) -> OType;
get_oracle_type(oracle_respond, _Type, [_, {typed, _,_Expr, OType} | _]) -> OType.
validate_oracle_type(Ann, QType, RType) ->
ensure_monomorphic(QType, {polymorphic_query_type, Ann, QType}),
ensure_monomorphic(RType, {polymorphic_response_type, Ann, RType}),
ensure_first_order(QType, {higher_order_query_type, Ann, QType}),
ensure_first_order(RType, {higher_order_response_type, Ann, RType}),
ok.
validate_aens_resolve_type(Ann, {variant, [[], [Type]]}) ->
ensure_monomorphic(Type, {polymorphic_aens_resolve, Ann, Type}),
ensure_first_order(Type, {higher_order_aens_resolve, Ann, Type}),
ok.
ensure_first_order_entrypoint(Ann, Args, Ret) ->
[ ensure_first_order(T, {higher_order_entrypoint_argument, Ann, X, T})
|| {X, T} <- Args ],
ensure_first_order(Ret, {higher_order_entrypoint_return, Ann, Ret}),
ok.
ensure_monomorphic(Type, Err) ->
case is_monomorphic(Type) of
true -> ok;
false -> fcode_error(Err)
end.
ensure_first_order(Type, Err) ->
case is_first_order(Type) of
true -> ok;
false -> fcode_error(Err)
end.
is_monomorphic({tvar, _}) -> false;
is_monomorphic(Ts) when is_list(Ts) -> lists:all(fun is_monomorphic/1, Ts);
is_monomorphic(Tup) when is_tuple(Tup) -> is_monomorphic(tuple_to_list(Tup));
is_monomorphic(_) -> true.
is_first_order({function, _, _}) -> false;
is_first_order(Ts) when is_list(Ts) -> lists:all(fun is_first_order/1, Ts);
is_first_order(Tup) when is_tuple(Tup) -> is_first_order(tuple_to_list(Tup));
is_first_order(_) -> true.
%% -- Pattern matching --
-spec alts_to_fcode(env(), ftype(), var_name(), [aeso_syntax:alt()]) -> fsplit().

72
src/aeso_ast_to_icode.erl
View File

@ -93,6 +93,8 @@ contract_to_icode([{letfun, Attrib, Name, Args, _What, Body={typed,_,_,T}}|Rest]
FunAttrs = [ stateful || proplists:get_value(stateful, Attrib, false) ] ++
[ payable || proplists:get_value(payable, Attrib, false) ] ++
[ private || is_private(Attrib, Icode) ],
[ check_entrypoint_type(Attrib, Name, Args, T)
|| aeso_syntax:get_ann(entrypoint, Attrib, false) ],
%% TODO: Handle types
FunName = ast_id(Name),
%% TODO: push funname to env
@ -105,7 +107,7 @@ contract_to_icode([{letfun, Attrib, Name, Args, _What, Body={typed,_,_,T}}|Rest]
#{ state_type := StateType } = Icode,
{#tuple{ cpts = [type_value(StateType), ast_body(Body, Icode)] },
{tuple, [typerep, ast_typerep(T, Icode)]}};
_ -> {ast_body(Body, Icode), ast_typerep(T, Icode)}
_ -> {ast_body(Body, Icode), ast_typerep1(T, Icode)}
end,
QName = aeso_icode:qualify(Name, Icode),
NewIcode = ast_fun_to_icode(ast_id(QName), FunAttrs, FunArgs, FunBody, TypeRep, Icode),
@ -121,7 +123,7 @@ ast_id({id, _, Id}) -> Id;
ast_id({qid, _, Id}) -> Id.
ast_args([{arg, _, Name, Type}|Rest], Acc, Icode) ->
ast_args(Rest, [{ast_id(Name), ast_type(Type, Icode)}| Acc], Icode);
ast_args(Rest, [{ast_id(Name), ast_typerep1(Type, Icode)}| Acc], Icode);
ast_args([], Acc, _Icode) -> lists:reverse(Acc).
ast_type(T, Icode) ->
@ -582,7 +584,7 @@ ast_body({block,As,[E|Rest]}, Icode) ->
#switch{expr=ast_body(E, Icode),
cases=[{#var_ref{name="_"},ast_body({block,As,Rest}, Icode)}]};
ast_body({lam,_,Args,Body}, Icode) ->
#lambda{args=[#arg{name = ast_id(P), type = ast_type(T, Icode)} || {arg,_,P,T} <- Args],
#lambda{args=[#arg{name = ast_id(P), type = ast_typerep1(T, Icode)} || {arg,_,P,T} <- Args],
body=ast_body(Body, Icode)};
ast_body({typed,_,{record,Attrs,Fields},{record_t,DefFields}}, Icode) ->
%% Compile as a tuple with the fields in the order they appear in the definition.
@ -717,6 +719,22 @@ map_upd(Key, Default, ValFun, Map = {typed, Ann, _, MapType}, Icode) ->
Args = [ast_body(Map, Icode), ast_body(Key, Icode), ast_body(Default, Icode), ast_body(ValFun, Icode)],
builtin_call(FunName, Args).
check_entrypoint_type(Ann, Name, Args, Ret) ->
Check = fun(T, Err) ->
case is_simple_type(T) of
false -> gen_error(Err);
true -> ok
end end,
[ Check(T, {entrypoint_argument_must_have_simple_type, Ann1, Name, X, T})
|| {arg, Ann1, X, T} <- Args ],
Check(Ret, {entrypoint_must_have_simple_return_type, Ann, Name, Ret}).
is_simple_type({tvar, _, _}) -> false;
is_simple_type({fun_t, _, _, _, _}) -> false;
is_simple_type(Ts) when is_list(Ts) -> lists:all(fun is_simple_type/1, Ts);
is_simple_type(T) when is_tuple(T) -> is_simple_type(tuple_to_list(T));
is_simple_type(_) -> true.
is_monomorphic({tvar, _, _}) -> false;
is_monomorphic([H|T]) ->
is_monomorphic(H) andalso is_monomorphic(T);
@ -757,42 +775,49 @@ make_type_def(Args, Def, Icode = #{ type_vars := TypeEnv }) ->
TVars = [ X || {tvar, _, X} <- Args ],
fun(Types) ->
TypeEnv1 = maps:from_list(lists:zip(TVars, Types)),
ast_typerep(Def, Icode#{ type_vars := maps:merge(TypeEnv, TypeEnv1) })
ast_typerep1(Def, Icode#{ type_vars := maps:merge(TypeEnv, TypeEnv1) })
end.
-spec ast_typerep(aeso_syntax:type()) -> aeb_aevm_data:type().
ast_typerep(Type) -> ast_typerep(Type, aeso_icode:new([])).
ast_typerep(Type) ->
ast_typerep(Type, aeso_icode:new([])).
ast_typerep({id, _, Name}, Icode) ->
ast_typerep(Type, Icode) ->
case is_simple_type(Type) of
false -> gen_error({not_a_simple_type, Type});
true -> ast_typerep1(Type, Icode)
end.
ast_typerep1({id, _, Name}, Icode) ->
lookup_type_id(Name, [], Icode);
ast_typerep({qid, _, Name}, Icode) ->
ast_typerep1({qid, _, Name}, Icode) ->
lookup_type_id(Name, [], Icode);
ast_typerep({con, _, _}, _) ->
ast_typerep1({con, _, _}, _) ->
word; %% Contract type
ast_typerep({bytes_t, _, Len}, _) ->
ast_typerep1({bytes_t, _, Len}, _) ->
bytes_t(Len);
ast_typerep({app_t, _, {I, _, Name}, Args}, Icode) when I =:= id; I =:= qid ->
ArgReps = [ ast_typerep(Arg, Icode) || Arg <- Args ],
ast_typerep1({app_t, _, {I, _, Name}, Args}, Icode) when I =:= id; I =:= qid ->
ArgReps = [ ast_typerep1(Arg, Icode) || Arg <- Args ],
lookup_type_id(Name, ArgReps, Icode);
ast_typerep({tvar,_,A}, #{ type_vars := TypeVars }) ->
ast_typerep1({tvar,_,A}, #{ type_vars := TypeVars }) ->
case maps:get(A, TypeVars, undefined) of
undefined -> word; %% We serialize type variables just as addresses in the originating VM.
Type -> Type
end;
ast_typerep({tuple_t,_,Cpts}, Icode) ->
{tuple, [ast_typerep(C, Icode) || C<-Cpts]};
ast_typerep({record_t,Fields}, Icode) ->
ast_typerep1({tuple_t,_,Cpts}, Icode) ->
{tuple, [ast_typerep1(C, Icode) || C<-Cpts]};
ast_typerep1({record_t,Fields}, Icode) ->
{tuple, [ begin
{field_t, _, _, T} = Field,
ast_typerep(T, Icode)
ast_typerep1(T, Icode)
end || Field <- Fields]};
ast_typerep({fun_t,_,_,_,_}, _Icode) ->
ast_typerep1({fun_t,_,_,_,_}, _Icode) ->
function;
ast_typerep({alias_t, T}, Icode) -> ast_typerep(T, Icode);
ast_typerep({variant_t, Cons}, Icode) ->
ast_typerep1({alias_t, T}, Icode) -> ast_typerep1(T, Icode);
ast_typerep1({variant_t, Cons}, Icode) ->
{variant, [ begin
{constr_t, _, _, Args} = Con,
[ ast_typerep(Arg, Icode) || Arg <- Args ]
[ ast_typerep1(Arg, Icode) || Arg <- Args ]
end || Con <- Cons ]}.
ttl_t(Icode) ->
@ -841,13 +866,6 @@ type_value({map, K, V}) ->
#tuple{ cpts = [#integer{ value = ?TYPEREP_MAP_TAG },
type_value(K), type_value(V)] }.
%% As abort is a built-in in the future it will be illegal to for
%% users to define abort. For the time being strip away all user
%% defined abort functions.
ast_fun_to_icode("abort", _Atts, _Args, _Body, _TypeRep, Icode) ->
%% Strip away all user defined abort functions.
Icode;
ast_fun_to_icode(Name, Attrs, Args, Body, TypeRep, #{functions := Funs} = Icode) ->
NewFuns = [{Name, Attrs, Args, Body, TypeRep}| Funs],
aeso_icode:set_functions(NewFuns, Icode).

2
test/contracts/complex_types.aes
View File

@ -50,7 +50,7 @@ contract ComplexTypes =
entrypoint remote_pair(n : int, s : string) : int * string =
state.worker.pair(gas = 10000, n, s)
entrypoint map(f, xs) =
function map(f, xs) =
switch(xs)
[] => []
x :: xs => f(x) :: map(f, xs)

7
test/contracts/local_poly_fail.aes Normal file
View File

@ -0,0 +1,7 @@
contract Fail =
entrypoint tttt() : bool * int =
let f(x : 'a) : 'a = x
(f(true), f(1))

5
test/contracts/test.aes
View File

@ -91,10 +91,11 @@ contract Identity =
// }
// let id(x) = x
// let main(xs) = map(double,xs)
entrypoint z(f,x) = x
function z(f,x) = x
function s(n) = (f,x)=>f(n(f,x))
function add(m,n) = (f,x)=>m(f,n(f,x))
entrypoint main(_) =
entrypoint main() =
let three=s(s(s(z)))
add(three,three)
(((i)=>i+1),0)

2
test/contracts/tuple_match.aes
View File

@ -1,6 +1,6 @@
contract TuplesMatch =
entrypoint tuplify3() = (t) => switch(t)
function tuplify3() = (t) => switch(t)
(x, y, z) => 3
entrypoint fst(p : int * string) =