Add 'protected' named argument to remote calls

If protected = true, the return type is wrapped in an option() which comes back
None if the remote call fails for any reason.
This commit is contained in:
Ulf Norell 2020-02-24 14:32:04 +01:00
parent d0caee24d9
commit ecbc15db1b
3 changed files with 95 additions and 20 deletions

View File

@ -20,6 +20,7 @@
| aeso_syntax:id() | aeso_syntax:qid() | aeso_syntax:id() | aeso_syntax:qid()
| aeso_syntax:con() | aeso_syntax:qcon() %% contracts | aeso_syntax:con() | aeso_syntax:qcon() %% contracts
| aeso_syntax:tvar() | aeso_syntax:tvar()
| {if_t, aeso_syntax:ann(), aeso_syntax:id(), utype(), utype()} %% Can branch on named argument (protected)
| uvar(). | uvar().
-type uvar() :: {uvar, aeso_syntax:ann(), reference()}. -type uvar() :: {uvar, aeso_syntax:ann(), reference()}.
@ -43,7 +44,14 @@
name :: aeso_syntax:id(), name :: aeso_syntax:id(),
type :: utype()}). type :: utype()}).
-type named_argument_constraint() :: #named_argument_constraint{}. -record(dependent_type_constraint,
{ named_args_t :: utype()
, named_args :: [aeso_syntax:arg_expr()]
, general_type :: utype()
, specialized_type :: utype()
, context :: term() }).
-type named_argument_constraint() :: #named_argument_constraint{} | #dependent_type_constraint{}.
-record(field_constraint, -record(field_constraint,
{ record_t :: utype() { record_t :: utype()
@ -232,16 +240,21 @@ bind_fields([], Env) -> Env;
bind_fields([{Id, Info} | Rest], Env) -> bind_fields([{Id, Info} | Rest], Env) ->
bind_fields(Rest, bind_field(Id, Info, Env)). bind_fields(Rest, bind_field(Id, Info, Env)).
%% Contract entrypoints take two named arguments (gas : int = Call.gas_left(), value : int = 0). %% Contract entrypoints take three named arguments
%% gas : int = Call.gas_left()
%% value : int = 0
%% protected : bool = false
contract_call_type({fun_t, Ann, [], Args, Ret}) -> contract_call_type({fun_t, Ann, [], Args, Ret}) ->
Id = fun(X) -> {id, Ann, X} end, Id = fun(X) -> {id, Ann, X} end,
Int = Id("int"), Int = Id("int"),
Typed = fun(E, T) -> {typed, Ann, E, T} end, Typed = fun(E, T) -> {typed, Ann, E, T} end,
Named = fun(Name, Default) -> {named_arg_t, Ann, Id(Name), Int, Default} end, Named = fun(Name, Default = {typed, _, _, T}) -> {named_arg_t, Ann, Id(Name), T, Default} end,
{fun_t, Ann, [Named("gas", Typed({app, Ann, Typed({qid, Ann, ["Call", "gas_left"]}, {fun_t, Ann, [Named("gas", Typed({app, Ann, Typed({qid, Ann, ["Call", "gas_left"]},
{fun_t, Ann, [], [], Int}), {fun_t, Ann, [], [], Int}),
[]}, Int)), []}, Int)),
Named("value", Typed({int, Ann, 0}, Int))], Args, Ret}. Named("value", Typed({int, Ann, 0}, Int)),
Named("protected", Typed({bool, Ann, false}, Id("bool")))],
Args, {if_t, Ann, Id("protected"), {app_t, Ann, {id, Ann, "option"}, [Ret]}, Ret}}.
-spec bind_contract(aeso_syntax:decl(), env()) -> env(). -spec bind_contract(aeso_syntax:decl(), env()) -> env().
bind_contract({contract, Ann, Id, Contents}, Env) -> bind_contract({contract, Ann, Id, Contents}, Env) ->
@ -1374,8 +1387,16 @@ infer_expr(Env, {app, Ann, Fun, Args0}) ->
NewFun={typed, _, _, FunType} = 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],
GeneralResultType = fresh_uvar(Ann),
ResultType = fresh_uvar(Ann), ResultType = fresh_uvar(Ann),
unify(Env, FunType, {fun_t, [], NamedArgsVar, ArgTypes, ResultType}, {infer_app, Fun, Args, FunType, ArgTypes}), When = {infer_app, Fun, NamedArgs1, Args, FunType, ArgTypes},
unify(Env, FunType, {fun_t, [], NamedArgsVar, ArgTypes, GeneralResultType}, When),
add_named_argument_constraint(
[#dependent_type_constraint{ named_args_t = NamedArgsVar,
named_args = NamedArgs1,
general_type = GeneralResultType,
specialized_type = ResultType,
context = When }]),
{typed, Ann, {app, Ann, NewFun, NamedArgs1 ++ NewArgs}, dereference(ResultType)} {typed, Ann, {app, Ann, NewFun, NamedArgs1 ++ NewArgs}, dereference(ResultType)}
end; end;
infer_expr(Env, {'if', Attrs, Cond, Then, Else}) -> infer_expr(Env, {'if', Attrs, Cond, Then, Else}) ->
@ -1534,7 +1555,7 @@ infer_op(Env, As, Op, Args, InferOp) ->
TypedArgs = [infer_expr(Env, A) || A <- Args], TypedArgs = [infer_expr(Env, A) || A <- Args],
ArgTypes = [T || {typed, _, _, T} <- TypedArgs], ArgTypes = [T || {typed, _, _, T} <- TypedArgs],
Inferred = {fun_t, _, _, OperandTypes, ResultType} = InferOp(Op), Inferred = {fun_t, _, _, OperandTypes, ResultType} = InferOp(Op),
unify(Env, ArgTypes, OperandTypes, {infer_app, Op, Args, Inferred, ArgTypes}), unify(Env, ArgTypes, OperandTypes, {infer_app, Op, [], Args, Inferred, ArgTypes}),
{typed, As, {app, As, Op, TypedArgs}, ResultType}. {typed, As, {app, As, Op, TypedArgs}, ResultType}.
infer_pattern(Env, Pattern) -> infer_pattern(Env, Pattern) ->
@ -1705,12 +1726,12 @@ create_constraints() ->
create_field_constraints(). create_field_constraints().
destroy_and_report_unsolved_constraints(Env) -> destroy_and_report_unsolved_constraints(Env) ->
solve_field_constraints(Env),
solve_named_argument_constraints(Env), solve_named_argument_constraints(Env),
solve_bytes_constraints(Env), solve_bytes_constraints(Env),
solve_field_constraints(Env),
destroy_and_report_unsolved_field_constraints(Env),
destroy_and_report_unsolved_bytes_constraints(Env), destroy_and_report_unsolved_bytes_constraints(Env),
destroy_and_report_unsolved_named_argument_constraints(Env). destroy_and_report_unsolved_named_argument_constraints(Env),
destroy_and_report_unsolved_field_constraints(Env).
%% -- Named argument constraints -- %% -- Named argument constraints --
@ -1750,8 +1771,42 @@ check_named_argument_constraint(Env,
type_error({bad_named_argument, Args, Id}), type_error({bad_named_argument, Args, Id}),
false; false;
[T] -> unify(Env, T, Type, {check_named_arg_constraint, C}), true [T] -> unify(Env, T, Type, {check_named_arg_constraint, C}), true
end;
check_named_argument_constraint(Env,
#dependent_type_constraint{ named_args_t = NamedArgsT0,
named_args = NamedArgs,
general_type = GenType,
specialized_type = SpecType,
context = When }) ->
NamedArgsT = dereference(NamedArgsT0),
case dereference(NamedArgsT0) of
[_ | _] = NamedArgsT ->
GetVal = fun(Name, Default) ->
hd([ Val || {named_arg, _, {id, _, N}, Val} <- NamedArgs, N == Name] ++
[ Default ])
end,
ArgEnv = maps:from_list([ {Name, GetVal(Name, Default)}
|| {named_arg_t, _, {id, _, Name}, _, Default} <- NamedArgsT ]),
unify(Env, specialize_dependent_type(ArgEnv, GenType), SpecType, When),
true;
_ -> unify(Env, GenType, SpecType, When), true
end. end.
specialize_dependent_type(Env, Type) ->
case dereference(Type) of
{if_t, _, {id, _, Arg}, Then, Else} ->
Val = maps:get(Arg, Env),
case Val of
{typed, _, {bool, _, true}, _} -> Then;
{typed, _, {bool, _, false}, _} -> Else;
_ ->
type_error({named_argument_must_be_literal_bool, Arg, Val}),
fresh_uvar(aeso_syntax:get_ann(Val))
end;
_ -> Type %% Currently no deep dependent types
end.
destroy_and_report_unsolved_named_argument_constraints(Env) -> destroy_and_report_unsolved_named_argument_constraints(Env) ->
Unsolved = solve_named_argument_constraints(Env, get_named_argument_constraints()), Unsolved = solve_named_argument_constraints(Env, get_named_argument_constraints()),
[ type_error({unsolved_named_argument_constraint, C}) || C <- Unsolved ], [ type_error({unsolved_named_argument_constraint, C}) || C <- Unsolved ],
@ -1977,9 +2032,11 @@ destroy_and_report_unsolved_field_constraints(Env) ->
{FieldCs, OtherCs} = {FieldCs, OtherCs} =
lists:partition(fun(#field_constraint{}) -> true; (_) -> false end, lists:partition(fun(#field_constraint{}) -> true; (_) -> false end,
get_field_constraints()), get_field_constraints()),
{CreateCs, ContractCs} = {CreateCs, OtherCs1} =
lists:partition(fun(#record_create_constraint{}) -> true; (_) -> false end, lists:partition(fun(#record_create_constraint{}) -> true; (_) -> false end,
OtherCs), OtherCs),
{ContractCs, []} =
lists:partition(fun(#is_contract_constraint{}) -> true; (_) -> false end, OtherCs1),
Unknown = solve_known_record_types(Env, FieldCs), Unknown = solve_known_record_types(Env, FieldCs),
if Unknown == [] -> ok; if Unknown == [] -> ok;
true -> true ->
@ -2185,6 +2242,9 @@ unify1(_Env, {qcon, _, Name}, {qcon, _, Name}, _When) ->
true; true;
unify1(_Env, {bytes_t, _, Len}, {bytes_t, _, Len}, _When) -> unify1(_Env, {bytes_t, _, Len}, {bytes_t, _, Len}, _When) ->
true; 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, {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);
@ -2245,6 +2305,8 @@ occurs_check1(R, {record_t, Fields}) ->
occurs_check(R, Fields); occurs_check(R, Fields);
occurs_check1(R, {field_t, _, _, T}) -> occurs_check1(R, {field_t, _, _, T}) ->
occurs_check(R, T); occurs_check(R, T);
occurs_check1(R, {if_t, _, _, Then, Else}) ->
occurs_check(R, [Then, Else]);
occurs_check1(R, [H | T]) -> occurs_check1(R, [H | T]) ->
occurs_check(R, H) orelse occurs_check(R, T); occurs_check(R, H) orelse occurs_check(R, T);
occurs_check1(_, []) -> false. occurs_check1(_, []) -> false.
@ -2641,6 +2703,9 @@ mk_error({mixed_record_and_map, Expr}) ->
Msg = io_lib:format("Mixed record fields and map keys in\n~s", Msg = io_lib:format("Mixed record fields and map keys in\n~s",
[pp_expr(" ", Expr)]), [pp_expr(" ", Expr)]),
mk_t_err(pos(Expr), Msg); mk_t_err(pos(Expr), Msg);
mk_error({named_argument_must_be_literal_bool, Name, Arg}) ->
Msg = io_lib:format("Invalid '~s' argument\n~s\nIt must be either 'true' or 'false'.", [Name, pp_expr(" ", instantiate(Arg))]),
mk_t_err(pos(Arg), Msg);
mk_error(Err) -> mk_error(Err) ->
Msg = io_lib:format("Unknown error: ~p\n", [Err]), Msg = io_lib:format("Unknown error: ~p\n", [Err]),
mk_t_err(pos(0, 0), Msg). mk_t_err(pos(0, 0), Msg).
@ -2659,7 +2724,7 @@ pp_when({check_typesig, Name, Inferred, Given}) ->
" inferred type: ~s\n" " inferred type: ~s\n"
" given type: ~s\n", " given type: ~s\n",
[Name, pp_loc(Given), pp(instantiate(Inferred)), pp(instantiate(Given))])}; [Name, pp_loc(Given), pp(instantiate(Inferred)), pp(instantiate(Given))])};
pp_when({infer_app, Fun, Args, Inferred0, ArgTypes0}) -> pp_when({infer_app, Fun, NamedArgs, Args, Inferred0, ArgTypes0}) ->
Inferred = instantiate(Inferred0), Inferred = instantiate(Inferred0),
ArgTypes = instantiate(ArgTypes0), ArgTypes = instantiate(ArgTypes0),
{pos(Fun), {pos(Fun),
@ -2668,6 +2733,7 @@ pp_when({infer_app, Fun, Args, Inferred0, ArgTypes0}) ->
"to arguments\n~s", "to arguments\n~s",
[pp_loc(Fun), [pp_loc(Fun),
pp_typed(" ", Fun, Inferred), pp_typed(" ", Fun, Inferred),
[ [pp_expr(" ", NamedArg), "\n"] || NamedArg <- NamedArgs ] ++
[ [pp_typed(" ", Arg, ArgT), "\n"] [ [pp_typed(" ", Arg, ArgT), "\n"]
|| {Arg, ArgT} <- lists:zip(Args, ArgTypes) ] ])}; || {Arg, ArgT} <- lists:zip(Args, ArgTypes) ] ])};
pp_when({field_constraint, FieldType0, InferredType0, Fld}) -> pp_when({field_constraint, FieldType0, InferredType0, Fld}) ->
@ -2744,6 +2810,12 @@ pp_when({list_comp, BindExpr, Inferred0, Expected0}) ->
io_lib:format("when checking rvalue of list comprehension binding at ~s\n~s\n" io_lib:format("when checking rvalue of list comprehension binding at ~s\n~s\n"
"against type \n~s\n", "against type \n~s\n",
[pp_loc(BindExpr), pp_typed(" ", BindExpr, Inferred), pp_type(" ", Expected)])}; [pp_loc(BindExpr), pp_typed(" ", BindExpr, Inferred), pp_type(" ", Expected)])};
pp_when({check_named_arg_constraint, C}) ->
{id, _, Name} = Arg = C#named_argument_constraint.name,
[Type | _] = [ Type || {named_arg_t, _, {id, _, Name1}, Type, _} <- C#named_argument_constraint.args, Name1 == Name ],
Err = io_lib:format("when checking named argument\n~s\nagainst inferred type\n~s",
[pp_typed(" ", Arg, Type), pp_type(" ", C#named_argument_constraint.type)]),
{pos(Arg), Err};
pp_when(unknown) -> {pos(0,0), ""}. pp_when(unknown) -> {pos(0,0), ""}.
-spec pp_why_record(why_record()) -> {pos(), iolist()}. -spec pp_why_record(why_record()) -> {pos(), iolist()}.
@ -2821,6 +2893,8 @@ pp({uvar, _, Ref}) ->
["?u" | integer_to_list(erlang:phash2(Ref, 16384)) ]; ["?u" | integer_to_list(erlang:phash2(Ref, 16384)) ];
pp({tvar, _, Name}) -> pp({tvar, _, Name}) ->
Name; Name;
pp({if_t, _, Id, Then, Else}) ->
["if(", pp([Id, Then, Else]), ")"];
pp({tuple_t, _, []}) -> pp({tuple_t, _, []}) ->
"unit"; "unit";
pp({tuple_t, _, Cpts}) -> pp({tuple_t, _, Cpts}) ->
@ -2832,8 +2906,8 @@ pp({app_t, _, T, []}) ->
pp(T); pp(T);
pp({app_t, _, Type, Args}) -> pp({app_t, _, Type, Args}) ->
[pp(Type), "(", 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({fun_t, _, Named = {uvar, _, _}, As, B}) -> pp({fun_t, _, Named = {uvar, _, _}, As, B}) ->
["(", pp(Named), " | ", pp(As), ") => ", pp(B)]; ["(", pp(Named), " | ", pp(As), ") => ", pp(B)];
pp({fun_t, _, Named, As, B}) when is_list(Named) -> pp({fun_t, _, Named, As, B}) when is_list(Named) ->

View File

@ -468,6 +468,8 @@ type_to_fcode(Env, Sub, {fun_t, _, Named, Args, Res}) ->
FNamed = [type_to_fcode(Env, Sub, Arg) || {named_arg_t, _, _, Arg, _} <- Named], FNamed = [type_to_fcode(Env, Sub, Arg) || {named_arg_t, _, _, Arg, _} <- Named],
FArgs = [type_to_fcode(Env, Sub, Arg) || Arg <- Args], FArgs = [type_to_fcode(Env, Sub, Arg) || Arg <- Args],
{function, FNamed ++ FArgs, type_to_fcode(Env, Sub, Res)}; {function, FNamed ++ FArgs, type_to_fcode(Env, Sub, Res)};
type_to_fcode(Env, Sub, {if_t, _, _, _, Else}) ->
type_to_fcode(Env, Sub, Else); %% Hacky: this is only for remote calls, in which case we want the unprotected type
type_to_fcode(_Env, _Sub, Type) -> type_to_fcode(_Env, _Sub, Type) ->
error({todo, Type}). error({todo, Type}).

View File

@ -257,6 +257,8 @@ type({args_t, _, Args}) ->
type({bytes_t, _, any}) -> text("bytes(_)"); type({bytes_t, _, any}) -> text("bytes(_)");
type({bytes_t, _, Len}) -> type({bytes_t, _, Len}) ->
text(lists:concat(["bytes(", Len, ")"])); text(lists:concat(["bytes(", Len, ")"]));
type({if_t, _, Id, Then, Else}) ->
beside(text("if"), args_type([Id, Then, Else]));
type({named_arg_t, _, Name, Type, _Default}) -> type({named_arg_t, _, Name, Type, _Default}) ->
%% Drop the default value %% Drop the default value
%% follow(hsep(typed(name(Name), Type), text("=")), expr(Default)); %% follow(hsep(typed(name(Name), Type), text("=")), expr(Default));
@ -283,12 +285,9 @@ tuple_type(Factors) ->
, text(")") , text(")")
]). ]).
-spec arg_expr(aeso_syntax:arg_expr()) -> doc(). -spec expr_p(integer(), aeso_syntax:arg_expr()) -> doc().
arg_expr({named_arg, _, Name, E}) -> expr_p(P, {named_arg, _, Name, E}) ->
follow(hsep(expr(Name), text("=")), expr(E)); paren(P > 100, follow(hsep(expr(Name), text("=")), expr(E)));
arg_expr(E) -> expr(E).
-spec expr_p(integer(), aeso_syntax:expr()) -> doc().
expr_p(P, {lam, _, Args, E}) -> expr_p(P, {lam, _, Args, E}) ->
paren(P > 100, follow(hsep(args(Args), text("=>")), expr_p(100, E))); paren(P > 100, follow(hsep(args(Args), text("=>")), expr_p(100, E)));
expr_p(P, If = {'if', Ann, Cond, Then, Else}) -> expr_p(P, If = {'if', Ann, Cond, Then, Else}) ->
@ -447,7 +446,7 @@ prefix(P, Op, A) ->
app(P, F, Args) -> app(P, F, Args) ->
paren(P > 900, paren(P > 900,
beside(expr_p(900, F), beside(expr_p(900, F),
tuple(lists:map(fun arg_expr/1, Args)))). tuple(lists:map(fun expr/1, Args)))).
field({field, _, LV, E}) -> field({field, _, LV, E}) ->
follow(hsep(lvalue(LV), text("=")), expr(E)); follow(hsep(lvalue(LV), text("=")), expr(E));