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

Split constraints from type checker

Browse Source
This commit is contained in:
Gaith Hallak 2023-04-29 11:25:55 +03:00
parent 9fe2696432
commit 565863681c
5 changed files with 629 additions and 541 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

589
src/aeso_ast_infer_types.erl
View File

@ -16,10 +16,6 @@
, infer/2 , infer/2
, unfold_types_in_type/2 , unfold_types_in_type/2
, unfold_types_in_type/3 , unfold_types_in_type/3
%% TODO: Newly added
, get_named_argument_constraint_name/1
, get_named_argument_constraint_args/1
, get_named_argument_constraint_type/1
]). ]).
%% Newly exported %% Newly exported
@ -27,6 +23,11 @@
, freshen_type/2 , freshen_type/2
, freshen_type_sig/2 , freshen_type_sig/2
, infer_const/2 , infer_const/2
, app_t/3
, unify/4
, create_freshen_tvars/0
, destroy_freshen_tvars/0
, freshen/1
]). ]).
-export_type([ utype/0 -export_type([ utype/0
, typesig/0 , typesig/0
@ -54,57 +55,6 @@
element(1, T) =:= con orelse element(1, T) =:= con orelse
element(1, T) =:= qcon). element(1, T) =:= qcon).
-type why_record() :: aeso_syntax:field(aeso_syntax:expr())
| {var_args, aeso_syntax:ann(), aeso_syntax:expr()}
| {proj, aeso_syntax:ann(), aeso_syntax:expr(), aeso_syntax:id()}.
-record(named_argument_constraint,
{args :: named_args_t(),
name :: aeso_syntax:id(),
type :: utype()}).
-record(dependent_type_constraint,
{ named_args_t :: named_args_t()
, 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_t :: utype()
, field :: aeso_syntax:id()
, field_t :: utype()
, kind :: project | create | update %% Projection constraints can match contract
, context :: why_record() }). %% types, but field constraints only record types.
%% Constraint checking that 'record_t' has precisely 'fields'.
-record(record_create_constraint,
{ record_t :: utype()
, fields :: [aeso_syntax:id()]
, context :: why_record() }).
-record(is_contract_constraint,
{ contract_t :: utype(),
context :: {contract_literal, aeso_syntax:expr()} |
{address_to_contract, aeso_syntax:ann()} |
{bytecode_hash, aeso_syntax:ann()} |
{var_args, aeso_syntax:ann(), aeso_syntax:expr()},
force_def = false :: boolean()
}).
-type field_constraint() :: #field_constraint{} | #record_create_constraint{} | #is_contract_constraint{}.
-type byte_constraint() :: {is_bytes, utype()}
| {add_bytes, aeso_syntax:ann(), concat | split, utype(), utype(), utype()}.
-type aens_resolve_constraint() :: {aens_resolve_type, utype()}.
-type oracle_type_constraint() :: {oracle_type, aeso_syntax:ann(), utype()}.
-type constraint() :: named_argument_constraint() | field_constraint() | byte_constraint()
| aens_resolve_constraint() | oracle_type_constraint().
-type type() :: aeso_syntax:type(). -type type() :: aeso_syntax:type().
-type name() :: string(). -type name() :: string().
-type typesig() :: {type_sig, aeso_syntax:ann(), type_constraints(), [aeso_syntax:named_arg_t()], [type()], type()}. -type typesig() :: {type_sig, aeso_syntax:ann(), type_constraints(), [aeso_syntax:named_arg_t()], [type()], type()}.
@ -165,11 +115,9 @@ get_option(A, B) -> aeso_tc_options:get_option(A, B).
when_option(A, B) -> aeso_tc_options:when_option(A, B). when_option(A, B) -> aeso_tc_options:when_option(A, B).
when_warning(A, B) -> aeso_tc_options:when_warning(A, B). when_warning(A, B) -> aeso_tc_options:when_warning(A, B).
%% -- New functions ---------------------------------------------------------- %% -------
get_named_argument_constraint_name(#named_argument_constraint{name = Name}) -> Name. ensure_first_order(A, B) -> aeso_tc_type_utils:ensure_first_order(A, B).
get_named_argument_constraint_args(#named_argument_constraint{args = Args}) -> Args.
get_named_argument_constraint_type(#named_argument_constraint{type = Type}) -> Type.
%% -- The rest --------------------------------------------------------------- %% -- The rest ---------------------------------------------------------------
@ -893,11 +841,11 @@ register_implementation(Id, Sig) ->
end. end.
infer_nonrec(Env, LetFun) -> infer_nonrec(Env, LetFun) ->
create_constraints(), aeso_tc_constraints:create_constraints(),
NewLetFun = {{_, Sig}, _} = infer_letfun(Env, LetFun), NewLetFun = {{_, Sig}, _} = infer_letfun(Env, LetFun),
check_special_funs(Env, NewLetFun), check_special_funs(Env, NewLetFun),
register_implementation(get_letfun_id(LetFun), Sig), register_implementation(get_letfun_id(LetFun), Sig),
solve_then_destroy_and_report_unsolved_constraints(Env), aeso_tc_constraints:solve_then_destroy_and_report_unsolved_constraints(Env),
Result = {TypeSig, _} = aeso_tc_type_utils:instantiate(NewLetFun), Result = {TypeSig, _} = aeso_tc_type_utils:instantiate(NewLetFun),
print_typesig(TypeSig), print_typesig(TypeSig),
Result. Result.
@ -915,7 +863,7 @@ check_special_funs(Env, {{"init", Type}, _}) ->
check_special_funs(_, _) -> ok. check_special_funs(_, _) -> ok.
infer_letrec(Env, Defs) -> infer_letrec(Env, Defs) ->
create_constraints(), aeso_tc_constraints:create_constraints(),
Funs = lists:map(fun({letfun, _, {id, Ann, Name}, _, _, _}) -> {Name, fresh_uvar(Ann)}; Funs = lists:map(fun({letfun, _, {id, Ann, Name}, _, _, _}) -> {Name, fresh_uvar(Ann)};
({fun_clauses, _, {id, Ann, Name}, _, _}) -> {Name, fresh_uvar(Ann)} ({fun_clauses, _, {id, Ann, Name}, _, _}) -> {Name, fresh_uvar(Ann)}
end, Defs), end, Defs),
@ -927,12 +875,12 @@ infer_letrec(Env, Defs) ->
Got = proplists:get_value(Name, Funs), Got = proplists:get_value(Name, Funs),
Expect = aeso_tc_type_utils:typesig_to_fun_t(TypeSig), Expect = aeso_tc_type_utils:typesig_to_fun_t(TypeSig),
unify(Env, Got, Expect, {check_typesig, Name, Got, Expect}), unify(Env, Got, Expect, {check_typesig, Name, Got, Expect}),
solve_constraints(Env), aeso_tc_constraints:solve_constraints(Env),
?PRINT_TYPES("Checked ~s : ~s\n", ?PRINT_TYPES("Checked ~s : ~s\n",
[Name, pp(aeso_tc_type_utils:dereference_deep(Got))]), [Name, pp(aeso_tc_type_utils:dereference_deep(Got))]),
Res Res
end || LF <- Defs ], end || LF <- Defs ],
solve_then_destroy_and_report_unsolved_constraints(Env), aeso_tc_constraints:solve_then_destroy_and_report_unsolved_constraints(Env),
TypeSigs = aeso_tc_type_utils:instantiate([Sig || {Sig, _} <- Inferred]), TypeSigs = aeso_tc_type_utils:instantiate([Sig || {Sig, _} <- Inferred]),
NewDefs = aeso_tc_type_utils:instantiate([D || {_, D} <- Inferred]), NewDefs = aeso_tc_type_utils:instantiate([D || {_, D} <- Inferred]),
[print_typesig(S) || S <- TypeSigs], [print_typesig(S) || S <- TypeSigs],
@ -1022,22 +970,6 @@ ensure_first_order_entrypoint({letfun, Ann, Id = {id, _, Name}, Args, Ret, _}) -
%% rather than being returned. %% rather than being returned.
ok. ok.
ensure_first_order(Type, Err) ->
is_first_order(Type) orelse type_error(Err).
is_first_order({fun_t, _, _, _, _}) -> 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.
ensure_monomorphic(Type, Err) ->
is_monomorphic(Type) orelse type_error(Err).
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.
check_state_init(Env) -> check_state_init(Env) ->
Top = aeso_tc_env:namespace(Env), Top = aeso_tc_env:namespace(Env),
StateType = aeso_tc_env:lookup_type(Env, {id, [{origin, system}], "state"}), StateType = aeso_tc_env:lookup_type(Env, {id, [{origin, system}], "state"}),
@ -1117,8 +1049,7 @@ infer_expr(_Env, Body={oracle_query_id, As, _}) ->
{typed, As, Body, {app_t, As, {id, As, "oracle_query"}, [Q, R]}}; {typed, As, Body, {app_t, As, {id, As, "oracle_query"}, [Q, R]}};
infer_expr(_Env, Body={contract_pubkey, As, _}) -> infer_expr(_Env, Body={contract_pubkey, As, _}) ->
Con = fresh_uvar(As), Con = fresh_uvar(As),
add_constraint([#is_contract_constraint{ contract_t = Con, aeso_tc_constraints:add_is_contract_constraint(Con, {contract_literal, Body}),
context = {contract_literal, Body} }]),
{typed, As, Body, Con}; {typed, As, Body, Con};
infer_expr(_Env, Body={id, As, "_"}) -> infer_expr(_Env, Body={id, As, "_"}) ->
{typed, As, Body, fresh_uvar(As)}; {typed, As, Body, fresh_uvar(As)};
@ -1214,17 +1145,17 @@ infer_expr(Env, {app, Ann, Fun, Args0} = App) ->
ResultType = fresh_uvar(Ann), ResultType = fresh_uvar(Ann),
unify(Env, FunType, {fun_t, [], NamedArgsVar, ArgTypes, GeneralResultType}, When), unify(Env, FunType, {fun_t, [], NamedArgsVar, ArgTypes, GeneralResultType}, When),
when_warning(warn_negative_spend, fun() -> warn_potential_negative_spend(Ann, NewFun1, NewArgs) end), when_warning(warn_negative_spend, fun() -> warn_potential_negative_spend(Ann, NewFun1, NewArgs) end),
[ add_constraint({aens_resolve_type, GeneralResultType}) [ aeso_tc_constraints:add_aens_resolve_constraint(GeneralResultType)
|| element(3, FunName) =:= ["AENS", "resolve"] ], || element(3, FunName) =:= ["AENS", "resolve"] ],
[ add_constraint({oracle_type, Ann, OType}) [ aeso_tc_constraints:add_oracle_type_constraint(Ann, OType)
|| OType <- [get_oracle_type(FunName, ArgTypes, GeneralResultType)], || OType <- [get_oracle_type(FunName, ArgTypes, GeneralResultType)],
OType =/= false ], OType =/= false ],
add_constraint( aeso_tc_constraints:add_dependent_type_constraint(
#dependent_type_constraint{ named_args_t = NamedArgsVar, NamedArgsVar,
named_args = NamedArgs1, NamedArgs1,
general_type = GeneralResultType, GeneralResultType,
specialized_type = ResultType, ResultType,
context = {check_return, App} }), {check_return, App}),
{typed, Ann, {app, Ann, NewFun1, NamedArgs1 ++ NewArgs}, aeso_tc_type_utils:dereference(ResultType)} {typed, Ann, {app, Ann, NewFun1, NamedArgs1 ++ NewArgs}, aeso_tc_type_utils:dereference(ResultType)}
end; end;
infer_expr(Env, {'if', Attrs, Cond, Then, Else}) -> infer_expr(Env, {'if', Attrs, Cond, Then, Else}) ->
@ -1244,19 +1175,13 @@ infer_expr(Env, {record, Attrs, Fields}) ->
NewFields = [{field, A, FieldName, infer_expr(Env, Expr)} NewFields = [{field, A, FieldName, infer_expr(Env, Expr)}
|| {field, A, FieldName, Expr} <- Fields], || {field, A, FieldName, Expr} <- Fields],
RecordType1 = unfold_types_in_type(Env, RecordType), RecordType1 = unfold_types_in_type(Env, RecordType),
add_constraint([ #record_create_constraint{ [ aeso_tc_constraints:add_record_create_constraint(
record_t = RecordType1, RecordType1,
fields = [ FieldName || {field, _, [{proj, _, FieldName}], _} <- Fields ], [ FieldName || {field, _, [{proj, _, FieldName}], _} <- Fields ],
context = Attrs } || not aeso_tc_env:in_pattern(Env) ] ++ Attrs)
[begin || not aeso_tc_env:in_pattern(Env) ],
[{proj, _, FieldName}] = LV, [ aeso_tc_constraints:add_field_constraint(RecordType1, FieldName, T, create, Fld)
#field_constraint{ || {Fld, {field, _, [{proj, _, FieldName}], {typed, _, _, T}}} <- lists:zip(Fields, NewFields) ],
record_t = RecordType1,
field = FieldName,
field_t = T,
kind = create,
context = Fld}
end || {Fld, {field, _, LV, {typed, _, _, T}}} <- lists:zip(Fields, NewFields)]),
{typed, Attrs, {record, Attrs, NewFields}, RecordType}; {typed, Attrs, {record, Attrs, NewFields}, RecordType};
infer_expr(Env, {record, Attrs, Record, Update}) -> infer_expr(Env, {record, Attrs, Record, Update}) ->
NewRecord = {typed, _, _, RecordType} = infer_expr(Env, Record), NewRecord = {typed, _, _, RecordType} = infer_expr(Env, Record),
@ -1265,12 +1190,12 @@ infer_expr(Env, {record, Attrs, Record, Update}) ->
infer_expr(Env, {proj, Attrs, Record, FieldName}) -> infer_expr(Env, {proj, Attrs, Record, FieldName}) ->
NewRecord = {typed, _, _, RecordType} = infer_expr(Env, Record), NewRecord = {typed, _, _, RecordType} = infer_expr(Env, Record),
FieldType = fresh_uvar(Attrs), FieldType = fresh_uvar(Attrs),
add_constraint([#field_constraint{ aeso_tc_constraints:add_field_constraint(
record_t = unfold_types_in_type(Env, RecordType), unfold_types_in_type(Env, RecordType),
field = FieldName, FieldName,
field_t = FieldType, FieldType,
kind = project, project,
context = {proj, Attrs, Record, FieldName} }]), {proj, Attrs, Record, FieldName}),
{typed, Attrs, {proj, Attrs, NewRecord, FieldName}, FieldType}; {typed, Attrs, {proj, Attrs, NewRecord, FieldName}, FieldType};
%% Maps %% Maps
infer_expr(Env, {map_get, Attrs, Map, Key}) -> %% map lookup infer_expr(Env, {map_get, Attrs, Map, Key}) -> %% map lookup
@ -1445,18 +1370,13 @@ check_contract_construction(Env, ForceDef, ContractT, Fun, NamedArgsT, ArgTypes,
InitT = fresh_uvar(Ann), InitT = fresh_uvar(Ann),
unify(Env, InitT, {fun_t, Ann, NamedArgsT, ArgTypes, fresh_uvar(Ann)}, {checking_init_args, Ann, ContractT, ArgTypes}), unify(Env, InitT, {fun_t, Ann, NamedArgsT, ArgTypes, fresh_uvar(Ann)}, {checking_init_args, Ann, ContractT, ArgTypes}),
unify(Env, RetT, ContractT, {return_contract, Fun, ContractT}), unify(Env, RetT, ContractT, {return_contract, Fun, ContractT}),
add_constraint( aeso_tc_constraints:add_field_constraint(
[ #field_constraint{ unfold_types_in_type(Env, ContractT),
record_t = unfold_types_in_type(Env, ContractT), {id, Ann, ?CONSTRUCTOR_MOCK_NAME},
field = {id, Ann, ?CONSTRUCTOR_MOCK_NAME}, InitT,
field_t = InitT, project,
kind = project, {var_args, Ann, Fun}),
context = {var_args, Ann, Fun} } aeso_tc_constraints:add_is_contract_constraint(ContractT, {var_args, Ann, Fun}, ForceDef),
, #is_contract_constraint{ contract_t = ContractT,
context = {var_args, Ann, Fun},
force_def = ForceDef
}
]),
ok. ok.
split_args(Args0) -> split_args(Args0) ->
@ -1467,11 +1387,7 @@ split_args(Args0) ->
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),
add_constraint( aeso_tc_constraints:add_named_argument_constraint(NamedArgs, Id, ArgType),
#named_argument_constraint{
args = NamedArgs,
name = Id,
type = ArgType }),
{named_arg, Ann, Id, CheckedExpr}. {named_arg, Ann, Id, CheckedExpr}.
check_map_update(Env, {field, Ann, [{map_get, Ann1, Key}], Val}, KeyType, ValType) -> check_map_update(Env, {field, Ann, [{map_get, Ann1, Key}], Val}, KeyType, ValType) ->
@ -1505,12 +1421,12 @@ check_record_update(Env, RecordType, Fld) ->
FunType = {fun_t, Ann1, [], [FldType], FldType}, FunType = {fun_t, Ann1, [], [FldType], FldType},
{field_upd, Ann, LV, check_expr(Env, Fun, FunType)} {field_upd, Ann, LV, check_expr(Env, Fun, FunType)}
end, end,
add_constraint([#field_constraint{ aeso_tc_constraints:add_field_constraint(
record_t = unfold_types_in_type(Env, RecordType), unfold_types_in_type(Env, RecordType),
field = FieldName, FieldName,
field_t = FldType, FldType,
kind = update, update,
context = Fld }]), Fld),
Fld1. Fld1.
infer_op(Env, As, Op, Args, InferOp) -> infer_op(Env, As, Op, Args, InferOp) ->
@ -1579,9 +1495,9 @@ infer_const(Env, {letval, Ann, TypedId = {typed, _, Id = {id, _, _}, Type}, Expr
{letval, Ann, TypedId, NewExpr}; {letval, Ann, TypedId, NewExpr};
infer_const(Env, {letval, Ann, Id = {id, AnnId, _}, Expr}) -> infer_const(Env, {letval, Ann, Id = {id, AnnId, _}, Expr}) ->
check_valid_const_expr(Expr) orelse type_error({invalid_const_expr, Id}), check_valid_const_expr(Expr) orelse type_error({invalid_const_expr, Id}),
create_constraints(), aeso_tc_constraints:create_constraints(),
NewExpr = {typed, _, _, Type} = infer_expr(aeso_tc_env:set_current_const(Id, Env), Expr), NewExpr = {typed, _, _, Type} = infer_expr(aeso_tc_env:set_current_const(Id, Env), Expr),
solve_then_destroy_and_report_unsolved_constraints(Env), aeso_tc_constraints:solve_then_destroy_and_report_unsolved_constraints(Env),
IdType = setelement(2, Type, AnnId), IdType = setelement(2, Type, AnnId),
NewId = {typed, aeso_syntax:get_ann(Id), Id, IdType}, NewId = {typed, aeso_syntax:get_ann(Id), Id, IdType},
aeso_tc_type_utils:instantiate({letval, Ann, NewId, NewExpr}). aeso_tc_type_utils:instantiate({letval, Ann, NewId, NewExpr}).
@ -1656,129 +1572,6 @@ free_vars(L) when is_list(L) ->
[V || Elem <- L, [V || Elem <- L,
V <- free_vars(Elem)]. V <- free_vars(Elem)].
%% -- Constraints --
create_constraints() ->
aeso_tc_ets_manager:ets_new(constraints, [ordered_set]).
-spec add_constraint(constraint() | [constraint()]) -> true.
add_constraint(Constraint) ->
aeso_tc_ets_manager:ets_insert_ordered(constraints, Constraint).
get_constraints() ->
aeso_tc_ets_manager:ets_tab2list_ordered(constraints).
destroy_constraints() ->
aeso_tc_ets_manager:ets_delete(constraints).
-spec solve_constraints(env()) -> ok.
solve_constraints(Env) ->
%% First look for record fields that appear in only one type definition
IsAmbiguous =
fun(#field_constraint{
record_t = RecordType,
field = Field={id, _Attrs, FieldName},
field_t = FieldType,
kind = Kind,
context = When }) ->
Arity = aeso_tc_type_utils:fun_arity(aeso_tc_type_utils:dereference_deep(FieldType)),
FieldInfos = case Arity of
none -> aeso_tc_env:lookup_record_field(Env, FieldName, Kind);
_ -> aeso_tc_env:lookup_record_field_arity(Env, FieldName, Arity, Kind)
end,
case FieldInfos of
[] ->
type_error({undefined_field, Field}),
false;
[Fld] ->
FldType = aeso_tc_env:field_info_field_t(Fld),
RecType = aeso_tc_env:field_info_record_t(Fld),
create_freshen_tvars(),
FreshFldType = freshen(FldType),
FreshRecType = freshen(RecType),
destroy_freshen_tvars(),
unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}),
unify(Env, FreshRecType, RecordType, {record_constraint, FreshRecType, RecordType, When}),
false;
_ ->
%% ambiguity--need cleverer strategy
true
end;
(_) -> true
end,
AmbiguousConstraints = lists:filter(IsAmbiguous, get_constraints()),
% The two passes on AmbiguousConstraints are needed
solve_ambiguous_constraints(Env, AmbiguousConstraints ++ AmbiguousConstraints).
-spec solve_ambiguous_constraints(env(), [constraint()]) -> ok.
solve_ambiguous_constraints(Env, Constraints) ->
Unknown = solve_known_record_types(Env, Constraints),
if Unknown == [] -> ok;
length(Unknown) < length(Constraints) ->
%% progress! Keep trying.
solve_ambiguous_constraints(Env, Unknown);
true ->
case solve_unknown_record_types(Env, Unknown) of
true -> %% Progress!
solve_ambiguous_constraints(Env, Unknown);
_ -> ok %% No progress. Report errors later.
end
end.
solve_then_destroy_and_report_unsolved_constraints(Env) ->
solve_constraints(Env),
destroy_and_report_unsolved_constraints(Env).
destroy_and_report_unsolved_constraints(Env) ->
{FieldCs, OtherCs} =
lists:partition(fun(#field_constraint{}) -> true; (_) -> false end,
get_constraints()),
{CreateCs, OtherCs1} =
lists:partition(fun(#record_create_constraint{}) -> true; (_) -> false end,
OtherCs),
{ContractCs, OtherCs2} =
lists:partition(fun(#is_contract_constraint{}) -> true; (_) -> false end, OtherCs1),
{NamedArgCs, OtherCs3} =
lists:partition(fun(#dependent_type_constraint{}) -> true;
(#named_argument_constraint{}) -> true;
(_) -> false
end, OtherCs2),
{BytesCs, OtherCs4} =
lists:partition(fun({is_bytes, _}) -> true;
({add_bytes, _, _, _, _, _}) -> true;
(_) -> false
end, OtherCs3),
{AensResolveCs, OtherCs5} =
lists:partition(fun({aens_resolve_type, _}) -> true;
(_) -> false
end, OtherCs4),
{OracleTypeCs, []} =
lists:partition(fun({oracle_type, _, _}) -> true;
(_) -> false
end, OtherCs5),
Unsolved = [ S || S <- [ solve_constraint(Env, aeso_tc_type_utils:dereference_deep(C)) || C <- NamedArgCs ],
S == unsolved ],
[ type_error({unsolved_named_argument_constraint, C}) || C <- Unsolved ],
Unknown = solve_known_record_types(Env, FieldCs),
if Unknown == [] -> ok;
true ->
case solve_unknown_record_types(Env, Unknown) of
true -> ok;
Errors -> [ type_error(Err) || Err <- Errors ]
end
end,
check_record_create_constraints(Env, CreateCs),
check_is_contract_constraints(Env, ContractCs),
check_bytes_constraints(Env, BytesCs),
check_aens_resolve_constraints(Env, AensResolveCs),
check_oracle_type_constraints(Env, OracleTypeCs),
destroy_constraints().
get_oracle_type({qid, _, ["Oracle", "register"]}, _ , OType) -> OType; get_oracle_type({qid, _, ["Oracle", "register"]}, _ , OType) -> OType;
get_oracle_type({qid, _, ["Oracle", "query"]}, [OType| _], _ ) -> OType; get_oracle_type({qid, _, ["Oracle", "query"]}, [OType| _], _ ) -> OType;
get_oracle_type({qid, _, ["Oracle", "get_question"]}, [OType| _], _ ) -> OType; get_oracle_type({qid, _, ["Oracle", "get_question"]}, [OType| _], _ ) -> OType;
@ -1788,276 +1581,6 @@ get_oracle_type({qid, _, ["Oracle", "check_query"]}, [OType| _], _ ) -> OTyp
get_oracle_type({qid, _, ["Oracle", "respond"]}, [OType| _], _ ) -> OType; get_oracle_type({qid, _, ["Oracle", "respond"]}, [OType| _], _ ) -> OType;
get_oracle_type(_Fun, _Args, _Ret) -> false. get_oracle_type(_Fun, _Args, _Ret) -> false.
%% -- Named argument constraints --
%% If false, a type error has been emitted, so it's safe to drop the constraint.
-spec check_named_argument_constraint(env(), named_argument_constraint()) -> true | false | unsolved.
check_named_argument_constraint(_Env, #named_argument_constraint{ args = {uvar, _, _} }) ->
unsolved;
check_named_argument_constraint(Env,
C = #named_argument_constraint{ args = Args,
name = Id = {id, _, Name},
type = Type }) ->
case [ T || {named_arg_t, _, {id, _, Name1}, T, _} <- Args, Name1 == Name ] of
[] ->
type_error({bad_named_argument, Args, Id}),
false;
[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 = {check_return, App} }) ->
NamedArgsT = aeso_tc_type_utils:dereference(NamedArgsT0),
case aeso_tc_type_utils: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 ]),
GenType1 = specialize_dependent_type(ArgEnv, GenType),
unify(Env, GenType1, SpecType, {check_expr, App, GenType1, SpecType}),
true;
_ -> unify(Env, GenType, SpecType, {check_expr, App, GenType, SpecType}), true
end.
specialize_dependent_type(Env, Type) ->
case aeso_tc_type_utils: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.
%% -- Bytes constraints --
solve_constraint(_Env, #field_constraint{record_t = {uvar, _, _}}) ->
not_solved;
solve_constraint(Env, C = #field_constraint{record_t = RecType,
field = FieldName,
field_t = FieldType,
context = When}) ->
RecId = record_type_name(RecType),
Attrs = aeso_syntax:get_ann(RecId),
case aeso_tc_env:lookup_type(Env, RecId) of
{_, {_Ann, {Formals, {What, Fields}}}} when What =:= record_t; What =:= contract_t ->
FieldTypes = [{Name, Type} || {field_t, _, {id, _, Name}, Type} <- Fields],
{id, _, FieldString} = FieldName,
case proplists:get_value(FieldString, FieldTypes) of
undefined ->
type_error({missing_field, FieldName, RecId}),
not_solved;
FldType ->
create_freshen_tvars(),
FreshFldType = freshen(FldType),
FreshRecType = freshen(app_t(Attrs, RecId, Formals)),
destroy_freshen_tvars(),
unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}),
unify(Env, FreshRecType, RecType, {record_constraint, FreshRecType, RecType, When}),
C
end;
_ ->
type_error({not_a_record_type, aeso_tc_type_utils:instantiate(RecType), When}),
not_solved
end;
solve_constraint(Env, C = #dependent_type_constraint{}) ->
check_named_argument_constraint(Env, C);
solve_constraint(Env, C = #named_argument_constraint{}) ->
check_named_argument_constraint(Env, C);
solve_constraint(_Env, {is_bytes, _}) -> ok;
solve_constraint(Env, {add_bytes, Ann, _, A0, B0, C0}) ->
A = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(A0)),
B = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(B0)),
C = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(C0)),
case {A, B, C} of
{{bytes_t, _, M}, {bytes_t, _, N}, _} -> unify(Env, {bytes_t, Ann, M + N}, C, {at, Ann});
{{bytes_t, _, M}, _, {bytes_t, _, R}} when R >= M -> unify(Env, {bytes_t, Ann, R - M}, B, {at, Ann});
{_, {bytes_t, _, N}, {bytes_t, _, R}} when R >= N -> unify(Env, {bytes_t, Ann, R - N}, A, {at, Ann});
_ -> ok
end;
solve_constraint(_, _) -> ok.
check_bytes_constraints(Env, Constraints) ->
InAddConstraint = [ T || {add_bytes, _, _, A, B, C} <- Constraints,
T <- [A, B, C],
element(1, T) /= bytes_t ],
%% Skip is_bytes constraints for types that occur in add_bytes constraints
%% (no need to generate error messages for both is_bytes and add_bytes).
Skip = fun({is_bytes, T}) -> lists:member(T, InAddConstraint);
(_) -> false end,
[ check_bytes_constraint(Env, C) || C <- Constraints, not Skip(C) ].
check_bytes_constraint(Env, {is_bytes, Type}) ->
Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)),
case Type1 of
{bytes_t, _, _} -> ok;
_ ->
type_error({unknown_byte_length, Type})
end;
check_bytes_constraint(Env, {add_bytes, Ann, Fun, A0, B0, C0}) ->
A = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(A0)),
B = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(B0)),
C = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(C0)),
case {A, B, C} of
{{bytes_t, _, _M}, {bytes_t, _, _N}, {bytes_t, _, _R}} ->
ok; %% If all are solved we checked M + N == R in solve_constraint.
_ -> type_error({unsolved_bytes_constraint, Ann, Fun, A, B, C})
end.
check_aens_resolve_constraints(_Env, []) ->
ok;
check_aens_resolve_constraints(Env, [{aens_resolve_type, Type} | Rest]) ->
Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)),
{app_t, _, {id, _, "option"}, [Type2]} = Type1,
case Type2 of
{id, _, "string"} -> ok;
{id, _, "address"} -> ok;
{con, _, _} -> ok;
{app_t, _, {id, _, "oracle"}, [_, _]} -> ok;
{app_t, _, {id, _, "oracle_query"}, [_, _]} -> ok;
_ -> type_error({invalid_aens_resolve_type, aeso_syntax:get_ann(Type), Type2})
end,
check_aens_resolve_constraints(Env, Rest).
check_oracle_type_constraints(_Env, []) ->
ok;
check_oracle_type_constraints(Env, [{oracle_type, Ann, OType} | Rest]) ->
Type = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(OType)),
{app_t, _, {id, _, "oracle"}, [QType, RType]} = Type,
ensure_monomorphic(QType, {invalid_oracle_type, polymorphic, query, Ann, Type}),
ensure_monomorphic(RType, {invalid_oracle_type, polymorphic, response, Ann, Type}),
ensure_first_order(QType, {invalid_oracle_type, higher_order, query, Ann, Type}),
ensure_first_order(RType, {invalid_oracle_type, higher_order, response, Ann, Type}),
check_oracle_type_constraints(Env, Rest).
%% -- Field constraints --
check_record_create_constraints(_, []) -> ok;
check_record_create_constraints(Env, [C | Cs]) ->
#record_create_constraint{
record_t = Type,
fields = Fields,
context = When } = C,
Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)),
try aeso_tc_env:lookup_type(Env, record_type_name(Type1)) of
{_QId, {_Ann, {_Args, {record_t, RecFields}}}} ->
ActualNames = [ Fld || {field_t, _, {id, _, Fld}, _} <- RecFields ],
GivenNames = [ Fld || {id, _, Fld} <- Fields ],
case ActualNames -- GivenNames of %% We know already that we don't have too many fields
[] -> ok;
Missing -> type_error({missing_fields, When, Type1, Missing})
end;
_ -> %% We can get here if there are other type errors.
ok
catch _:_ -> %% Might be unsolved, we get a different error in that case
ok
end,
check_record_create_constraints(Env, Cs).
is_contract_defined(C) ->
aeso_tc_ets_manager:ets_lookup(defined_contracts, qname(C)) =/= [].
check_is_contract_constraints(_Env, []) -> ok;
check_is_contract_constraints(Env, [C | Cs]) ->
#is_contract_constraint{ contract_t = Type, context = Cxt, force_def = ForceDef } = C,
Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)),
TypeName = record_type_name(Type1),
case aeso_tc_env:lookup_type(Env, TypeName) of
{_, {_Ann, {[], {contract_t, _}}}} ->
case not ForceDef orelse is_contract_defined(TypeName) of
true -> ok;
false -> type_error({contract_lacks_definition, Type1, Cxt})
end;
_ -> type_error({not_a_contract_type, Type1, Cxt})
end,
check_is_contract_constraints(Env, Cs).
-spec solve_unknown_record_types(env(), [field_constraint()]) -> true | [tuple()].
solve_unknown_record_types(Env, Unknown) ->
UVars = lists:usort([UVar || #field_constraint{record_t = UVar = {uvar, _, _}} <- Unknown]),
Solutions = [solve_for_uvar(Env, UVar, [{Kind, When, Field}
|| #field_constraint{record_t = U, field = Field, kind = Kind, context = When} <- Unknown,
U == UVar])
|| UVar <- UVars],
case lists:member(true, Solutions) of
true -> true;
false -> Solutions
end.
%% This will solve all kinds of constraints but will only return the
%% unsolved field constraints
-spec solve_known_record_types(env(), [constraint()]) -> [field_constraint()].
solve_known_record_types(Env, Constraints) ->
DerefConstraints = lists:map(fun(C = #field_constraint{record_t = RecordType}) ->
C#field_constraint{record_t = aeso_tc_type_utils:dereference(RecordType)};
(C) -> aeso_tc_type_utils:dereference_deep(C)
end, Constraints),
SolvedConstraints = lists:map(fun(C) -> solve_constraint(Env, aeso_tc_type_utils:dereference_deep(C)) end, DerefConstraints),
Unsolved = DerefConstraints--SolvedConstraints,
lists:filter(fun(#field_constraint{}) -> true; (_) -> false end, Unsolved).
record_type_name({app_t, _Attrs, RecId, _Args}) when ?is_type_id(RecId) ->
RecId;
record_type_name(RecId) when ?is_type_id(RecId) ->
RecId;
record_type_name(_Other) ->
%% io:format("~p is not a record type\n", [Other]),
{id, [{origin, system}], "not_a_record_type"}.
solve_for_uvar(Env, UVar = {uvar, Attrs, _}, Fields0) ->
Fields = [{Kind, Fld} || {Kind, _, Fld} <- Fields0],
[{_, When, _} | _] = Fields0, %% Get the location from the first field
%% If we have 'create' constraints they must be complete.
Covering = lists:usort([ Name || {create, {id, _, Name}} <- Fields ]),
%% Does this set of fields uniquely identify a record type?
FieldNames = [ Name || {_Kind, {id, _, Name}} <- Fields ],
UniqueFields = lists:usort(FieldNames),
Candidates = [aeso_tc_env:field_info_record_t(Fld) || Fld <- aeso_tc_env:lookup_record_field(Env, hd(FieldNames))],
TypesAndFields = [case aeso_tc_env:lookup_type(Env, record_type_name(RecType)) of
{_, {_, {_, {record_t, RecFields}}}} ->
{RecType, [Field || {field_t, _, {id, _, Field}, _} <- RecFields]};
{_, {_, {_, {contract_t, ConFields}}}} ->
%% TODO: is this right?
{RecType, [Field || {field_t, _, {id, _, Field}, _} <- ConFields]};
false -> %% impossible?
error({no_definition_for, record_type_name(RecType), in, Env})
end
|| RecType <- Candidates],
PartialSolutions =
lists:sort([{RecType, if Covering == [] -> []; true -> RecFields -- Covering end}
|| {RecType, RecFields} <- TypesAndFields,
UniqueFields -- RecFields == []]),
Solutions = [RecName || {RecName, []} <- PartialSolutions],
case {Solutions, PartialSolutions} of
{[], []} ->
{no_records_with_all_fields, Fields};
{[], _} ->
case PartialSolutions of
[{RecType, Missing} | _] -> %% TODO: better error if ambiguous
{missing_fields, When, RecType, Missing}
end;
{[RecType], _} ->
RecName = record_type_name(RecType),
{_, {_, {Formals, {_RecOrCon, _}}}} = aeso_tc_env:lookup_type(Env, RecName),
create_freshen_tvars(),
FreshRecType = freshen(app_t(Attrs, RecName, Formals)),
destroy_freshen_tvars(),
unify(Env, UVar, FreshRecType, {solve_rec_type, UVar, Fields}),
true;
{StillPossible, _} ->
{ambiguous_record, Fields, StillPossible}
end.
%% During type inference, record types are represented by their %% During type inference, record types are represented by their
%% names. But, before we pass the typed program to the code generator, %% names. But, before we pass the typed program to the code generator,
%% we replace record types annotating expressions with their %% we replace record types annotating expressions with their
@ -2365,7 +1888,7 @@ freshen(Ann, {tvar, _, Name}) ->
NewT; NewT;
freshen(Ann, {bytes_t, _, any}) -> freshen(Ann, {bytes_t, _, any}) ->
X = fresh_uvar(Ann), X = fresh_uvar(Ann),
add_constraint({is_bytes, X}), aeso_tc_constraints:add_is_bytes_constraint(X),
X; X;
freshen(Ann, T) when is_tuple(T) -> freshen(Ann, T) when is_tuple(T) ->
list_to_tuple(freshen(Ann, tuple_to_list(T))); list_to_tuple(freshen(Ann, tuple_to_list(T)));
@ -2381,12 +1904,10 @@ freshen_type_sig(Ann, TypeSig = {type_sig, _, Constr, _, _, _}) ->
apply_typesig_constraint(_Ann, none, _FunT) -> ok; apply_typesig_constraint(_Ann, none, _FunT) -> ok;
apply_typesig_constraint(Ann, address_to_contract, {fun_t, _, [], [_], Type}) -> apply_typesig_constraint(Ann, address_to_contract, {fun_t, _, [], [_], Type}) ->
add_constraint([#is_contract_constraint{ contract_t = Type, aeso_tc_constraints:add_is_contract_constraint(Type, {address_to_contract, Ann});
context = {address_to_contract, Ann}}]);
apply_typesig_constraint(Ann, bytes_concat, {fun_t, _, [], [A, B], C}) -> apply_typesig_constraint(Ann, bytes_concat, {fun_t, _, [], [A, B], C}) ->
add_constraint({add_bytes, Ann, concat, A, B, C}); aeso_tc_constraints:add_add_bytes_constraint(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_constraint({add_bytes, Ann, split, A, B, C}); aeso_tc_constraints:add_add_bytes_constraint(Ann, split, A, B, C);
apply_typesig_constraint(Ann, bytecode_hash, {fun_t, _, _, [Con], _}) -> apply_typesig_constraint(Ann, bytecode_hash, {fun_t, _, _, [Con], _}) ->
add_constraint([#is_contract_constraint{ contract_t = Con, aeso_tc_constraints:add_is_contract_constraint(Con, {bytecode_hash, Ann}).
context = {bytecode_hash, Ann} }]).

551
src/aeso_tc_constraints.erl Normal file
View File

@ -0,0 +1,551 @@
-module(aeso_tc_constraints).
-export([ solve_constraints/1
, solve_then_destroy_and_report_unsolved_constraints/1
, create_constraints/0
, add_is_contract_constraint/2
, add_is_contract_constraint/3
, add_is_bytes_constraint/1
, add_add_bytes_constraint/5
, add_aens_resolve_constraint/1
, add_oracle_type_constraint/2
, add_named_argument_constraint/3
, add_field_constraint/5
, add_dependent_type_constraint/5
, add_record_create_constraint/3
]).
%% -- Duplicated types -------------------------------------------------------
-type uvar() :: {uvar, aeso_syntax:ann(), reference()}.
-type named_args_t() :: uvar() | [{named_arg_t, aeso_syntax:ann(), aeso_syntax:id(), utype(), aeso_syntax:expr()}].
-type utype() :: aeso_ast_infer_types:utype().
%% -- Duplicated macros ------------------------------------------------------
-define(is_type_id(T), element(1, T) =:= id orelse
element(1, T) =:= qid orelse
element(1, T) =:= con orelse
element(1, T) =:= qcon).
%% -- Circular dependency ----------------------------------------------------
fresh_uvar(A) -> aeso_ast_infer_types:fresh_uvar(A).
freshen(A) -> aeso_ast_infer_types:freshen(A).
create_freshen_tvars() -> aeso_ast_infer_types:create_freshen_tvars().
destroy_freshen_tvars() -> aeso_ast_infer_types:destroy_freshen_tvars().
unify(A, B, C, D) -> aeso_ast_infer_types:unify(A, B, C, D).
unfold_types_in_type(A, B) -> aeso_ast_infer_types:unfold_types_in_type(A, B).
app_t(A, B, C) -> aeso_ast_infer_types:app_t(A, B, C).
%% -- Moved functions --------------------------------------------------------
qname(A) -> aeso_tc_name_manip:qname(A).
%% -------
type_error(A) -> aeso_tc_errors:type_error(A).
%% -------
ensure_monomorphic(A, B) -> aeso_tc_type_utils:ensure_monomorphic(A, B).
ensure_first_order(A, B) -> aeso_tc_type_utils:ensure_first_order(A, B).
%% ---------------------------------------------------------------------------
-type env() :: aeso_tc_env:env().
-type why_record() :: aeso_syntax:field(aeso_syntax:expr())
| {var_args, aeso_syntax:ann(), aeso_syntax:expr()}
| {proj, aeso_syntax:ann(), aeso_syntax:expr(), aeso_syntax:id()}.
-record(named_argument_constraint,
{args :: named_args_t(),
name :: aeso_syntax:id(),
type :: utype()}).
-record(dependent_type_constraint,
{ named_args_t :: named_args_t()
, 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_t :: utype()
, field :: aeso_syntax:id()
, field_t :: utype()
, kind :: project | create | update %% Projection constraints can match contract
, context :: why_record() }). %% types, but field constraints only record types.
%% Constraint checking that 'record_t' has precisely 'fields'.
-record(record_create_constraint,
{ record_t :: utype()
, fields :: [aeso_syntax:id()]
, context :: why_record() }).
-record(is_contract_constraint,
{ contract_t :: utype(),
context :: {contract_literal, aeso_syntax:expr()} |
{address_to_contract, aeso_syntax:ann()} |
{bytecode_hash, aeso_syntax:ann()} |
{var_args, aeso_syntax:ann(), aeso_syntax:expr()},
force_def = false :: boolean()
}).
-type field_constraint() :: #field_constraint{} | #record_create_constraint{} | #is_contract_constraint{}.
-type byte_constraint() :: {is_bytes, utype()}
| {add_bytes, aeso_syntax:ann(), concat | split, utype(), utype(), utype()}.
-type aens_resolve_constraint() :: {aens_resolve_type, utype()}.
-type oracle_type_constraint() :: {oracle_type, aeso_syntax:ann(), utype()}.
-type constraint() :: named_argument_constraint() | field_constraint() | byte_constraint()
| aens_resolve_constraint() | oracle_type_constraint().
-spec add_constraint(constraint()) -> true.
add_constraint(Constraint) ->
aeso_tc_ets_manager:ets_insert_ordered(constraints, Constraint).
add_is_contract_constraint(ContractT, Context) ->
add_constraint(
#is_contract_constraint{
contract_t = ContractT,
context = Context }).
add_is_contract_constraint(ContractT, Context, ForceDef) ->
add_constraint(
#is_contract_constraint{
contract_t = ContractT,
context = Context,
force_def = ForceDef }).
add_aens_resolve_constraint(Type) ->
add_constraint({aens_resolve_type, Type}).
add_oracle_type_constraint(Ann, Type) ->
add_constraint({oracle_type, Ann, Type}).
add_named_argument_constraint(Args, Name, Type) ->
add_constraint(
#named_argument_constraint{
args = Args,
name = Name,
type = Type }).
add_is_bytes_constraint(Type) ->
add_constraint({is_bytes, Type}).
add_add_bytes_constraint(Ann, Kind, A, B, C) ->
add_constraint({add_bytes, Ann, Kind, A, B, C}).
add_field_constraint(RecordT, Field, FieldT, Kind, Context) ->
add_constraint(#field_constraint{
record_t = RecordT,
field = Field,
field_t = FieldT,
kind = Kind,
context = Context }).
add_dependent_type_constraint(NamedArgsT, NamedArgs, GeneralType, SpecializedType, Context) ->
add_constraint(#dependent_type_constraint{
named_args_t = NamedArgsT,
named_args = NamedArgs,
general_type = GeneralType,
specialized_type = SpecializedType,
context = Context }).
add_record_create_constraint(RecordT, Fields, Context) ->
add_constraint(#record_create_constraint{
record_t = RecordT,
fields = Fields,
context = Context }).
create_constraints() ->
aeso_tc_ets_manager:ets_new(constraints, [ordered_set]).
get_constraints() ->
aeso_tc_ets_manager:ets_tab2list_ordered(constraints).
destroy_constraints() ->
aeso_tc_ets_manager:ets_delete(constraints).
-spec solve_constraints(env()) -> ok.
solve_constraints(Env) ->
%% First look for record fields that appear in only one type definition
IsAmbiguous =
fun(#field_constraint{
record_t = RecordType,
field = Field={id, _Attrs, FieldName},
field_t = FieldType,
kind = Kind,
context = When }) ->
Arity = aeso_tc_type_utils:fun_arity(aeso_tc_type_utils:dereference_deep(FieldType)),
FieldInfos = case Arity of
none -> aeso_tc_env:lookup_record_field(Env, FieldName, Kind);
_ -> aeso_tc_env:lookup_record_field_arity(Env, FieldName, Arity, Kind)
end,
case FieldInfos of
[] ->
type_error({undefined_field, Field}),
false;
[Fld] ->
FldType = aeso_tc_env:field_info_field_t(Fld),
RecType = aeso_tc_env:field_info_record_t(Fld),
create_freshen_tvars(),
FreshFldType = freshen(FldType),
FreshRecType = freshen(RecType),
destroy_freshen_tvars(),
unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}),
unify(Env, FreshRecType, RecordType, {record_constraint, FreshRecType, RecordType, When}),
false;
_ ->
%% ambiguity--need cleverer strategy
true
end;
(_) -> true
end,
AmbiguousConstraints = lists:filter(IsAmbiguous, get_constraints()),
% The two passes on AmbiguousConstraints are needed
solve_ambiguous_constraints(Env, AmbiguousConstraints ++ AmbiguousConstraints).
-spec solve_ambiguous_constraints(env(), [constraint()]) -> ok.
solve_ambiguous_constraints(Env, Constraints) ->
Unknown = solve_known_record_types(Env, Constraints),
if Unknown == [] -> ok;
length(Unknown) < length(Constraints) ->
%% progress! Keep trying.
solve_ambiguous_constraints(Env, Unknown);
true ->
case solve_unknown_record_types(Env, Unknown) of
true -> %% Progress!
solve_ambiguous_constraints(Env, Unknown);
_ -> ok %% No progress. Report errors later.
end
end.
solve_then_destroy_and_report_unsolved_constraints(Env) ->
solve_constraints(Env),
destroy_and_report_unsolved_constraints(Env).
destroy_and_report_unsolved_constraints(Env) ->
{FieldCs, OtherCs} =
lists:partition(fun(#field_constraint{}) -> true; (_) -> false end,
get_constraints()),
{CreateCs, OtherCs1} =
lists:partition(fun(#record_create_constraint{}) -> true; (_) -> false end,
OtherCs),
{ContractCs, OtherCs2} =
lists:partition(fun(#is_contract_constraint{}) -> true; (_) -> false end, OtherCs1),
{NamedArgCs, OtherCs3} =
lists:partition(fun(#dependent_type_constraint{}) -> true;
(#named_argument_constraint{}) -> true;
(_) -> false
end, OtherCs2),
{BytesCs, OtherCs4} =
lists:partition(fun({is_bytes, _}) -> true;
({add_bytes, _, _, _, _, _}) -> true;
(_) -> false
end, OtherCs3),
{AensResolveCs, OtherCs5} =
lists:partition(fun({aens_resolve_type, _}) -> true;
(_) -> false
end, OtherCs4),
{OracleTypeCs, []} =
lists:partition(fun({oracle_type, _, _}) -> true;
(_) -> false
end, OtherCs5),
Unsolved = [ S || S <- [ solve_constraint(Env, aeso_tc_type_utils:dereference_deep(C)) || C <- NamedArgCs ],
S == unsolved ],
[ type_error({unsolved_named_argument_constraint, Name, Type})
|| #named_argument_constraint{name = Name, type = Type} <- Unsolved ],
Unknown = solve_known_record_types(Env, FieldCs),
if Unknown == [] -> ok;
true ->
case solve_unknown_record_types(Env, Unknown) of
true -> ok;
Errors -> [ type_error(Err) || Err <- Errors ]
end
end,
check_record_create_constraints(Env, CreateCs),
check_is_contract_constraints(Env, ContractCs),
check_bytes_constraints(Env, BytesCs),
check_aens_resolve_constraints(Env, AensResolveCs),
check_oracle_type_constraints(Env, OracleTypeCs),
destroy_constraints().
%% If false, a type error has been emitted, so it's safe to drop the constraint.
-spec check_named_argument_constraint(env(), named_argument_constraint()) -> true | false | unsolved.
check_named_argument_constraint(_Env, #named_argument_constraint{ args = {uvar, _, _} }) ->
unsolved;
check_named_argument_constraint(Env,
#named_argument_constraint{ args = Args,
name = Id = {id, _, Name},
type = Type }) ->
case [ T || {named_arg_t, _, {id, _, Name1}, T, _} <- Args, Name1 == Name ] of
[] ->
type_error({bad_named_argument, Args, Id}),
false;
[T] -> unify(Env, T, Type, {check_named_arg_constraint, Args, Id, Type}), true
end;
check_named_argument_constraint(Env,
#dependent_type_constraint{ named_args_t = NamedArgsT0,
named_args = NamedArgs,
general_type = GenType,
specialized_type = SpecType,
context = {check_return, App} }) ->
NamedArgsT = aeso_tc_type_utils:dereference(NamedArgsT0),
case aeso_tc_type_utils: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 ]),
GenType1 = specialize_dependent_type(ArgEnv, GenType),
unify(Env, GenType1, SpecType, {check_expr, App, GenType1, SpecType}),
true;
_ -> unify(Env, GenType, SpecType, {check_expr, App, GenType, SpecType}), true
end.
specialize_dependent_type(Env, Type) ->
case aeso_tc_type_utils: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.
%% -- Bytes constraints --
solve_constraint(_Env, #field_constraint{record_t = {uvar, _, _}}) ->
not_solved;
solve_constraint(Env, C = #field_constraint{record_t = RecType,
field = FieldName,
field_t = FieldType,
context = When}) ->
RecId = record_type_name(RecType),
Attrs = aeso_syntax:get_ann(RecId),
case aeso_tc_env:lookup_type(Env, RecId) of
{_, {_Ann, {Formals, {What, Fields}}}} when What =:= record_t; What =:= contract_t ->
FieldTypes = [{Name, Type} || {field_t, _, {id, _, Name}, Type} <- Fields],
{id, _, FieldString} = FieldName,
case proplists:get_value(FieldString, FieldTypes) of
undefined ->
type_error({missing_field, FieldName, RecId}),
not_solved;
FldType ->
create_freshen_tvars(),
FreshFldType = freshen(FldType),
FreshRecType = freshen(app_t(Attrs, RecId, Formals)),
destroy_freshen_tvars(),
unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}),
unify(Env, FreshRecType, RecType, {record_constraint, FreshRecType, RecType, When}),
C
end;
_ ->
type_error({not_a_record_type, aeso_tc_type_utils:instantiate(RecType), When}),
not_solved
end;
solve_constraint(Env, C = #dependent_type_constraint{}) ->
check_named_argument_constraint(Env, C);
solve_constraint(Env, C = #named_argument_constraint{}) ->
check_named_argument_constraint(Env, C);
solve_constraint(_Env, {is_bytes, _}) -> ok;
solve_constraint(Env, {add_bytes, Ann, _, A0, B0, C0}) ->
A = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(A0)),
B = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(B0)),
C = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(C0)),
case {A, B, C} of
{{bytes_t, _, M}, {bytes_t, _, N}, _} -> unify(Env, {bytes_t, Ann, M + N}, C, {at, Ann});
{{bytes_t, _, M}, _, {bytes_t, _, R}} when R >= M -> unify(Env, {bytes_t, Ann, R - M}, B, {at, Ann});
{_, {bytes_t, _, N}, {bytes_t, _, R}} when R >= N -> unify(Env, {bytes_t, Ann, R - N}, A, {at, Ann});
_ -> ok
end;
solve_constraint(_, _) -> ok.
check_bytes_constraints(Env, Constraints) ->
InAddConstraint = [ T || {add_bytes, _, _, A, B, C} <- Constraints,
T <- [A, B, C],
element(1, T) /= bytes_t ],
%% Skip is_bytes constraints for types that occur in add_bytes constraints
%% (no need to generate error messages for both is_bytes and add_bytes).
Skip = fun({is_bytes, T}) -> lists:member(T, InAddConstraint);
(_) -> false end,
[ check_bytes_constraint(Env, C) || C <- Constraints, not Skip(C) ].
check_bytes_constraint(Env, {is_bytes, Type}) ->
Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)),
case Type1 of
{bytes_t, _, _} -> ok;
_ ->
type_error({unknown_byte_length, Type})
end;
check_bytes_constraint(Env, {add_bytes, Ann, Fun, A0, B0, C0}) ->
A = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(A0)),
B = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(B0)),
C = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(C0)),
case {A, B, C} of
{{bytes_t, _, _M}, {bytes_t, _, _N}, {bytes_t, _, _R}} ->
ok; %% If all are solved we checked M + N == R in solve_constraint.
_ -> type_error({unsolved_bytes_constraint, Ann, Fun, A, B, C})
end.
check_aens_resolve_constraints(_Env, []) ->
ok;
check_aens_resolve_constraints(Env, [{aens_resolve_type, Type} | Rest]) ->
Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)),
{app_t, _, {id, _, "option"}, [Type2]} = Type1,
case Type2 of
{id, _, "string"} -> ok;
{id, _, "address"} -> ok;
{con, _, _} -> ok;
{app_t, _, {id, _, "oracle"}, [_, _]} -> ok;
{app_t, _, {id, _, "oracle_query"}, [_, _]} -> ok;
_ -> type_error({invalid_aens_resolve_type, aeso_syntax:get_ann(Type), Type2})
end,
check_aens_resolve_constraints(Env, Rest).
check_oracle_type_constraints(_Env, []) ->
ok;
check_oracle_type_constraints(Env, [{oracle_type, Ann, OType} | Rest]) ->
Type = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(OType)),
{app_t, _, {id, _, "oracle"}, [QType, RType]} = Type,
ensure_monomorphic(QType, {invalid_oracle_type, polymorphic, query, Ann, Type}),
ensure_monomorphic(RType, {invalid_oracle_type, polymorphic, response, Ann, Type}),
ensure_first_order(QType, {invalid_oracle_type, higher_order, query, Ann, Type}),
ensure_first_order(RType, {invalid_oracle_type, higher_order, response, Ann, Type}),
check_oracle_type_constraints(Env, Rest).
%% -- Field constraints --
check_record_create_constraints(_, []) -> ok;
check_record_create_constraints(Env, [C | Cs]) ->
#record_create_constraint{
record_t = Type,
fields = Fields,
context = When } = C,
Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)),
try aeso_tc_env:lookup_type(Env, record_type_name(Type1)) of
{_QId, {_Ann, {_Args, {record_t, RecFields}}}} ->
ActualNames = [ Fld || {field_t, _, {id, _, Fld}, _} <- RecFields ],
GivenNames = [ Fld || {id, _, Fld} <- Fields ],
case ActualNames -- GivenNames of %% We know already that we don't have too many fields
[] -> ok;
Missing -> type_error({missing_fields, When, Type1, Missing})
end;
_ -> %% We can get here if there are other type errors.
ok
catch _:_ -> %% Might be unsolved, we get a different error in that case
ok
end,
check_record_create_constraints(Env, Cs).
is_contract_defined(C) ->
aeso_tc_ets_manager:ets_lookup(defined_contracts, qname(C)) =/= [].
check_is_contract_constraints(_Env, []) -> ok;
check_is_contract_constraints(Env, [C | Cs]) ->
#is_contract_constraint{ contract_t = Type, context = Cxt, force_def = ForceDef } = C,
Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)),
TypeName = record_type_name(Type1),
case aeso_tc_env:lookup_type(Env, TypeName) of
{_, {_Ann, {[], {contract_t, _}}}} ->
case not ForceDef orelse is_contract_defined(TypeName) of
true -> ok;
false -> type_error({contract_lacks_definition, Type1, Cxt})
end;
_ -> type_error({not_a_contract_type, Type1, Cxt})
end,
check_is_contract_constraints(Env, Cs).
-spec solve_unknown_record_types(env(), [field_constraint()]) -> true | [tuple()].
solve_unknown_record_types(Env, Unknown) ->
UVars = lists:usort([UVar || #field_constraint{record_t = UVar = {uvar, _, _}} <- Unknown]),
Solutions = [solve_for_uvar(Env, UVar, [{Kind, When, Field}
|| #field_constraint{record_t = U, field = Field, kind = Kind, context = When} <- Unknown,
U == UVar])
|| UVar <- UVars],
case lists:member(true, Solutions) of
true -> true;
false -> Solutions
end.
%% This will solve all kinds of constraints but will only return the
%% unsolved field constraints
-spec solve_known_record_types(env(), [constraint()]) -> [field_constraint()].
solve_known_record_types(Env, Constraints) ->
DerefConstraints = lists:map(fun(C = #field_constraint{record_t = RecordType}) ->
C#field_constraint{record_t = aeso_tc_type_utils:dereference(RecordType)};
(C) -> aeso_tc_type_utils:dereference_deep(C)
end, Constraints),
SolvedConstraints = lists:map(fun(C) -> solve_constraint(Env, aeso_tc_type_utils:dereference_deep(C)) end, DerefConstraints),
Unsolved = DerefConstraints--SolvedConstraints,
lists:filter(fun(#field_constraint{}) -> true; (_) -> false end, Unsolved).
record_type_name({app_t, _Attrs, RecId, _Args}) when ?is_type_id(RecId) ->
RecId;
record_type_name(RecId) when ?is_type_id(RecId) ->
RecId;
record_type_name(_Other) ->
%% io:format("~p is not a record type\n", [Other]),
{id, [{origin, system}], "not_a_record_type"}.
solve_for_uvar(Env, UVar = {uvar, Attrs, _}, Fields0) ->
Fields = [{Kind, Fld} || {Kind, _, Fld} <- Fields0],
[{_, When, _} | _] = Fields0, %% Get the location from the first field
%% If we have 'create' constraints they must be complete.
Covering = lists:usort([ Name || {create, {id, _, Name}} <- Fields ]),
%% Does this set of fields uniquely identify a record type?
FieldNames = [ Name || {_Kind, {id, _, Name}} <- Fields ],
UniqueFields = lists:usort(FieldNames),
Candidates = [aeso_tc_env:field_info_record_t(Fld) || Fld <- aeso_tc_env:lookup_record_field(Env, hd(FieldNames))],
TypesAndFields = [case aeso_tc_env:lookup_type(Env, record_type_name(RecType)) of
{_, {_, {_, {record_t, RecFields}}}} ->
{RecType, [Field || {field_t, _, {id, _, Field}, _} <- RecFields]};
{_, {_, {_, {contract_t, ConFields}}}} ->
%% TODO: is this right?
{RecType, [Field || {field_t, _, {id, _, Field}, _} <- ConFields]};
false -> %% impossible?
error({no_definition_for, record_type_name(RecType), in, Env})
end
|| RecType <- Candidates],
PartialSolutions =
lists:sort([{RecType, if Covering == [] -> []; true -> RecFields -- Covering end}
|| {RecType, RecFields} <- TypesAndFields,
UniqueFields -- RecFields == []]),
Solutions = [RecName || {RecName, []} <- PartialSolutions],
case {Solutions, PartialSolutions} of
{[], []} ->
{no_records_with_all_fields, Fields};
{[], _} ->
case PartialSolutions of
[{RecType, Missing} | _] -> %% TODO: better error if ambiguous
{missing_fields, When, RecType, Missing}
end;
{[RecType], _} ->
RecName = record_type_name(RecType),
{_, {_, {Formals, {_RecOrCon, _}}}} = aeso_tc_env:lookup_type(Env, RecName),
create_freshen_tvars(),
FreshRecType = freshen(app_t(Attrs, RecName, Formals)),
destroy_freshen_tvars(),
unify(Env, UVar, FreshRecType, {solve_rec_type, UVar, Fields}),
true;
{StillPossible, _} ->
{ambiguous_record, Fields, StillPossible}
end.

4
src/aeso_tc_errors.erl
View File

@ -210,9 +210,7 @@ mk_error({bad_named_argument, Args, Name}) ->
[ io_lib:format("\n - `~s`", [pp_typed("", Arg, Type)]) [ io_lib:format("\n - `~s`", [pp_typed("", Arg, Type)])
|| {named_arg_t, _, Arg, Type, _} <- Args ]]), || {named_arg_t, _, Arg, Type, _} <- Args ]]),
mk_t_err(pos(Name), Msg); mk_t_err(pos(Name), Msg);
mk_error({unsolved_named_argument_constraint, C}) -> mk_error({unsolved_named_argument_constraint, Name, Type}) ->
Name = aeso_ast_infer_types:get_named_argument_constraint_name(C),
Type = aeso_ast_infer_types:get_named_argument_constraint_type(C),
Msg = io_lib:format("Named argument ~s supplied to function with unknown named arguments.", Msg = io_lib:format("Named argument ~s supplied to function with unknown named arguments.",
[pp_typed("", Name, Type)]), [pp_typed("", Name, Type)]),
mk_t_err(pos(Name), Msg); mk_t_err(pos(Name), Msg);

8
src/aeso_tc_pp.erl
View File

@ -131,11 +131,11 @@ pp_when({list_comp, BindExpr, Inferred0, Expected0}) ->
{pos(BindExpr), {pos(BindExpr),
io_lib:format("when checking rvalue of list comprehension binding `~s` against type `~s`", io_lib:format("when checking rvalue of list comprehension binding `~s` against type `~s`",
[pp_typed("", BindExpr, Inferred), pp_type(Expected)])}; [pp_typed("", BindExpr, Inferred), pp_type(Expected)])};
pp_when({check_named_arg_constraint, C}) -> pp_when({check_named_arg_constraint, CArgs, CName, CType}) ->
{id, _, Name} = Arg = aeso_ast_infer_types:get_named_argument_constraint_name(C), {id, _, Name} = Arg = CName,
[Type | _] = [ Type || {named_arg_t, _, {id, _, Name1}, Type, _} <- aeso_ast_infer_types:get_named_argument_constraint_args(C), Name1 == Name ], [Type | _] = [ Type || {named_arg_t, _, {id, _, Name1}, Type, _} <- CArgs, Name1 == Name ],
Err = io_lib:format("when checking named argument `~s` against inferred type `~s`", Err = io_lib:format("when checking named argument `~s` against inferred type `~s`",
[pp_typed("", Arg, Type), pp_type(aeso_ast_infer_types:get_named_argument_constraint_type(C))]), [pp_typed("", Arg, Type), pp_type(CType)]),
{pos(Arg), Err}; {pos(Arg), Err};
pp_when({checking_init_args, Ann, Con0, ArgTypes0}) -> pp_when({checking_init_args, Ann, Con0, ArgTypes0}) ->
Con = aeso_tc_type_utils:instantiate(Con0), Con = aeso_tc_type_utils:instantiate(Con0),

18
src/aeso_tc_type_utils.erl
View File

@ -5,6 +5,8 @@
, instantiate/1 , instantiate/1
, typesig_to_fun_t/1 , typesig_to_fun_t/1
, fun_arity/1 , fun_arity/1
, ensure_first_order/2
, ensure_monomorphic/2
]). ]).
typesig_to_fun_t({type_sig, Ann, _Constr, Named, Args, Res}) -> typesig_to_fun_t({type_sig, Ann, _Constr, Named, Args, Res}) ->
@ -62,3 +64,19 @@ integer_to_tvar(X) ->
fun_arity({fun_t, _, _, Args, _}) -> length(Args); fun_arity({fun_t, _, _, Args, _}) -> length(Args);
fun_arity(_) -> none. fun_arity(_) -> none.
ensure_monomorphic(Type, Err) ->
is_monomorphic(Type) orelse aeso_tc_errors:type_error(Err).
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.
ensure_first_order(Type, Err) ->
is_first_order(Type) orelse aeso_tc_errors:type_error(Err).
is_first_order({fun_t, _, _, _, _}) -> 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.