% -----------------------------------------------------------------------------
%  (C) Altran Praxis Limited
% -----------------------------------------------------------------------------
% 
%  The SPARK toolset is free software; you can redistribute it and/or modify it
%  under terms of the GNU General Public License as published by the Free
%  Software Foundation; either version 3, or (at your option) any later
%  version. The SPARK toolset 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 General
%  Public License for more details. You should have received a copy of the GNU
%  General Public License distributed with the SPARK toolset; see file
%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
%  the license.
% 
% =============================================================================

%###############################################################################
% PURPOSE
%-------------------------------------------------------------------------------
% Loads all rules for this session.
%###############################################################################

%###############################################################################
%MODULE
%###############################################################################
:- module(load__rules, [load_rules/0]).

%###############################################################################
%DEPENDENCIES
%###############################################################################

:- use_module('data__declarations.pro',
              [find_core_type/2]).

:- use_module('data__data_files.pro',
              [get_datafiles_rule/1,
               get_datafiles_global_user_rule/1,
               get_datafiles_local_user_rule/1]).

:- use_module('data__rules.pro',
              [add_rule/8,
               get_rule/8,
               prune_rule/8]).

:- use_module('data__switches.pro',
              [get_switch_user_rules/1]).

:- use_module('parseutilities.pro',
              [inside_selected_character_class/2,
               parse_atom/5,
               parse_atom_silent/4]).

:- use_module('simplifier_ioutilities.pro',
              [convert_file_for_display/2]).

:- use_module('data__formats.pro',
              [add_type/2]).

:- use_module('ioutilities.pro',
              [show_error/2]).

%###############################################################################
%TYPES
%###############################################################################

:- add_type('RuleStatus',
            [accepted,
             rejected]).

%###############################################################################
%DATA
%###############################################################################

%###############################################################################
%PREDICATES
%###############################################################################

%===============================================================================
% load_rules.
%-------------------------------------------------------------------------------
% Load the rules for this session. The rules are retrieved from the
% available rule files.
%===============================================================================










load_rules :-
    process_standard_rulefile,
    fail.

load_rules :-
    get_switch_user_rules(on),
    user_rulefile_name(RuleFile_Atom),
    convert_file_for_display(RuleFile_Atom, DisplayRuleFile_Atom),


    write('Reading '),
    write(DisplayRuleFile_Atom),
    write(' (for user-defined proof rules)'),
    nl,


    user:assert_log_fact(read_in_user_rule_file, DisplayRuleFile_Atom),

    process_rulefile(rlu, RuleFile_Atom),
    fail.

load_rules :-
    restructure_rules,
    !.

%-------------------------------------------------------------------------------

user_rulefile_name(FILE):-
    get_datafiles_global_user_rule(FILE).

user_rulefile_name(FILE):-
    get_datafiles_local_user_rule(FILE).

%-------------------------------------------------------------------------------

process_standard_rulefile :-
        get_datafiles_rule(RuleFile_Atom),
        !,
        see(RuleFile_Atom),
        repeat,
           read(RULE),
           process_rule(RULE, RuleFile_Atom),
        /* UNTIL */ RULE = end_of_file,
        !,
        seen.

%-------------------------------------------------------------------------------

process_rule(RuleName_Atom: LHS_Exp may_be_replaced_by RHS_Exp, RuleFile_Atom) :-
    ground(LHS_Exp),
    ground(RHS_Exp),

    user:simplify(RHS_Exp, NewRHS_Exp),
    add_rule(RuleFile_Atom,
             RuleName_Atom,
             rls,
             hint_rewrite_one_direction,
             equation,
             [LHS_Exp],
             [NewRHS_Exp],
             []),
    !.

process_rule(RuleName_Atom: LHS_Exp may_be_replaced_by RHS_Exp if Condition_ExpList, RuleFile_Atom) :-
    add_rule(RuleFile_Atom,
             RuleName_Atom,
             rls,
             hint_rewrite_one_direction,
             equation,
             [LHS_Exp],
             [RHS_Exp],
             Condition_ExpList),
        !.

process_rule(RuleName_Atom: LHS_Exp may_be_replaced_by RHS_Exp, RuleFile_Atom) :-
    add_rule(RuleFile_Atom,
             RuleName_Atom,
             rls,
             hint_rewrite_one_direction,
             equation,
             [LHS_Exp],
             [RHS_Exp],
             []),
        !.

