/*  ANALYSE.PL  */
 
 
:- module analyse.
 
 
:- public analyse_fact/2,
          analyse_question/1.
 
 
/*
SPECIFICATION
-------------
 
PUBLIC analyse_fact( FactNumber+, Fact+ ):
 
Writes Fact with its number in "analysed" form as described in script 4.
This entails writing it in Logic syntax, preceding the head of Fact by
'for all HV', where HV is a list of variables which occur only in the
head, and preceding its tail by 'there exist(s) TV such that' where TV is
the variables occurring only in the tail.
 
Incorrect facts just come out as 'N contains an error'.
 
 
PUBLIC analyse_fact( Question+ ):
 
Writes Question in analysed form. This is as for the analysed form of
tails, but the question is preceded by 'Is there any'/'Are there any'
 
Incorrect questions come out as 'the question contains an error'.
*/
 
 
/*
IMPLEMENTATION
--------------
 
To analyse a fact, we collect its variables, separating them into those
that occur in the head (and possibly in the tail as well), and those
that occur only in the tail. We then pretty-print, using a modification
of the SDO rules used by 'show', and inserting phrases denoting
existential or universal quantifiers in appropriate places. The SDO
rules peculiar to this module live in ANALYSE_SDO.
 
Analysing questions is similar, except that we don't need to separate
the two kinds of variable, since we only have existentially quantified
ones.
 
As variables are stored in unordered lists (or at least the order is not
helpful to _finding_ a variable), the predicates are not particularly
efficient. However, the lists will typically be small (0 to 2 variables
each), so this is not important.
 
See the implementation notes for SHOW.PL concerning variable unbinding
and failure.
*/
 
 
:- needs
    assign_variable_names / 1,
    fact_vs_clause_and_vars / 3,
    is_good_fact / 1,
    is_good_question / 1,
    output / 1,
    question_vs_goal_and_vars / 3.
 
 
analyse_fact( FactNumber, Fact ) :-
    analyse_fact_1( FactNumber, Fact ),
    fail.
 
analyse_fact( FactNumber, Fact ).
 
 
analyse_fact_1( FactNumber, Fact ) :-
    is_good_fact( Fact ),
    !,
    fact_vs_clause_and_vars( Fact, Clause, Vars ),
    head_tail_vars( Clause, HeadVars, TailVars ),
    assign_variable_names( Vars ),
    pretty( analysed_numbered_rule_out( FactNumber, Clause,
                                        HeadVars, TailVars ),
            78,
            prolog
          ),
    output('.'~ ).
 
analyse_fact_1( FactNumber, Fact ) :-
    output( FactNumber...'contains an error.'~ ).
 
 
analyse_question( Question ) :-
    analyse_question_1( Question ),
    fail.
 
analyse_question( Question ).
 
 
analyse_question_1( Question ) :-
    is_good_question( Question ),
    !,
    question_vs_goal_and_vars( Question, Goal, Vars ),
    assign_variable_names( Vars ),
    varnames_to_vars( Vars, Vs ),
    pretty( analysed_question_out( Goal, Vs ),
            78,
            prolog
          ),
    output('?'~ ).
 
analyse_question_1( Question ) :-
    output( 'The question contains an error.'~ ).
 
 
/*  head_tail_vars( Clause+, HeadVars-, TailVars- ):
        HeadVars is a list of the variables that appear in Clause's head
        but not its tail; TailVars is the rest, those in its tail only.
        In both lists, variables appear in the same order as in Clause.
*/
head_tail_vars( (Head:-Tail), HeadVars, TailVars ) :-
    !,
    vars_in( Head, [], [], HeadVars ),
    vars_in( Tail, HeadVars, [], TailVars ).
 
head_tail_vars( Head, HeadVars, [] ) :-
    vars_in( Head, [], [], HeadVars ).
 
 
/*  vars_in( V, ToBeExcluded+, Vars0+, Vars- ):
        V is a variable: the other arguments are, or will be unified
        with, lists of variables.
        If V is in TobeExcluded or Vars0, Vars = Vars0.
        Otherwise Vars = Vars0 with V inserted at the end.
*/
vars_in( V, ToBeExcluded, Vars, Vars ) :-
    var( V ),
    strict_member( V, ToBeExcluded ),
    !.
 
vars_in( V, ToBeExcluded, Vars0, Vars ) :-
    var( V ),
    unite_var( V, Vars0, Vars ).
 
vars_in( A, _, Vars, Vars ) :-
    atomic( A ), !.
 
vars_in( A, ToBeExcluded, Vars0, Vars ) :-
    A =.. [ _ | Args ],
    vars_in_1( Args, ToBeExcluded, Vars0, Vars ).
 
 
/*  vars_in_1( L+, ToBeExcluded+, Vars0+, Vars- ):
        Apply vars_in to each element of L.
*/
vars_in_1( [], _, Vars, Vars ) :- !.
 
vars_in_1( [H|T], ToBeExcluded, Vars0, Vars ) :-
    vars_in( H, ToBeExcluded, Vars0, Vars1 ),
    vars_in_1( T, ToBeExcluded, Vars1, Vars ).
 
 
/*  unite_var( V, Vars0+, Vars- ):
        Vars is the union of Vars0 and [V]. V is added, if at all, at
        the end.
*/
unite_var( V, [], [V] ) :- !.
 
unite_var( V, [Var0|RestVars0], [Var0|RestVars0] ) :-
    V == Var0,
    !.
 
unite_var( V, [Var0|RestVars0], [Var0|RestVars] ) :-
    unite_var( V, RestVars0, RestVars ).
 
 
/*  strict_member( Y, L+ ):
        True if there is an element of L which is identical (==) to Y.
*/
strict_member( Y, [X|_] ) :-
    Y == X,
    !.
 
strict_member( X, [_|Y] ) :-
    strict_member( X, Y ).
 
 
varnames_to_vars( [], [] ) :- !.
 
varnames_to_vars( [var(Var,_)|VarnamesRest], [Var|VarsRest] ) :-
    varnames_to_vars( VarnamesRest, VarsRest ).
 
 
:- endmodule.
