%%% 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

%%% @author Istvan Bozo <bozo_i@inf.elte.hu>
%%% @author D�niel Horp�csi <daniel_h@inf.elte.hu>

-module(refqc_extract_fun).

-include_lib("referl_qc/include/prop_based_testing.hrl").
-include_lib("referl_qc/include/qc.hrl").

%% Random module based testing callbacks
-export([prepare/1, perform_and_check/2]).
%% Interface
-export([prop_extract_fun/0]).

-record(data, {file, compresult1, newfuncl, unusedvars, funclause,
               varbindings, varreferences, variables, expr, funrefstruct}).

prop_extract_fun() ->
    ?FORALL(Args, ?LAZY(?QCGEN:gen_args(extfun)),
            perform_and_check(nothing, Args)).

show_comp_info(Data,CompResult) ->
    %% this helps to determine which selection for extraction causes
    %% the error
    case CompResult of
        {error, ErrorList, _WarningList} ->
            io:format("The transformation resulted incompilable code.~n"),
            io:format("Extracted expressions:~p~n",
                      [lists:flatten(?Syn:tree_text(Data#data.expr))]),
            io:format("~nErrors by the compiler :~p~n", [ErrorList]);
        {ok, _} ->
            ok
    end.

%% If the original module does not contain any errors the
%% transormation must preserve this state (it is not allowed to
%% introduce compile time errors).
prop_compile(Data) ->
    AfterCompileFun = fun(CompResult2) -> show_comp_info(Data,CompResult2) end,
    File = Data#data.file,
    CompResult = Data#data.compresult1,
    ?QCCOMMON:prop_compile(File, CompResult, AfterCompileFun).

%% The extract function transformation must not introduce unused
%% variable warnings
prop_unused_vars(Data) ->
    Variables2 =
        lists:usort(
          ?Query:exec(Data#data.newfuncl,
                      ?Query:seq(?Clause:body(), ?Expr:variables()))),
    %% Unused variables in the body of the source function
    UnusedVars2 =
        lists:flatten(
          [?Query:exec(Var, ?Var:bindings())
           || Var <- Variables2,
              ?Query:exec(Var, ?Var:references()) == []]),
    (UnusedVars2 -- Data#data.unusedvars) == [].

%% The transformation must not change the function call structure of
%% the module, except the newly created function definition and its
%% call, the newly created function must have only one application
prop_call_struct(Data) ->
    NewFuns = ?Query:exec(Data#data.newfuncl,
                          ?Query:seq([?Clause:form(),
                                      ?Form:module(),
                                      ?Mod:locals()])),
    NewFunRefStruct =
        [{lists:usort(?Query:exec(Fun, ?Fun:definition())),
          lists:usort(?Query:exec(Fun, ?Fun:applications()))}
         || Fun <- NewFuns],
    NewFun =
        ?Query:exec(Data#data.newfuncl, ?Query:seq([?Clause:form(),
                                                    ?Form:func()])),
    {FunDef, FunApps} = {lists:usort(?Query:exec(NewFun, ?Fun:definition())),
                         lists:usort(?Query:exec(NewFun, ?Fun:applications()))},

    (lists:usort(Data#data.funrefstruct ++ [{FunDef, FunApps}]) ==
         lists:usort(NewFunRefStruct)) andalso length(FunDef) == 1 andalso
        length(FunApps) == 1.

%% The variables must have the same number of bindings before and
%% after the transformation. The number of references is less or equal
%% as before the transformation. The number of bound variables in the
%% affected function body must be the same as the sum of bound
%% variables in the not affected code part of the functiona body and
%% the bound variables in the body of the extracted function
prop_bindings(Data) ->
    UntouchedNodeVars =
        lists:usort(?Query:exec(Data#data.funclause,
                                ?Query:seq([?Clause:body(),
                                            ?Expr:variables()]))),
    %% only the variables which are bound in the newly extracted
    %% function body
    TouchedNodeVars =
        lists:usort(?Query:exec(Data#data.newfuncl,
                                ?Query:seq([?Clause:body(),
                                            ?Expr:variables()])))
        --
        lists:usort(?Query:exec(Data#data.newfuncl,
                                ?Query:seq([?Clause:patterns(),
                                            ?Expr:variables()]))),
    VarReferences2 =
        lists:sort([{lists:sort(?Query:exec(Var, ?Var:bindings())),
                     length(?Query:exec(Var, ?Var:references()))}
                    || Var <- UntouchedNodeVars]),
    VarBindings2 =
        [lists:sort(?Query:exec(Var, ?Var:bindings()))
         || Var <- UntouchedNodeVars ++ TouchedNodeVars],

    %% Binding structure must be the same
    (VarBindings2 -- Data#data.varbindings == []) andalso
    %% the number of references is less or equal as before the
    %% transformation
        compare_ref_struct(Data#data.varreferences, VarReferences2) andalso
    %% the number of bound variables in the affected function body
    %% must be the same as the sum of bound variables in the not
    %% affected code part of the functiona body and the bound
    %% variables in the body of the extracted function
        length(Data#data.variables) ==
        length(UntouchedNodeVars ++ TouchedNodeVars).

collect_data_for_properties(Args, Expr) ->
    File = refqc_common:get_file(Args),
    CompResult1 = compile:file(File, [strong_validation, return_errors]),
    FunClause = ?Query:exec(Expr, ?Query:seq([?Expr:clause(),
                                              ?Clause:funcl()])),
    Variables = lists:usort(?Query:exec(FunClause,
                                        ?Query:seq([?Clause:body(),
                                                    ?Expr:variables()]))),
    VarBindings = [ lists:sort(?Query:exec(Var, ?Var:bindings()))
                    || Var <- Variables],
    VarReferences =
        lists:sort(
          [ {lists:sort(?Query:exec(Var, ?Var:bindings())),
             length(?Query:exec(Var, ?Var:references()))}
            || Var <- Variables]),
    %% Unused variables in the body of the source function
    UnusedVars = lists:flatten(
                   [ ?Query:exec(Var, ?Var:bindings())
                     || Var <- Variables,
                        ?Query:exec(Var, ?Var:references()) == []]),
    Module = ?Query:exec(FunClause, ?Query:seq([?Clause:form(),
                                                ?Form:module()])),
    LocalFuns = ?Query:exec(Module, ?Mod:locals()),
    FunRefStruct =
        [ {lists:usort(?Query:exec(Fun, ?Fun:definition())),
           lists:usort(?Query:exec(Fun, ?Fun:applications()))}
          || Fun <- LocalFuns],
    #data{file = File,
          compresult1 = CompResult1,
          unusedvars = UnusedVars,
          funclause = FunClause,
          varbindings = VarBindings,
          varreferences = VarReferences,
          variables = Variables,
          expr = Expr,
          funrefstruct = FunRefStruct}.


compare_ref_struct([{L1, N1}|T1], [{L1, N2}|T2]) when N1 >= N2 ->
    compare_ref_struct(T1,T2);
compare_ref_struct([{L1, _}|T1], [{L2, N2}|T2]) when L1 < L2 ->
    compare_ref_struct(T1, [{L2, N2}|T2]);
compare_ref_struct([{L1, N1}|T1], [{L2, _}|T2]) when L1 > L2 ->
    compare_ref_struct([{L1, N1}|T1], T2);
compare_ref_struct(_, []) ->
    true;
compare_ref_struct(_,_) ->
    false.



%% =============================================================================
%% Random module based testing callbacks

prepare(_Mods) -> ?LAZY(?QCGEN:gen_args(extfun)).

perform_and_check(_, {_, _, [Expr|Args]}) ->
    %% refqc_common:initialize(Dir),
    D = collect_data_for_properties(Args, Expr),
    InnerExprs = ?Query:exec(Expr, ?Expr:deep_sub()) ++ [Expr],

    Result = reftest_utils:exec_transform(extract_fun, Args),
    NewFunCl = ?Query:exec(hd(tl(InnerExprs)),
                           ?Query:seq([?Expr:clause(), ?Clause:funcl()])),
    Data = D#data{newfuncl = NewFunCl},

    case Result of
        {result, _, _} ->
            prop_compile(Data) andalso prop_unused_vars(Data) andalso
                prop_call_struct(Data) andalso prop_bindings(Data);
        {abort,{_ErrorDesc, ErrorMessage}} ->
            io:format("Transformation aborted:~n\t~s~n", [ErrorMessage]),
            true
    end.
