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

Clean up constraint solving a bit

Browse Source
This commit is contained in:
Hans Svensson 2023-08-07 17:45:01 +02:00
parent 86d7b36ba7
commit 6207cd09e2
1 changed files with 42 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

98
src/aeso_ast_infer_types.erl
View File

@ -2609,22 +2609,19 @@ solve_constraints(Env) ->
end; end;
(_) -> true (_) -> true
end, end,
AmbiguousConstraints = lists:filter(IsAmbiguous, get_constraints()),
% The two passes on AmbiguousConstraints are needed solve_ambiguous_constraints(Env, lists:filter(IsAmbiguous, get_constraints())).
solve_ambiguous_constraints(Env, AmbiguousConstraints ++ AmbiguousConstraints).
-spec solve_ambiguous_constraints(env(), [constraint()]) -> ok. -spec solve_ambiguous_constraints(env(), [constraint()]) -> ok.
solve_ambiguous_constraints(Env, Constraints) -> solve_ambiguous_constraints(Env, Constraints) ->
Unknown = solve_known_record_types(Env, Constraints), Unsolved = solve_constraints(Env, Constraints),
if Unknown == [] -> ok; if length(Unsolved) < length(Constraints) ->
length(Unknown) < length(Constraints) ->
%% progress! Keep trying. %% progress! Keep trying.
solve_ambiguous_constraints(Env, Unknown); solve_ambiguous_constraints(Env, Unsolved);
true -> true ->
case solve_unknown_record_types(Env, Unknown) of case solve_unknown_record_types(Env, Unsolved) of
true -> %% Progress! true -> %% Progress!
solve_ambiguous_constraints(Env, Unknown); solve_ambiguous_constraints(Env, Unsolved);
_ -> ok %% No progress. Report errors later. _ -> ok %% No progress. Report errors later.
end end
end. end.
@ -2661,17 +2658,13 @@ destroy_and_report_unsolved_constraints(Env) ->
(_) -> false (_) -> false
end, OtherCs5), end, OtherCs5),
Unsolved = [ S || S <- [ solve_constraint(Env, dereference_deep(C)) || C <- NamedArgCs ], UnsolvedNamedArgCs = solve_constraints(Env, NamedArgCs),
S == unsolved ], [ type_error({unsolved_named_argument_constraint, C}) || C <- UnsolvedNamedArgCs ],
[ type_error({unsolved_named_argument_constraint, C}) || C <- Unsolved ],
Unknown = solve_known_record_types(Env, FieldCs), UnsolvedFieldCs = solve_constraints(Env, FieldCs),
if Unknown == [] -> ok; case solve_unknown_record_types(Env, UnsolvedFieldCs) of
true -> true -> ok;
case solve_unknown_record_types(Env, Unknown) of Errors -> [ type_error(Err) || Err <- Errors ]
true -> ok;
Errors -> [ type_error(Err) || Err <- Errors ]
end
end, end,
check_record_create_constraints(Env, CreateCs), check_record_create_constraints(Env, CreateCs),
@ -2693,20 +2686,21 @@ get_oracle_type(_Fun, _Args, _Ret) -> false.
%% -- Named argument constraints -- %% -- Named argument constraints --
%% If false, a type error has been emitted, so it's safe to drop the constraint. %% True if solved (unified or type error), false otherwise
-spec check_named_argument_constraint(env(), named_argument_constraint()) -> true | false | unsolved. -spec check_named_argument_constraint(env(), named_argument_constraint()) -> true | false.
check_named_argument_constraint(_Env, #named_argument_constraint{ args = {uvar, _, _} }) -> check_named_argument_constraint(_Env, #named_argument_constraint{ args = {uvar, _, _} }) ->
unsolved; false;
check_named_argument_constraint(Env, check_named_argument_constraint(Env,
C = #named_argument_constraint{ args = Args, C = #named_argument_constraint{ args = Args,
name = Id = {id, _, Name}, name = Id = {id, _, Name},
type = Type }) -> type = Type }) ->
case [ T || {named_arg_t, _, {id, _, Name1}, T, _} <- Args, Name1 == Name ] of case [ T || {named_arg_t, _, {id, _, Name1}, T, _} <- Args, Name1 == Name ] of
[] -> [] ->
type_error({bad_named_argument, Args, Id}), type_error({bad_named_argument, Args, Id});
false; [T] ->
[T] -> unify(Env, T, Type, {check_named_arg_constraint, C}), true unify(Env, T, Type, {check_named_arg_constraint, C})
end; end,
true;
check_named_argument_constraint(Env, check_named_argument_constraint(Env,
#dependent_type_constraint{ named_args_t = NamedArgsT0, #dependent_type_constraint{ named_args_t = NamedArgsT0,
named_args = NamedArgs, named_args = NamedArgs,
@ -2723,10 +2717,11 @@ check_named_argument_constraint(Env,
ArgEnv = maps:from_list([ {Name, GetVal(Name, Default)} ArgEnv = maps:from_list([ {Name, GetVal(Name, Default)}
|| {named_arg_t, _, {id, _, Name}, _, Default} <- NamedArgsT ]), || {named_arg_t, _, {id, _, Name}, _, Default} <- NamedArgsT ]),
GenType1 = specialize_dependent_type(ArgEnv, GenType), GenType1 = specialize_dependent_type(ArgEnv, GenType),
unify(Env, GenType1, SpecType, {check_expr, App, GenType1, SpecType}), unify(Env, GenType1, SpecType, {check_expr, App, GenType1, SpecType});
true; _ ->
_ -> unify(Env, GenType, SpecType, {check_expr, App, GenType, SpecType}), true unify(Env, GenType, SpecType, {check_expr, App, GenType, SpecType})
end. end,
true.
specialize_dependent_type(Env, Type) -> specialize_dependent_type(Env, Type) ->
case dereference(Type) of case dereference(Type) of
@ -2744,12 +2739,13 @@ specialize_dependent_type(Env, Type) ->
%% -- Bytes constraints -- %% -- Bytes constraints --
%% Returns true if solved (unified or type error)
solve_constraint(_Env, #field_constraint{record_t = {uvar, _, _}}) -> solve_constraint(_Env, #field_constraint{record_t = {uvar, _, _}}) ->
not_solved; false;
solve_constraint(Env, C = #field_constraint{record_t = RecType, solve_constraint(Env, #field_constraint{record_t = RecType,
field = FieldName, field = FieldName,
field_t = FieldType, field_t = FieldType,
context = When}) -> context = When}) ->
RecId = record_type_name(RecType), RecId = record_type_name(RecType),
Attrs = aeso_syntax:get_ann(RecId), Attrs = aeso_syntax:get_ann(RecId),
case lookup_type(Env, RecId) of case lookup_type(Env, RecId) of
@ -2758,26 +2754,24 @@ solve_constraint(Env, C = #field_constraint{record_t = RecType,
{id, _, FieldString} = FieldName, {id, _, FieldString} = FieldName,
case proplists:get_value(FieldString, FieldTypes) of case proplists:get_value(FieldString, FieldTypes) of
undefined -> undefined ->
type_error({missing_field, FieldName, RecId}), type_error({missing_field, FieldName, RecId});
not_solved;
FldType -> FldType ->
create_freshen_tvars(), create_freshen_tvars(),
FreshFldType = freshen(FldType), FreshFldType = freshen(FldType),
FreshRecType = freshen(app_t(Attrs, RecId, Formals)), FreshRecType = freshen(app_t(Attrs, RecId, Formals)),
destroy_freshen_tvars(), destroy_freshen_tvars(),
unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}), unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}),
unify(Env, FreshRecType, RecType, {record_constraint, FreshRecType, RecType, When}), unify(Env, FreshRecType, RecType, {record_constraint, FreshRecType, RecType, When})
C
end; end;
_ -> _ ->
type_error({not_a_record_type, instantiate(RecType), When}), type_error({not_a_record_type, instantiate(RecType), When})
not_solved end,
end; true;
solve_constraint(Env, C = #dependent_type_constraint{}) -> solve_constraint(Env, C = #dependent_type_constraint{}) ->
check_named_argument_constraint(Env, C); check_named_argument_constraint(Env, C);
solve_constraint(Env, C = #named_argument_constraint{}) -> solve_constraint(Env, C = #named_argument_constraint{}) ->
check_named_argument_constraint(Env, C); check_named_argument_constraint(Env, C);
solve_constraint(_Env, {is_bytes, _}) -> ok; solve_constraint(_Env, {is_bytes, _}) -> false;
solve_constraint(Env, {add_bytes, Ann, _, A0, B0, C0}) -> 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)),
@ -2786,9 +2780,9 @@ solve_constraint(Env, {add_bytes, Ann, _, A0, B0, C0}) ->
{{bytes_t, _, M}, {bytes_t, _, N}, _} -> unify(Env, {bytes_t, Ann, M + N}, C, {at, Ann}); {{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, _, 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 _ -> false
end; end;
solve_constraint(_, _) -> ok. solve_constraint(_, _) -> false.
check_bytes_constraints(Env, Constraints) -> check_bytes_constraints(Env, Constraints) ->
InAddConstraint = [ T || {add_bytes, _, _, A, B, C} <- Constraints, InAddConstraint = [ T || {add_bytes, _, _, A, B, C} <- Constraints,
@ -2897,17 +2891,9 @@ solve_unknown_record_types(Env, Unknown) ->
false -> Solutions false -> Solutions
end. end.
%% This will solve all kinds of constraints but will only return the -spec solve_constraints(env(), [constraint()]) -> [constraint()].
%% unsolved field constraints solve_constraints(Env, Constraints) ->
-spec solve_known_record_types(env(), [constraint()]) -> [field_constraint()]. [ C1 || C <- Constraints, C1 <- [dereference_deep(C)], not solve_constraint(Env, C1) ].
solve_known_record_types(Env, Constraints) ->
DerefConstraints = lists:map(fun(C = #field_constraint{record_t = RecordType}) ->
C#field_constraint{record_t = dereference(RecordType)};
(C) -> dereference_deep(C)
end, Constraints),
SolvedConstraints = lists:map(fun(C) -> solve_constraint(Env, 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) -> record_type_name({app_t, _Attrs, RecId, _Args}) when ?is_type_id(RecId) ->
RecId; RecId;