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

Solve constraints together and in the order they are added (#360)

Browse Source 
* Solve named argument constraints when record type dereferencing fails

* Revert "Solve named argument constraints when record type dereferencing fails"

This reverts commit ca38a171a9eefdddbc3f6a41f8a268c42662cd7a.

* Solve constraints together and in order

* Fix dialyzer warnings

* Add comment on solve_known_record_types

* Remove unused function
This commit is contained in:
Gaith Hallak 2021-12-16 13:54:06 +02:00 committed by GitHub
parent 40c78c1707
commit 60f3a484e6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 200 additions and 224 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

407
src/aeso_ast_infer_types.erl
View File

@ -84,6 +84,11 @@
-type field_constraint() :: #field_constraint{} | #record_create_constraint{} | #is_contract_constraint{}. -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 constraint() :: named_argument_constraint() | field_constraint() | byte_constraint().
-record(field_info, -record(field_info,
{ ann :: aeso_syntax:ann() { ann :: aeso_syntax:ann()
, field_t :: utype() , field_t :: utype()
@ -1312,7 +1317,7 @@ infer_nonrec(Env, LetFun) ->
create_constraints(), create_constraints(),
NewLetFun = infer_letfun(Env, LetFun), NewLetFun = infer_letfun(Env, LetFun),
check_special_funs(Env, NewLetFun), check_special_funs(Env, NewLetFun),
destroy_and_report_unsolved_constraints(Env), solve_then_destroy_and_report_unsolved_constraints(Env),
Result = {TypeSig, _} = instantiate(NewLetFun), Result = {TypeSig, _} = instantiate(NewLetFun),
print_typesig(TypeSig), print_typesig(TypeSig),
Result. Result.
@ -1344,12 +1349,12 @@ infer_letrec(Env, Defs) ->
Got = proplists:get_value(Name, Funs), Got = proplists:get_value(Name, Funs),
Expect = typesig_to_fun_t(TypeSig), Expect = typesig_to_fun_t(TypeSig),
unify(Env, Got, Expect, {check_typesig, Name, Got, Expect}), unify(Env, Got, Expect, {check_typesig, Name, Got, Expect}),
solve_field_constraints(Env), solve_constraints(Env),
?PRINT_TYPES("Checked ~s : ~s\n", ?PRINT_TYPES("Checked ~s : ~s\n",
[Name, pp(dereference_deep(Got))]), [Name, pp(dereference_deep(Got))]),
Res Res
end || LF <- Defs ], end || LF <- Defs ],
destroy_and_report_unsolved_constraints(Env), solve_then_destroy_and_report_unsolved_constraints(Env),
TypeSigs = instantiate([Sig || {Sig, _} <- Inferred]), TypeSigs = instantiate([Sig || {Sig, _} <- Inferred]),
NewDefs = instantiate([D || {_, D} <- Inferred]), NewDefs = instantiate([D || {_, D} <- Inferred]),
[print_typesig(S) || S <- TypeSigs], [print_typesig(S) || S <- TypeSigs],
@ -1539,7 +1544,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),
constrain([#is_contract_constraint{ contract_t = Con, add_constraint([#is_contract_constraint{ contract_t = Con,
context = {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, "_"}) ->
@ -1636,7 +1641,7 @@ infer_expr(Env, {app, Ann, Fun, Args0} = App) ->
fun() -> register_function_call(Namespace ++ qname(CurrentFun), Name) end), fun() -> register_function_call(Namespace ++ qname(CurrentFun), Name) end),
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_named_argument_constraint( add_constraint(
#dependent_type_constraint{ named_args_t = NamedArgsVar, #dependent_type_constraint{ named_args_t = NamedArgsVar,
named_args = NamedArgs1, named_args = NamedArgs1,
general_type = GeneralResultType, general_type = GeneralResultType,
@ -1661,19 +1666,19 @@ 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),
constrain([ #record_create_constraint{ add_constraint([ #record_create_constraint{
record_t = RecordType1, record_t = RecordType1,
fields = [ FieldName || {field, _, [{proj, _, FieldName}], _} <- Fields ], fields = [ FieldName || {field, _, [{proj, _, FieldName}], _} <- Fields ],
context = Attrs } || not Env#env.in_pattern ] ++ context = Attrs } || not Env#env.in_pattern ] ++
[begin [begin
[{proj, _, FieldName}] = LV, [{proj, _, FieldName}] = LV,
#field_constraint{ #field_constraint{
record_t = RecordType1, record_t = RecordType1,
field = FieldName, field = FieldName,
field_t = T, field_t = T,
kind = create, kind = create,
context = Fld} context = Fld}
end || {Fld, {field, _, LV, {typed, _, _, T}}} <- lists:zip(Fields, NewFields)]), 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),
@ -1682,7 +1687,7 @@ 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),
constrain([#field_constraint{ add_constraint([#field_constraint{
record_t = unfold_types_in_type(Env, RecordType), record_t = unfold_types_in_type(Env, RecordType),
field = FieldName, field = FieldName,
field_t = FieldType, field_t = FieldType,
@ -1787,7 +1792,7 @@ 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}),
constrain( add_constraint(
[ #field_constraint{ [ #field_constraint{
record_t = unfold_types_in_type(Env, ContractT), record_t = unfold_types_in_type(Env, ContractT),
field = {id, Ann, ?CONSTRUCTOR_MOCK_NAME}, field = {id, Ann, ?CONSTRUCTOR_MOCK_NAME},
@ -1809,7 +1814,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_named_argument_constraint( add_constraint(
#named_argument_constraint{ #named_argument_constraint{
args = NamedArgs, args = NamedArgs,
name = Id, name = Id,
@ -1847,7 +1852,7 @@ 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,
constrain([#field_constraint{ add_constraint([#field_constraint{
record_t = unfold_types_in_type(Env, RecordType), record_t = unfold_types_in_type(Env, RecordType),
field = FieldName, field = FieldName,
field_t = FldType, field_t = FldType,
@ -1987,9 +1992,8 @@ next_count() ->
%% Clean up all the ets tables (in case of an exception) %% Clean up all the ets tables (in case of an exception)
ets_tables() -> ets_tables() ->
[options, type_vars, type_defs, record_fields, named_argument_constraints, [options, type_vars, constraints, freshen_tvars, type_errors,
field_constraints, freshen_tvars, type_errors, defined_contracts, defined_contracts, warnings, function_calls, all_functions].
warnings, function_calls, all_functions].
clean_up_ets() -> clean_up_ets() ->
[ catch ets_delete(Tab) || Tab <- ets_tables() ], [ catch ets_delete(Tab) || Tab <- ets_tables() ],
@ -2073,43 +2077,111 @@ when_option(Opt, Do) ->
%% -- Constraints -- %% -- Constraints --
create_constraints() -> create_constraints() ->
create_named_argument_constraints(), ets_new(constraints, [ordered_set]).
create_bytes_constraints(),
create_field_constraints(). -spec add_constraint(constraint() | [constraint()]) -> true.
add_constraint(Constraint) ->
ets_insert_ordered(constraints, Constraint).
get_constraints() ->
ets_tab2list_ordered(constraints).
destroy_constraints() ->
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 }) ->
case lookup_record_field(Env, FieldName, Kind) of
[] ->
type_error({undefined_field, Field}),
false;
[#field_info{field_t = FldType, record_t = RecType}] ->
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) -> destroy_and_report_unsolved_constraints(Env) ->
solve_field_constraints(Env), {FieldCs, OtherCs} =
solve_named_argument_constraints(Env), lists:partition(fun(#field_constraint{}) -> true; (_) -> false end,
solve_bytes_constraints(Env), get_constraints()),
destroy_and_report_unsolved_bytes_constraints(Env), {CreateCs, OtherCs1} =
destroy_and_report_unsolved_named_argument_constraints(Env), lists:partition(fun(#record_create_constraint{}) -> true; (_) -> false end,
destroy_and_report_unsolved_field_constraints(Env). 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, []} =
lists:partition(fun({is_bytes, _}) -> true;
({add_bytes, _, _, _, _, _}) -> true;
(_) -> false
end, OtherCs3),
Unsolved = [ S || S <- [ solve_constraint(Env, 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),
destroy_constraints().
%% -- Named argument constraints -- %% -- Named argument constraints --
create_named_argument_constraints() ->
ets_new(named_argument_constraints, [ordered_set]).
destroy_named_argument_constraints() ->
ets_delete(named_argument_constraints).
get_named_argument_constraints() ->
ets_tab2list_ordered(named_argument_constraints).
-spec add_named_argument_constraint(named_argument_constraint()) -> ok.
add_named_argument_constraint(Constraint) ->
ets_insert_ordered(named_argument_constraints, Constraint),
ok.
solve_named_argument_constraints(Env) ->
Unsolved = solve_named_argument_constraints(Env, get_named_argument_constraints()),
Unsolved == [].
-spec solve_named_argument_constraints(env(), [named_argument_constraint()]) -> [named_argument_constraint()].
solve_named_argument_constraints(Env, Constraints0) ->
[ C || C <- dereference_deep(Constraints0),
unsolved == check_named_argument_constraint(Env, C) ].
%% If false, a type error has been emitted, so it's safe to drop the constraint. %% 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. -spec check_named_argument_constraint(env(), named_argument_constraint()) -> true | false | unsolved.
check_named_argument_constraint(_Env, #named_argument_constraint{ args = {uvar, _, _} }) -> check_named_argument_constraint(_Env, #named_argument_constraint{ args = {uvar, _, _} }) ->
@ -2159,34 +2231,43 @@ specialize_dependent_type(Env, Type) ->
_ -> Type %% Currently no deep dependent types _ -> Type %% Currently no deep dependent types
end. end.
destroy_and_report_unsolved_named_argument_constraints(Env) ->
Unsolved = solve_named_argument_constraints(Env, get_named_argument_constraints()),
[ type_error({unsolved_named_argument_constraint, C}) || C <- Unsolved ],
destroy_named_argument_constraints(),
ok.
%% -- Bytes constraints -- %% -- Bytes constraints --
-type byte_constraint() :: {is_bytes, utype()} solve_constraint(_Env, #field_constraint{record_t = {uvar, _, _}}) ->
| {add_bytes, aeso_syntax:ann(), concat | split, utype(), utype(), utype()}. not_solved;
solve_constraint(Env, C = #field_constraint{record_t = RecType,
create_bytes_constraints() -> field = FieldName,
ets_new(bytes_constraints, [ordered_set]). field_t = FieldType,
context = When}) ->
get_bytes_constraints() -> RecId = record_type_name(RecType),
ets_tab2list_ordered(bytes_constraints). Attrs = aeso_syntax:get_ann(RecId),
case lookup_type(Env, RecId) of
-spec add_bytes_constraint(byte_constraint()) -> true. {_, {_Ann, {Formals, {What, Fields}}}} when What =:= record_t; What =:= contract_t ->
add_bytes_constraint(Constraint) -> FieldTypes = [{Name, Type} || {field_t, _, {id, _, Name}, Type} <- Fields],
ets_insert_ordered(bytes_constraints, Constraint). {id, _, FieldString} = FieldName,
case proplists:get_value(FieldString, FieldTypes) of
solve_bytes_constraints(Env) -> undefined ->
[ solve_bytes_constraint(Env, C) || C <- get_bytes_constraints() ], type_error({missing_field, FieldName, RecId}),
ok. not_solved;
FldType ->
solve_bytes_constraint(_Env, {is_bytes, _}) -> ok; create_freshen_tvars(),
solve_bytes_constraint(Env, {add_bytes, Ann, _, A0, B0, C0}) -> 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, 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, dereference(A0)), A = unfold_types_in_type(Env, dereference(A0)),
B = unfold_types_in_type(Env, dereference(B0)), B = unfold_types_in_type(Env, dereference(B0)),
C = unfold_types_in_type(Env, dereference(C0)), C = unfold_types_in_type(Env, dereference(C0)),
@ -2195,13 +2276,10 @@ solve_bytes_constraint(Env, {add_bytes, Ann, _, A0, B0, C0}) ->
{{bytes_t, _, M}, _, {bytes_t, _, R}} when R >= M -> unify(Env, {bytes_t, Ann, R - M}, B, {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}); {_, {bytes_t, _, N}, {bytes_t, _, R}} when R >= N -> unify(Env, {bytes_t, Ann, R - N}, A, {at, Ann});
_ -> ok _ -> ok
end. end;
solve_constraint(_, _) -> ok.
destroy_bytes_constraints() -> check_bytes_constraints(Env, Constraints) ->
ets_delete(bytes_constraints).
destroy_and_report_unsolved_bytes_constraints(Env) ->
Constraints = get_bytes_constraints(),
InAddConstraint = [ T || {add_bytes, _, _, A, B, C} <- Constraints, InAddConstraint = [ T || {add_bytes, _, _, A, B, C} <- Constraints,
T <- [A, B, C], T <- [A, B, C],
element(1, T) /= bytes_t ], element(1, T) /= bytes_t ],
@ -2209,8 +2287,7 @@ destroy_and_report_unsolved_bytes_constraints(Env) ->
%% (no need to generate error messages for both is_bytes and add_bytes). %% (no need to generate error messages for both is_bytes and add_bytes).
Skip = fun({is_bytes, T}) -> lists:member(T, InAddConstraint); Skip = fun({is_bytes, T}) -> lists:member(T, InAddConstraint);
(_) -> false end, (_) -> false end,
[ check_bytes_constraint(Env, C) || C <- Constraints, not Skip(C) ], [ check_bytes_constraint(Env, C) || C <- Constraints, not Skip(C) ].
destroy_bytes_constraints().
check_bytes_constraint(Env, {is_bytes, Type}) -> check_bytes_constraint(Env, {is_bytes, Type}) ->
Type1 = unfold_types_in_type(Env, instantiate(Type)), Type1 = unfold_types_in_type(Env, instantiate(Type)),
@ -2225,33 +2302,12 @@ check_bytes_constraint(Env, {add_bytes, Ann, Fun, A0, B0, C0}) ->
C = unfold_types_in_type(Env, instantiate(C0)), C = unfold_types_in_type(Env, instantiate(C0)),
case {A, B, C} of case {A, B, C} of
{{bytes_t, _, _M}, {bytes_t, _, _N}, {bytes_t, _, _R}} -> {{bytes_t, _, _M}, {bytes_t, _, _N}, {bytes_t, _, _R}} ->
ok; %% If all are solved we checked M + N == R in solve_bytes_constraint. ok; %% If all are solved we checked M + N == R in solve_constraint.
_ -> type_error({unsolved_bytes_constraint, Ann, Fun, A, B, C}) _ -> type_error({unsolved_bytes_constraint, Ann, Fun, A, B, C})
end. end.
%% -- Field constraints -- %% -- Field constraints --
create_field_constraints() ->
%% A relation from uvars to constraints
ets_new(field_constraints, [ordered_set]).
destroy_field_constraints() ->
ets_delete(field_constraints).
-spec constrain([field_constraint()]) -> true.
constrain(FieldConstraints) ->
ets_insert_ordered(field_constraints, FieldConstraints).
-spec get_field_constraints() -> [field_constraint()].
get_field_constraints() ->
ets_tab2list_ordered(field_constraints).
solve_field_constraints(Env) ->
FieldCs =
lists:filter(fun(#field_constraint{}) -> true; (_) -> false end,
get_field_constraints()),
solve_field_constraints(Env, FieldCs).
check_record_create_constraints(_, []) -> ok; check_record_create_constraints(_, []) -> ok;
check_record_create_constraints(Env, [C | Cs]) -> check_record_create_constraints(Env, [C | Cs]) ->
#record_create_constraint{ #record_create_constraint{
@ -2292,49 +2348,6 @@ check_is_contract_constraints(Env, [C | Cs]) ->
end, end,
check_is_contract_constraints(Env, Cs). check_is_contract_constraints(Env, Cs).
-spec solve_field_constraints(env(), [field_constraint()]) -> ok.
solve_field_constraints(Env, Constraints) ->
%% 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 }) ->
case lookup_record_field(Env, FieldName, Kind) of
[] ->
type_error({undefined_field, Field}),
false;
[#field_info{field_t = FldType, record_t = RecType}] ->
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 end,
AmbiguousConstraints = lists:filter(IsAmbiguous, Constraints),
solve_ambiguous_field_constraints(Env, AmbiguousConstraints).
-spec solve_ambiguous_field_constraints(env(), [field_constraint()]) -> ok.
solve_ambiguous_field_constraints(Env, Constraints) ->
Unknown = solve_known_record_types(Env, Constraints),
if Unknown == [] -> ok;
length(Unknown) < length(Constraints) ->
%% progress! Keep trying.
solve_ambiguous_field_constraints(Env, Unknown);
true ->
case solve_unknown_record_types(Env, Unknown) of
true -> %% Progress!
solve_ambiguous_field_constraints(Env, Unknown);
_ -> ok %% No progress. Report errors later.
end
end.
-spec solve_unknown_record_types(env(), [field_constraint()]) -> true | [tuple()]. -spec solve_unknown_record_types(env(), [field_constraint()]) -> true | [tuple()].
solve_unknown_record_types(Env, Unknown) -> solve_unknown_record_types(Env, Unknown) ->
UVars = lists:usort([UVar || #field_constraint{record_t = UVar = {uvar, _, _}} <- Unknown]), UVars = lists:usort([UVar || #field_constraint{record_t = UVar = {uvar, _, _}} <- Unknown]),
@ -2347,69 +2360,17 @@ solve_unknown_record_types(Env, Unknown) ->
false -> Solutions false -> Solutions
end. end.
-spec solve_known_record_types(env(), [field_constraint()]) -> [field_constraint()]. %% 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) -> solve_known_record_types(Env, Constraints) ->
DerefConstraints = DerefConstraints = lists:map(fun(C = #field_constraint{record_t = RecordType}) ->
[ C#field_constraint{record_t = dereference(RecordType)} C#field_constraint{record_t = dereference(RecordType)};
|| C = #field_constraint{record_t = RecordType} <- Constraints ], (C) -> dereference_deep(C)
SolvedConstraints = end, Constraints),
[begin SolvedConstraints = lists:map(fun(C) -> solve_constraint(Env, dereference_deep(C)) end, DerefConstraints),
#field_constraint{record_t = RecType, Unsolved = DerefConstraints--SolvedConstraints,
field = FieldName, lists:filter(fun(#field_constraint{}) -> true; (_) -> false end, Unsolved).
field_t = FieldType,
context = When} = C,
RecId = record_type_name(RecType),
Attrs = aeso_syntax:get_ann(RecId),
case 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, instantiate(RecType), When}),
not_solved
end
end
|| C <- DerefConstraints,
case C#field_constraint.record_t of
{uvar, _, _} -> false;
_ -> true
end],
DerefConstraints--SolvedConstraints.
destroy_and_report_unsolved_field_constraints(Env) ->
{FieldCs, OtherCs} =
lists:partition(fun(#field_constraint{}) -> true; (_) -> false end,
get_field_constraints()),
{CreateCs, OtherCs1} =
lists:partition(fun(#record_create_constraint{}) -> true; (_) -> false end,
OtherCs),
{ContractCs, []} =
lists:partition(fun(#is_contract_constraint{}) -> true; (_) -> false end, OtherCs1),
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),
destroy_field_constraints(),
ok.
record_type_name({app_t, _Attrs, RecId, _Args}) when ?is_type_id(RecId) -> record_type_name({app_t, _Attrs, RecId, _Args}) when ?is_type_id(RecId) ->
RecId; RecId;
@ -2717,7 +2678,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_bytes_constraint({is_bytes, X}), add_constraint({is_bytes, 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)));
@ -2733,14 +2694,14 @@ 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}) ->
constrain([#is_contract_constraint{ contract_t = Type, add_constraint([#is_contract_constraint{ contract_t = Type,
context = {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_bytes_constraint({add_bytes, Ann, concat, A, B, C}); add_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_constraint({add_bytes, Ann, split, A, B, C});
apply_typesig_constraint(Ann, bytecode_hash, {fun_t, _, _, [Con], _}) -> apply_typesig_constraint(Ann, bytecode_hash, {fun_t, _, _, [Con], _}) ->
constrain([#is_contract_constraint{ contract_t = Con, add_constraint([#is_contract_constraint{ contract_t = Con,
context = {bytecode_hash, Ann} }]). context = {bytecode_hash, Ann} }]).

6
test/aeso_compiler_tests.erl
View File

@ -168,6 +168,7 @@ compilable_contracts() ->
"maps", "maps",
"oracles", "oracles",
"remote_call", "remote_call",
"remote_call_ambiguous_record",
"simple", "simple",
"simple_storage", "simple_storage",
"spend_test", "spend_test",
@ -676,7 +677,10 @@ failing_contracts() ->
<<?Pos(15, 5) <<?Pos(15, 5)
"Cannot unify bytes(26)\n" "Cannot unify bytes(26)\n"
" and bytes(25)\n" " and bytes(25)\n"
"at line 15, column 5">>, "when checking the type of the expression at line 15, column 5\n"
" Bytes.concat(x, y) : bytes(26)\n"
"against the expected type\n"
" bytes(25)">>,
<<?Pos(17, 5) <<?Pos(17, 5)
"Failed to resolve byte array lengths in call to Bytes.concat with arguments of type\n" "Failed to resolve byte array lengths in call to Bytes.concat with arguments of type\n"
" - bytes(6) (at line 16, column 24)\n" " - bytes(6) (at line 16, column 24)\n"

11
test/contracts/remote_call_ambiguous_record.aes Normal file
View File

@ -0,0 +1,11 @@
contract interface Coin =
entrypoint mint : () => int
contract interface OtherCoin =
entrypoint mint : () => int
main contract Main =
function mkCoin() : Coin = ct_11111111111111111111111111111115rHyByZ
entrypoint foo() : int =
let r = mkCoin()
r.mint()