%%% 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 This module evaluates the semantic graph belonging to a function
%%% and tries to do as much symbolic computation as possible. The resulting
%%% data structure can be used to compare functions based on semantics.

%%% @author Elroy Jumpertz <elroy.jumpertz@student.ru.nl>

%%% Data types:

%%% {expr_seq, {[ExprList]}}
%%% {expr_choice, {[ExprList]}}
%%% {application, {FunName, [Arg1, ..., Argn]}}
%%% {case_expr, {[HeadExprs1, ..., HeadExprn],
%%%     [
%%%         {pattern, {Lhs1, {expr_seq, {[Rhs1, ..., Rhsn]}}},
%%%         {pattern, {Lhs1, {expr_seq, {[Rhs1, ..., Rhsn]}}},
%%%         ...
%%%     ]
%%% }}}}
%%% {match_expr, {LhsExpr, ValueList}}
%%% {infix_expr, {Operator, ValueListLhs, ValueListRhs}}
%%% [{constant, {atom, Value}}]
%%% [{constant, {boolean, Value}}]
%%% [{constant, {char, Value}}]
%%% [{constant, {float, Value}}]
%%% [{constant, {integer, Value}}]
%%% [{constant, {string, Value}}]
%%% {variable, {IntName}} % changed to {variable, {Name}}

%%% Option flag     | Argument | Explanation
%%% ----------------+----------+------------
%%% call_depth      | integer  | The depth with which function calls are evaluated
%%% abstr_fun_names | boolean  | Don't use the function names in application nodes, but use `function' instead
%%% fold_case_expr  | boolean  | Represent case expressions as a list of possible outcomes
%%% canonical       | boolean  | Simplify the semantic tree by removing expr_seq and expr_choice nodes with a single child

-module(refqc_sc_symcomp).
-vsn("$Rev: 17551 $").

-compile(export_all).

-include_lib("referl_qc/include/refqc_sc.hrl").

%%% ===========================================================================
%%% Debug functions

d(Message) ->
    io:format("Debug: ~p~n", [Message]).

%%% ===========================================================================
%%% Top-down evaluation functions

eval_expr_list(Exprs, State) ->
    {SemTree, State2} = eval_expr_list2(Exprs, State),
    {{expr_seq, {SemTree}}, State2}.

eval_expr_list2([], State) ->
    {[], State};
eval_expr_list2([Expr|Exprs], State) ->
    {SemTree, State2} = eval(Expr, State),
    {SemTrees, State3} = eval_expr_list2(Exprs, State2),
    {[SemTree] ++ SemTrees, State3}.

eval(Expr, State) ->
    eval(?Expr:type(Expr), Expr, State).

