Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Define subtyping of unions with type difference #566

Draft
wants to merge 27 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
c66cfb4
Sketch a Common Test dynamic suite shape
erszcz Jun 2, 2024
3993820
Add Makefile ct rule which labels a test run with git commit
erszcz Jun 2, 2024
d97a9f4
Get should_fail test generation to work
erszcz Jun 2, 2024
a46d2a0
Generate all tests for a given path
erszcz Jun 2, 2024
193dcb0
Generate SUITE:all/0 dynamically
erszcz Jun 2, 2024
81e8526
Define all/0 tests manually
erszcz Jun 2, 2024
4213687
Make paths relative to app location
erszcz Jun 2, 2024
57b9ee2
Use EUnit macros for CLI readability
erszcz Jun 2, 2024
fcb443d
Clean up
erszcz Jun 2, 2024
f150d53
Make test template function configurable, pass params from the top
erszcz Jun 2, 2024
34aa4a4
Extract gradualizer_dynamic_suite
erszcz Jun 2, 2024
2c4df55
Add test/should_pass_SUITE.erl
erszcz Jun 2, 2024
0983a7a
Rename: test/should_pass/module_info.erl -> test/should_pass/module_i…
erszcz Jun 2, 2024
b1d8222
Don't explicitly enable maybe_expr
erszcz Jun 2, 2024
e345dc1
Add test/known_problems_should_fail_SUITE.erl
erszcz Jun 2, 2024
314ca8b
Add test/known_problems_should_pass_SUITE.erl
erszcz Jun 2, 2024
b7d3c32
Parallelize CT tests
erszcz Jun 2, 2024
a14c026
Try defining subtype(union(), union()) with type_diff()
erszcz May 30, 2024
50fde32
Add gradualizer_cache:clear/1
erszcz May 31, 2024
a26bb4e
fixup! Try defining subtype(union(), union()) with type_diff()
erszcz May 31, 2024
e15dcbe
fixup! Try defining subtype(union(), union()) with type_diff()
erszcz May 31, 2024
23cfff8
Move should-fail tests which now fail where they belong
erszcz May 31, 2024
11a25b6
Move different_normalization_levels.erl as it now passes
erszcz May 31, 2024
9490673
fixup! Move should-fail tests which now fail where they belong
erszcz May 31, 2024
c594241
Adjust CT test sets
erszcz Jun 2, 2024
cd9603f
Adjust tests of unions with any() member
erszcz Jun 2, 2024
4f1468f
wip
erszcz Jun 1, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -149,6 +149,9 @@ eunit: compile-tests
erl $(ERL_OPTS) -noinput -pa ebin -pa test -eval \
'$(erl_run_eunit), halt().'

ct:
@rebar3 ct --label "git: $$(git describe --tags --always) $$(git diff --no-ext-diff --quiet --exit-code || echo '(modified)')"

cli-tests: bin/gradualizer test/arg.beam
# CLI test cases
# 1. When checking a dir with erl files, erl file names are printed
Expand Down
5 changes: 1 addition & 4 deletions rebar.config
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,7 @@
{deps,
[
{proper, {git, "https://github.com/proper-testing/proper.git", {branch, "master"}}}
]},
%% see the maybe expression fail;
%% the VM also needs to be configured to load the module
{erl_opts, [{feature,maybe_expr,enable}]}
]}
]}
]}.

Expand Down
8 changes: 8 additions & 0 deletions src/gradualizer_cache.erl
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@

%% API
-export([start_link/1,
clear/1,
get/2,
store/3]).

Expand Down Expand Up @@ -66,6 +67,13 @@ store_(Cache, Key, Value) ->
ok
end.

clear(glb) -> clear_(?GLB_CACHE);
clear(subtype) -> clear_(?SUB_CACHE).

clear_(Cache) ->
ets:delete_all_objects(Cache),
ok.

