%%% 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 Daniel Horpacsi <daniel_h@inf.elte.hu>

-module(refqc_rename_var).
-vsn("$Rev: $ ").

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

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

get_position(Args) ->
    {position, Pos} = lists:keyfind(position, 1, Args),
    Pos.

prop_rename_var() ->
    Files = ?QCCOMMON:get_files_in_database(),
    ?FORALL(Args, ?LAZY(?QCGEN:gen_args(renvar, {files, Files})), %% TODO: likely crashes
            perform_and_check({files, Files}, Args)).

%% The binding and reference structure of the variable must be the
%% same as before the transformation.
prop_binding_struct(Occurrences, Struct) ->
    [NewVarNode] = lists:usort(?Query:exec(Occurrences, ?Expr:variables())), % is this usort really needed?
    Struct == ?QCCOMMON:get_binding_struct(NewVarNode).

%% The binding and reference structure after the renaming to the
%% original name must result the same binding and reference structure
%% as at the base state.
prop_binding_struct_reverse(Args, Occurrences, Struct) ->
    Result = reftest_utils:exec_transform(rename_var, Args),
    case Result of
        {result, _, _} -> prop_binding_struct(Occurrences, Struct);
        _ -> true
    end.

invert_args(Args, Name) ->
    {position, Position} = lists:keyfind(position, 1, Args),
    [{file, ?QCCOMMON:get_file(Args)},
     {position, Position},
     {varname, Name}].

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

prepare(Mods) -> ?LAZY(?QCGEN:gen_args(renvar, {modules, Mods})).

perform_and_check(_ModsOrFiles, {_, _, Args}) ->
    ?IMPLIES(
       get_position(Args) > 0,
       begin
           VarNode = ?Args:variable(Args),
           Name = ?Var:name(VarNode),
           Occurrences = ?Query:exec(VarNode, ?Var:occurrences()),
           Struct = ?QCCOMMON:get_binding_struct(VarNode),
           File = ?QCCOMMON:get_file(Args),
           CompResult1 = compile:file(File, [strong_validation, return_errors]),
           
           %% Files = ?QCCOMMON:get_files_in_database(),
           %% OptionList = [{call_depth, 0}], % todo: maybe not so hard-coded :)
           %% SemTreesBefore = ?QCCOMMON:generate_semtrees(Files, OptionList),  ... "unknown expression type"
           
           Result =  reftest_utils:exec_transform(rename_var, Args),
           case Result of
               {result, _, _} ->
                   ?QCCOMMON:prop_compile(File, CompResult1)
                       andalso prop_binding_struct(Occurrences, Struct) andalso
                       prop_binding_struct_reverse(invert_args(Args, Name), Occurrences, Struct);
               %% andalso ?QCCOMMON:prop_semtree(SemTreesBefore, Files, OptionList);
               _ ->
                   true
           end
       end).