eval(application, Expr, State) ->
    FunNode = ?Query:exec(Expr, ?Expr:function()),
    Children = get_children_n(Expr),
    FunName = ?Expr:value(hd(Children)),
    AbstractFunNames = option_value(abstr_fun_names, State),
    AppNodeFunName =
        if AbstractFunNames ->
            function;
        true ->
            FunName
        end,
    FunArgsCaller = tl(Children), % can be []
    Arity = length(FunArgsCaller),
    {{expr_seq, {SemTreesCaller}}, State2} = eval_expr_list(FunArgsCaller, State),
    CallDepth = options_get_call_depth(State2),
    if CallDepth > 0 ->
        Clauses = get_function_clauses(FunNode),
        case Clauses of
            error -> % function not found
                {{application, {AppNodeFunName, SemTreesCaller}}, State2};
            _ ->
                Patterns = get_function_patterns(Clauses),
                case get_matching_function_clause(Patterns, SemTreesCaller) of
                    no_match ->
                        {{application, {AppNodeFunName, SemTreesCaller}}, State2};
                    ClauseNr ->
                        MatchingPattern = lists:nth(ClauseNr, Patterns),
                        TempState1 = substitute_function_arguments(MatchingPattern, SemTreesCaller, #state{}),
                        TempState2 = TempState1#state{optionlist = State2#state.optionlist},
                        TempState3 = option_update(call_depth, CallDepth - 1, TempState2),
                        {ReturnValSemTree, _} = returnvalue2(FunName, Arity, ClauseNr, TempState3),
                        case ReturnValSemTree of
                            error ->
                                {{application, {AppNodeFunName, SemTreesCaller}}, State2};
                            _ ->
                                {ReturnValSemTree, State2}
                        end
                end
        end;
    true ->
        {{application, {AppNodeFunName, SemTreesCaller}}, State2}
    end;

eval(parenthesis, Expr, State) ->
    eval(get_child(Expr), State);

%% fix
% eval_case_expr(Expr, St, OptionList) ->
%    Clauses = ?Query:exec(Expr, ?Expr:clauses()),
%    [HeadExprs|PatternExprs] = [?Query:exec(Clause, ?Clause:exprs()) || Clause <- Clauses],
%    {{expr_seq, {HeadExprSemTrees}}, StBefore} = eval_expr_list(HeadExprs, St, OptionList),
%    {PatternExprSemTrees, StAfter} = eval_pattern_list(PatternExprs, StBefore, OptionList),
%    FoldCaseExpr = option_value(fold_case_expr, OptionList),
%    if FoldCaseExpr ->
%        {{expr_choice, {fold_case_expr(HeadExprSemTrees, PatternExprSemTrees)}}, StBefore};
%    true ->
%        {{case_expr, {HeadExprSemTrees, PatternExprSemTrees}}, StAfter}
%    end.

eval(match_expr, Expr, State) ->
    {LhsExpr, RhsExpr} = get_children_2(Expr),
    {LhsSemTree, State2} = eval(LhsExpr, State),
    {RhsSemTree, State3} = eval(RhsExpr, State2),
    case LhsSemTree of
        {variable, {IntVarName}} ->
            State4 = ?St:update_list(IntVarName, make_list(RhsSemTree), State3),
            % d(make_list(RhsSemTree)),
            {{match_expr, {LhsSemTree, make_list(RhsSemTree)}}, State4};
        _ ->
            {{match_expr, {not_supported}}, State3}
    end;

eval(infix_expr, Expr, State) ->
    {LhsExpr, RhsExpr} = get_children_2(Expr),
    Op = ?Expr:value(Expr),
    {LhsSemTree, State2} = eval(LhsExpr, State),
    {RhsSemTree, State3} = eval(RhsExpr, State2),
    d(LhsSemTree),
    d(RhsSemTree),
    LhsValueList = make_list(strip_choice(LhsSemTree)),
    RhsValueList = make_list(strip_choice(RhsSemTree)),
    Combinations = [{LhsVal, RhsVal} || LhsVal <- LhsValueList, RhsVal <- RhsValueList],
    Solutions = lists:usort(eval_infix_operands(Combinations, Op)),
    % if length(Solutions) == 1 ->
    %    {Solutions, State3}; % maybe remove this case
    % true ->
        {{expr_choice, {Solutions}}, State3};
    % end;

eval(atom, Expr, State) ->
    Value = ?Expr:value(Expr),
    if is_boolean(Value) ->
        % {[{constant, {boolean, Value}}], State};
        {{expr_choice, {[{constant, {boolean, Value}}]}}, State};
    true ->
        % {[{constant, {atom, Value}}], State}
        {{expr_choice, {[{constant, {atom, Value}}]}}, State}
    end;

eval(char, Expr, State) ->
    % {[{constant, {char, ?Expr:value(Expr)}}], State};
    {{expr_choice, {[{constant, {char, ?Expr:value(Expr)}}]}}, State};

eval(float, Expr, State) ->
    % {[{constant, {float, ?Expr:value(Expr)}}], State};
    {{expr_choice, {[{constant, {float, ?Expr:value(Expr)}}]}}, State};

eval(integer, Expr, State) ->
    % {[{constant, {integer, ?Expr:value(Expr)}}], State};
    {{expr_choice, {[{constant, {integer, ?Expr:value(Expr)}}]}}, State};

eval(string, Expr, State) ->
    % {[{constant, {string, ?Expr:value(Expr)}}], State};
    {{expr_choice, {[{constant, {string, ?Expr:value(Expr)}}]}}, State};

eval(variable, Expr, State = #state{}) ->
    RealVarName = ?Expr:value(Expr),
    case ?St:get_internal_varname(RealVarName, State) of
        {ok, IntVarName} ->
            case ?St:lookup(IntVarName, State) of
                {ok, ValueList} ->
                    % if length(ValueList) == 1 ->
                    %    {ValueList, State}; % maybe remove this case
                    % true ->
                        % d(ValueList),
                        {{expr_choice, {ValueList}}, State};
                    % end;
                error ->
                    {{variable, {IntVarName}}, State}
            end;
        error ->
            {IntVarName, State2} = ?St:create_internal_varname(RealVarName, State),
            {{variable, {IntVarName}}, State2}
    end;

eval(Expr, _, _) ->
    d(Expr),
    throw("Unknown expression type.").

%% fix
% eval_pattern_list([], St, _) ->
%    {[], St};
% eval_pattern_list([Pattern|Patterns], St, OptionList) ->
%   Pat = hd(Pattern),
%    Exprs = tl(Pattern),
%    {PatSemTree, St2} = eval_expr(Pat, St, OptionList),
%    {{expr_seq, {ExprsSemTree}}, St3} = eval_expr_list(Exprs, St2, OptionList),
%    {SemTrees, St4} = eval_pattern_list(Patterns, St3, OptionList),
%    {[{pattern, {PatSemTree, {expr_seq, {ExprsSemTree}}}}] ++ SemTrees, St4}.

eval_infix_operands([], _) ->
    [];
eval_infix_operands([{Val1, Val2}|Vals], Op) ->
    SemTree =
        case {Val1, Val2} of
            {{constant, {Type1, Value1}}, {constant, {Type2, Value2}}} ->
                apply_operator(Op, {Type1, Value1}, {Type2, Value2});
            {Other1, Other2} ->
                {infix_expr, {Op, Other1, Other2}}
        end,
    SemTrees = eval_infix_operands(Vals, Op),
    SemTrees ++ [SemTree].

%% fix
%% try to evaluate the return value of the case expression
% fold_case_expr(Head, Patterns) ->
    % BUG: does not update symbol table
%    Head2 = 
%        case hd(Head) of
%            {expr_choice, {ValueList}} ->
%                ValueList;
%            Other ->
%                Other
%        end,
%    Is_constant =
%        fun(SemNode) ->
%            {Name, _} = SemNode,
%            Name == constant
%        end,
%    All_constant = lists:all(Is_constant, Head2),
%    if All_constant ->
%        fold_pattern_list(Head2, Patterns, []);
%    true ->
%        enumerate_patterns(Patterns, [])
%    end.

%% fix
% enumerate_patterns([], Sol) ->
%    Sol ++ [{runtime_error, {no_match}}];
% enumerate_patterns([Pattern|Patterns], Sol) ->
%    {pattern, {_, {expr_seq, {Exprs}}}} = Pattern,
%    enumerate_patterns(Patterns, Sol ++ [{expr_seq, {Exprs}}]).

%% fix
% fold_pattern_list([], _, Sol) ->
%    Sol;
% fold_pattern_list(_, [], Sol) ->
%    Sol ++ [{runtime_error, {no_match}}];
% fold_pattern_list(Head, [Pattern|Patterns], Sol) ->
%    {pattern, {Pats, {expr_seq, {Exprs}}}} = Pattern,
%    if Pats == [{variable, {"_"}}] ->
%        Sol ++ [{expr_seq, {Exprs}}];
%    true ->
%        Int = list_intersection(Head, Pats),
%        if Int /= [] ->
%            if length(Pats) == 1 ->
%                Head2 = Head -- Pats;
%            true ->
%                Head2 = Head
%            end,
%            fold_pattern_list(Head2, Patterns, Sol ++ [{expr_seq, {Exprs}}]);
%        true ->
%            fold_pattern_list(Head, Patterns, Sol)
%        end
%    end.
        

%%% ===========================================================================
%%% Helper functions

get_files() ->
    ?Graph:path(?Graph:root(), [file]).

get_fun(FileNodes, FunName, Arity) ->
    Fun = ?Query:exec(FileNodes, ?Query:seq([?File:module(), ?Mod:local(FunName, Arity)])),
    case Fun of
        [] ->
            error;
        Other ->
            Other
    end.

get_exprs(FunNode, ClauseNr) ->
    Clauses = ?Query:exec(FunNode, ?Query:seq([?Fun:definition(), ?Form:clauses()])),
    if (length(Clauses) >= ClauseNr) and (ClauseNr > 0) ->
        Clause = lists:nth(ClauseNr, Clauses),
        ?Query:exec(Clause, ?Clause:exprs());
    true ->
        error
    end.

get_child(Expr) ->
    hd(?Query:exec(Expr, ?Expr:children())).

get_children_2(Expr) ->
    Children = ?Query:exec(Expr, ?Expr:children()),
    {hd(Children), hd(tl(Children))}.

get_children_n(Expr) ->
    ?Query:exec(Expr, ?Expr:children()).

apply_operator(Op, {_, Value1}, {_, Value2}) ->
    CombValue =
        case Op of
            '+' -> Value1 + Value2;
            '-' -> Value1 - Value2;
            '*' -> Value1 * Value2;
            '/' -> Value1 / Value2;
            '>' -> Value1 > Value2;
            '<' -> Value1 < Value2
        end,
    {constant, {get_type(CombValue), CombValue}}.

get_type(X) ->
    % chars will be integers, and strings will be lists
    % important: evaluate is_boolean before is_atom, because 'true' and 'false' are both
    if is_integer(X)    -> integer;
    is_float(X)         -> float;
    is_boolean(X)       -> boolean;
    is_atom(X)          -> atom;
    is_list(X)          -> list;
    true                -> throw("Unknown data type.")
    end.

semantic_to_symbolic_node(Node) ->
    Value = ?Expr:value(Node),
    case ?Expr:type(Node) of
        variable ->
            {variable, Value};
        _ ->
            {constant, {get_type(Value), Value}}
    end.

get_function_clauses(FunNode) ->
    Clauses = ?Query:exec(FunNode, ?Query:seq([?Fun:definition(), ?Form:clauses()])),
    case Clauses of
        [] ->
            error;
        _ ->
            % [?Query:exec(Clause, ?Clause:patterns()) || Clause <- Clauses]
            Clauses
    end.

get_function_patterns(Clauses) ->
    [?Query:exec(Clause, ?Clause:patterns()) || Clause <- Clauses].

get_matching_function_clause(ArgExprCalleeClauses, ArgSemTreesCaller) ->
    get_matching_function_clause2(ArgExprCalleeClauses, ArgSemTreesCaller, 1).

get_matching_function_clause2(_, [], _) ->
    1; % no arguments, so arity 0, so the first clause MUST match
get_matching_function_clause2([], _, _) ->
    no_match;
get_matching_function_clause2([ArgExprCalleeThisClause|ArgExprCalleeOtherClauses], ArgSemTreesCaller, Index) ->
    EqAcc = match_clause_arguments(ArgExprCalleeThisClause, ArgSemTreesCaller, []),
    AllTrue = list_all_true(EqAcc),
    if AllTrue ->
        % this function clause matches the arguments
        Index;
    true ->
        % no match
        get_matching_function_clause2(ArgExprCalleeOtherClauses, ArgSemTreesCaller, Index + 1)
    end.

match_clause_arguments([], _, EqAcc) ->
    EqAcc;
match_clause_arguments([ArgExprCallee|ArgExprs], [ArgSemTreeCaller|ArgSemTrees], EqAcc) ->
    {ArgSemTreeCallee, _} = eval(ArgExprCallee, #state{}),
    ArgSemTreeCaller2 = strip_choice(ArgSemTreeCaller),
    Equal =
        if length(ArgSemTreeCaller2) > 1 ->
            % multiple possible values are not supported
            false;
        true ->
            argument_equality(strip_list(ArgSemTreeCallee), strip_list(ArgSemTreeCaller2))
        end,
    match_clause_arguments(ArgExprs, ArgSemTrees, EqAcc ++ [Equal]).

argument_equality(ArgCallee, ArgCaller) ->
    case {ArgCallee, ArgCaller} of
        {{constant, _}, {constant, _}} ->
            ArgCallee == ArgCaller;
        {{variable, _}, {constant, _}} ->
            true;
        {{variable, _}, {variable, _}} ->
            true;
        _ ->
            false
    end.

substitute_function_arguments([], _, State) ->
    State;
substitute_function_arguments([PatternExpr|PatternExprs], [CallerSemTree|CallerSemTrees], State = #state{}) ->
    Kind = ?Expr:type(PatternExpr),
    if Kind == variable ->
        RealVarName = ?Expr:value(PatternExpr),
        IntVarName =
            case ?St:get_internal_varname(RealVarName, State) of
            {ok, VarName} ->
                State2 = State,
                VarName;
            error ->
                {VarName, State2} = ?St:create_internal_varname(RealVarName, State),
                VarName
            end,
        State3 = ?St:update_list(IntVarName, make_list(strip_choice(CallerSemTree)), State2);
    true ->
        State3 = State
    end,
    substitute_function_arguments(PatternExprs, CallerSemTrees, State3).

list_intersection(L1, L2) ->
    ordsets:intersection(ordsets:from_list(L1), ordsets:from_list(L2)).

make_list(Element) ->
    if is_list(Element) ->
        Element;
    true ->
        [Element]
    end.

strip_list(Element) ->
    if is_list(Element) ->
        hd(Element);
    true ->
        Element
    end.

strip_choice(Element) ->
    case Element of
        {expr_choice, {Y}} ->
            Y;
        Other ->
            Other
    end.

list_all_true(L) ->
    Is_true =
        fun(Element) ->
            Element == true
        end,
    lists:all(Is_true, L).

%%% ===========================================================================
%%% OptionList functions

option_value(Option, State) ->
    OptionList = State#state.optionlist,
    case lists:keyfind(Option, 1, OptionList) of
        {_, OptionValue} ->
            OptionValue;
        false ->
            error
    end.

option_update(OptionName, NewValue, State) ->
    OptionList = State#state.optionlist,
    OptionList2 = lists:keystore(OptionName, 1, OptionList, {OptionName, NewValue}),
    State#state{optionlist = OptionList2}.

options_get_call_depth(State) ->
    Cd = option_value(call_depth, State),
    case Cd of
        error ->
            0; % default call depth is 0
        _ ->
            Cd
    end.

%%% ===========================================================================
%%% Main functions

%% export this function
sc(FunName, Arity, ClauseNr) ->
    sc2(FunName, Arity, ClauseNr, #state{}).

%% export this function
sc(FunName, Arity, ClauseNr, OptionList) ->
    sc2(FunName, Arity, ClauseNr, #state{optionlist = OptionList}).

sc2(FunName, Arity, ClauseNr, State = #state{}) ->
    {{expr_seq, {SemTree}}, State2} = symcomp(FunName, Arity, ClauseNr, State),
    case SemTree of
        error ->
            {error, State2};
        _ ->
            Canonical = option_value(canonical, State2),
            case Canonical of
            true ->
                {canonize({expr_seq, {SemTree}}), State2};
            _ ->
                {{expr_seq, {SemTree}}, State2}
            end
    end.

%% export this function
returnvalue(FunName, Arity, ClauseNr) ->
    returnvalue2(FunName, Arity, ClauseNr, #state{}).

%% export this function    
returnvalue(FunName, Arity, ClauseNr, OptionList) ->
    returnvalue2(FunName, Arity, ClauseNr, #state{optionlist = OptionList}).

returnvalue2(FunName, Arity, ClauseNr, State = #state{}) ->
    {{expr_seq, {SemTree}}, State2} = symcomp(FunName, Arity, ClauseNr, State),
    case SemTree of
        error ->
            {error, State2};
        _ ->
            Canonical = option_value(canonical, State2),
            case Canonical of
            true ->
                {canonize(lists:last(SemTree)), State2};
            _ ->
                {lists:last(SemTree), State2}
            end
    end.

symcomp(FunName, Arity, ClauseNr, State = #state{}) ->
    FunNode = get_fun(get_files(), FunName, Arity),
    case FunNode of
        error ->
            d("FunNode not found: " ++ FunName),
            {{expr_seq, {error}}, State};
        _ ->
            Exprs = get_exprs(FunNode, ClauseNr),
            case Exprs of
                error ->
                    {{expr_seq, {error}}, State};
                _ ->
                    eval_expr_list(Exprs, State)
            end
    end.

canonize([]) ->
    [];
canonize([SemNode|SemNodes]) ->
    [canonize(SemNode)] ++ canonize(SemNodes);
canonize({expr_seq, {Contents}}) ->
    if length(Contents) == 1 ->
        canonize(hd(Contents));
    true ->
        {expr_seq, {canonize(Contents)}}
    end;
canonize({expr_choice, {Contents}}) ->
    if length(Contents) == 1 ->
        canonize(hd(Contents));
    true ->
        {expr_choice, {canonize(Contents)}}
    end;
canonize({application, {FunName, ArgList}}) ->
    {application, {FunName, canonize(ArgList)}};
canonize({match_expr, {Lhs, Rhs}}) ->
    {match_expr, {canonize(Lhs), canonize(Rhs)}};
canonize({infix_expr, {Op, Lhs, Rhs}}) ->
    {infix_expr, {Op, canonize(Lhs), canonize(Rhs)}};
canonize(Other) ->
    Other.