process_rule(RuleName_Atom: RHS_Exp may_be_deduced, RuleFile_Atom) :-
    nonvar(RHS_Exp),
    add_rule(RuleFile_Atom,
             RuleName_Atom,
             rls,
             hint_direct_introduce,
             implication,
             [],
             [RHS_Exp],
             []),
    !.

process_rule(RuleName_Atom: RHS_Exp may_be_deduced_from LHS_ExpList, RuleFile_Atom) :-
    add_rule(RuleFile_Atom,
             RuleName_Atom,
             rls,
             hint_conditional_introduce,
             implication,
             LHS_ExpList,
             [RHS_Exp],
             []),
        !.

process_rule(_X, _File) :-
    !.

%===============================================================================
%process_rulefile(+RuleSource, +RuleFile_Atom).
%-------------------------------------------------------------------------------
% Retrieve rules from a rule file.
%===============================================================================

process_rulefile(RuleSource, RuleFile_Atom) :-
    open(RuleFile_Atom, read, RuleFile_Stream),
    process_rulefile_x(RuleSource, RuleFile_Atom, RuleFile_Stream),
    close(RuleFile_Stream),
    !.

%-------------------------------------------------------------------------------

process_rulefile_x(RuleSource, RuleFile_Atom, RuleFile_Stream):-
    repeat,
    on_exception(Exception,
                 read(RuleFile_Stream,
                      CandidateRule_Any),
                 user_rule_syntax_error(Exception,
                                        RuleFile_Atom)),
    process_candidate_rule(RuleSource, RuleFile_Atom, CandidateRule_Any),
    !.

%-------------------------------------------------------------------------------

% Finish at end_of_file.
process_candidate_rule(_RuleSource, _RuleFile_Atom, CandidateRule_Any) :-
    CandidateRule_Any == end_of_file,
    !.

% Process and backtrack if not end of file.
process_candidate_rule(RuleSource, RuleFile_Atom, CandidateRule_Any) :-
    process_candidate_rule_x(RuleSource, RuleFile_Atom, CandidateRule_Any),
    fail.

%-------------------------------------------------------------------------------

process_candidate_rule_x(RuleSource, RuleFile_Atom, CandidateRule_Any) :-
    check_candidate_rule(RuleFile_Atom, CandidateRule_Any),
    store_rule(RuleSource, RuleFile_Atom, CandidateRule_Any),
    !.

%-------------------------------------------------------------------------------

store_rule(RuleSource, RuleFile_Atom, (RuleId: Rule_Exp)):-
    % Extract rule components.
    extract_items_from_rule_exp(Rule_Exp,
                                RuleHeuristic,
                               RuleLogic,
                                LHS_ExpList,
                                RHS_ExpList,
                                Condition_ExpList),
    add_rule(RuleFile_Atom,
             RuleId,
             RuleSource,
             RuleHeuristic,
             RuleLogic,
             LHS_ExpList,
             RHS_ExpList,
             Condition_ExpList),
    !.

%-------------------------------------------------------------------------------



user_rule_syntax_error(Exception, File) :-
    Exception = error(_, syntax_error(_,LineNumber,Message,_,_)),
    atom_concat(Message, ' on line ', Message2),
    number_codes(LineNumber, LineNumberCodes),
    atom_codes(LineNumberAtom, LineNumberCodes),
    atom_concat(Message2, LineNumberAtom, Message3),
    rulefile_complain('Prolog syntax error', Message3, File),
    fail.

%===============================================================================
%check_candidate_rule(+RuleFile_Atom, +WholeRule_Any).
%-------------------------------------------------------------------------------
% Check purely for legal rule syntax (not semantics).
% Checks are:
% - Rule is not just a variable.
% - Rule is of the form "Name: Rule",
% - The Name is either an atom, or of the form Atom(Integer),
% - The atomic rulename starts with a lowercase letter, and consists of
%   lowercase letters, digits and underscores,
% - The integer argument in the name, if present, is non-negative,
% - The Rule part is one of:
%    * Predicate may_be_deduced[_from Conditions]
%    * OldExpr may_be_replaced_by NewExpr [if Conditions]
%    * OldExpr & NewExpr are_interchangeable [if Conditions],
% - The Conditions part, if present, is a well-formed list,
% - Any goal(Immediate) elements of the Conditions list has a Immediate part
%   which is one of:
%    * (X,Y)         ["and"]
%    * (X;Y)         ["or"]
%    * integer(X)
%    * intexp(X)
%    * checktype(X,Y)
%    * simplify(X,Y),
% - The rule Name is unique within the given File.
%
% If any of these conditions do not hold, the predicate fails. As errors
% are encountered they are logged and displayed on screen.
%===============================================================================