%%===================================================================
%% gen_server callbacks
%%===================================================================
Expand Down
28 changes: 21 additions & 7 deletions src/typechecker.erl
Original file line number Diff line number Diff line change
Expand Up @@ -361,11 +361,23 @@ compat_ty({type, _, 'fun', [{type, _, product, Args1}, Res1]},
{Aps, constraints:combine(Cs, Css, Env)};

%% Unions
compat_ty({type, _, union, Tys1}, {type, _, union, Tys2}, Seen, Env) ->
lists:foldl(fun (Ty1, {Seen1, C1}) ->
{Seen2, C2} = any_type(Ty1, Tys2, Seen1, Env),
{Seen2, constraints:combine(C1, C2, Env)}
end, {Seen, constraints:empty()}, Tys1);
compat_ty({type, _, union, Tys1} = U1, {type, _, union, Tys2} = U2, Seen, Env) ->
IsAny = fun
(?type(any)) -> true;
(_) -> false
end,
case lists:any(IsAny, Tys1) of
true -> ret(Seen);
false ->
case lists:any(IsAny, Tys2) of
true -> ret(Seen);
false ->
case type_diff(U1, U2, Env) of
?type(none) -> ret(Seen);
_ -> throw(nomatch)
end
end
end;
compat_ty(Ty1, {type, _, union, Tys2}, Seen, Env) ->
any_type(Ty1, Tys2, Seen, Env);
compat_ty({type, _, union, Tys1}, Ty2, Seen, Env) ->
Expand Down Expand Up @@ -5746,8 +5758,10 @@ type_check_forms(Forms, Opts) ->
%% a Gradualizer (NOT the checked program!) error.
-spec type_check_form_with_timeout(expr(), [any()], boolean(), env(), [any()]) -> [any()].
type_check_form_with_timeout(Function, Errors, StopOnFirstError, Env, Opts) ->
%% TODO: make FormCheckTimeOut configurable
FormCheckTimeOut = ?form_check_timeout_ms,
FormCheckTimeOut = case lists:keyfind(form_check_timeout_ms, 1, Opts) of
false -> ?form_check_timeout_ms;
{form_check_timeout_ms, MS} -> MS
end,
?verbose(Env, "Spawning async task...~n", []),
Self = self(),
Task = fun () ->
Expand Down
50 changes: 50 additions & 0 deletions test/gradualizer_dynamic_suite.erl
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
-module(gradualizer_dynamic_suite).

-export([reload/1]).

-include_lib("common_test/include/ct.hrl").
-include_lib("stdlib/include/assert.hrl").

reload(Config) ->
Module = ?config(dynamic_suite_module, Config),
Path = ?config(dynamic_suite_test_path, Config),
?assert(Module /= undefined),
?assert(Path /= undefined),
Forms = get_forms(Module),
FilesForms = map_erl_files(fun (File) ->
make_test_form(Forms, File, Config)
end, Path),
{TestFiles, TestForms} = lists:unzip(FilesForms),
TestNames = [ list_to_atom(filename:basename(File, ".erl")) || File <- TestFiles ],
ct:pal("All tests found under ~s:\n~p\n", [Path, TestNames]),
NewForms = Forms ++ TestForms ++ [{eof, 0}],
{ok, _} = merl:compile_and_load(NewForms),
{ok, TestNames}.

map_erl_files(Fun, Dir) ->
Files = filelib:wildcard(filename:join(Dir, "*.erl")),
[{filename:basename(File), Fun(File)} || File <- Files].

make_test_form(Forms, File, Config) ->
TestTemplateName = ?config(dynamic_test_template, Config),
?assert(TestTemplateName /= undefined),
TestTemplate = merl:quote("'@Name'(_) -> _@Body."),
{function, _Anno, _Name, 1, Clauses} = lists:keyfind(TestTemplateName, 3, Forms),
[{clause, _, _Args, _Guards, ClauseBodyTemplate}] = Clauses,
TestName = filename:basename(File, ".erl"),
ClauseBody = merl:subst(ClauseBodyTemplate, [{'File', erl_syntax:string(File)}]),
TestEnv = [
{'Name', erl_syntax:atom(TestName)},
{'Body', ClauseBody}
],
erl_syntax:revert(merl:subst(TestTemplate, TestEnv)).

get_forms(Module) ->
ModPath = code:which(Module),
{ok, {Module, [Abst]}} = beam_lib:chunks(ModPath, [abstract_code]),
{abstract_code, {raw_abstract_v1, Forms}} = Abst,
StripEnd = fun
({eof, _}) -> false;
(_) -> true
end,
lists:filter(StripEnd, Forms).
26 changes: 1 addition & 25 deletions test/known_problems/should_fail/poly_should_fail.erl
Original file line number Diff line number Diff line change
Expand Up @@ -8,12 +8,10 @@
id_id_atom_is_int/1,
id_fun_id_atom_is_int/1,
use_flatten/1,
use_maps_get/3,
use_generic_hd/1,
use_generic_hd_var/1,
inference1/1,
inference2/1,
invariant_tyvar/2
inference2/1
]).

