% -----------------------------------------------------------------------------
%  (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.
% 
% =============================================================================


(consult) :-
        (
           command_arg(filename, FILENAME),
           !
        ;
           prompt_user('Filename? '),
           rread(FILENAME)
        ),
        inform_user,
        user_rules(FILENAME),
        !.


user_rules(FNAME) :-
        atom(FNAME),
        file_exists_and_is_readable(FNAME),
        (
           plain_output(off),
           get_file_attrib(FNAME, [FULL_NAME|_], _),
           record_consultation_of(FULL_NAME)
        ;
           plain_output(on),
           record_consultation_of(FNAME)
        ),
        see(FNAME),
        seen,
        see(FNAME),
        retractall(banned_rule(FNAME,_)),
        process_rulefile(FNAME),
        write('Rulefile '),
        print(FNAME),
        write(' processed.'),
        nl,
        seen,                                                   /* CFR015 */
        see_correct_input_stream,                           /* CFR015,051 */
        !.                                                      /* CFR051 */
user_rules(FNAME) :-
        atom(FNAME),
        \+ file_exists_and_is_readable(FNAME),
        write('Warning: '),
        print(FNAME),
        write(' does not exist or cannot be read.'),
        nl,
        !,
        fail.


inform_user :-
   write('-------------------------------------------------------------------'),
   nl,
   write('Badly-formed  rules will now be displayed on the screen as they are'),
   nl,
   write('read and possibly on subsequent  consultations  of  this  rulefile.'),
   nl,
   write('-------------------------------------------------------------------'),
   nl,
   write('Watch for other messages informing you of bad rulenames or improper'),
   nl,
   write('rule  conditions;  bad  rules  will  not  be  used  by the checker.'),
   nl,
   write('If too serious an error is found, the rulefile  may  be  abandoned.'),
   nl,
   write('-------------------------------------------------------------------'),
   nl, !.


process_rulefile(FNAME) :-
   repeat,
    read_term_and_layout(RULE),
    process_single_rule(FNAME, RULE, RULENAME, PF, OK),
    (
       var(OK),
       add_rulefacts(FNAME,RULENAME,PF)
    ;
       nonvar(OK),
       report_bad_rule(FNAME,RULE,RULENAME,OK)
    ),
   /*until*/ (RULE=end_of_file ; bad_rulefile, scrap_rulefile(FNAME)), !,
    (
       logfact(text, _)
    ;
       assertz(logfact(text, 'No errors trapped in reading this rulefile.'))
    ),
    !.


process_single_rule(FNAME, RULE, _, _, _) :-
    nonvar(RULE),
    RULE = (A : B),
    nonvar(A),
    A = (rule_family NAME),
    atom(NAME),
    nonvar(B),
    !,
    RNAME =.. [NAME,_],
    save_requirements(FNAME, RNAME, B),
    !,
    fail.
process_single_rule(FNAME, RULE, RULENAME, PF, OK) :-
    check_structure(RULE,RULENAME,BODY,CONDITIONS,OK),
    check_rulename(RULENAME,OK),
    check_conditions(CONDITIONS,OK),
    check_body(BODY,PF,OK),
    check_rule_family_declared(FNAME, RULENAME, PF, OK),
    !.


save_requirements(FNAME, RNAME, REST & REQ) :-
    save_single_requirement(FNAME, RNAME, REQ),
    save_requirements(FNAME, RNAME, REST),
    !.
save_requirements(FNAME, RNAME, REQ) :-
    save_single_requirement(FNAME, RNAME, REQ),
    !.


save_single_requirement(FNAME, RNAME, REQ) :-
    nonvar(REQ),
    REQ = (EXPR requires CONSTRAINTS),
    check_constraints(CONSTRAINTS),
    check_all_requirements(EXPR, CONSTRAINTS),
    maybe_add(user_classification(EXPR, FNAME, RNAME, CONSTRAINTS)),
    !.


check_constraints([H|T]) :-
    nonvar(H),
    H = (V:C),
    var(V),
    atom(C),
    ( C=i ; C=ir ; C=ire ; C=e ; C=any ),
    check_constraints(T),
    !.
check_constraints([]) :- !.


check_all_requirements(EXPR, CONSTRAINTS) :-
    \+ any_holes_left(EXPR, CONSTRAINTS),
    !.


any_holes_left(EXPR, CONSTRAINTS) :-
    instantiate_all_vars(EXPR, CONSTRAINTS),
    novars(EXPR),
    !,
    fail.
any_holes_left(_EXPR, _CONSTRAINTS) :- !.


instantiate_all_vars(_EXPR, []) :- !.
instantiate_all_vars(EXPR, [(H:X) | T]) :-
    H=X,
    instantiate_all_vars(EXPR, T),
    !.

check_structure(RULE,RULENAME,BODY,CONDITIONS,_) :-
    nonvar(RULE),
    (
       RULE = (RULENAME: (BODY if CONDITIONS))
    ;
       RULE = (RULENAME: (B may_be_deduced_from CONDITIONS)),
       BODY = infer(B)
    ;
       RULE = (RULENAME: (B may_be_deduced)),
       CONDITIONS = [],
       BODY = infer(B)
    ;
       RULE = (RULENAME: BODY),
       CONDITIONS = []
    ), !.
check_structure(_,_,_,_,bad_structure) :- !.


check_rulename(RULENAME,_) :-
       nonvar(RULENAME),
       RULENAME=..[PF,ARG],
       atom(PF),
       integer(ARG),
       ARG >= 0,
       !.
check_rulename(_,bad_rulename) :- !.
check_rulename(_,_).


check_conditions(CONDITIONS,OK) :-
    nonvar(CONDITIONS),
    (
       CONDITIONS=[]
    ;
       CONDITIONS=[COND|REST],
       good_condition(COND),
       check_conditions(REST,OK)
    ), !.
check_conditions(_,bad_conditions) :- !.
check_conditions(_,_).


good_condition(V) :- var(V), !.
good_condition(goal(G)) :-
    !,
    permitted_immediate(G),
    !.
good_condition(_V).


permitted_immediate(G) :-
    var(G),
    !,
    fail.
permitted_immediate(','(G1,G2)) :-
    permitted_immediate(G1),
    permitted_immediate(G2),
    !.
permitted_immediate(';'(G1,G2)) :-
    permitted_immediate(G1),
    permitted_immediate(G2),
    !.
permitted_immediate(not G) :-
    permitted_immediate(G).
permitted_immediate(checktype(_,_)).
permitted_immediate(type(_,_)).
permitted_immediate(enumeration(_,_)).
permitted_immediate(enumeration_list(_,_)).
permitted_immediate(last(_,_)).
permitted_immediate(in_order(_,_,_)).
permitted_immediate(_ = _).
permitted_immediate(_ \= _).
permitted_immediate(in(_,_)).
permitted_immediate(subset(_,_)).
permitted_immediate(subst_vbl(_,_,_,_)).
permitted_immediate(strict_sublist(_,_)).
permitted_immediate(append(_,_,_)).
permitted_immediate(set_union(_,_,_)).
permitted_immediate(set_intersect(_,_,_)).
permitted_immediate(set_lacking(_,_,_)).
permitted_immediate(simplify(_,_)).
permitted_immediate(integer(_)).
permitted_immediate(nonvar(_)).
permitted_immediate(var(_)).
permitted_immediate(atom(_)).
permitted_immediate(atomic(_)).
permitted_immediate(length(_,_)).
permitted_immediate(element(_,_,_)).
permitted_immediate(iss(_,_)).
permitted_immediate(genvar(_,_)).

% Make these predicate calls, potentially made via the goal portion of user
% created external rules, visible to the spxref tool.

% These predicates are implemented as part of the checker. Note that some
% are also called internally by the checker.
:- public checktype/2.
:- public enumeration/2.
:- public enumeration_list/2.
:- public genvar/2.
:- public in_order/3.
:- public iss/2.
:- public set_intersect/3.
:- public set_lacking/3.
:- public set_union/3.
:- public simplify/2.
:- public strict_sublist/2.
:- public subst_vbl/4.
:- public type/2.

% These predicates are standard in sicstus, or provided through a sicstus
% library. The spxref tool is weak in processing these, thus it is
% preferable to suppress their public declarations.
% :- public append/3.
% :- public atom/1.
% :- public atomic/1.
% :- public element/3.
% :- public in/2.
% :- public integer/1.
% :- public last/2.
% :- public length/2.
% :- public nonvar/1.
% :- public var/1.

% The built-in rules make use of further predicates, not available to user
% created external rules. Here, these potential command calls are also made
% visible to the spxref tool.
:- public build_other_cases/4.
:- public find_element/3.
:- public is_in/2.
:- public make_record_equality_goal/4.
:- public mk__function_name/3.
:- public norm_typed_expr/3.
:- public novars/1.
:- public record_function/6.
:- public try_deduce/1.

check_body(BODY,[PF|REST],_) :-
    nonvar(BODY),
    (
       BODY=(F may_be_replaced_by G),
       REST=[]
    ;
       BODY=(F & G are_interchangeable),
       (
          var(G),
          REST=[_]
       ;
          nonvar(G),
          G=..[GOP|GArgs],
          make_up(R,GOP,GArgs),
          REST=[R]
       )
    ;
       BODY=infer(F),
       REST=[]
    ),
    (
       var(F),
       PF=(_)
    ;
       nonvar(F),
       F=..[FOP|FArgs],
       make_up(PF,FOP,FArgs)
    ), !.
check_body(_,_,bad_body) :- !.
check_body(_,_,_).


check_rule_family_declared(FNAME, RULENAME, PF, OK) :-
        var(OK),
        !,
        PF=[X|R],
        (
           var(X),
           XX=(_)
        ;
           X=..[XOP|Xargs],
           make_up(XX,XOP,Xargs)
        ),
        !,
        (
           user_classification(XX, FNAME, RULENAME, _)
        ;
           OK = rule_family_not_declared_for_this_usage
        ),
        !,
        (
           R=[]
        ;
           R=[Y],
           (
              var(Y),
              YY=(_)
           ;
              Y=..[YOP|Yargs],
              make_up(YY,YOP,Yargs)
           ),
           !,
           (
              user_classification(YY, FNAME, RULENAME, _)
           ;
              OK = rule_family_not_declared_for_this_usage
           )
        ),
        !.
check_rule_family_declared(_,_,_,_).


add_rulefacts(FNAME,RULENAME,[PF]) :-
    (
       rulefile(F,FNAME),
       var(F)
    ;
       var(PF),
       retractall(user_rulefile(_,FNAME)),
       assertz(user_rulefile(_,FNAME))
    ;
       rulefile(PF,FNAME)
    ;
       assertz(user_rulefile(PF,FNAME))
    ),
    (
       rulefile(FNAME,RULENAME)
    ;
       RULENAME=..[FAMILY,_MEMBER],
       RN=..[FAMILY,_],
       assertz(user_rulefile(FNAME,RN))
    ), !.
add_rulefacts(FNAME,RULENAME,[PF1,PF2]) :-
    add_rulefacts(FNAME,RULENAME,[PF1]),
    add_rulefacts(FNAME,RULENAME,[PF2]),
    !.


report_bad_rule(_,end_of_file,_,_) :- !.
report_bad_rule(_,RULE,RULENAME,WARNING) :-
    write('!!! '),
    print(RULE),
    nl,
    write('*** WARNING: Rule '),
    print(RULENAME),
    write(' -- '),
    print(WARNING),
    maybe_add(logfact(text, 'Error(s) were found in consulting this rulefile')),
    nl,
    fail.
report_bad_rule(_,_,RULENAME,bad_rulename) :-
    var(RULENAME),
    assertz(bad_rulefile),
    write('*** ERROR TOO SERIOUS: Cannot use this file as it stands.'),
    nl,
    write('PROCESSING ABORTED.'),
    nl,
    nl,
    maybe_add(logfact(text, 'SERIOUS ERROR: Could not accept this file for use.')),
    !.
report_bad_rule(_,_,_,bad_rulename) :- nl, !.
report_bad_rule(FNAME,_,RULENAME,_) :-
    assertz(banned_rule(FNAME,RULENAME)),
    nl,
    !.


scrap_rulefile(FNAME) :-
    retractall(user_rulefile(_,FNAME)),
    retractall(user_rulefile(FNAME,_)),
    retractall(user_classification(_,FNAME,_,_)),
    retractall(banned_rule(FNAME,_)),
    retractall(bad_rulefile),
    !.


record_consultation_of(_) :-
        record_consults(off),
        !.
record_consultation_of(FULL_NAME) :-
        assertz(logfact((consult), FULL_NAME)),
        !.
%###############################################################################
%END-OF-FILE