check_candidate_rule(RuleFile_Atom, WholeRule_Any) :-
    check_rule_structure(RuleFile_Atom, WholeRule_Any, RuleStatus),
    check_candidate_rule_x(RuleStatus),
    !.

%-------------------------------------------------------------------------------

% Succeed if rule was accepted.
check_candidate_rule_x(accepted):-
    !.

% Fail if rule was not accepted.
check_candidate_rule_x(rejected):-
    !,
    fail.

%-------------------------------------------------------------------------------

% It is an error to only have a prolog variable.
check_rule_structure(RuleFile_Atom, WholeRule_Any, rejected):-
    var(WholeRule_Any),
    rulefile_complain('Invalid rule (Prolog wildcard) in rulefile', [], RuleFile_Atom),
    !.

% Rule is to be of form: Name: Rule
check_rule_structure(RuleFile_Atom, (RuleId: Rule_Exp), RuleStatus):-
    check_rule_id(RuleFile_Atom, RuleId, One_RuleStatus),
    check_rule_exp(RuleFile_Atom, RuleId, Rule_Exp, Two_RuleStatus),

    determine_overall_rule_status([One_RuleStatus, Two_RuleStatus], RuleStatus),
    !.

% From above, rule is off the wrong structure.
check_rule_structure(RuleFile_Atom, WholeRule_Any, rejected):-
    rulefile_complain('Illegal rule syntax in rulefile', WholeRule_Any, RuleFile_Atom),
    !.

%===============================================================================
%check_rule_id(+RuleFile_Atom, +RuleId, -RuleStatus).
%-------------------------------------------------------------------------------
% Checks the rule identifier, storing and reporting any errors, and setting
% RuleStatus accordingly.
%===============================================================================

% It is an error to only have a prolog variable.
check_rule_id(RuleFile_Atom, RuleId, rejected):-
    var(RuleId),
    rulefile_complain('Invalid rulename (Prolog wildcard) in rule', [], RuleFile_Atom),
    !.

% Rule name is of form: name.
check_rule_id(RuleFile_Atom, RuleId, RuleStatus):-
    functor(RuleId, Base_Atom, 0),
    check_base(RuleFile_Atom, Base_Atom, One_RuleStatus),
    check_unique(RuleFile_Atom, Base_Atom, Two_RuleStatus),

    determine_overall_rule_status([One_RuleStatus, Two_RuleStatus], RuleStatus),
    !.

% Rule name is of form: name(10).
check_rule_id(RuleFile_Atom, RuleId, RuleStatus):-
    functor(RuleId, Base_Atom, 1),
    arg(1, RuleId, Sub_Int),
    check_base(RuleFile_Atom, Base_Atom, One_RuleStatus),
    check_sub(RuleFile_Atom, Base_Atom, Sub_Int, Two_RuleStatus),
    check_unique(RuleFile_Atom, RuleId, Three_RuleStatus),

    determine_overall_rule_status([One_RuleStatus, Two_RuleStatus, Three_RuleStatus], RuleStatus),
    !.

% From above, ruleid is off the wrong structure.
check_rule_id(RuleFile_Atom, RuleId, rejected):-
    rulefile_complain('Illegal rulename syntax in rulefile', RuleId, RuleFile_Atom),
    !.

%===============================================================================
% check_base(+RuleFile_Atom, +Base_Atom, -RuleStatus).
%-------------------------------------------------------------------------------
% Checks the rule base name, storing and reporting any errors, and setting
% RuleStatus accordingly.
%===============================================================================

% Make the parse_legal_base_name call visible to the spxref tool.
:- public parse_legal_base_name/2.

