%%% This file is part of RefactorErl.
%%%
%%% RefactorErl is free software: you can redistribute it and/or modify
%%% it under the terms of the GNU Lesser General Public License as published
%%% by the Free Software Foundation, either version 3 of the License, or
%%% (at your option) any later version.
%%%
%%% RefactorErl is distributed in the hope that it will be useful,
%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%%% GNU Lesser General Public License for more details.
%%%
%%% You should have received a copy of the GNU Lesser General Public License
%%% along with RefactorErl.  If not, see <http://plc.inf.elte.hu/erlang/>.
%%%
%%% The Original Code is RefactorErl.
%%%
%%% The Initial Developer of the Original Code is Eötvös Loránd University.
%%% Portions created  by Eötvös Loránd University and ELTE-Soft Ltd.
%%% are Copyright 2007-2025 Eötvös Loránd University, ELTE-Soft Ltd.
%%% and Ericsson Hungary. All Rights Reserved.


%%% ============================================================================
%%% Module information

%%% @doc Type inference related code.

%%% @author Drienyovszky D�niel <monogram@inf.elte.hu>

%%% NB.: This module depends on the internals of dialyzer and HiPE,
%%% particularily on the type representation used
-module(refqc_dd_types).
-vsn("$Rev: 17551 $").

-export([t_to_gen/1, t_to_pattern_gen/1]).
-export([infer/3, is_subtype/2]).
-include_lib("referl_qc/include/prop_based_testing.hrl").

%%=============================================================================
%%
%% Type inferencing using dialyzer
%%
%%=============================================================================

-define(PLT, ".refactorerl.plt").

%% @doc Infers the type of the given function.
%% @spec infer(atom(), atom(), integer()) -> erl_type()
infer(M, F, A) ->
    Plt = dialyzer_plt:from_file(?PLT),
    {CS, CG} = collect([filename:join(?TestDir, atom_to_list(M) ++ ".erl")]),
    SCG = strip_callgraph(CG),
    NPlt = dialyzer_succ_typings:analyze_callgraph(SCG, Plt, CS),
    case dialyzer_plt:lookup(NPlt, {M, F, A}) of
        none             -> throw(error);
        {value, {_R, As}} -> As
    end.

strip_callgraph(CG) ->
    {SC, _} = dialyzer_callgraph:remove_external(CG),
    dialyzer_callgraph:finalize(SC).

collect(Files) ->
    CS = dialyzer_codeserver:new(),
    CG = dialyzer_callgraph:new(),
    lists:foldl(fun analyze/2, {CS, CG}, Files).

analyze(File, State) ->
    Opts = dialyzer_utils:src_compiler_opts(),
    case dialyzer_utils:get_abstract_code_from_src(File, Opts) of
        {error, Reason} ->
            io:format("error: ~p~n", [Reason]);
        {ok, AbsCode} ->
            case dialyzer_utils:get_core_from_abstract_code(AbsCode, Opts) of
                {error, Reason} ->
                    io:format("error: ~p~n", [Reason]);
                {ok, Core} ->
                    analyze_core(Core, File, State)
            end
    end.

analyze_core(Core, File, {CS, CG}) ->
    Mod = list_to_atom(filename:basename(File, ".erl")),
    Label = dialyzer_codeserver:get_next_core_label(CS),
    {Tree, NewLabel} = cerl_trees:label(cerl:from_records(Core), Label),
    CS1 = dialyzer_codeserver:insert(Mod, Tree, CS),
    CS2 = dialyzer_codeserver:set_next_core_label(NewLabel, CS1),
    CG1 = dialyzer_callgraph:scan_core_tree(Tree, CG),
    {CS2, CG1}.



%%=============================================================================
%%
%% Definition of the type structure
%%
%%=============================================================================

%%-----------------------------------------------------------------------------
%% Limits
%%