-spec id(A) -> A.
Expand Down Expand Up @@ -56,11 +54,6 @@ pass_id_to_takes_int_to_bool_fun() ->
use_flatten(ListOfListsOfAtoms) ->
lists:flatten(ListOfListsOfAtoms).

%% Type variables in maps usually result in any().
-spec use_maps_get(atom(), #{atom() => binary()}, not_found) -> float() | not_found.
use_maps_get(Key, Map, NotFound) ->
maps:get(Key, Map, NotFound).

%% We do not support polymorphic intersection functions yet.
%% When calling intersection functions, type variables are replaced with any().

Expand Down Expand Up @@ -88,20 +81,3 @@ inference1(L) ->
-spec inference2([integer()]) -> [atom()].
inference2(L) ->
lists:map(fun (I) -> I * 2 end, L).

%% The type variable `A` in `id_fun_arg/2` is invariant in its result type.
%% Thus, if there are multiple possible substitutions, none of them is minimal.
%% In this case we choose `A = the_lower_bound_of_A | any()' which is a bit
%% lenient in some cases, as shown in invariant_tyvar/2. Hopefully, invariant
%% type variables are very rare.

-spec id_fun_arg(fun ((A) -> B), A) -> {fun ((A) -> B), A}.
id_fun_arg(Fun, Arg) -> {Fun, Arg}.

-spec positive(number()) -> boolean().
positive(N) -> N > 0.

-spec invariant_tyvar(integer(), boolean()) -> any().
invariant_tyvar(Int, Bool) ->
{Fun, _Arg} = id_fun_arg(fun positive/1, Int),
Fun(Bool).
90 changes: 90 additions & 0 deletions test/known_problems_should_fail_SUITE.erl
Original file line number Diff line number Diff line change
@@ -0,0 +1,90 @@
-module(known_problems_should_fail_SUITE).

-compile([export_all, nowarn_export_all]).

%% EUnit has some handy macros, so let's use it, too
-include_lib("eunit/include/eunit.hrl").

%% Test server callbacks
-export([suite/0,
all/0,
groups/0,
init_per_suite/1, end_per_suite/1,
init_per_group/2, end_per_group/2,
init_per_testcase/2, end_per_testcase/2]).

suite() ->
[{timetrap, {minutes, 10}}].

init_per_suite(Config0) ->
AppBase = code:lib_dir(gradualizer),
Config = [
{dynamic_suite_module, ?MODULE},
{dynamic_suite_test_path, filename:join(AppBase, "test/known_problems/should_fail")},
{dynamic_test_template, known_problems_should_fail_template}
] ++ Config0,
{ok, _} = application:ensure_all_started(gradualizer),
ok = load_prerequisites(AppBase),
{ok, TestNames} = gradualizer_dynamic_suite:reload(Config),
case all_tests() of
TestNames -> ok;
_ -> ct:fail("Please update all_tests/0 to list all tests")
end,
Config.

load_prerequisites(AppBase) ->
%% exhaustive_user_type.erl is referenced by exhaustive_remote_user_type.erl
gradualizer_db:import_erl_files([filename:join(AppBase, "test/should_fail/exhaustive_user_type.erl")]),
ok.

end_per_suite(_Config) ->
ok = application:stop(gradualizer),
ok.

init_per_group(_GroupName, Config) ->
Config.

end_per_group(_GroupName, _Config) ->
ok.

init_per_testcase(_TestCase, Config) ->
Config.

end_per_testcase(_TestCase, _Config) ->
ok.

all() ->
[{group, all_tests}].

groups() ->
[{all_tests, [parallel], all_tests()}].

all_tests() ->
[arith_op,binary_comprehension,case_pattern_should_fail,
exhaustive_argumentwise,exhaustive_expr,exhaustive_map_variants,
exhaustive_remote_map_variants,guard_should_fail,infer_any_pattern,
intersection_with_any_should_fail,intersection_with_unreachable,
lambda_wrong_args,map_refinement_fancy,poly_lists_map_should_fail,
poly_should_fail,recursive_types_should_fail,refine_ty_vars,sample].

known_problems_should_fail_template(_@File) ->
Result = safe_type_check_file(_@File, [return_errors]),
case Result of
crash ->
ok;
Errors ->
ErrorsExceptTimeouts = lists:filter(
fun ({_File, {form_check_timeout, _}}) -> false; (_) -> true end,
Errors),
?assertEqual(0, length(ErrorsExceptTimeouts))
end.

safe_type_check_file(File) ->
safe_type_check_file(File, []).

safe_type_check_file(File, Opts) ->
try
gradualizer:type_check_file(File, Opts)
catch
_:_ -> crash
end.
85 changes: 85 additions & 0 deletions test/known_problems_should_pass_SUITE.erl
Original file line number Diff line number Diff line change
@@ -0,0 +1,85 @@
-module(known_problems_should_pass_SUITE).

-compile([export_all, nowarn_export_all]).

%% EUnit has some handy macros, so let's use it, too
-include_lib("eunit/include/eunit.hrl").

%% Test server callbacks
-export([suite/0,
all/0,
groups/0,
init_per_suite/1, end_per_suite/1,
init_per_group/2, end_per_group/2,
init_per_testcase/2, end_per_testcase/2]).

suite() ->
[{timetrap, {minutes, 10}}].

init_per_suite(Config0) ->
AppBase = code:lib_dir(gradualizer),
Config = [
{dynamic_suite_module, ?MODULE},
{dynamic_suite_test_path, filename:join(AppBase, "test/known_problems/should_pass")},
{dynamic_test_template, known_problems_should_pass_template}
] ++ Config0,
{ok, _} = application:ensure_all_started(gradualizer),
ok = load_prerequisites(AppBase),
{ok, TestNames} = gradualizer_dynamic_suite:reload(Config),
case all_tests() of
TestNames -> ok;
_ -> ct:fail("Please update all_tests/0 to list all tests")
end,
Config.

load_prerequisites(_AppBase) ->
ok.

end_per_suite(_Config) ->
ok = application:stop(gradualizer),
ok.

init_per_group(_GroupName, Config) ->
Config.

end_per_group(_GroupName, _Config) ->
ok.

init_per_testcase(_TestCase, Config) ->
Config.

end_per_testcase(_TestCase, _Config) ->
ok.

all() ->
[{group, all_tests}].

groups() ->
[{all_tests, [parallel], all_tests()}].

all_tests() ->
[arith_op_arg_types,binary_exhaustiveness_checking_should_pass,
call_intersection_function_with_union_arg_should_pass,elixir_list_first,
error_in_guard,fun_subtyping,generator_var_shadow,
inner_union_subtype_of_root_union,intersection_should_pass,
intersection_with_any,list_concat_op_should_pass,list_tail,
map_pattern_duplicate_key,maybe_expr,poly_should_pass,poly_type_vars,
recursive_types,refine_bound_var_on_mismatch,
refine_bound_var_with_guard_should_pass,refine_comparison_should_pass,
refine_list_tail,union_fun].

known_problems_should_pass_template(_@File) ->
{ok, Forms} = gradualizer_file_utils:get_forms_from_erl(_@File, []),
ExpectedErrors = typechecker:number_of_exported_functions(Forms),
ReturnedErrors = length(safe_type_check_file(_@File, [return_errors])),
?assertEqual(ExpectedErrors, ReturnedErrors).

safe_type_check_file(File) ->
safe_type_check_file(File, []).

safe_type_check_file(File, Opts) ->
try
gradualizer:type_check_file(File, Opts)
catch
_:_ -> crash
end.
Loading
Loading