% Must be atom and in particular form.
check_base(_RuleFile_Atom, Base_Atom, accepted):-
    atom(Base_Atom),
    atom_chars(Base_Atom, BaseName_CharList),
    phrase(parse_legal_base_name, BaseName_CharList),
    !.

% From above, base rule name is flawed.
% Specific error message for not starting with a lower case character.
check_base(RuleFile_Atom, Base_Atom, rejected):-
    atom(Base_Atom),
    atom_chars(Base_Atom, [BaseName_CharList | _T_BaseName_CharList]),
    \+ inside_selected_character_class([lower_case_char], BaseName_CharList),

    rulefile_complain('Illegal rulename (does not start with a lowercase letter)',
                      Base_Atom,
                      RuleFile_Atom),
    !.

% From above, base rule name is flawed.
% Use general error message.
check_base(RuleFile_Atom, Base_Atom, rejected):-
    rulefile_complain('Illegal rulename (only lowercase letters, digits and underscores allowed)',
                      Base_Atom,
                      RuleFile_Atom),
    !.

%-------------------------------------------------------------------------------

parse_legal_base_name -->
    % Must lead with a lower case character.
    parse_atom_silent([lower_case_char], oneormore),
    % May follow with lower case characters, numbers or underscores.
    parse_atom_silent([lower_case_char, numeric, under_score], zeroormore),
    !.

%===============================================================================
% check_sub(+RuleFile_Atom, +Base_Atom, +Sub_Int, -RuleStatus).
%-------------------------------------------------------------------------------
% Checks the rule sub-part, storing and reporting any errors, and setting
% RuleStatus accordingly.
%===============================================================================

% Must be an integer, greater than or equal to 0.
check_sub(_RuleFile_Atom, _Base_Atom, Sub_Int, accepted):-
    integer(Sub_Int),
    Sub_Int>= 0,
    !.

% From above, is error.
check_sub(RuleFile_Atom, Base_Atom, Sub_Int, rejected):-
    functor(RuleId, Base_Atom, 1),
    arg(1, RuleId, Sub_Int),
    rulefile_complain('Illegal rule number in rule family', RuleId, RuleFile_Atom),
    !.

%===============================================================================
% check_unique(+RuleFile_Atom, +RuleId, -RuleStatus).
%-------------------------------------------------------------------------------
% Checks that the rule is unique, storing and reporting any errors, and
% setting RuleStatus accordingly.
%===============================================================================

check_unique(RuleFile_Atom, RuleId, accepted):-
    \+ get_rule(RuleFile_Atom,
                RuleId,
                _RuleSource,
                _RuleHeuristic,
                _RuleLogic,
                _LHS_ExpList,
                _RHS_ExpList,
                _Condition_ExpList),
    !.

check_unique(RuleFile_Atom, RuleId, rejected):-
    rulefile_complain('Illegal redeclaration of rule within rulefile', RuleId, RuleFile_Atom),
    !.

%===============================================================================
% check_rule_exp(+RuleFile_Atom, +Rule_Exp, -RuleStatus).
%-------------------------------------------------------------------------------
% Checks the rule expression is well formed, storing and reporting any
% errors, and setting RuleStatus accordingly.
%===============================================================================




% It is an error to only have a prolog variable.
check_rule_exp(RuleFile_Atom, RuleId, Rule_Exp, rejected):-
    var(Rule_Exp),
    rulefile_complain('Illegal rule body (Prolog wildcard)', RuleId, RuleFile_Atom),
    !.

check_rule_exp(RuleFile_Atom, RuleId, Rule_Exp, RuleStatus):-
    extract_items_from_rule_exp(Rule_Exp,
                                _RuleHeuristic,
                                RuleLogic,
                                LHS_ExpList,
                                _RHS_ExpList,
                                Condition_ExpList),
    check_condition_list(RuleFile_Atom, RuleId, Condition_ExpList, One_RuleStatus),
    check_implication_conditions(RuleFile_Atom, RuleId, RuleLogic, LHS_ExpList, Two_RuleStatus),

    determine_overall_rule_status([One_RuleStatus, Two_RuleStatus], RuleStatus),
    !.

% From above, error encountered.
check_rule_exp(RuleFile_Atom, RuleId, _Rule_Exp, rejected) :-
    rulefile_complain('Illegal rule body (malformed expression) in rulefile', RuleId, RuleFile_Atom),
    !.