-define(TUPLE_TAG_LIMIT, 5).
-define(TUPLE_ARITY_LIMIT, 10).
-define(SET_LIMIT, 13).
-define(MAX_BYTE, 255).
-define(MAX_CHAR, 16#10ffff).

-define(WIDENING_LIMIT, 7).
-define(UNIT_MULTIPLIER, 8).

-define(TAG_IMMED1_SIZE, 4).
-define(BITS, (erlang:system_info(wordsize) * 8) - ?TAG_IMMED1_SIZE).

%%-----------------------------------------------------------------------------
%% Type tags and qualifiers
%%

-define(atom_tag,       atom).
-define(binary_tag,     binary).
-define(function_tag,   function).
-define(identifier_tag, identifier).
-define(list_tag,       list).
-define(matchstate_tag, matchstate).
-define(nil_tag,        nil).
-define(number_tag,     number).
-define(opaque_tag,     opaque).
-define(product_tag,    product).
-define(remote_tag,     remote).
-define(tuple_set_tag,  tuple_set).
-define(tuple_tag,      tuple).
-define(union_tag,      union).
-define(var_tag,        var).

-type tag()  :: ?atom_tag | ?binary_tag | ?function_tag | ?identifier_tag
              | ?list_tag | ?matchstate_tag | ?nil_tag | ?number_tag
              | ?opaque_tag | ?product_tag | ?tuple_tag | ?tuple_set_tag
              | ?union_tag | ?var_tag.

-define(float_qual,     float).
-define(integer_qual,   integer).
-define(nonempty_qual,  nonempty).
-define(pid_qual,       pid).
-define(port_qual,      port).
-define(reference_qual, reference).
-define(unknown_qual,   unknown).

-type qual() :: ?float_qual | ?integer_qual | ?nonempty_qual | ?pid_qual
              | ?port_qual | ?reference_qual | ?unknown_qual | {_, _}.

%%-----------------------------------------------------------------------------
%% The type representation
%%

-define(any,  any).
-define(none, none).
-define(unit, unit).
 %% Generic constructor.
-record(c, {tag :: tag(), elements = [], qualifier = ?unknown_qual :: qual()}).

%% -opaque erl_type() :: ?any | ?none | ?unit | #c{}.

%%-----------------------------------------------------------------------------
%% Auxiliary types and convenient macros
%%

-type rng_elem()   :: 'pos_inf' | 'neg_inf' | integer().

-record(int_set, {set :: [integer()]}).
-record(int_rng, {from :: rng_elem(), to :: rng_elem()}).
%% -record(opaque,  {mod :: module(), name :: atom(),
%%        args = [], struct :: erl_type()}).
%% -record(remote,  {mod:: module(), name :: atom(), args = []}).

-define(atom(Set),                 #c{tag=?atom_tag, elements=Set}).
-define(bitstr(Unit, Base),        #c{tag=?binary_tag, elements=[Unit,Base]}).
-define(float,                     ?number(?any, ?float_qual)).
-define(function(Domain, Range),   #c{tag=?function_tag,
                      elements=[Domain, Range]}).
-define(identifier(Types),         #c{tag=?identifier_tag, elements=Types}).
-define(integer(Types),            ?number(Types, ?integer_qual)).
-define(int_range(From, To),       ?integer(#int_rng{from=From, to=To})).
-define(int_set(Set),              ?integer(#int_set{set=Set})).
-define(list(Types, Term, Size),   #c{tag=?list_tag, elements=[Types,Term],
                      qualifier=Size}).
-define(nil,                       #c{tag=?nil_tag}).
-define(nonempty_list(Types, Term),?list(Types, Term, ?nonempty_qual)).
-define(number(Set, Qualifier),    #c{tag=?number_tag, elements=Set,
                      qualifier=Qualifier}).
-define(opaque(Optypes),           #c{tag=?opaque_tag, elements=Optypes}).
-define(product(Types),            #c{tag=?product_tag, elements=Types}).
-define(remote(RemTypes),          #c{tag=?remote_tag, elements=RemTypes}).
-define(tuple(Types, Arity, Qual), #c{tag=?tuple_tag, elements=Types,
                      qualifier={Arity, Qual}}).
-define(tuple_set(Tuples),         #c{tag=?tuple_set_tag, elements=Tuples}).
-define(var(Id),                   #c{tag=?var_tag, elements=Id}).

-define(matchstate(P, Slots),      #c{tag=?matchstate_tag, elements=[P,Slots]}).
-define(any_matchstate,            ?matchstate(t_bitstr(), ?any)).

-define(byte,                      ?int_range(0, ?MAX_BYTE)).
-define(char,                      ?int_range(0, ?MAX_CHAR)).
-define(integer_pos,               ?int_range(1, pos_inf)).
-define(integer_non_neg,           ?int_range(0, pos_inf)).
-define(integer_neg,               ?int_range(neg_inf, -1)).

%%-----------------------------------------------------------------------------
%% Unions
%%

-define(union(List), #c{tag=?union_tag, elements=[_,_,_,_,_,_,_,_,_,_]=List}).

-define(atom_union(T),       ?union([T,?none,?none,?none,?none,?none,?none,?none,?none,?none])).
-define(bitstr_union(T),     ?union([?none,T,?none,?none,?none,?none,?none,?none,?none,?none])).
-define(function_union(T),   ?union([?none,?none,T,?none,?none,?none,?none,?none,?none,?none])).
-define(identifier_union(T), ?union([?none,?none,?none,T,?none,?none,?none,?none,?none,?none])).
-define(list_union(T),       ?union([?none,?none,?none,?none,T,?none,?none,?none,?none,?none])).
-define(number_union(T),     ?union([?none,?none,?none,?none,?none,T,?none,?none,?none,?none])).
-define(tuple_union(T),      ?union([?none,?none,?none,?none,?none,?none,T,?none,?none,?none])).
-define(matchstate_union(T), ?union([?none,?none,?none,?none,?none,?none,?none,T,?none,?none])).
-define(opaque_union(T),     ?union([?none,?none,?none,?none,?none,?none,?none,?none,T,?none])).
-define(remote_union(T),     ?union([?none,?none,?none,?none,?none,?none,?none,?none,?none,T])).
-define(integer_union(T),    ?number_union(T)).
-define(float_union(T),      ?number_union(T)).
-define(nil_union(T),        ?list_union(T)).





%% @doc This function is used by the random code generator. Tests
%% wether one type is a subtype of the other.
%% @spec is_subtype(erl_type(), erl_type()) -> bool()
is_subtype(?union(Types), T2) ->
    lists:any(fun(T) -> is_subtype(T, T2) end,
              lists:filter(fun(T) ->  T =/= ?none end, Types));
is_subtype(T1, T2) ->
    erl_types:t_is_subtype(T1, T2) orelse erl_types:t_is_subtype(T2, T1).








%%=============================================================================
%%
%% QC generator from type description creating Erlang terms
%%
%%=============================================================================

%% @doc Converts a type specification to a QC generator.
%% @spec t_to_gen(erl_type()) -> generator(term())
t_to_gen(L) when is_list(L) ->
  lists:map(fun t_to_gen/1, L);
t_to_gen(?any) ->
  int();
%% t_to_gen(?none, _RecDict) ->
%%   "none()";
%% t_to_gen(?unit, _RecDict) ->
%%   "no_return()";
t_to_gen(?atom(?any)) ->
    [choose($a, $z) | list(choose($a, $z))];
t_to_gen(?atom(Set)) ->
    elements(Set);

%% t_to_gen(?bitstr(8, 0), _RecDict) ->
%%   "binary()";
%% t_to_gen(?bitstr(0, 0), _RecDict) ->
%%   "<<>>";
%% t_to_gen(?bitstr(0, B), _RecDict) ->
%%   io_lib:format("<<_:~w>>", [B]);
%% t_to_gen(?bitstr(U, 0), _RecDict) ->
%%   io_lib:format("<<_:_*~w>>", [U]);
%% t_to_gen(?bitstr(U, B), _RecDict) ->
%%   io_lib:format("<<_:~w,_:_*~w>>", [B, U]);

%% t_to_gen(?function(?any, ?any), _RecDict) ->
%%   "fun()";
%% t_to_gen(?function(?any, Range), RecDict) ->
%%   "fun((...) -> " ++ t_to_gen(Range, RecDict) ++ ")";
%% t_to_gen(?function(?product(ArgList), Range), RecDict) ->
%%   "fun((" ++ comma_sequence(ArgList, RecDict) ++ ") -> "
%%     ++ t_to_gen(Range, RecDict) ++ ")";

%% t_to_gen(?identifier(Set), _RecDict) ->
%%   if Set =:= ?any -> "identifier()";
%%      true -> sequence([io_lib:format("~w()", [T])
%%             || T <- set_to_list(Set)], [], " | ")
%%   end;
%% t_to_gen(?opaque(Set), _RecDict) ->
%%   sequence([case is_opaque_builtin(Mod, Name) of
%%        true  -> io_lib:format("~w()", [Name]);
%%        false -> io_lib:format("~w:~w()", [Mod, Name])
%%      end
%%      || #opaque{mod = Mod, name = Name} <- set_to_list(Set)], [], " | ");
%% t_to_gen(?matchstate(Pres, Slots), RecDict) ->
%%   io_lib:format("ms(~s,~s)", [t_to_gen(Pres, RecDict),
%%                t_to_gen(Slots,RecDict)]);

t_to_gen(?nil) ->
    [];
%% t_to_gen(?nonempty_list(Contents, Termination), RecDict) ->
%%   ContentString = t_to_gen(Contents, RecDict),
%%   case Termination of
%%     ?nil ->
%%       case Contents of
%%  ?char -> "nonempty_string()";
%%  _ -> "["++ContentString++",...]"
%%       end;
%%     ?any ->
%%       %% Just a safety check.
%%       case Contents =:= ?any of
%%  true -> ok;
%%  false ->
%%    erlang:error({illegal_list, ?nonempty_list(Contents, Termination)})
%%       end,
%%       "nonempty_maybe_improper_list()";
%%     _ ->
%%       case t_is_subtype(t_nil(), Termination) of
%%  true ->
%%    "nonempty_maybe_improper_list("++ContentString++","
%%      ++t_to_gen(Termination, RecDict)++")";
%%  false ->
%%    "nonempty_improper_list("++ContentString++","
%%      ++t_to_gen(Termination, RecDict)++")"
%%       end
%%   end;

t_to_gen(?list(Contents, _, _)) ->
    list(t_to_gen(Contents));
%% t_to_gen(?list(Contents, Termination, ?unknown_qual), RecDict) ->
%%   ContentString = t_to_gen(Contents, RecDict),
%%   case Termination of
%%     ?nil ->
%%       case Contents of
%%  ?char -> "string()";
%%  _ -> "["++ContentString++"]"
%%       end;
%%     ?any ->
%%       %% Just a safety check.
%%       %% case Contents =:= ?any of
%%       %%   true -> ok;
%%       %%   false ->
%%       %%     L = ?list(Contents, Termination, ?unknown_qual),
%%       %%     erlang:error({illegal_list, L})
%%       %% end,
%%       "maybe_improper_list()";
%%     _ ->
%%       case t_is_subtype(t_nil(), Termination) of
%%  true ->
%%    "maybe_improper_list("++ContentString++","
%%      ++t_to_gen(Termination, RecDict)++")";
%%  false ->
%%    "improper_list("++ContentString++","
%%      ++t_to_gen(Termination, RecDict)++")"
%%       end
%%   end;

t_to_gen(?int_set(Set)) ->
    elements(Set);
%% t_to_gen(?byte) -> "byte()";
%% t_to_gen(?char) -> "char()";
%% t_to_gen(?integer_pos) -> "pos_integer()";
%% t_to_gen(?integer_non_neg) -> "non_neg_integer()";
%% t_to_gen(?integer_neg) -> "neg_integer()";
t_to_gen(?int_range(From, To)) ->
    choose(From, To);
t_to_gen(?integer(?any)) ->
    int();
t_to_gen(?float) ->
    real();
t_to_gen(?number(?any, ?unknown_qual)) ->
    int();

t_to_gen(?product(_List)) ->
  throw("product unimplemented");

t_to_gen(?tuple(?any, ?any, ?any)) ->
  {};

t_to_gen(?tuple(Elements, _, _)) when is_list(Elements) ->
  ?LET(L, lists:map(fun t_to_gen/1, Elements), list_to_tuple(L));

t_to_gen(?tuple(Elements, _Arity, _)) -> %% TODO: does arity have a mening?
  ?LET(L, list(t_to_gen(Elements)), list_to_tuple(L));

%% t_to_gen(?tuple(Elements, Arity, _)) when is_list(Elements) ->
%%     ?LET(L, lists:map(fun t_to_gen/1, Elements),
%%          list_to_tuple(L));
%% t_to_gen(?tuple(Elements, _Arity, ?any)) ->
%%     ?LET(L, list(t_to_gen(Elements)),
%%          list_to_tuple(L));

t_to_gen(?tuple_set(_) = S) ->
  oneof([t_to_gen(T) || T <- erl_types:t_tuple_subtypes(S), T =/= ?none]);

t_to_gen(?union(Types)) ->
  oneof([t_to_gen(T) || T <- Types, T =/= ?none]);

t_to_gen(T) ->
  io:format("t_to_gen:~p~n", [T]),
  throw(unimplemented).


%%=============================================================================
%%
%% QC generator from type description creating Erlang patterns
%%
%%=============================================================================

varname() ->
    ?LET({C, Cs},
         {choose($A, $Z), list(oneof([choose($a, $z), choose($A, $Z)]))},
         [C|Cs]).

val_or_var(Gen) ->
    oneof([Gen, {variable, varname()}]).

%% @doc This function is used by the random code generator. It
%% converts a type specification to a QC generator for patterns.
%% @spec t_to_pattern_gen(erl_type()) -> generator()
t_to_pattern_gen(L) when is_list(L) ->
    lists:map(fun t_to_pattern_gen/1, L);

t_to_pattern_gen(?any) ->
  {variable, varname()};

t_to_pattern_gen(?list(Contents, ?nil, ?unknown_qual)) ->
    list(t_to_pattern_gen(Contents));

t_to_pattern_gen(?tuple(Elements, _Arity, ?any)) ->
    ?LET(L, lists:map(fun t_to_pattern_gen/1, Elements), list_to_tuple(L));

t_to_pattern_gen(?tuple(Elements, Arity, _Tag)) ->
    t_to_pattern_gen(?tuple(Elements, Arity, ?any));

t_to_pattern_gen(?tuple_set(_) = S) ->
    oneof([t_to_pattern_gen(T) || T <- erl_types:t_tuple_subtypes(S),
                                  T =/= ?none]);

t_to_pattern_gen(?union(Types)) ->
    oneof([{variable, varname()} | [t_to_pattern_gen(T) || T <- Types,
                                                           T =/= ?none]]);

t_to_pattern_gen(X) ->
    val_or_var(t_to_gen(X)).
