Proper checking of types
This commit is contained in:
parent
dfa286d43c
commit
d9188d58a7
@ -95,6 +95,7 @@
|
|||||||
-record(env,
|
-record(env,
|
||||||
{ scopes = #{ [] => #scope{}} :: #{ qname() => scope() }
|
{ scopes = #{ [] => #scope{}} :: #{ qname() => scope() }
|
||||||
, vars = [] :: [{name(), var_info()}]
|
, vars = [] :: [{name(), var_info()}]
|
||||||
|
, typevars = unrestricted :: unrestricted | [name()]
|
||||||
, fields = #{} :: #{ name() => [field_info()] } %% fields are global
|
, fields = #{} :: #{ name() => [field_info()] } %% fields are global
|
||||||
, namespace = [] :: qname()
|
, namespace = [] :: qname()
|
||||||
}).
|
}).
|
||||||
@ -135,6 +136,18 @@ bind_vars([], Env) -> Env;
|
|||||||
bind_vars([{X, T} | Vars], Env) ->
|
bind_vars([{X, T} | Vars], Env) ->
|
||||||
bind_vars(Vars, bind_var(X, T, Env)).
|
bind_vars(Vars, bind_var(X, T, Env)).
|
||||||
|
|
||||||
|
-spec bind_tvars([aeso_syntax:tvar()], env()) -> env().
|
||||||
|
bind_tvars(Xs, Env) ->
|
||||||
|
Env#env{ typevars = [X || {tvar, _, X} <- Xs] }.
|
||||||
|
|
||||||
|
-spec check_tvar(env(), aeso_syntax:tvar()) -> aeso_syntax:tvar() | no_return().
|
||||||
|
check_tvar(#env{ typevars = TVars}, T = {tvar, _, X}) ->
|
||||||
|
case TVars == unrestricted orelse lists:member(X, TVars) of
|
||||||
|
true -> ok;
|
||||||
|
false -> type_error({unbound_type_variable, T})
|
||||||
|
end,
|
||||||
|
T.
|
||||||
|
|
||||||
-spec bind_fun(name(), type() | typesig(), env()) -> env().
|
-spec bind_fun(name(), type() | typesig(), env()) -> env().
|
||||||
bind_fun(X, Type, Env) ->
|
bind_fun(X, Type, Env) ->
|
||||||
Ann = aeso_syntax:get_ann(Type),
|
Ann = aeso_syntax:get_ann(Type),
|
||||||
@ -159,6 +172,19 @@ bind_type(X, Ann, Def, Env) ->
|
|||||||
Scope#scope{ types = [{X, {Ann, Def}} | Types] }
|
Scope#scope{ types = [{X, {Ann, Def}} | Types] }
|
||||||
end).
|
end).
|
||||||
|
|
||||||
|
%% Bind state primitives
|
||||||
|
-spec bind_state(env()) -> env().
|
||||||
|
bind_state(Env) ->
|
||||||
|
Ann = [{origin, system}],
|
||||||
|
Unit = {tuple_t, Ann, []},
|
||||||
|
State =
|
||||||
|
case lookup_type(Env, {id, Ann, "state"}) of
|
||||||
|
{S, _} -> {qid, Ann, S};
|
||||||
|
false -> Unit
|
||||||
|
end,
|
||||||
|
bind_funs([{"state", State},
|
||||||
|
{"put", {fun_t, Ann, [], [State], Unit}}], Env).
|
||||||
|
|
||||||
-spec bind_field(name(), field_info(), env()) -> env().
|
-spec bind_field(name(), field_info(), env()) -> env().
|
||||||
bind_field(X, Info, Env = #env{ fields = Fields }) ->
|
bind_field(X, Info, Env = #env{ fields = Fields }) ->
|
||||||
Fields1 = maps:update_with(X, fun(Infos) -> [Info | Infos] end, [Info], Fields),
|
Fields1 = maps:update_with(X, fun(Infos) -> [Info | Infos] end, [Info], Fields),
|
||||||
@ -300,7 +326,6 @@ global_env() ->
|
|||||||
String = {id, Ann, "string"},
|
String = {id, Ann, "string"},
|
||||||
Address = {id, Ann, "address"},
|
Address = {id, Ann, "address"},
|
||||||
Event = {id, Ann, "event"},
|
Event = {id, Ann, "event"},
|
||||||
State = {id, Ann, "state"},
|
|
||||||
Hash = {id, Ann, "hash"},
|
Hash = {id, Ann, "hash"},
|
||||||
Bits = {id, Ann, "bits"},
|
Bits = {id, Ann, "bits"},
|
||||||
Oracle = fun(Q, R) -> {app_t, Ann, {id, Ann, "oracle"}, [Q, R]} end,
|
Oracle = fun(Q, R) -> {app_t, Ann, {id, Ann, "oracle"}, [Q, R]} end,
|
||||||
@ -331,9 +356,6 @@ global_env() ->
|
|||||||
%% TTL constructors
|
%% TTL constructors
|
||||||
{"RelativeTTL", Fun1(Int, TTL)},
|
{"RelativeTTL", Fun1(Int, TTL)},
|
||||||
{"FixedTTL", Fun1(Int, TTL)},
|
{"FixedTTL", Fun1(Int, TTL)},
|
||||||
%% State
|
|
||||||
{"state", State},
|
|
||||||
{"put", Fun1(State, Unit)},
|
|
||||||
%% Abort
|
%% Abort
|
||||||
{"abort", Fun1(String, A)}])
|
{"abort", Fun1(String, A)}])
|
||||||
, types = MkDefs(
|
, types = MkDefs(
|
||||||
@ -356,7 +378,7 @@ global_env() ->
|
|||||||
{"difficulty", Int},
|
{"difficulty", Int},
|
||||||
{"gas_limit", Int},
|
{"gas_limit", Int},
|
||||||
{"event", Fun1(Event, Unit)}])
|
{"event", Fun1(Event, Unit)}])
|
||||||
, types = MkDefs([{"TTL", 0}]) },
|
, types = MkDefs([{"ttl", 0}]) },
|
||||||
|
|
||||||
ContractScope = #scope
|
ContractScope = #scope
|
||||||
{ funs = MkDefs(
|
{ funs = MkDefs(
|
||||||
@ -488,17 +510,17 @@ infer(Contracts, Options) ->
|
|||||||
|
|
||||||
-spec infer1(env(), [aeso_syntax:decl()], [aeso_syntax:decl()]) -> [aeso_syntax:decl()].
|
-spec infer1(env(), [aeso_syntax:decl()], [aeso_syntax:decl()]) -> [aeso_syntax:decl()].
|
||||||
infer1(_, [], Acc) -> lists:reverse(Acc);
|
infer1(_, [], Acc) -> lists:reverse(Acc);
|
||||||
infer1(Env, [Contract = {contract, Ann, ConName, Code} | Rest], Acc) ->
|
infer1(Env, [{contract, Ann, ConName, Code} | Rest], Acc) ->
|
||||||
%% do type inference on each contract independently.
|
%% do type inference on each contract independently.
|
||||||
check_scope_name_clash(Env, contract, ConName),
|
check_scope_name_clash(Env, contract, ConName),
|
||||||
{Env1, Code1} = infer_contract_top(push_scope(contract, ConName, Env), Code),
|
{Env1, Code1} = infer_contract_top(push_scope(contract, ConName, Env), contract, Code),
|
||||||
Contract1 = {contract, Ann, ConName, Code1},
|
Contract1 = {contract, Ann, ConName, Code1},
|
||||||
Env2 = pop_scope(Env1),
|
Env2 = pop_scope(Env1),
|
||||||
Env3 = bind_contract(Contract, Env2),
|
Env3 = bind_contract(Contract1, Env2),
|
||||||
infer1(Env3, Rest, [Contract1 | Acc]);
|
infer1(Env3, Rest, [Contract1 | Acc]);
|
||||||
infer1(Env, [{namespace, Ann, Name, Code} | Rest], Acc) ->
|
infer1(Env, [{namespace, Ann, Name, Code} | Rest], Acc) ->
|
||||||
check_scope_name_clash(Env, namespace, Name),
|
check_scope_name_clash(Env, namespace, Name),
|
||||||
{Env1, Code1} = infer_contract_top(push_scope(namespace, Name, Env), Code),
|
{Env1, Code1} = infer_contract_top(push_scope(namespace, Name, Env), namespace, Code),
|
||||||
Namespace1 = {namespace, Ann, Name, Code1},
|
Namespace1 = {namespace, Ann, Name, Code1},
|
||||||
infer1(pop_scope(Env1), Rest, [Namespace1 | Acc]).
|
infer1(pop_scope(Env1), Rest, [Namespace1 | Acc]).
|
||||||
|
|
||||||
@ -508,13 +530,13 @@ check_scope_name_clash(Env, Kind, Name) ->
|
|||||||
#scope{ kind = K, ann = Ann } ->
|
#scope{ kind = K, ann = Ann } ->
|
||||||
create_type_errors(),
|
create_type_errors(),
|
||||||
type_error({duplicate_scope, Kind, Name, K, Ann}),
|
type_error({duplicate_scope, Kind, Name, K, Ann}),
|
||||||
destroy_and_report_type_errors()
|
destroy_and_report_type_errors(Env)
|
||||||
end.
|
end.
|
||||||
|
|
||||||
-spec infer_contract_top(env(), [aeso_syntax:decl()]) -> {env(), [aeso_syntax:decl()]}.
|
-spec infer_contract_top(env(), contract | namespace, [aeso_syntax:decl()]) -> {env(), [aeso_syntax:decl()]}.
|
||||||
infer_contract_top(Env, Defs0) ->
|
infer_contract_top(Env, Kind, Defs0) ->
|
||||||
Defs = desugar(Defs0),
|
Defs = desugar(Defs0),
|
||||||
{Env1, Defs1} = infer_contract(Env, Defs),
|
{Env1, Defs1} = infer_contract(Env, Kind, Defs),
|
||||||
Env2 = on_current_scope(Env1, fun(Scope) -> unfold_record_types(Env1, Scope) end),
|
Env2 = on_current_scope(Env1, fun(Scope) -> unfold_record_types(Env1, Scope) end),
|
||||||
Defs2 = unfold_record_types(Env2, Defs1),
|
Defs2 = unfold_record_types(Env2, Defs1),
|
||||||
{Env2, Defs2}.
|
{Env2, Defs2}.
|
||||||
@ -528,17 +550,22 @@ infer_constant({letval, Attrs,_Pattern, Type, E}) ->
|
|||||||
|
|
||||||
%% infer_contract takes a proplist mapping global names to types, and
|
%% infer_contract takes a proplist mapping global names to types, and
|
||||||
%% a list of definitions.
|
%% a list of definitions.
|
||||||
-spec infer_contract(env(), [aeso_syntax:decl()]) -> {env(), [aeso_syntax:decl()]}.
|
-spec infer_contract(env(), contract | namespace, [aeso_syntax:decl()]) -> {env(), [aeso_syntax:decl()]}.
|
||||||
infer_contract(Env, Defs) ->
|
infer_contract(Env, What, Defs) ->
|
||||||
Kind = fun({type_def, _, _, _, _}) -> type;
|
Kind = fun({type_def, _, _, _, _}) -> type;
|
||||||
({letfun, _, _, _, _, _}) -> function;
|
({letfun, _, _, _, _, _}) -> function;
|
||||||
({fun_decl, _, _, _}) -> prototype
|
({fun_decl, _, _, _}) -> prototype
|
||||||
end,
|
end,
|
||||||
Get = fun(K) -> [ Def || Def <- Defs, Kind(Def) == K ] end,
|
Get = fun(K) -> [ Def || Def <- Defs, Kind(Def) == K ] end,
|
||||||
{Env1, TypeDefs} = check_typedefs(Env, Get(type)),
|
{Env1, TypeDefs} = check_typedefs(Env, Get(type)),
|
||||||
ProtoSigs = [ check_fundecl(Env1, Decl) || Decl <- Get(prototype) ],
|
Env2 =
|
||||||
|
case What of
|
||||||
|
namespace -> Env1;
|
||||||
|
contract -> bind_state(Env1) %% bind state and put
|
||||||
|
end,
|
||||||
|
{ProtoSigs, Decls} = lists:unzip([ check_fundecl(Env1, Decl) || Decl <- Get(prototype) ]),
|
||||||
create_type_errors(),
|
create_type_errors(),
|
||||||
Env2 = bind_funs(ProtoSigs, Env1),
|
Env3 = bind_funs(ProtoSigs, Env2),
|
||||||
Functions = Get(function),
|
Functions = Get(function),
|
||||||
%% Check for duplicates in Functions (we turn it into a map below)
|
%% Check for duplicates in Functions (we turn it into a map below)
|
||||||
_ = bind_funs([{Fun, {tuple_t, Ann, []}} || {letfun, Ann, {id, _, Fun}, _, _, _} <- Functions],
|
_ = bind_funs([{Fun, {tuple_t, Ann, []}} || {letfun, Ann, {id, _, Fun}, _, _, _} <- Functions],
|
||||||
@ -548,9 +575,9 @@ infer_contract(Env, Defs) ->
|
|||||||
DepGraph = maps:map(fun(_, Def) -> aeso_syntax_utils:used_ids(Def) end, FunMap),
|
DepGraph = maps:map(fun(_, Def) -> aeso_syntax_utils:used_ids(Def) end, FunMap),
|
||||||
SCCs = aeso_utils:scc(DepGraph),
|
SCCs = aeso_utils:scc(DepGraph),
|
||||||
%% io:format("Dependency sorted functions:\n ~p\n", [SCCs]),
|
%% io:format("Dependency sorted functions:\n ~p\n", [SCCs]),
|
||||||
{Env3, Defs1} = check_sccs(Env2, FunMap, SCCs, []),
|
{Env4, Defs1} = check_sccs(Env3, FunMap, SCCs, []),
|
||||||
destroy_and_report_type_errors(),
|
destroy_and_report_type_errors(Env4),
|
||||||
{Env3, TypeDefs ++ Defs1}.
|
{Env4, TypeDefs ++ Decls ++ Defs1}.
|
||||||
|
|
||||||
-spec check_typedefs(env(), [aeso_syntax:decl()]) -> {env(), [aeso_syntax:decl()]}.
|
-spec check_typedefs(env(), [aeso_syntax:decl()]) -> {env(), [aeso_syntax:decl()]}.
|
||||||
check_typedefs(Env, Defs) ->
|
check_typedefs(Env, Defs) ->
|
||||||
@ -560,7 +587,7 @@ check_typedefs(Env, Defs) ->
|
|||||||
DepGraph = maps:map(fun(_, Def) -> aeso_syntax_utils:used_types(Def) end, TypeMap),
|
DepGraph = maps:map(fun(_, Def) -> aeso_syntax_utils:used_types(Def) end, TypeMap),
|
||||||
SCCs = aeso_utils:scc(DepGraph),
|
SCCs = aeso_utils:scc(DepGraph),
|
||||||
{Env1, Defs1} = check_typedef_sccs(Env, TypeMap, SCCs, []),
|
{Env1, Defs1} = check_typedef_sccs(Env, TypeMap, SCCs, []),
|
||||||
destroy_and_report_type_errors(),
|
destroy_and_report_type_errors(Env),
|
||||||
{Env1, Defs1}.
|
{Env1, Defs1}.
|
||||||
|
|
||||||
-spec check_typedef_sccs(env(), #{ name() => aeso_syntax:decl() },
|
-spec check_typedef_sccs(env(), #{ name() => aeso_syntax:decl() },
|
||||||
@ -571,17 +598,18 @@ check_typedef_sccs(Env, TypeMap, [{acyclic, Name} | SCCs], Acc) ->
|
|||||||
case maps:get(Name, TypeMap, undefined) of
|
case maps:get(Name, TypeMap, undefined) of
|
||||||
undefined -> check_typedef_sccs(Env, TypeMap, SCCs, Acc); %% Builtin type
|
undefined -> check_typedef_sccs(Env, TypeMap, SCCs, Acc); %% Builtin type
|
||||||
{type_def, Ann, D, Xs, Def0} ->
|
{type_def, Ann, D, Xs, Def0} ->
|
||||||
Def = check_event(Env, Name, Ann, Def0),
|
Def = check_event(Env, Name, Ann, check_typedef(bind_tvars(Xs, Env), Def0)),
|
||||||
Acc1 = [{type_def, Ann, D, Xs, Def} | Acc],
|
Acc1 = [{type_def, Ann, D, Xs, Def} | Acc],
|
||||||
Env1 = bind_type(Name, Ann, {Xs, Def}, Env),
|
Env1 = bind_type(Name, Ann, {Xs, Def}, Env),
|
||||||
case Def of
|
case Def of
|
||||||
{alias_t, _} -> check_typedef_sccs(Env1, TypeMap, SCCs, Acc1); %% TODO: check these
|
{alias_t, _} -> check_typedef_sccs(Env1, TypeMap, SCCs, Acc1);
|
||||||
{record_t, Fields} ->
|
{record_t, Fields} ->
|
||||||
RecTy = app_t(Ann, D, Xs),
|
%% check_type to get qualified name
|
||||||
|
RecTy = check_type(Env1, app_t(Ann, D, Xs)),
|
||||||
Env2 = check_fields(Env1, TypeMap, RecTy, Fields),
|
Env2 = check_fields(Env1, TypeMap, RecTy, Fields),
|
||||||
check_typedef_sccs(Env2, TypeMap, SCCs, Acc1);
|
check_typedef_sccs(Env2, TypeMap, SCCs, Acc1);
|
||||||
{variant_t, Cons} ->
|
{variant_t, Cons} ->
|
||||||
Target = app_t(Ann, D, Xs),
|
Target = check_type(Env1, app_t(Ann, D, Xs)),
|
||||||
ConType = fun([]) -> Target; (Args) -> {type_sig, Ann, [], Args, Target} end,
|
ConType = fun([]) -> Target; (Args) -> {type_sig, Ann, [], Args, Target} end,
|
||||||
ConTypes = [ begin
|
ConTypes = [ begin
|
||||||
{constr_t, _, {con, _, Con}, Args} = ConDef,
|
{constr_t, _, {con, _, Con}, Args} = ConDef,
|
||||||
@ -597,6 +625,65 @@ check_typedef_sccs(Env, TypeMap, [{cyclic, Names} | SCCs], Acc) ->
|
|||||||
type_error({recursive_types_not_implemented, lists:map(Id, Names)}),
|
type_error({recursive_types_not_implemented, lists:map(Id, Names)}),
|
||||||
check_typedef_sccs(Env, TypeMap, SCCs, Acc).
|
check_typedef_sccs(Env, TypeMap, SCCs, Acc).
|
||||||
|
|
||||||
|
-spec check_typedef(env(), aeso_syntax:typedef()) -> aeso_syntax:typedef().
|
||||||
|
check_typedef(Env, {alias_t, Type}) ->
|
||||||
|
{alias_t, check_type(Env, Type)};
|
||||||
|
check_typedef(Env, {record_t, Fields}) ->
|
||||||
|
{record_t, [ {field_t, Ann, Id, check_type(Env, Type)} || {field_t, Ann, Id, Type} <- Fields ]};
|
||||||
|
check_typedef(Env, {variant_t, Cons}) ->
|
||||||
|
{variant_t, [ {constr_t, Ann, Con, [ check_type(Env, Arg) || Arg <- Args ]}
|
||||||
|
|| {constr_t, Ann, Con, Args} <- Cons ]}.
|
||||||
|
|
||||||
|
-spec check_type(env(), aeso_syntax:type()) -> aeso_syntax:type().
|
||||||
|
check_type(Env, T) ->
|
||||||
|
check_type(Env, T, 0).
|
||||||
|
|
||||||
|
%% Check a type against an arity.
|
||||||
|
-spec check_type(env(), utype(), non_neg_integer()) -> utype().
|
||||||
|
check_type(Env, T = {tvar, _, _}, Arity) ->
|
||||||
|
[ type_error({higher_kinded_typevar, T}) || Arity /= 0 ],
|
||||||
|
check_tvar(Env, T);
|
||||||
|
check_type(_Env, X = {id, _, "_"}, Arity) ->
|
||||||
|
ensure_base_type(X, Arity),
|
||||||
|
X;
|
||||||
|
check_type(Env, X = {Tag, _, _}, Arity) when Tag == con; Tag == qcon; Tag == id; Tag == qid ->
|
||||||
|
case lookup_type(Env, X) of
|
||||||
|
{Q, {_, Def}} ->
|
||||||
|
Arity1 = case Def of
|
||||||
|
{builtin, Ar} -> Ar;
|
||||||
|
{Args, _} -> length(Args)
|
||||||
|
end,
|
||||||
|
[ type_error({wrong_type_arguments, X, Arity, Arity1}) || Arity /= Arity1 ],
|
||||||
|
set_qname(Q, X);
|
||||||
|
false -> type_error({unbound_type, X}), X
|
||||||
|
end;
|
||||||
|
check_type(Env, Type = {tuple_t, Ann, Types}, Arity) ->
|
||||||
|
ensure_base_type(Type, Arity),
|
||||||
|
{tuple_t, Ann, [ check_type(Env, T, 0) || T <- Types ]};
|
||||||
|
check_type(Env, {app_t, Ann, Type, Types}, Arity) ->
|
||||||
|
Types1 = [ check_type(Env, T, 0) || T <- Types ],
|
||||||
|
Type1 = check_type(Env, Type, Arity + length(Types)),
|
||||||
|
{app_t, Ann, Type1, Types1};
|
||||||
|
check_type(Env, Type = {fun_t, Ann, NamedArgs, Args, Ret}, Arity) ->
|
||||||
|
ensure_base_type(Type, Arity),
|
||||||
|
NamedArgs1 = [ check_named_arg(Env, NamedArg) || NamedArg <- NamedArgs ],
|
||||||
|
Args1 = [ check_type(Env, Arg, 0) || Arg <- Args ],
|
||||||
|
Ret1 = check_type(Env, Ret, 0),
|
||||||
|
{fun_t, Ann, NamedArgs1, Args1, Ret1};
|
||||||
|
check_type(_Env, Type = {uvar, _, _}, Arity) ->
|
||||||
|
ensure_base_type(Type, Arity),
|
||||||
|
Type.
|
||||||
|
|
||||||
|
ensure_base_type(Type, Arity) ->
|
||||||
|
[ type_error({wrong_type_arguments, Type, Arity, 0}) || Arity /= 0 ],
|
||||||
|
ok.
|
||||||
|
|
||||||
|
-spec check_named_arg(env(), aeso_syntax:named_arg_t()) -> aeso_syntax:named_arg_t().
|
||||||
|
check_named_arg(Env, {named_arg_t, Ann, Id, Type, Default}) ->
|
||||||
|
Type1 = check_type(Env, Type),
|
||||||
|
{typed, _, Default1, _} = check_expr(Env, Default, Type1),
|
||||||
|
{named_arg_t, Ann, Id, Type1, Default1}.
|
||||||
|
|
||||||
-spec check_fields(env(), #{ name() => aeso_syntax:decl() }, type(), [aeso_syntax:field_t()]) -> env().
|
-spec check_fields(env(), #{ name() => aeso_syntax:decl() }, type(), [aeso_syntax:field_t()]) -> env().
|
||||||
check_fields(Env, _TypeMap, _, []) -> Env;
|
check_fields(Env, _TypeMap, _, []) -> Env;
|
||||||
check_fields(Env, TypeMap, RecTy, [{field_t, Ann, Id, Type} | Fields]) ->
|
check_fields(Env, TypeMap, RecTy, [{field_t, Ann, Id, Type} | Fields]) ->
|
||||||
@ -622,7 +709,6 @@ check_event_con(Env, {constr_t, Ann, Con, Args}) ->
|
|||||||
Indexed = [ T || T <- Args, IsIndexed(T) == indexed ],
|
Indexed = [ T || T <- Args, IsIndexed(T) == indexed ],
|
||||||
NonIndexed = Args -- Indexed,
|
NonIndexed = Args -- Indexed,
|
||||||
[ check_event_arg_type(Env, Ix, Type) || {Ix, Type} <- lists:zip(Indices, Args) ],
|
[ check_event_arg_type(Env, Ix, Type) || {Ix, Type} <- lists:zip(Indices, Args) ],
|
||||||
%% TODO: Is is possible to check also the types of arguments in a sensible way?
|
|
||||||
[ type_error({event_0_to_3_indexed_values, Con}) || length(Indexed) > 3 ],
|
[ type_error({event_0_to_3_indexed_values, Con}) || length(Indexed) > 3 ],
|
||||||
[ type_error({event_0_to_1_string_values, Con}) || length(NonIndexed) > 1 ],
|
[ type_error({event_0_to_1_string_values, Con}) || length(NonIndexed) > 1 ],
|
||||||
{constr_t, [{indices, Indices} | Ann], Con, Args}.
|
{constr_t, [{indices, Indices} | Ann], Con, Args}.
|
||||||
@ -690,9 +776,10 @@ check_reserved_entrypoints(Funs) ->
|
|||||||
|| {Name, Def} <- maps:to_list(Funs), lists:member(Name, Reserved) ],
|
|| {Name, Def} <- maps:to_list(Funs), lists:member(Name, Reserved) ],
|
||||||
ok.
|
ok.
|
||||||
|
|
||||||
-spec check_fundecl(env(), aeso_syntax:decl()) -> {name(), typesig()}.
|
-spec check_fundecl(env(), aeso_syntax:decl()) -> {{name(), typesig()}, aeso_syntax:decl()}.
|
||||||
check_fundecl(_Env, {fun_decl, Ann, {id, _, Name}, {fun_t, _, Named, Args, Ret}}) ->
|
check_fundecl(Env, {fun_decl, Ann, Id = {id, _, Name}, Type = {fun_t, _, _, _, _}}) ->
|
||||||
{Name, {type_sig, Ann, Named, Args, Ret}}; %% TODO: actually check that the type makes sense!
|
Type1 = {fun_t, _, Named, Args, Ret} = check_type(Env, Type),
|
||||||
|
{{Name, {type_sig, Ann, Named, Args, Ret}}, {fun_decl, Ann, Id, Type1}};
|
||||||
check_fundecl(_, {fun_decl, _Attrib, {id, _, Name}, Type}) ->
|
check_fundecl(_, {fun_decl, _Attrib, {id, _, Name}, Type}) ->
|
||||||
error({fundecl_must_have_funtype, Name, Type}).
|
error({fundecl_must_have_funtype, Name, Type}).
|
||||||
|
|
||||||
@ -713,7 +800,7 @@ check_special_funs(Env, {{"init", Type}, _}) ->
|
|||||||
%% We might have implicit (no) state.
|
%% We might have implicit (no) state.
|
||||||
case lookup_type(Env, {id, [], "state"}) of
|
case lookup_type(Env, {id, [], "state"}) of
|
||||||
false -> {tuple_t, [{origin, system}], []};
|
false -> {tuple_t, [{origin, system}], []};
|
||||||
_ -> {id, [{origin, system}], "state"}
|
{S, _} -> {qid, [], S}
|
||||||
end,
|
end,
|
||||||
unify(Env, Res, State, {checking_init_type, Ann});
|
unify(Env, Res, State, {checking_init_type, Ann});
|
||||||
check_special_funs(_, _) -> ok.
|
check_special_funs(_, _) -> ok.
|
||||||
@ -743,8 +830,8 @@ infer_letrec(Env, {letrec, Attrs, Defs}) ->
|
|||||||
{TypeSigs, {letrec, Attrs, NewDefs}}.
|
{TypeSigs, {letrec, Attrs, NewDefs}}.
|
||||||
|
|
||||||
infer_letfun(Env, {letfun, Attrib, {id, NameAttrib, Name}, Args, What, Body}) ->
|
infer_letfun(Env, {letfun, Attrib, {id, NameAttrib, Name}, Args, What, Body}) ->
|
||||||
ArgTypes = [{ArgName, arg_type(T)} || {arg, _, ArgName, T} <- Args],
|
ArgTypes = [{ArgName, check_type(Env, arg_type(T))} || {arg, _, ArgName, T} <- Args],
|
||||||
ExpectedType = arg_type(What),
|
ExpectedType = check_type(Env, arg_type(What)),
|
||||||
NewBody={typed, _, _, ResultType} = check_expr(bind_vars(ArgTypes, Env), Body, ExpectedType),
|
NewBody={typed, _, _, ResultType} = check_expr(bind_vars(ArgTypes, Env), Body, ExpectedType),
|
||||||
NewArgs = [{arg, A1, {id, A2, ArgName}, T}
|
NewArgs = [{arg, A1, {id, A2, ArgName}, T}
|
||||||
|| {{_, T}, {arg, A1, {id, A2, ArgName}, _}} <- lists:zip(ArgTypes, Args)],
|
|| {{_, T}, {arg, A1, {id, A2, ArgName}, _}} <- lists:zip(ArgTypes, Args)],
|
||||||
@ -822,7 +909,8 @@ infer_expr(Env, {list, As, Elems}) ->
|
|||||||
NewElems = [check_expr(Env, X, ElemType) || X <- Elems],
|
NewElems = [check_expr(Env, X, ElemType) || X <- Elems],
|
||||||
{typed, As, {list, As, NewElems}, {app_t, As, {id, As, "list"}, [ElemType]}};
|
{typed, As, {list, As, NewElems}, {app_t, As, {id, As, "list"}, [ElemType]}};
|
||||||
infer_expr(Env, {typed, As, Body, Type}) ->
|
infer_expr(Env, {typed, As, Body, Type}) ->
|
||||||
{typed, _, NewBody, NewType} = check_expr(Env, Body, Type),
|
Type1 = check_type(Env, Type),
|
||||||
|
{typed, _, NewBody, NewType} = check_expr(Env, Body, Type1),
|
||||||
{typed, As, NewBody, NewType};
|
{typed, As, NewBody, NewType};
|
||||||
infer_expr(Env, {app, Ann, Fun, Args0}) ->
|
infer_expr(Env, {app, Ann, Fun, Args0}) ->
|
||||||
%% TODO: fix parser to give proper annotation for normal applications!
|
%% TODO: fix parser to give proper annotation for normal applications!
|
||||||
@ -925,7 +1013,7 @@ infer_expr(Env, {block, Attrs, Stmts}) ->
|
|||||||
{typed, Attrs, {block, Attrs, NewStmts}, BlockType};
|
{typed, Attrs, {block, Attrs, NewStmts}, BlockType};
|
||||||
infer_expr(Env, {lam, Attrs, Args, Body}) ->
|
infer_expr(Env, {lam, Attrs, Args, Body}) ->
|
||||||
ArgTypes = [fresh_uvar(As) || {arg, As, _, _} <- Args],
|
ArgTypes = [fresh_uvar(As) || {arg, As, _, _} <- Args],
|
||||||
ArgPatterns = [{typed, As, Pat, T} || {arg, As, Pat, T} <- Args],
|
ArgPatterns = [{typed, As, Pat, check_type(Env, T)} || {arg, As, Pat, T} <- Args],
|
||||||
ResultType = fresh_uvar(Attrs),
|
ResultType = fresh_uvar(Attrs),
|
||||||
{'case', _, {typed, _, {tuple, _, NewArgPatterns}, _}, NewBody} =
|
{'case', _, {typed, _, {tuple, _, NewArgPatterns}, _}, NewBody} =
|
||||||
infer_case(Env, Attrs, {tuple, Attrs, ArgPatterns}, {tuple_t, Attrs, ArgTypes}, Body, ResultType),
|
infer_case(Env, Attrs, {tuple, Attrs, ArgPatterns}, {tuple_t, Attrs, ArgTypes}, Body, ResultType),
|
||||||
@ -1526,8 +1614,8 @@ unify1(_Env, {qcon, _, Name}, {qcon, _, Name}, _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}, When) ->
|
||||||
unify(Env, Named1, Named2, When) andalso
|
unify(Env, Named1, Named2, When) andalso
|
||||||
unify(Env, Args1, Args2, When) andalso unify(Env, Result1, Result2, When);
|
unify(Env, Args1, Args2, When) andalso unify(Env, Result1, Result2, When);
|
||||||
unify1(Env, {app_t, _, {id, _, F}, Args1}, {app_t, _, {id, _, F}, Args2}, When)
|
unify1(Env, {app_t, _, {Tag, _, F}, Args1}, {app_t, _, {Tag, _, F}, Args2}, When)
|
||||||
when length(Args1) == length(Args2) ->
|
when length(Args1) == length(Args2), Tag == id orelse Tag == qid ->
|
||||||
unify(Env, Args1, Args2, When);
|
unify(Env, Args1, Args2, When);
|
||||||
unify1(Env, {tuple_t, _, As}, {tuple_t, _, Bs}, When)
|
unify1(Env, {tuple_t, _, As}, {tuple_t, _, Bs}, When)
|
||||||
when length(As) == length(Bs) ->
|
when length(As) == length(Bs) ->
|
||||||
@ -1662,14 +1750,31 @@ type_error(Err) ->
|
|||||||
create_type_errors() ->
|
create_type_errors() ->
|
||||||
ets_new(type_errors, [bag]).
|
ets_new(type_errors, [bag]).
|
||||||
|
|
||||||
destroy_and_report_type_errors() ->
|
destroy_and_report_type_errors(Env) ->
|
||||||
Errors = ets_tab2list(type_errors),
|
Errors = ets_tab2list(type_errors),
|
||||||
%% io:format("Type errors now: ~p\n", [Errors]),
|
%% io:format("Type errors now: ~p\n", [Errors]),
|
||||||
PPErrors = [ pp_error(Err) || Err <- Errors ],
|
PPErrors = [ pp_error(unqualify(Env, Err)) || Err <- Errors ],
|
||||||
ets_delete(type_errors),
|
ets_delete(type_errors),
|
||||||
Errors /= [] andalso
|
Errors /= [] andalso
|
||||||
error({type_errors, [lists:flatten(Err) || Err <- PPErrors]}).
|
error({type_errors, [lists:flatten(Err) || Err <- PPErrors]}).
|
||||||
|
|
||||||
|
%% Strip current namespace from error message for nicer printing.
|
||||||
|
unqualify(#env{ namespace = NS }, {qid, Ann, Xs}) ->
|
||||||
|
qid(Ann, unqualify1(NS, Xs));
|
||||||
|
unqualify(#env{ namespace = NS }, {qcon, Ann, Xs}) ->
|
||||||
|
qcon(Ann, unqualify1(NS, Xs));
|
||||||
|
unqualify(Env, T) when is_tuple(T) ->
|
||||||
|
list_to_tuple(unqualify(Env, tuple_to_list(T)));
|
||||||
|
unqualify(Env, [H | T]) -> [unqualify(Env, H) | unqualify(Env, T)];
|
||||||
|
unqualify(_Env, X) -> X.
|
||||||
|
|
||||||
|
unqualify1(NS, Xs) ->
|
||||||
|
try lists:split(length(NS), Xs) of
|
||||||
|
{NS, Ys} -> Ys;
|
||||||
|
_ -> Xs
|
||||||
|
catch _:_ -> Xs
|
||||||
|
end.
|
||||||
|
|
||||||
pp_error({cannot_unify, A, B, When}) ->
|
pp_error({cannot_unify, A, B, When}) ->
|
||||||
io_lib:format("Cannot unify ~s\n"
|
io_lib:format("Cannot unify ~s\n"
|
||||||
" and ~s\n"
|
" and ~s\n"
|
||||||
@ -1907,8 +2012,8 @@ pp({tuple_t, _, Cpts}) ->
|
|||||||
["(", pp(Cpts), ")"];
|
["(", pp(Cpts), ")"];
|
||||||
pp({app_t, _, T, []}) ->
|
pp({app_t, _, T, []}) ->
|
||||||
pp(T);
|
pp(T);
|
||||||
pp({app_t, _, {id, _, Name}, Args}) ->
|
pp({app_t, _, Type, Args}) ->
|
||||||
[Name, "(", pp(Args), ")"];
|
[pp(Type), "(", pp(Args), ")"];
|
||||||
pp({named_arg_t, _, Name, Type, Default}) ->
|
pp({named_arg_t, _, Name, Type, Default}) ->
|
||||||
[pp(Name), " : ", pp(Type), " = ", pp(Default)];
|
[pp(Name), " : ", pp(Type), " = ", pp(Default)];
|
||||||
pp({fun_t, _, Named = {uvar, _, _}, As, B}) ->
|
pp({fun_t, _, Named = {uvar, _, _}, As, B}) ->
|
||||||
|
@ -58,7 +58,7 @@ contract_to_icode([{namespace, _, Name, Defs} | Rest], Icode) ->
|
|||||||
NS = aeso_icode:get_namespace(Icode),
|
NS = aeso_icode:get_namespace(Icode),
|
||||||
Icode1 = contract_to_icode(Defs, aeso_icode:enter_namespace(Name, Icode)),
|
Icode1 = contract_to_icode(Defs, aeso_icode:enter_namespace(Name, Icode)),
|
||||||
contract_to_icode(Rest, aeso_icode:set_namespace(NS, Icode1));
|
contract_to_icode(Rest, aeso_icode:set_namespace(NS, Icode1));
|
||||||
contract_to_icode([{type_def, _Attrib, {id, _, Name}, Args, Def} | Rest],
|
contract_to_icode([{type_def, _Attrib, Id = {id, _, Name}, Args, Def} | Rest],
|
||||||
Icode = #{ types := Types, constructors := Constructors }) ->
|
Icode = #{ types := Types, constructors := Constructors }) ->
|
||||||
TypeDef = make_type_def(Args, Def, Icode),
|
TypeDef = make_type_def(Args, Def, Icode),
|
||||||
NewConstructors =
|
NewConstructors =
|
||||||
@ -70,7 +70,8 @@ contract_to_icode([{type_def, _Attrib, {id, _, Name}, Args, Def} | Rest],
|
|||||||
maps:from_list([ {QName(Con), Tag} || {Tag, Con} <- lists:zip(Tags, Cons) ]);
|
maps:from_list([ {QName(Con), Tag} || {Tag, Con} <- lists:zip(Tags, Cons) ]);
|
||||||
_ -> #{}
|
_ -> #{}
|
||||||
end,
|
end,
|
||||||
Icode1 = Icode#{ types := Types#{ Name => TypeDef },
|
{_, _, TName} = aeso_icode:qualify(Id, Icode),
|
||||||
|
Icode1 = Icode#{ types := Types#{ TName => TypeDef },
|
||||||
constructors := maps:merge(Constructors, NewConstructors) },
|
constructors := maps:merge(Constructors, NewConstructors) },
|
||||||
Icode2 = case Name of
|
Icode2 = case Name of
|
||||||
"state" when Args == [] -> Icode1#{ state_type => ast_typerep(Def, Icode) };
|
"state" when Args == [] -> Icode1#{ state_type => ast_typerep(Def, Icode) };
|
||||||
@ -108,9 +109,11 @@ contract_to_icode([{letrec,_,Defs}|Rest], Icode) ->
|
|||||||
%% just to parse a list of (mutually recursive) definitions.
|
%% just to parse a list of (mutually recursive) definitions.
|
||||||
contract_to_icode(Defs++Rest, Icode);
|
contract_to_icode(Defs++Rest, Icode);
|
||||||
contract_to_icode([], Icode) -> Icode;
|
contract_to_icode([], Icode) -> Icode;
|
||||||
contract_to_icode(_Code, Icode) ->
|
contract_to_icode([{fun_decl, _, _, _} | Code], Icode) ->
|
||||||
%% TODO debug output for debug("Unhandled code ~p~n",[Code]),
|
contract_to_icode(Code, Icode);
|
||||||
Icode.
|
contract_to_icode([Decl | Code], Icode) ->
|
||||||
|
io:format("Unhandled declaration: ~p\n", [Decl]),
|
||||||
|
contract_to_icode(Code, Icode).
|
||||||
|
|
||||||
ast_id({id, _, Id}) -> Id;
|
ast_id({id, _, Id}) -> Id;
|
||||||
ast_id({qid, _, Id}) -> Id.
|
ast_id({qid, _, Id}) -> Id.
|
||||||
@ -167,10 +170,10 @@ ast_body({qid, _, ["Chain", "spend"]}, _Icode) ->
|
|||||||
gen_error({underapplied_primitive, 'Chain.spend'});
|
gen_error({underapplied_primitive, 'Chain.spend'});
|
||||||
|
|
||||||
%% State
|
%% State
|
||||||
ast_body({id, _, "state"}, _Icode) -> prim_state;
|
ast_body({qid, _, [Con, "state"]}, #{ contract_name := Con }) -> prim_state;
|
||||||
ast_body(?id_app("put", [NewState], _, _), Icode) ->
|
ast_body(?qid_app([Con, "put"], [NewState], _, _), Icode = #{ contract_name := Con }) ->
|
||||||
#prim_put{ state = ast_body(NewState, Icode) };
|
#prim_put{ state = ast_body(NewState, Icode) };
|
||||||
ast_body({id, _, "put"}, _Icode) ->
|
ast_body({qid, _, [Con, "put"]}, #{ contract_name := Con }) ->
|
||||||
gen_error({underapplied_primitive, put}); %% TODO: eta
|
gen_error({underapplied_primitive, put}); %% TODO: eta
|
||||||
|
|
||||||
%% Abort
|
%% Abort
|
||||||
|
@ -161,8 +161,10 @@ create_calldata(Contract, Function, Argument) when is_map(Contract) ->
|
|||||||
|
|
||||||
|
|
||||||
get_arg_icode(Funs) ->
|
get_arg_icode(Funs) ->
|
||||||
[Args] = [ Args || {[_, ?CALL_NAME], _, _, {funcall, _, Args}, _} <- Funs ],
|
case [ Args || {[_, ?CALL_NAME], _, _, {funcall, _, Args}, _} <- Funs ] of
|
||||||
Args.
|
[Args] -> Args;
|
||||||
|
[] -> error({missing_call_function, Funs})
|
||||||
|
end.
|
||||||
|
|
||||||
get_call_type([{contract, _, _, Defs}]) ->
|
get_call_type([{contract, _, _, Defs}]) ->
|
||||||
case [ {lists:last(QFunName), FunType}
|
case [ {lists:last(QFunName), FunType}
|
||||||
|
@ -236,8 +236,10 @@ type({app_t, _, Type, Args}) ->
|
|||||||
beside(type(Type), tuple_type(Args));
|
beside(type(Type), tuple_type(Args));
|
||||||
type({tuple_t, _, Args}) ->
|
type({tuple_t, _, Args}) ->
|
||||||
tuple_type(Args);
|
tuple_type(Args);
|
||||||
type({named_arg_t, _, Name, Type, Default}) ->
|
type({named_arg_t, _, Name, Type, _Default}) ->
|
||||||
follow(hsep(typed(name(Name), Type), text("=")), expr(Default));
|
%% Drop the default value
|
||||||
|
%% follow(hsep(typed(name(Name), Type), text("=")), expr(Default));
|
||||||
|
typed(name(Name), Type);
|
||||||
|
|
||||||
type(R = {record_t, _}) -> typedef(R);
|
type(R = {record_t, _}) -> typedef(R);
|
||||||
type(T = {id, _, _}) -> name(T);
|
type(T = {id, _, _}) -> name(T);
|
||||||
|
@ -75,7 +75,8 @@ compilable_contracts() ->
|
|||||||
"builtin_bug",
|
"builtin_bug",
|
||||||
"builtin_map_get_bug",
|
"builtin_map_get_bug",
|
||||||
"nodeadcode",
|
"nodeadcode",
|
||||||
"deadcode"
|
"deadcode",
|
||||||
|
"variant_types"
|
||||||
].
|
].
|
||||||
|
|
||||||
%% Contracts that should produce type errors
|
%% Contracts that should produce type errors
|
||||||
@ -181,4 +182,11 @@ failing_contracts() ->
|
|||||||
, {"bad_events2",
|
, {"bad_events2",
|
||||||
[<<"The event constructor BadEvent1 (at line 9, column 7) has too many string values (max 1)">>,
|
[<<"The event constructor BadEvent1 (at line 9, column 7) has too many string values (max 1)">>,
|
||||||
<<"The event constructor BadEvent2 (at line 10, column 7) has too many indexed values (max 3)">>]}
|
<<"The event constructor BadEvent2 (at line 10, column 7) has too many indexed values (max 3)">>]}
|
||||||
|
, {"type_clash",
|
||||||
|
[<<"Cannot unify int\n"
|
||||||
|
" and string\n"
|
||||||
|
"when checking the record projection at line 12, column 40\n"
|
||||||
|
" r.foo : (gas : int, value : int) => Remote.themap\n"
|
||||||
|
"against the expected type\n"
|
||||||
|
" (gas : int, value : int) => map(string, int)">>]}
|
||||||
].
|
].
|
||||||
|
13
test/contracts/type_clash.aes
Normal file
13
test/contracts/type_clash.aes
Normal file
@ -0,0 +1,13 @@
|
|||||||
|
|
||||||
|
contract Remote =
|
||||||
|
|
||||||
|
type themap = map(int, string)
|
||||||
|
function foo : () => themap
|
||||||
|
|
||||||
|
contract Main =
|
||||||
|
|
||||||
|
type themap = map(string, int)
|
||||||
|
|
||||||
|
// Should fail
|
||||||
|
function foo(r : Remote) : themap = r.foo()
|
||||||
|
|
Loading…
x
Reference in New Issue
Block a user