%-------------------------------------------------------------------------------

% If implication, do check left hand side as if conditions.
check_implication_conditions(RuleFile_Atom, RuleId, implication, LHS_ExpList, RuleStatus):-
    check_condition_list(RuleFile_Atom, RuleId, LHS_ExpList, RuleStatus),
    !.

% From above is not implication.
check_implication_conditions(_RuleFile_Atom, _RuleId, _RuleLogic, _LHS_ExpList, accepted):-
    !.

%-------------------------------------------------------------------------------

check_condition_list(_RuleFile_Atom, _RuleId, Condition_ExpList, accepted):-
    % Must not be just a variable.
    \+ var(Condition_ExpList),
    legal_conditions(Condition_ExpList),
    !.

% From above, is in error.
check_condition_list(RuleFile_Atom, RuleId, _Condition_ExpList, rejected):-
    rulefile_complain('Illegal conditions list in rule', RuleId, RuleFile_Atom),
    !.

%-------------------------------------------------------------------------------

% All conditions valid.
legal_conditions([]):-
    !.

legal_conditions([H_Condition_Exp | T_Condition_ExpList]):-
    legal_condition(H_Condition_Exp),
    legal_conditions(T_Condition_ExpList).

%-------------------------------------------------------------------------------

% Accept if just a variable.
legal_condition(Condition_Exp) :-
    var(Condition_Exp),
    !.

% If an executable goal, must take one of the legal forms.
legal_condition(goal(Goal_Exp)) :-
        !,
        check_legal_goal_exp(Goal_Exp),
        !.

% If none of the above, is taken to be a valid expression.
legal_condition(_):-
        !.

%-------------------------------------------------------------------------------

% Must not be just a variable.
check_legal_goal_exp(Goal_Exp):-
    var(Goal_Exp),
    !,
    fail.

% Legal terminal forms.
check_legal_goal_exp(integer(_Any)).
check_legal_goal_exp(intexp(_Any)).
check_legal_goal_exp(checktype(_X_Any, _Y_Any)).
check_legal_goal_exp(simplify(_X_Any,_Y_Any)).

% Legal composite forms.
check_legal_goal_exp((LHS_Exp,RHS_Exp)) :-
    !,
    check_legal_goal_exp(LHS_Exp),
    check_legal_goal_exp(RHS_Exp).

check_legal_goal_exp((LHS_Exp;RHS_Exp)) :-
    !,
    check_legal_goal_exp(LHS_Exp),
    check_legal_goal_exp(RHS_Exp).

%===============================================================================
% determine_overall_rule_status(+RuleStatus_List, -RuleStatus).
%-------------------------------------------------------------------------------
% Combines a collection of rule status indicators as a single status. This
% mechanism allows for the rule checking to be proceed without many
% confusing failure points and potential backtracking.
%===============================================================================

% No occurrence of rejected as accepted.
determine_overall_rule_status(RuleStatus_List, accepted):-
    \+ member(rejected, RuleStatus_List),
    !.

% From above, rejected is present at least once.
determine_overall_rule_status(_RuleStatus_List, rejected):-
    !.

%===============================================================================
% rulefile_complain(+Complaint, +Argument, +File).
%-------------------------------------------------------------------------------
% Report an error in a rulefile.
%===============================================================================


rulefile_complain(Complaint, Argument, File) :-
        convert_file_for_display(File, DisplayFile),

        print('!!! Erroneous entry in rulefile '),
        print(DisplayFile),
        nl,
        print('!!! '),
        print(Complaint),
        (
           Argument = []
        ;
           nl,
           print('!!! Involving: '),
           print(Argument)
        ),
        nl,
        nl,
        /* Record detection of syntax error in log file. */
        user:assert_log_fact(rule_syntax_error(Complaint, Argument, File), []),
        !.

%===============================================================================
% extract_items_from_rule_exp(+Rule_Exp,
%                             -RuleHeuristic,
%                             -RuleLogic,
%                             -LHS_ExpList,
%                             -RHS_ExpList,
%                             -Condition_ExpList).
%-------------------------------------------------------------------------------
% Given a rule expression Rule_Exp, extract its various attributes. Will
% fail if the rue expression is flawed.
%===============================================================================

