Skip to content

Commit

Permalink
Merge pull request #573 from erszcz/drop-infer-flag
Browse files Browse the repository at this point in the history
Drop the --infer flag
  • Loading branch information
erszcz authored Oct 11, 2024
2 parents fd564a4 + d3968cf commit 112646d
Show file tree
Hide file tree
Showing 24 changed files with 85 additions and 203 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ bin/gradualizer: $(beams) ebin/gradualizer.app

.PHONY: gradualize
gradualize: escript
@bin/gradualizer --infer --solve_constraints --specs_override_dir priv/extra_specs/ \
@bin/gradualizer --solve_constraints --specs_override_dir priv/extra_specs/ \
-pa ebin --color ebin | grep -v -f gradualize-ignore.lst

.PHONY: nocrashongradualize
Expand Down
3 changes: 1 addition & 2 deletions src/gradualizer.erl
Original file line number Diff line number Diff line change
Expand Up @@ -425,7 +425,6 @@ type_of(Expr) ->
%% '''
-spec type_of(string(), typechecker:env()) -> typechecker:type().
type_of(Expr, Env) ->
AlwaysInfer = Env#env{infer = true},
[Form] = gradualizer_lib:ensure_form_list(merl:quote(lists:flatten(Expr))),
{Ty, _Env} = typechecker:type_check_expr(AlwaysInfer, Form),
{Ty, _Env} = typechecker:type_check_expr(Env, Form),
Ty.
5 changes: 0 additions & 5 deletions src/gradualizer_cli.erl
Original file line number Diff line number Diff line change
Expand Up @@ -70,10 +70,7 @@ print_usage() ->
io:format(" arguments are treated as filenames, even if~n"),
io:format(" they start with hyphens.~n"),
io:format(" -h, --help display this help and exit~n"),
io:format(" --infer Infer type information from literals and other~n"),
io:format(" language constructs~n"),
io:format(" --no_infer Only use type information from function specs~n"),
io:format(" - the default behaviour~n"),
io:format(" --verbose Show what Gradualizer is doing~n"),
io:format(" -pa, --path_add Add the specified directory to the beginning of~n"),
io:format(" the code path; see erl -pa [string]~n"),
Expand Down Expand Up @@ -109,8 +106,6 @@ parse_opts([A | Args], Opts) ->
case A of
"-h" -> {[], [help]};
"--help" -> {[], [help]};
"--infer" -> parse_opts(Args, [infer | Opts]);
"--no_infer" -> parse_opts(Args, [{infer, false} | Opts]);
"--verbose" -> parse_opts(Args, [verbose | Opts]);
"-pa" -> handle_path_add(A, Args, Opts);
"--path_add" -> handle_path_add(A, Args, Opts);
Expand Down
127 changes: 29 additions & 98 deletions src/typechecker.erl
Original file line number Diff line number Diff line change
Expand Up @@ -1869,26 +1869,13 @@ do_type_check_expr(Env, {'case', _, Expr, Clauses}) ->
{Ty, union_var_binds(Env1, VB, Env)};
do_type_check_expr(Env, {tuple, _, TS}) ->
{Tys, VarBindsList} = lists:unzip([ type_check_expr(Env, Expr) || Expr <- TS ]),
InferredTy =
case not Env#env.infer andalso
lists:all(fun({type, _, any, []}) -> true;
(_) -> false
end, Tys) of
true ->
type(any);
false ->
%% at least one element in the tuple has a type inferred from a spec
type(tuple, Tys)
end,
InferredTy = type(tuple, Tys),
{InferredTy, union_var_binds(VarBindsList, Env)};
do_type_check_expr(Env, {cons, _, Head, Tail}) ->
{Ty1, VB1} = type_check_expr(Env, Head),
{Ty2, VB2} = type_check_expr(Env, Tail),
VB = union_var_binds(VB1, VB2, Env),
case {Ty1, Ty2} of
{?type(any), ?type(any)} when not Env#env.infer ->
%% No type information to propagate
{type(any), VB};
{_, ?type(any)} ->
%% Propagate type information from head
{type(nonempty_list, [Ty1]), VB};
Expand Down Expand Up @@ -1922,14 +1909,8 @@ do_type_check_expr(Env, {bin, _, BinElements} = BinExpr) ->
type_check_expr_in(Env, Ty, Expr)
end,
BinElements),
RetTy = if
Env#env.infer ->
%% Infer the size parameters of the bitstring
gradualizer_bin:compute_type(BinExpr);
not Env#env.infer ->
type(any)
end,
RetTy = ?assert_type(RetTy, type()),
%% Infer the size parameters of the bitstring
RetTy = gradualizer_bin:compute_type(BinExpr),
{RetTy, union_var_binds(VarBinds, Env)};
do_type_check_expr(Env, {call, _, {atom, _, TypeOp}, [Expr, {string, _, TypeStr} = TypeLit]})
when TypeOp == '::'; TypeOp == ':::' ->
Expand Down Expand Up @@ -1975,46 +1956,24 @@ do_type_check_expr(Env, {bc, _, Expr, Qualifiers}) ->
do_type_check_expr(Env, {block, _, Block}) ->
type_check_block(Env, Block);

% Don't return the type of anything other than something
% which ultimately comes from a function type spec.
do_type_check_expr(#env{infer = false} = Env, {string, _, _}) ->
{type(any), Env};
do_type_check_expr(#env{infer = false} = Env, {nil, _}) ->
{type(any), Env};
do_type_check_expr(#env{infer = false} = Env, {atom, _, _Atom}) ->
{type(any), Env};
do_type_check_expr(#env{infer = false} = Env, {integer, _, _N}) ->
{type(any), Env};
do_type_check_expr(#env{infer = false} = Env, {float, _, _F}) ->
{type(any), Env};
do_type_check_expr(#env{infer = false} = Env, {char, _, _C}) ->
{type(any), Env};

%% When infer = true, we do propagate the types of literals,
%% list cons, tuples, etc.
do_type_check_expr(#env{infer = true} = Env, {string, _, Chars}) ->
do_type_check_expr(Env, {string, _, Chars}) ->
ActualTy = infer_literal_string(Chars, Env),
{ActualTy, Env};
do_type_check_expr(#env{infer = true} = Env, {nil, _}) ->
do_type_check_expr(Env, {nil, _}) ->
{type(nil), Env};
do_type_check_expr(#env{infer = true} = Env, {Tag, _, Value})
do_type_check_expr(Env, {Tag, _, Value})
when Tag =:= atom;
Tag =:= integer;
Tag =:= char ->
{singleton(Tag, Value), Env};
do_type_check_expr(#env{infer = true} = Env, {float, _, _F}) ->
do_type_check_expr(Env, {float, _, _F}) ->
{type(float), Env};

%% Maps
do_type_check_expr(Env, {map, _, Assocs}) ->
{AssocTys, VB} = type_check_assocs(Env, Assocs),
case Env#env.infer of
true ->
MapTy = update_map_type(type(map, []), AssocTys),
{MapTy, VB};
false ->
{type(any), VB}
end;
MapTy = update_map_type(type(map, []), AssocTys),
{MapTy, VB};
do_type_check_expr(Env, {map, _, UpdateExpr, Assocs}) ->
{Ty, VBExpr} = type_check_expr(Env, UpdateExpr),
{AssocTys, VBAssocs} = type_check_assocs(Env, Assocs),
Expand Down Expand Up @@ -2058,14 +2017,9 @@ do_type_check_expr(Env, {record, Anno, Record, Fields}) ->
VB = type_check_fields(Env, Rec, Fields),
{RecTy, VB};
do_type_check_expr(Env, {record_index, Anno, Name, FieldWithAnno}) ->
case Env#env.infer of
true ->
RecFields = get_record_fields(Name, Anno, Env),
Index = get_rec_field_index(FieldWithAnno, RecFields),
{{integer, erl_anno:new(0), Index}, Env};
false ->
{type(any), Env}
end;
RecFields = get_record_fields(Name, Anno, Env),
Index = get_rec_field_index(FieldWithAnno, RecFields),
{{integer, erl_anno:new(0), Index}, Env};

%% Functions
do_type_check_expr(Env, {'fun', _, {clauses, Clauses}}) ->
Expand Down Expand Up @@ -2097,16 +2051,11 @@ do_type_check_expr(Env, {'fun', P, {function, M, F, A}}) ->
do_type_check_expr(Env, {named_fun, _, FunName, Clauses}) ->
%% Pick a type for the fun itself, to be used when checking references to
%% itself inside the fun, e.g. recursive calls.
FunTy = if
Env#env.infer ->
%% Create a fun type of the correct arity
%% on the form fun((_,_,_) -> any()).
[{clause, _, Params, _Guards, _Block} | _] = Clauses,
Arity = arity(length(Params)),
create_fun_type(Arity, type(any));
not Env#env.infer ->
type(any)
end,
%% Create a fun type of the correct arity
%% on the form fun((_,_,_) -> any()).
[{clause, _, Params, _Guards, _Block} | _] = Clauses,
Arity = arity(length(Params)),
FunTy = create_fun_type(Arity, type(any)),
NewEnv = add_var_binds(Env#env{venv = #{FunName => FunTy}}, Env, Env),
type_check_fun(NewEnv, Clauses);

Expand Down Expand Up @@ -2235,16 +2184,11 @@ type_check_fun(Env, Clauses) ->
%% accurate type to the whole expression.
%% TODO: Modify OTP's type syntax to allow returning an intersection type.
{RetTy, _VB} = infer_clauses(Env, Clauses),
FunTy = case RetTy of
{type, _, any, []} when not Env#env.infer ->
type(any);
_SomeTypeToPropagate ->
%% Create a fun type with the correct arity on the form
%% fun((any(), any(), ...) -> RetTy).
[{clause, _, Params, _Guards, _Body} | _] = Clauses,
Arity = arity(length(Params)),
create_fun_type(Arity, RetTy)
end,
%% Create a fun type with the correct arity on the form
%% fun((any(), any(), ...) -> RetTy).
[{clause, _, Params, _Guards, _Body} | _] = Clauses,
Arity = arity(length(Params)),
FunTy = create_fun_type(Arity, RetTy),
%% Variable bindings inside the fun clauses are local inside the fun.
{FunTy, Env}.

Expand Down Expand Up @@ -2559,7 +2503,7 @@ minimal_substitution(Cs, ResTy) ->
-spec infer_arg_types([expr()], env()) -> [type()].
infer_arg_types(Args, Env) ->
lists:map(fun (Arg) ->
{ArgTy, _VB} = type_check_expr(Env#env{infer = true}, Arg),
{ArgTy, _VB} = type_check_expr(Env, Arg),
ArgTy
end, Args).

Expand Down Expand Up @@ -2612,17 +2556,7 @@ compat_arith_type(Ty1, Ty2, Env) ->
-spec type_check_comprehension(env(), _, expr(), _) -> {type(), env()}.
type_check_comprehension(Env, lc, Expr, []) ->
{Ty, _VB} = type_check_expr(Env, Expr),
RetTy = case Ty of
{type, _, any, []} when not Env#env.infer ->
%% No type information to propagate. We don't infer a
%% list type of the list comprehension when inference
%% is disabled.
type(any);
_ ->
%% Propagate the type information
{type, erl_anno:new(0), list, [Ty]}
end,
RetTy = ?assert_type(RetTy, type()),
RetTy = {type, erl_anno:new(0), list, [Ty]},
{RetTy, Env};
type_check_comprehension(Env, bc, Expr, []) ->
{Ty, _VB} = type_check_expr(Env, Expr),
Expand Down Expand Up @@ -2795,7 +2729,7 @@ do_type_check_expr_in(Env, ResTy, {tuple, _, TS} = Tup) ->
{elem_tys, Tyss} ->
case type_check_tuple_union_in(Env, Tyss, TS) of
none ->
{Ty, _VB} = type_check_expr(Env#env{infer = true}, Tup),
{Ty, _VB} = type_check_expr(Env, Tup),
throw(type_error(Tup, Ty, ResTy));
VBs ->
union_var_binds(VBs, Env)
Expand All @@ -2804,7 +2738,7 @@ do_type_check_expr_in(Env, ResTy, {tuple, _, TS} = Tup) ->
{_Tys, VBs} = lists:unzip([type_check_expr(Env, Expr) || Expr <- TS ]),
union_var_binds(VBs, Env);
{type_error, _} ->
{Ty, _VB} = type_check_expr(Env#env{infer = true}, Tup),
{Ty, _VB} = type_check_expr(Env, Tup),
throw(type_error(Tup, Ty, ResTy))
end;

Expand Down Expand Up @@ -2958,8 +2892,6 @@ do_type_check_expr_in(Env, Ty, {'fun', _, {clauses, Clauses}} = Fun) ->
end;
do_type_check_expr_in(Env, ResTy, Expr = {'fun', P, {function, Name, Arity}}) ->
case get_bounded_fun_type_list(Name, Arity, Env, P) of
[?type(any)] when not Env#env.infer ->
Env;
[?type(any)] ->
FunType = create_fun_type(Arity, type(any)),
case subtype(FunType, ResTy, Env) of
Expand Down Expand Up @@ -3259,7 +3191,7 @@ type_check_logic_op_in(Env, ResTy, {op, _, Op, Arg1, Arg2} = OrigExpr) when Op =
VarBinds2 = type_check_expr_in(EnvArg2, ResTy, Arg2),
union_var_binds(VarBinds1, VarBinds2, Env);
false ->
{Arg2Ty, _VB} = type_check_expr(Env#env{infer = true}, Arg2),
{Arg2Ty, _VB} = type_check_expr(Env, Arg2),
Ty = type(union, [Arg2Ty, Target]),
throw(type_error(OrigExpr, Ty, ResTy))
end;
Expand Down Expand Up @@ -3500,8 +3432,8 @@ type_check_comprehension_in(Env, ResTy, OrigExpr, Compr, Expr, P, [Pred | Quals]
-spec type_check_assocs(env(), _) -> {[type()], env()}.
type_check_assocs(Env, [{Assoc, _P, Key, Val}| Assocs])
when Assoc == map_field_assoc orelse Assoc == map_field_exact ->
{KeyTy, _KeyVB} = type_check_expr(Env#env{infer = true}, Key),
{ValTy, _ValVB} = type_check_expr(Env#env{infer = true}, Val),
{KeyTy, _KeyVB} = type_check_expr(Env, Key),
{ValTy, _ValVB} = type_check_expr(Env, Val),
{AssocTys, VB} = type_check_assocs(Env, Assocs),
{[type(Assoc, [KeyTy, ValTy]) | AssocTys], VB};
type_check_assocs(Env, []) ->
Expand Down Expand Up @@ -5829,7 +5761,6 @@ create_env(#parsedata{module = Module
tenv = TEnv,
imported = Imported,
%% Store some type checking options in the environment
infer = proplists:get_bool(infer, Opts),
verbose = proplists:get_bool(verbose, Opts),
union_size_limit = proplists:get_value(union_size_limit, Opts,
default_union_size_limit()),
Expand Down
1 change: 0 additions & 1 deletion src/typechecker.hrl
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@
imported = #{} :: #{{atom(), arity()} => module()},
venv = #{} :: typechecker:venv(),
tenv :: gradualizer_lib:tenv(),
infer = false :: boolean(),
verbose = false :: boolean(),
exhaust = true :: boolean(),
%% Controls driving the type checking algorithm
Expand Down
11 changes: 2 additions & 9 deletions test/gradualizer_cli_tests.erl
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
help_test() ->
?assertEqual(help, gradualizer_cli:handle_args([])),
?assertEqual(help, gradualizer_cli:handle_args(["--help"])),
?assertEqual(help, gradualizer_cli:handle_args(["--infer", "-h", "other.junk"])).
?assertEqual(help, gradualizer_cli:handle_args(["-h", "other.junk"])).

help_output_no_halt_test() ->
%% This gives code coverage to the printing of the help text.
Expand All @@ -18,19 +18,12 @@ version_test() ->

no_file_test() ->
?assertMatch({error, "No files"++_},
gradualizer_cli:handle_args(["--infer"])).
gradualizer_cli:handle_args(["--solve_constraints"])).

invalid_arg_test() ->
?assertMatch({error, "Unknown"++_},
gradualizer_cli:handle_args(["--invalid-arg", "file.erl"])).

infer_test() ->
{ok, _Files, Opts} = gradualizer_cli:handle_args(["--infer", "--", "file.erl"]),
?assert(proplists:get_bool(infer, Opts)).
no_infer_test() ->
{ok, _Files, Opts} = gradualizer_cli:handle_args(["--no_infer", "file.erl"]),
?assertNot(proplists:get_bool(infer, Opts)).

verbose_test() ->
{ok, _Files, Opts} = gradualizer_cli:handle_args(["--verbose", "file.erl"]),
?assert(proplists:get_bool(verbose, Opts)).
Expand Down
2 changes: 0 additions & 2 deletions test/known_problems/should_fail/infer_any_pattern.erl
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,6 @@

-export([pat_any/1]).

-gradualizer([infer]).

%% We would expect (at least when infer mode is enabled) that type of
%% I, S and L is integer(), string() and list() respectively but
%% currently they all become any()
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
-module(binary_exhaustiveness_checking_should_pass).

-gradualizer([infer]).

-export([f/0]).

-spec f() -> ok.
Expand Down
15 changes: 1 addition & 14 deletions test/known_problems/should_pass/poly_should_pass.erl
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,7 @@

-gradualizer([solve_constraints]).

-export([find1/0,
l/0]).

-spec lookup(T1, [{T1, T2}]) -> (none | T2).
lookup(_, []) -> none;
lookup(K, [{K, V}|_]) -> V;
lookup(K, [_|KVs]) -> lookup(K, KVs).

-spec find1() -> string().
find1() ->
case lookup(0, [{0, "s"}]) of
none -> "default";
V -> V
end.
-export([l/0]).

-type t1() :: {}.
-type t2() :: binary().
Expand Down
1 change: 0 additions & 1 deletion test/should_fail/infer_enabled.erl
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
-module(infer_enabled).

-gradualizer(infer).
-export([f/0]).

f() ->
Expand Down
1 change: 0 additions & 1 deletion test/should_fail/list_infer_fail.erl
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
-module(list_infer_fail).

-gradualizer(infer).
-export([f/0]).

f() ->
Expand Down
1 change: 0 additions & 1 deletion test/should_fail/map_failing_expr.erl
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
-module(map_failing_expr).
-gradualizer([infer]).

-export([foo/0, bar/0]).

Expand Down
11 changes: 10 additions & 1 deletion test/should_fail/named_fun_fail.erl
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
-module(named_fun_fail).

-export([bar/0, baz/1]).
-export([bar/0, baz/1, sum/1]).

-spec foo(integer()) -> integer().
foo(N) -> N.
Expand All @@ -11,3 +11,12 @@ bar() -> foo(fun F(0) -> 0; F(X) -> F(X - 1) end).
baz(I) ->
O = I({}),
O.

-spec sum([integer()]) -> integer().
sum(Ints) ->
F = fun Sum(Acc, [Int | Rest]) ->
Sum(Acc + Int, Rest);
Sum(Acc, []) ->
Acc
end,
F(Ints).
Loading

0 comments on commit 112646d

Please sign in to comment.