Pushed the clone example through the typechecker

This commit is contained in:
radrow 2021-04-19 15:43:20 +02:00
parent dcb311a754
commit 59b9036a7b
5 changed files with 123 additions and 47 deletions

View File

@ -20,7 +20,7 @@
-include("aeso_utils.hrl"). -include("aeso_utils.hrl").
-type utype() :: {fun_t, aeso_syntax:ann(), named_args_t(), [utype()], utype()} -type utype() :: {fun_t, aeso_syntax:ann(), named_args_t(), [utype()] | var_args, utype()}
| {app_t, aeso_syntax:ann(), utype(), [utype()]} | {app_t, aeso_syntax:ann(), utype(), [utype()]}
| {tuple_t, aeso_syntax:ann(), [utype()]} | {tuple_t, aeso_syntax:ann(), [utype()]}
| aeso_syntax:id() | aeso_syntax:qid() | aeso_syntax:id() | aeso_syntax:qid()
@ -408,6 +408,7 @@ global_env() ->
FunC = fun(C, Ts, T) -> {type_sig, Ann, C, [], Ts, T} end, FunC = fun(C, Ts, T) -> {type_sig, Ann, C, [], Ts, T} end,
Fun = fun(Ts, T) -> FunC(none, Ts, T) end, Fun = fun(Ts, T) -> FunC(none, Ts, T) end,
Fun1 = fun(S, T) -> Fun([S], T) end, Fun1 = fun(S, T) -> Fun([S], T) end,
FunCN = fun(C, Named, Normal, Ret) -> {type_sig, Ann, C, Named, Normal, Ret} end,
%% Lambda = fun(Ts, T) -> {fun_t, Ann, [], Ts, T} end, %% Lambda = fun(Ts, T) -> {fun_t, Ann, [], Ts, T} end,
%% Lambda1 = fun(S, T) -> Lambda([S], T) end, %% Lambda1 = fun(S, T) -> Lambda([S], T) end,
StateFun = fun(Ts, T) -> {type_sig, [stateful|Ann], none, [], Ts, T} end, StateFun = fun(Ts, T) -> {type_sig, [stateful|Ann], none, [], Ts, T} end,
@ -473,7 +474,18 @@ global_env() ->
{"block_height", Int}, {"block_height", Int},
{"difficulty", Int}, {"difficulty", Int},
{"gas_limit", Int}, {"gas_limit", Int},
{"bytecode_hash", Fun1(Address, Option(Hash))}, {"bytecode_hash",Fun1(Address, Option(Hash))},
{"create", FunCN(create,
[ {named_arg_t, Ann, {id, Ann, "value"}, Int, {int, Ann, 0}}
, {named_arg_t, Ann, {id, Ann, "code"}, A, undefined}
], var_args, A)},
{"clone", FunCN(clone,
[ {named_arg_t, Ann, {id, Ann, "gas"}, Int,
{qid, Ann, ["Call","gas_left"]}}
, {named_arg_t, Ann, {id, Ann, "value"}, Int, {int, Ann, 0}}
, {named_arg_t, Ann, {id, Ann, "protected"}, Bool, {bool, Ann, false}}
, {named_arg_t, Ann, {id, Ann, "ref"}, A, undefined}
], var_args, A)},
%% Tx constructors %% Tx constructors
{"GAMetaTx", Fun([Address, Int], GAMetaTx)}, {"GAMetaTx", Fun([Address, Int], GAMetaTx)},
{"PayingForTx", Fun([Address, Int], PayForTx)}, {"PayingForTx", Fun([Address, Int], PayForTx)},
@ -1447,8 +1459,7 @@ infer_expr(Env, {typed, As, Body, Type}) ->
{typed, _, NewBody, NewType} = check_expr(Env, Body, Type1), {typed, _, NewBody, NewType} = check_expr(Env, Body, Type1),
{typed, As, NewBody, NewType}; {typed, As, NewBody, NewType};
infer_expr(Env, {app, Ann, Fun, Args0} = App) -> infer_expr(Env, {app, Ann, Fun, Args0} = App) ->
NamedArgs = [ Arg || Arg = {named_arg, _, _, _} <- Args0 ], {NamedArgs, Args} = split_args(Args0),
Args = Args0 -- NamedArgs,
case aeso_syntax:get_ann(format, Ann) of case aeso_syntax:get_ann(format, Ann) of
infix -> infix ->
infer_op(Env, Ann, Fun, Args, fun infer_infix/1); infer_op(Env, Ann, Fun, Args, fun infer_infix/1);
@ -1457,10 +1468,27 @@ infer_expr(Env, {app, Ann, Fun, Args0} = App) ->
_ -> _ ->
NamedArgsVar = fresh_uvar(Ann), NamedArgsVar = fresh_uvar(Ann),
NamedArgs1 = [ infer_named_arg(Env, NamedArgsVar, Arg) || Arg <- NamedArgs ], NamedArgs1 = [ infer_named_arg(Env, NamedArgsVar, Arg) || Arg <- NamedArgs ],
%% TODO: named args constraints NewFun = {typed, _, _, FunType0} = infer_expr(Env, Fun),
NewFun={typed, _, _, FunType} = infer_expr(Env, Fun),
NewArgs = [infer_expr(Env, A) || A <- Args], NewArgs = [infer_expr(Env, A) || A <- Args],
ArgTypes = [T || {typed, _, _, T} <- NewArgs], ArgTypes = [T || {typed, _, _, T} <- NewArgs],
FunType =
case Fun of
{qid, _, ["Chain", "clone"]} ->
{fun_t, FunAnn, NamedArgsT, var_args, RetT} = FunType0,
{typed, CAnn, Contract, ContractT} =
case [Contract || {named_arg, _, {id, _, "ref"}, Contract} <- NamedArgs1] of
[C] -> C;
_ -> type_error({clone_no_contract, Ann})
end,
NamedArgsTNoRef =
lists:filter(fun({named_arg_t, _, {id, _, "ref"}, _, _}) -> false; (_) -> true end, NamedArgsT),
{typed, _, _, InitT} =
infer_expr(Env, {proj, CAnn, Contract, {id, [], "init"}}),
unify(Env, InitT, {fun_t, FunAnn, NamedArgsTNoRef, ArgTypes, fresh_uvar(CAnn)}, checking_init_todo),
unify(Env, RetT, ContractT, dupadupa_todo),
{fun_t, FunAnn, NamedArgsT, ArgTypes, RetT};
_ -> FunType0
end,
GeneralResultType = fresh_uvar(Ann), GeneralResultType = fresh_uvar(Ann),
ResultType = fresh_uvar(Ann), ResultType = fresh_uvar(Ann),
When = {infer_app, Fun, NamedArgs1, Args, FunType, ArgTypes}, When = {infer_app, Fun, NamedArgs1, Args, FunType, ArgTypes},
@ -1576,6 +1604,11 @@ infer_expr(Env, Let = {letfun, Attrs, _, _, _, _}) ->
type_error({missing_body_for_let, Attrs}), type_error({missing_body_for_let, Attrs}),
infer_expr(Env, {block, Attrs, [Let, abort_expr(Attrs, "missing body")]}). infer_expr(Env, {block, Attrs, [Let, abort_expr(Attrs, "missing body")]}).
split_args(Args0) ->
NamedArgs = [ Arg || Arg = {named_arg, _, _, _} <- Args0 ],
Args = Args0 -- NamedArgs,
{NamedArgs, Args}.
infer_named_arg(Env, NamedArgs, {named_arg, Ann, Id, E}) -> infer_named_arg(Env, NamedArgs, {named_arg, Ann, Id, E}) ->
CheckedExpr = {typed, _, _, ArgType} = infer_expr(Env, E), CheckedExpr = {typed, _, _, ArgType} = infer_expr(Env, E),
check_stateful_named_arg(Env, Id, E), check_stateful_named_arg(Env, Id, E),
@ -2348,6 +2381,8 @@ unify1(_Env, {bytes_t, _, Len}, {bytes_t, _, Len}, _When) ->
unify1(Env, {if_t, _, {id, _, Id}, Then1, Else1}, {if_t, _, {id, _, Id}, Then2, Else2}, When) -> unify1(Env, {if_t, _, {id, _, Id}, Then1, Else1}, {if_t, _, {id, _, Id}, Then2, Else2}, When) ->
unify(Env, Then1, Then2, When) andalso unify(Env, Then1, Then2, When) andalso
unify(Env, Else1, Else2, When); unify(Env, Else1, Else2, When);
unify1(Env, {fun_t, _, Named1, var_args, Result1}, {fun_t, _, Named2, Args2, Result2}, When) ->
error(unify_varargs); %% TODO
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)
when length(Args1) == length(Args2) -> when length(Args1) == length(Args2) ->
unify(Env, Named1, Named2, When) andalso unify(Env, Named1, Named2, When) andalso
@ -2358,6 +2393,9 @@ unify1(Env, {app_t, _, {Tag, _, F}, Args1}, {app_t, _, {Tag, _, F}, 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) ->
unify(Env, As, Bs, When); unify(Env, As, Bs, When);
unify1(Env, {named_arg_t, _, Id1, Type1, _}, {named_arg_t, _, Id2, Type2, _}, When) ->
unify1(Env, Id1, Id2, {arg_name, When}), %% TODO
unify1(Env, Type1, Type2, When);
%% The grammar is a bit inconsistent about whether types without %% The grammar is a bit inconsistent about whether types without
%% arguments are represented as applications to an empty list of %% arguments are represented as applications to an empty list of
%% parameters or not. We therefore allow them to unify. %% parameters or not. We therefore allow them to unify.
@ -2465,7 +2503,9 @@ apply_typesig_constraint(Ann, address_to_contract, {fun_t, _, [], [_], Type}) ->
apply_typesig_constraint(Ann, bytes_concat, {fun_t, _, [], [A, B], C}) -> apply_typesig_constraint(Ann, bytes_concat, {fun_t, _, [], [A, B], C}) ->
add_bytes_constraint({add_bytes, Ann, concat, A, B, C}); add_bytes_constraint({add_bytes, Ann, concat, A, B, C});
apply_typesig_constraint(Ann, bytes_split, {fun_t, _, [], [C], {tuple_t, _, [A, B]}}) -> apply_typesig_constraint(Ann, bytes_split, {fun_t, _, [], [C], {tuple_t, _, [A, B]}}) ->
add_bytes_constraint({add_bytes, Ann, split, A, B, C}). add_bytes_constraint({add_bytes, Ann, split, A, B, C});
apply_typesig_constraint(Ann, clone, {fun_t, _, Named, var_args, Ret}) ->
ok.
%% Dereferences all uvars and replaces the uninstantiated ones with a %% Dereferences all uvars and replaces the uninstantiated ones with a
%% succession of tvars. %% succession of tvars.

View File

@ -139,7 +139,7 @@
-type fun_env() :: #{ sophia_name() => {fun_name(), non_neg_integer()} }. -type fun_env() :: #{ sophia_name() => {fun_name(), non_neg_integer()} }.
-type con_env() :: #{ sophia_name() => con_tag() }. -type con_env() :: #{ sophia_name() => con_tag() }.
-type child_con_env() :: #{sophia_name() => fcode()}. -type child_con_env() :: #{sophia_name() => fcode()}.
-type builtins() :: #{ sophia_name() => {builtin(), non_neg_integer() | none} }. -type builtins() :: #{ sophia_name() => {builtin(), non_neg_integer() | none | variable} }.
-type context() :: {main_contract, string()} -type context() :: {main_contract, string()}
| {namespace, string()} | {namespace, string()}
@ -232,7 +232,7 @@ builtins() ->
Scopes = [{[], [{"abort", 1}, {"require", 2}]}, Scopes = [{[], [{"abort", 1}, {"require", 2}]},
{["Chain"], [{"spend", 2}, {"balance", 1}, {"block_hash", 1}, {"coinbase", none}, {["Chain"], [{"spend", 2}, {"balance", 1}, {"block_hash", 1}, {"coinbase", none},
{"timestamp", none}, {"block_height", none}, {"difficulty", none}, {"timestamp", none}, {"block_height", none}, {"difficulty", none},
{"gas_limit", none}]}, {"gas_limit", none}, {"bytecode_hash", 1}, {"create", variable}, {"clone", variable}]},
{["Contract"], [{"address", none}, {"balance", none}, {"creator", none}]}, {["Contract"], [{"address", none}, {"balance", none}, {"creator", none}]},
{["Call"], [{"origin", none}, {"caller", none}, {"value", none}, {"gas_price", none}, {["Call"], [{"origin", none}, {"caller", none}, {"value", none}, {"gas_price", none},
{"gas_left", 0}]}, {"gas_left", 0}]},
@ -692,11 +692,18 @@ expr_to_fcode(Env, _Type, {app, _Ann, {Op, _}, [A]}) when is_atom(Op) ->
end; end;
%% Function calls %% Function calls
expr_to_fcode(Env, _Type, {app, _, Fun = {typed, _, _, {fun_t, _, NamedArgsT, _, _}}, Args}) -> expr_to_fcode(Env, _Type, {app, _, Fun = {typed, _, _, {fun_t, _, NamedArgsT, ArgsT, _}}, Args}) ->
Args1 = get_named_args(NamedArgsT, Args), Args1 = get_named_args(NamedArgsT, Args),
FArgs = [expr_to_fcode(Env, Arg) || Arg <- Args1], FArgs = [expr_to_fcode(Env, Arg) || Arg <- Args1],
case expr_to_fcode(Env, Fun) of case expr_to_fcode(Env, Fun) of
{builtin_u, B, _Ar, TypeArgs} -> builtin_to_fcode(state_layout(Env), B, FArgs ++ TypeArgs); {builtin_u, B, _Ar, TypeArgs} -> builtin_to_fcode(state_layout(Env), B, FArgs ++ TypeArgs);
{builtin_u, chain_clone, _Ar} ->
case ArgsT of
[_Con|InitArgs] ->
FInitArgsT = {tuple, [type_to_fcode(Env, T) || T <- InitArgs]},
builtin_to_fcode(state_layout(Env), chain_clone, [FInitArgsT|FArgs]);
[] -> error(wtf) %% FIXME
end;
{builtin_u, B, _Ar} -> builtin_to_fcode(state_layout(Env), B, FArgs); {builtin_u, B, _Ar} -> builtin_to_fcode(state_layout(Env), B, FArgs);
{def_u, F, _Ar} -> {def, F, FArgs}; {def_u, F, _Ar} -> {def, F, FArgs};
{remote_u, ArgsT, RetT, Ct, RFun} -> {remote, ArgsT, RetT, Ct, RFun, FArgs}; {remote_u, ArgsT, RetT, Ct, RFun} -> {remote, ArgsT, RetT, Ct, RFun, FArgs};

View File

@ -555,7 +555,31 @@ builtin_to_scode(Env, aens_lookup, [_Name] = Args) ->
builtin_to_scode(_Env, auth_tx_hash, []) -> builtin_to_scode(_Env, auth_tx_hash, []) ->
[aeb_fate_ops:auth_tx_hash(?a)]; [aeb_fate_ops:auth_tx_hash(?a)];
builtin_to_scode(_Env, auth_tx, []) -> builtin_to_scode(_Env, auth_tx, []) ->
[aeb_fate_ops:auth_tx(?a)]. [aeb_fate_ops:auth_tx(?a)];
builtin_to_scode(Env, chain_bytecode_hash, [_Addr] = Args) ->
call_to_scode(Env, aeb_fate_ops:bytecode_hash(?a), Args);
builtin_to_scode(Env, chain_clone,
[InitArgs, _GasCap = {con,[0,1],0,[]}, Prot, Value, Contract | InitArgs]) ->
error(InitArgs),
TypeRep = xd,
call_to_scode(Env, aeb_fate_ops:clone(?a, ?a, ?a, ?a),
[Contract, TypeRep, Value, Prot | InitArgs]
);
builtin_to_scode(Env, chain_clone,
[_GasCap = {con,[0,1],0,[]}, Prot, Value, Contract | InitArgs]) ->
TypeRep = xd,
call_to_scode(Env, aeb_fate_ops:clone(?a, ?a, ?a, ?a),
[Contract, TypeRep, Value, Prot | InitArgs]
);
builtin_to_scode(Env, chain_create,
[_GasCap = {con,[0,1],0,[]}, Prot, Value, Contract | InitArgs]) ->
TypeRep = xd,
call_to_scode(Env, aeb_fate_ops:clone(?a, ?a, ?a, ?a),
[Contract, TypeRep, Value, Prot | InitArgs]
).
%% -- Operators -- %% -- Operators --

View File

@ -23,6 +23,7 @@ test_cases(1) ->
#{name => <<"C">>, #{name => <<"C">>,
type_defs => [], type_defs => [],
payable => true, payable => true,
kind => contract_main,
functions => functions =>
[#{name => <<"a">>, [#{name => <<"a">>,
arguments => arguments =>
@ -31,16 +32,17 @@ test_cases(1) ->
returns => <<"int">>, returns => <<"int">>,
stateful => true, stateful => true,
payable => true}]}}, payable => true}]}},
DecACI = <<"payable contract C =\n" DecACI = <<"payable main contract C =\n"
" payable entrypoint a : (int) => int\n">>, " payable entrypoint a : (int) => int\n">>,
{Contract,MapACI,DecACI}; {Contract,MapACI,DecACI};
test_cases(2) -> test_cases(2) ->
Contract = <<"contract C =\n" Contract = <<"main contract C =\n"
" type allan = int\n" " type allan = int\n"
" entrypoint a(i : allan) = i+1\n">>, " entrypoint a(i : allan) = i+1\n">>,
MapACI = #{contract => MapACI = #{contract =>
#{name => <<"C">>, payable => false, #{name => <<"C">>, payable => false,
kind => contract_main,
type_defs => type_defs =>
[#{name => <<"allan">>, [#{name => <<"allan">>,
typedef => <<"int">>, typedef => <<"int">>,
@ -53,12 +55,12 @@ test_cases(2) ->
returns => <<"int">>, returns => <<"int">>,
stateful => false, stateful => false,
payable => false}]}}, payable => false}]}},
DecACI = <<"contract C =\n" DecACI = <<"main contract C =\n"
" type allan = int\n" " type allan = int\n"
" entrypoint a : (C.allan) => int\n">>, " entrypoint a : (C.allan) => int\n">>,
{Contract,MapACI,DecACI}; {Contract,MapACI,DecACI};
test_cases(3) -> test_cases(3) ->
Contract = <<"contract C =\n" Contract = <<"main contract C =\n"
" type state = unit\n" " type state = unit\n"
" datatype event = SingleEventDefined\n" " datatype event = SingleEventDefined\n"
" datatype bert('a) = Bin('a)\n" " datatype bert('a) = Bin('a)\n"
@ -71,7 +73,7 @@ test_cases(3) ->
#{<<"C.bert">> => [<<"string">>]}}], #{<<"C.bert">> => [<<"string">>]}}],
name => <<"a">>,returns => <<"int">>, name => <<"a">>,returns => <<"int">>,
stateful => false, payable => false}], stateful => false, payable => false}],
name => <<"C">>, payable => false, name => <<"C">>, payable => false, kind => contract_main,
event => #{variant => [#{<<"SingleEventDefined">> => []}]}, event => #{variant => [#{<<"SingleEventDefined">> => []}]},
state => <<"unit">>, state => <<"unit">>,
type_defs => type_defs =>
@ -80,7 +82,7 @@ test_cases(3) ->
#{variant => #{variant =>
[#{<<"Bin">> => [<<"'a">>]}]}, [#{<<"Bin">> => [<<"'a">>]}]},
vars => [#{name => <<"'a">>}]}]}}, vars => [#{name => <<"'a">>}]}]}},
DecACI = <<"contract C =\n" DecACI = <<"main contract C =\n"
" type state = unit\n" " type state = unit\n"
" datatype event = SingleEventDefined\n" " datatype event = SingleEventDefined\n"
" datatype bert('a) = Bin('a)\n" " datatype bert('a) = Bin('a)\n"

View File

@ -127,6 +127,7 @@ compile(Backend, Name, Options) ->
%% compilable_contracts() -> [ContractName]. %% compilable_contracts() -> [ContractName].
%% The currently compilable contracts. %% The currently compilable contracts.
compilable_contracts() -> ["clone"]; % FIXME remove
compilable_contracts() -> compilable_contracts() ->
["complex_types", ["complex_types",
"counter", "counter",
@ -180,7 +181,8 @@ compilable_contracts() ->
"more_strings", "more_strings",
"protected_call", "protected_call",
"hermetization_turnoff", "hermetization_turnoff",
"multiple_contracts" "multiple_contracts",
"clone"
]. ].
not_compilable_on(fate) -> []; not_compilable_on(fate) -> [];
@ -205,6 +207,7 @@ debug_mode_contracts() ->
-define(TYPE_ERROR(Name, Errs), ?ERROR("Type", Name, Errs)). -define(TYPE_ERROR(Name, Errs), ?ERROR("Type", Name, Errs)).
-define(PARSE_ERROR(Name, Errs), ?ERROR("Parse", Name, Errs)). -define(PARSE_ERROR(Name, Errs), ?ERROR("Parse", Name, Errs)).
failing_contracts() -> []; % FIXME remove
failing_contracts() -> failing_contracts() ->
{ok, V} = aeso_compiler:numeric_version(), {ok, V} = aeso_compiler:numeric_version(),
Version = list_to_binary(string:join([integer_to_list(N) || N <- V], ".")), Version = list_to_binary(string:join([integer_to_list(N) || N <- V], ".")),