extract_items_from_rule_exp(RHS_Exp may_be_deduced,
                            hint_direct_introduce,
                            implication,
                            [],
                            [RHS_Exp],
                            []):-
    !.

extract_items_from_rule_exp(RHS_Exp may_be_deduced_from LHS_ExpList,
                            hint_conditional_introduce,
                            implication,
                            LHS_ExpList,
                            [RHS_Exp],
                            []):-
    !.

extract_items_from_rule_exp(LHS_Exp may_be_replaced_by RHS_Exp,
                            hint_rewrite_one_direction,
                            equation,
                            [LHS_Exp],
                            [RHS_Exp],
                            []):-
    !.

extract_items_from_rule_exp(LHS_Exp may_be_replaced_by RHS_Exp if Condition_ExpList,
                            hint_rewrite_one_direction,
                            equation,
                            [LHS_Exp],
                            [RHS_Exp],
                            Condition_ExpList):-
    !.

extract_items_from_rule_exp(LHS_Exp & RHS_Exp are_interchangeable,
                            hint_rewrite_both_directions,
                            equation,
                            [LHS_Exp],
                            [RHS_Exp],
                            []):-
    !.


extract_items_from_rule_exp(LHS_Exp & RHS_Exp are_interchangeable if Condition_ExpList,
                            hint_rewrite_both_directions,
                            equation,
                            [LHS_Exp],
                            [RHS_Exp],
                            Condition_ExpList):-
    !.

%===============================================================================
% restructure_rules.
%-------------------------------------------------------------------------------
% To ease the applicability of rules, they are restructured into a
% standardised form.
%===============================================================================












restructure_rules :-
    get_rule(RuleFile_Atom,
             RuleId,
             RuleSource,
             RuleHeuristic,
             RuleLogic,
             LHS_ExpList,
             RHS_ExpList,
             Condition_ExpList),
    prune_rule(RuleFile_Atom,
               RuleId,
               RuleSource,
               RuleHeuristic,
               RuleLogic,
               LHS_ExpList,
               RHS_ExpList,
               Condition_ExpList),
    restructure_rule_exp_list(LHS_ExpList, RestructuredLHS_ExpList),
    restructure_rule_exp_list(RHS_ExpList, RestructuredRHS_ExpList),
    restructure_rule_exp_list(Condition_ExpList, RestructuredCondition_ExpList),
    add_rule(RuleFile_Atom,
             RuleId,
             RuleSource,
             RuleHeuristic,
             RuleLogic,
             RestructuredLHS_ExpList,
             RestructuredRHS_ExpList,
             RestructuredCondition_ExpList),
    fail.

restructure_rules :-
    !.

%-------------------------------------------------------------------------------

restructure_rule_exp_list([], []):-
    !.

restructure_rule_exp_list([H_In_Exp | T_In_ExpList],
                          [H_Out_Exp | T_Out_ExpList]):-
    restructure_rule_exp(H_In_Exp, H_Out_Exp),
    restructure_rule_exp_list(T_In_ExpList,
                              T_Out_ExpList).

%-------------------------------------------------------------------------------

% Preserve meta variables.
restructure_rule_exp(In_m_Out_m_Exp, In_m_Out_m_Exp):-
    var(In_m_Out_m_Exp),
    !.


% Adopt core type for quantified variables. As VCs are loaded, they are
% processed by restructure_formula/2, replacing quantified variable types
% with their core type. Here, the same normalization is applied to rules,
% to increase the likelihood of the two forms matching.

% Adopt core type for universally quantified variables.
restructure_rule_exp(for_all(V:T, P), for_all(V:CT, NewP)) :-
    !,
    find_core_type(T, CT),
    restructure_rule_exp(P, NewP),
    !.

% Adopt core type for extensionally quantified variables.
restructure_rule_exp(for_some(V:T, P), for_some(V:CT, NewP)) :-
    !,
    find_core_type(T, CT),
    restructure_rule_exp(P, NewP),
    !.

% From above, no changes. Recursive over arguments.
restructure_rule_exp(In_Exp, Out_Exp):-
    In_Exp=..[Functor_Atom | Args_ExpList],
    restructure_rule_exp_list(Args_ExpList, NewArgs_ExpList),
    Out_Exp=..[Functor_Atom | NewArgs_ExpList],
    !.

%###############################################################################
%END-OF-FILE