/*  AND_OR.PL  */
 
 
:- module and_or.
 
 
:- public trace_goals/3,
          why_goals/5.
 
 
/*
SPECIFICATION
-------------
 
 
PUBLIC trace_goals( Goals+, Varnames+, Where+ ):
------------------------------------------------
 
Goals is a list of goals, with variable names Varnames. trace_goals
traces their execution, displaying its messages to the standard output.
If Where=screen, this is the screen, else a printer. This is used
in controlling how the TLI interacts.
 
 
PUBLIC why_goals( Goals+, Varnames+, AndList-, SF-, Where+ ):
-------------------------------------------------------------
 
Goals and Varnames are as above. why_goals executes the goals
to completion, and instantiates AndList to the resulting and-list.
 
SF becomes 's' if the goals succeeded, 'f' if they failed, and
'a' if it was aborted.
 
For the format of and-lists, see the next section.
 
 
And-or-trees: representation.
-----------------------------
 
These are quite complicated, and it will help if you can read about
and-or-trees in
    "The Transparent Prolog Machine: Visualising Logic Programs",
    by Marc Eisenstadt, Mike Brayshaw and Jocelyn Ireson-Paine,
    Intellect,
    1991.
 
Failing this, try calling why_goals on a few simple goals, e.g.
    why_goals( [true], [], AndList, SF ).
    why_goals( [a(X)], [], AndList, SF ).
    why_goals( [a(X),fail], [], AndList, SF ).
    why_goals( [a(X),b(Y),fail], [], AndList, SF ).
    (...etc...)
where you have various unconditional clauses for a and b. You can leave
the Varnames argument as []: the names are not essential to construction
of the tree. The trees rapidly get complicated: use pp from PP.SDO, or
some other general-purpose pretty-printer to pretty-print them in a
clearly indented format with plenty of space. In case you don't
want to do this, I include some sample outputs later.           
 
 
Briefly, an and-or tree contains all the information about how a set of
Prolog goals was proven, including details of failures on the way. It
contains two types of node: and-nodes, and or-nodes. These nodes are
collected into lists: and-lists, and or-lists. And-lists correspond to a
conjunction of goals, and have one branch (element) leading off them for
each simple goal. Thus the list for
    a(X),fail
would have one branch for a(X) and one for fail.
 
When we draw and-or-trees, it's convenient to talk about branches.
However, I represent the tree as lists, so each branch corresponds
to one list element.
 
In an and-list, all but the final goal will have succeeded (you can't
continue past a failure); the final goal may either succeed or fail.
 
 
Each element (branch) of an and-list is an and-node. This contains
information about its goal: the goal itself, the variables bound
when the goal was called, whether it succeeded or failed, and (if
it succeeded), the variables in force after the call.
 
 
An and-node also contains information about how the goal was proven. If
the goal had clauses (rather than being a primitive goal like 'true',
or a system predicate), then its and-node contains an or-list. This
represents the set of alternative clauses used in proving the
goal. All but the final clause will have failed, or been forced to fail
when the goal was backtracked into from outside. This is the converse
of the condition mentioned above for and-lists: you can't select another
alternative if the previous one has just succeeded.
 
 
Each element of an or-list corresponds to one clause. In this
implementation, this contains the clause's textbase number (or position
in the database, if taken therefrom). If the clause was a conditional
one, it will have a tail; this will determine another and-list, for the
goals in that tail. And so the tree continues until we reach primitive
goals.
 
 
There is one complication. Consider the query
    a(X), write(X), b(Y), write(X+Y), fail.
where we have clauses
    a(1). a(2).
    b(3). b(4).
 
The and-list for this will be something like
    [
        and-node for a(X):
        [
            or-node for a(1)
            or-node for a(2)
        ]
        and-node for write(X),
        and-node for b(Y),
        [
            or-node for b(3)
            or-node for b(4)
        ]
        and-node for write(X+Y)
        and-node for fail
    ]
 
Now, the call to write(X) will be re-done twice. The second time is after
a(X) has been backtracked into by the fail. Similarly, the call to b(Y)
will be re-done twice, and that for write(X+Y) will be re-done four
times, once for each value of X and Y. All this is familiar to anyone
who knows backtracking.
 
The complication is that the and-node for a(X) has to record two sets
of new variable bindings, one for the solution X=1 and one for X=2.
The and-node for write(X) is even worse, because it has to record two
calls, write(1) and write(2). All but the last once succeeded, but
were subsequently backtracked over: in TPM terminology, they're called
"ghosts".
 
The multiple sets of bindings are managed by storing a list of bindings.
And the multiple calls are managed by having the tail of an and-list
be a list of lists, one for each continuation. In my representation,
the inner lists are wrapped in the functor 'fd', for "forward".            
 
 
Sample and-or-trees.
--------------------
 
why_goals([true],[],AndList,SF):
[ a( success(true),
     true,
     [s(bs([], 0, [])) | _1],
     bs([], 0, [])
  ),
  fd([])
]
 
 
why_goals([fail],[],AndList,SF):
[a(fail(fail), fail, _1, bs([], 0, [])) | _2]
 
 
why_goals([a(_1)],[],AndList,SF):
[ a( [ o( success(unify_with_unconditional_fact(a(_0))),
          clause(db <> 1, a(1), [], []),
          bs([], 1, [])
       )
     ],
     a(_0),
     [s(bs([], 1, [0 = 1])) | _1],
     bs([], 1, [])
  ),
  fd([])
]
 
 
why_goals([a(_1), fail],[],AndList,SF):
[ a( [ o( success(unify_with_unconditional_fact(a(_0))),
          clause(db <> 1, a(1), [], []),
          bs([], 1, [])
       ),
       o( success(unify_with_unconditional_fact(a(_0))),
          clause(db <> 2, a(2), [], []),
          bs([], 1, [])
       )
     ],
     a(_0),
     [ s(bs([], 1, [0 = 1])),
       s(bs([], 1, [0 = 2]))
     ],
     bs([], 1, [])
  ),
  fd( [ a(fail(fail), fail, _1, bs([], 1, [0 = 1]))
      ]
  ),
  fd( [ a(fail(fail), fail, _1, bs([], 1, [0 = 2]))
      ]
  )
]
 
 
why_goals([a(_1), b(_2)],[],AndList,SF):
[ a( [ o( success(unify_with_unconditional_fact(a(_0))),
          clause(db <> 1, a(1), [], []),
          bs([], 2, [])
       )
     ],
     a(_0),
     [s(bs([], 2, [0 = 1])) | _1],
     bs([], 2, [])
  ),
  fd( [ a( [ o( success(unify_with_unconditional_fact(b(_1))),
                clause(db <> 1, b(3), [], []),
                bs([], 2, [0 = 1])
             )
           ],
           b(_1),
           [s(bs([], 2, [1 = 3, 0 = 1])) | _1],
           bs([], 2, [0 = 1])
        ),
        fd([])
      ]
  )
]
 
 
why_goals([a(_1), b(_2), fail],[],AndList,SF):
[ a( [ o( success(unify_with_unconditional_fact(a(_0))),
          clause(db <> 1, a(1), [], []),
          bs([], 2, [])
       ),
       o( success(unify_with_unconditional_fact(a(_0))),
          clause(db <> 2, a(2), [], []),
          bs([], 2, [])
       )
     ],
     a(_0),
     [ s(bs([], 2, [0 = 1])),
       s(bs([], 2, [0 = 2]))
     ],
     bs([], 2, [])
  ),
  fd( [ a( [ o( success(unify_with_unconditional_fact(b(_1))),
                clause(db <> 1, b(3), [], []),
                bs([], 2, [0 = 1])
             ),
             o( success(unify_with_unconditional_fact(b(_1))),
                clause(db <> 2, b(4), [], []),
                bs([], 2, [0 = 1])
             )
           ],
           b(_1),
           [ s(bs([], 2, [1 = 3, 0 = 1])),
             s(bs([], 2, [1 = 4, 0 = 1]))
           ],
           bs([], 2, [0 = 1])
        ),
        fd( [ a( fail(fail),
                 fail,
                 _1,
                 bs([], 2, [1 = 3, 0 = 1])
              )
            ]
        ),
        fd( [ a( fail(fail),
                 fail,
                 _1,
                 bs([], 2, [1 = 4, 0 = 1])
              )
            ]
        )
      ]
  ),
  fd( [ a( [ o( success(unify_with_unconditional_fact(b(_1))),
                clause(db <> 1, b(3), [], []),
                bs([], 2, [0 = 2])
             ),
             o( success(unify_with_unconditional_fact(b(_1))),
                clause(db <> 2, b(4), [], []),
                bs([], 2, [0 = 2])
             )
           ],
           b(_1),
           [ s(bs([], 2, [1 = 3, 0 = 2])),
             s(bs([], 2, [1 = 4, 0 = 2]))
           ],
           bs([], 2, [0 = 2])
        ),
        fd( [ a( fail(fail),
                 fail,
                 _1,
                 bs([], 2, [1 = 3, 0 = 2])
              )
            ]
        ),
        fd( [ a( fail(fail),
                 fail,
                 _1,
                 bs([], 2, [1 = 4, 0 = 2])
              )
            ]
        )
      ]
  )
]
 
 
why_goals([a(_1), b(_2), _1 > 1],[],AndList,SF):
[ a( [ o( success(unify_with_unconditional_fact(a(_0))),
          clause(db <> 1, a(1), [], []),
          bs([], 2, [])
       ),
       o( success(unify_with_unconditional_fact(a(_0))),
          clause(db <> 2, a(2), [], []),
          bs([], 2, [])
       )
     ],
     a(_0),
     [ s(bs([], 2, [0 = 1])),
       s(bs([], 2, [0 = 2]))
     ],
     bs([], 2, [])
  ),
  fd( [ a( [ o( success(unify_with_unconditional_fact(b(_1))),
                clause(db <> 1, b(3), [], []),
                bs([], 2, [0 = 1])
             ),
             o( success(unify_with_unconditional_fact(b(_1))),
                clause(db <> 2, b(4), [], []),
                bs([], 2, [0 = 1])
             )
           ],
           b(_1),
           [ s(bs([], 2, [1 = 3, 0 = 1])),
             s(bs([], 2, [1 = 4, 0 = 1]))
           ],
           bs([], 2, [0 = 1])
        ),
        fd( [ a( fail(system_call(_0 > 1)),
                 _0 > 1,
                 _1,
                 bs([], 2, [1 = 3, 0 = 1])
              )
            ]
        ),
        fd( [ a( fail(system_call(_0 > 1)),
                 _0 > 1,
                 _1,
                 bs([], 2, [1 = 4, 0 = 1])
              )
            ]
        )
      ]
  ),
  fd( [ a( [ o( success(unify_with_unconditional_fact(b(_1))),
                clause(db <> 1, b(3), [], []),
                bs([], 2, [0 = 2])
             )
           ],
           b(_1),
           [s(bs([], 2, [1 = 3, 0 = 2])) | _1],
           bs([], 2, [0 = 2])
        ),
        fd( [ a( success(system_call(_0 > 1)),
                 _0 > 1,
                 [s(bs([], 2, [1 = 3, 0 = 2])) | _1],
                 bs([], 2, [1 = 3, 0 = 2])
              ),
              fd([])
            ]
        )
      ]
  )
]
 
 
why_goals([a(_1), write(_1), b(_2), write(_1 + _2), fail],[],AndList,SF):
[ a( [ o( success(unify_with_unconditional_fact(a(_0))),
          clause(db <> 1, a(1), [], []),
          bs([], 2, [])
       ),
       o( success(unify_with_unconditional_fact(a(_0))),
          clause(db <> 2, a(2), [], []),
          bs([], 2, [])
       )
     ],
     a(_0),
     [ s(bs([], 2, [0 = 1])),
       s(bs([], 2, [0 = 2]))
     ],
     bs([], 2, [])
  ),
  fd( [ a( success(system_call(write(_0))),
           write(_0),
           [s(bs([], 2, [0 = 1])) | _1],
           bs([], 2, [0 = 1])
        ),
        fd( [ a( [ o( success(unify_with_unconditional_fact(b(_1))),
                      clause(db <> 1, b(3), [], []),
                      bs([], 2, [0 = 1])
                   ),
                   o( success(unify_with_unconditional_fact(b(_1))),
                      clause(db <> 2, b(4), [], []),
                      bs([], 2, [0 = 1])
                   )
                 ],
                 b(_1),
                 [ s(bs([], 2, [1 = 3, 0 = 1])),
                   s(bs([], 2, [1 = 4, 0 = 1]))
                 ],
                 bs([], 2, [0 = 1])
              ),
              fd( [ a( success(system_call(write(_0 + _1))),
                       write(_0 + _1),
                       [s(bs([], 2, [1 = 3, 0 = 1])) | _1],
                       bs([], 2, [1 = 3, 0 = 1])
                    ),
                    fd( [ a( fail(fail),
                             fail,
                             _1,
                             bs([], 2, [1 = 3, 0 = 1])
                          )
                        ]
                    )
                  ]
              ),
              fd( [ a( success(system_call(write(_0 + _1))),
                       write(_0 + _1),
                       [s(bs([], 2, [1 = 4, 0 = 1])) | _1],
                       bs([], 2, [1 = 4, 0 = 1])
                    ),
                    fd( [ a( fail(fail),
                             fail,
                             _1,
                             bs([], 2, [1 = 4, 0 = 1])
                          )
                        ]
                    )
                  ]
              )
            ]
        )
      ]
  ),
  fd( [ a( success(system_call(write(_0))),
           write(_0),
           [s(bs([], 2, [0 = 2])) | _1],
           bs([], 2, [0 = 2])
        ),
        fd( [ a( [ o( success(unify_with_unconditional_fact(b(_1))),
                      clause(db <> 1, b(3), [], []),
                      bs([], 2, [0 = 2])
                   ),
                   o( success(unify_with_unconditional_fact(b(_1))),
                      clause(db <> 2, b(4), [], []),
                      bs([], 2, [0 = 2])
                   )
                 ],
                 b(_1),
                 [ s(bs([], 2, [1 = 3, 0 = 2])),
                   s(bs([], 2, [1 = 4, 0 = 2]))
                 ],
                 bs([], 2, [0 = 2])
              ),
              fd( [ a( success(system_call(write(_0 + _1))),
                       write(_0 + _1),
                       [s(bs([], 2, [1 = 3, 0 = 2])) | _1],
                       bs([], 2, [1 = 3, 0 = 2])
                    ),
                    fd( [ a( fail(fail),
                             fail,
                             _1,
                             bs([], 2, [1 = 3, 0 = 2])
                          )
                        ]
                    )
                  ]
              ),
              fd( [ a( success(system_call(write(_0 + _1))),
                       write(_0 + _1),
                       [s(bs([], 2, [1 = 4, 0 = 2])) | _1],
                       bs([], 2, [1 = 4, 0 = 2])
                    ),
                    fd( [ a( fail(fail),
                             fail,
                             _1,
                             bs([], 2, [1 = 4, 0 = 2])
                          )
                        ]
                    )
                  ]
              )
            ]
        )
      ]
  )
]
 
 
Prolog representation of and-or-trees.
--------------------------------------
 
 
An and-list for Goal is:
        [ a decorated_and_node | a list of fd's ]
 
An fd is:
        a list of elements, each being
            fd(and-list)
 
A decorated-and-node for Goal is:
        a( AndNode, Goal, SF, Bindings )
        where
            SF is a list of elements of the form s(NewBindings).
            Each element gives the bindings in force after Goal
            succeeded. There is a list because execution may
            have moved forward through Goal more than once (see
            remark about "ghosts" earlier).
            Bindings are those in force before it was called.
 
An and-node for Goal is:
        success(true)                           { for Goal=true }
        fail(fail)                              { for Goal=fail }
        success(!)                              { for Goal=! }        
        success(system_call(Goal))              { if Goal is a system call }
        fail(untraceable_system_call(Goal))     { if Goal is an untraceable system call
                                                  (>1 solution) }
        success(forced_by_user)                 { If Goal represents a call of the
                                                  TLI which succeeded (user replied 'no')}
        fail(forced_by_user)                    { If Goal represents a call of the
                                                  TLI which failed (user replied 'yes')}
        not(AN)                                 { for not(G), where AN
                                                  is the and-node for G }
        fail(looping_goal(Goal))                { if Goal has an infinite loop }
        fail(clause_error(Goal))                { if there is a textbase/database
                                                  mismatch in Goal's clauses }
        fail(no_clauses(Goal))                  { if Goal has no clauses }
        an or_list
 
An or-list for Goal is:
        fail(no_more_clauses(Goal))             { if there are no more clauses
                                                  for Goal }
        a list of decorated-or-nodes
 
A decorated-or-node for Goal is:
        o( OrNode, Goal, Binding )
 
An or-node for Goal is:
        success(unify_with_unconditional_fact(Goal))    { if head-unification with an
                                                          unconditional fact
                                                          succeeds }
        fail(unify_with_unconditional_fact(Goal))       { if it fails }
        fail(unify_with_conditional_fact(Goal))         { if head-unification with
                                                          a conditional fact
                                                          fails }
        an and-list                                     { if it succeeds }
 
 
A binding-set (usually named as Bindings, etc.) is:
        bs( Varnames, MaxV, Substs )
        where
            Varnames is the original variable-name list (should be
            the same in all binding-sets for a given top-level goal);
            Substs is a substitution-list;
            MaxV can be ignored.
 
 
In terms being traced, we represent variables as terms of the form
'$VAR'(N), and not as Prolog variables. This is done by calling
numbervars. To distinguish this representation of variables from
ordinary Prolog variables, I'll call them mc-variables ("meta-constant
variables", meaning "mc-level variables represented as meta-level
constants"). This leads us to the structure of substitution-lists:
 
 
A substitution list is
        a list of elements of the form
            N = Term
        indicating that mc-variable '$VAR'(N) is bound to Term.
*/
 
 
/*
IMPLEMENTATION
--------------
 
 
Generating and-or trees - using transformations.
------------------------------------------------
 
In "The Logic Programming Tutor", I said that I wrote the generator by
performing program transformations. I started from a program which
generates all the and-or tree branches for a goal's execution. (What the
TPM book calls the "code space"). Neglecting details of unification,
variables, etc, this program ("code-space generator") looks like this:
 
    and_list( [Goal1|GoalsN], [Node1|NodesN] ) :-
        and_list( Goal1, Node1 ),
        and_list( GoalsN, NodesN ).
 
    and_list( [], [] ).
 
 
    and_node( true, true ).
 
    and_node( fail, fail ).
 
    and_node( Goal, Node ) :-
        clause_list_for( Goal, Clauses ),
        or_list( Goal, Clauses ).
 
 
    or_list( [Clause1|ClausesN], [Node1|NodesN] ) :-
        or_list( Clause1, Node1 ),
        or_list( ClausesN, NodesN ).
 
    or_list( [], [] ).
 
 
    or_node( Clause, Node ) :-
        tail_for( Clause, Tail ),
        and_list( Tail, Node ).
 
This generates _all_ branches, even those which would not normally be
generated by Prolog. It also generates them in an order which is
different from that in which their tips are actually executed, as can be
seen from the fact that in the query
    p(X), q(Y)
given clauses
    p(1). p(2).
    q(3). q(4).
it will generate the node for p(2) before that for q(3).
 
My next step was to transform the program so as to delay the execution
of some branches, and alter the order in which others were generated. I
did this by returning terms which represent the goals to be called if
the delayed branches are ever needed:
 
    or_list( [Clause1|ClausesN], Delayed, SF, [Node1|NodesN] ) :-
        or_list( Clause1, Node1 ),
        (
            SF = failure
        ->
            or_list( ClausesN, NodesN ),
            Delayed = true
        ;
            Delayed = or_list( ClausesN, NodesN ).
            %  Clause1 succeeded, so we don't call or_list
            %  on ClausesN. Instead we return a term representing
            %  that call, which we may one day actually execute.
        ).
 
This enables one to alter execution order while keeping the same basic
structure. (There is also a nice explanation of the way that the
variables such as NodesN are left uninstiantiated, but may become
instantiated later.) If done correctly, it will preserve correctness.
 
Unfortunately the program I derived turned out to be incorrect: I
hadn't been formal enough about applying the transformations, and had to
rely on some informal steps. I can't see how to do it formally, and
would welcome advice.
 
 
Generating and-or trees: the CSG/CP model.
------------------------------------------
 
The generator presented here therefore relies partly on knowledge of how
Prolog "ought" to be interpreted, i.e. the current-stack-of-goals and
choice-points model presented in the TPM book referred to above. If
anyone knows how to derive this rigorously by transformations, I'd like
to know how, as I said above.
 
I would also welcome advice on how to read this code declaratively.
The presence of uninstantiated variables in the trees makes this
difficult.
 
At any point in the program, there is a current stack of goals (CSG),
representing the goals left to be executed. There is also a stack of
choice-points (CP), representing the choice points. Each choice-point
includes a pointer to a clause to be executed, and a CSG of its own.
 
In terms of denotational semantics, the CSG holds the success
continuation, and the CP holds the failure continuation.
 
CSG and CP are represented as follows:                
 
A CSG is:
    a list of delayed-and-lists.
 
A delayed-and-list is:
    and_list( Goal1, GoalsN, Ancs, Bindings, WE, DANsN )
    where
        Goal1 is the goal just executed (used for diagnostics only);
        GoalsN are the goals to be executed;
        Ancs is a list of ancestors of these goals;
        Bindings is the bindings in force just after Goal1;
        WE is a "write-environment", specifying how output is to be
        done if control reaches these goals;
        DANsN is a list of decorated-and-nodes, to represent the
        and-list formed by obeying GoalsN.
 
A CP is:
    a list of delayed-or-lists.
 
A delayed-or-list is:
    or_list( Clause1, ClausesN, Ancs, Bindings, CSG, WE, DONsN )
    where
        Clause1 is the clause last used (used for diagnostics only);
        ClausesN are the clauses remaining;
        Ancs is the ancestors of these clauses; its first element is
        the goal which the clauses belong to;
        Bindings is the bindings in force before the clauses are tried;
        CSG is the current stack of goals in force at this point;
        WE is a write-environment;
        DONsN is a list of decorated-or-nodes, to represent the
        or-list formed by using ClausesN.
 
If you take all the GoalsN in a CSG (i.e. append them all together),
it forms all the outstanding goals. The reason I have represented the
CSG as a list of delayed-and-nodes is that retains the link with with
the code-space generator program. The same applies to the CP.
 
To justify the generator to yourself, if unfamiliar with the CSG/CP
model, read the tutorial chapter in the TPM book.
 
Incidentally, you can implement a range of exotic control structures
given access to these continuations. For example, the catch/throw
pair found in some LISPs.
 
 
How variables are represented.
------------------------------
 
As mentioned above, before tracing, we apply numbervars to all our
goals, replacing variables by terms '$VAR'(N). We do the same with all
clauses we use during proving. This means we can handle all our
variables as constants, which makes the unification algorithm
straightforward. I actually took this idea from David Bowen's and-or tree
program (in the public domain DEC-10 library).
 
A variable binding is represented by terms
    N = Value
where Value can be any term. It may of course contain variables. In
particular, it may be a variable. In this case, it will be represented
as '$VAR'(M) and not just M (obviously, otherwise it would look like an
integer). In other words, the '$VAR'(...) is only omitted on the
left-hand side of the =.
 
A set of bindings is, as mentioned above, represented as
    bs( Varnames, MaxV, Substs )
where Substs is a list of N=Value. MaxV is the greatest N in Substs. It
is needed so that future calls of numbervars know what number to
start at.
 
 
Terminology about variables and terms.
--------------------------------------
 
An mc-variable is
    '$VAR'(N)
As mentioned above, I use "mc-variable" to mean "variable represented
as meta-constant".
 
An n-variable is
    N, i.e. just the integer.
    These occur in substitution lists.
 
A Prolog-variable is
    A variable represented as itself, i.e. a Prolog variable!
 
An mc-term is
    a term in which all variables are represented by subterms of the
    form '$VAR'(N), where N is a non-negative integer. I.e. a term
    in which all variables are represented as mc-variables.
 
A Prolog-term is
    a term in which all variables are represented by Prolog variables,
    i.e. the usual representation. These are needed when doing system
    calls: we have to convert mc-terms back into Prolog terms.
 
 
Miscellaneous data structures.
------------------------------
 
A write-environment or we is
    we( trace, Level, Where )
    we( no_trace, Level, Where )
    where
        Level is a non-negative integer specifying indentation.
        Where is 'screen' or something else.
 
We's are passed around in delayed-or-lists and delayed-and-lists so that
the indentation can be reset to that in force last time the clause
or goal was used. 'trace' is set by why_goals and trace_goals.
 
 
An ancestors-list is
    a list of goals, with the newest at the front. The final element
    is 'TOP', standing for the top-level interpreter. The list
    therefore contains all the and-nodes on the currently-explored
    path through the and-or tree.
 
 
A clause-list is
        a list of elements of the form
            clause(Number,Head,TailList,Varnames)
        where Number is either the clause's number (for clauses taken
        from the textbase), or db<>(its relative position) (for clauses
        taken from the database);
        Head is its head;
        TailList is its tail as a list of goals;
        Varnames is its variable names, in the format used by the editor.
 
 
Note that conjunctions of goals are represented as lists.
 
 
Note that CSGs and CPs can also contain other terms. These do not
affect the progress of tracing, but generate diagnostics or pass back
information:
     sc( Clause1, WE ) (in CSG)
        Report Clause's success in WE.
 
    call( Goal ) (in CSG and CP)
        Call Goal. This is used to pass back success/fail information
        to why_goals and not.
 
    set(SF) (in CSG)
        Used to append an s(...) element to the SF part of a
        decorated-and-node.
 
    fc( Goal, Bindings, WE ) (in CP)
        Report Goal's failure in WE. Use Bindings when writing out Goal.
 
    cut( AfterClause, Goal, Bindings, WE, DONsN ) (in CP)
        Report that the clauses after AfterClause were cut.
 
 
The top-level interpreter.
--------------------------
 
If the whole of a user's query succeeds, we want to call a TLI and
ask whether another solution is wanted (Prolog mode), or to force
a failure (Logic mode). We arrange for this by appending the special
goal
    $tli(Varnames)
to the user's query, so that it's called on success. This forces a
call to a simulated top-level interpreter.
 
 
Variable names.
---------------
 
When writing out goals and variables, we replace variables by their
names if these were given to the top-level goal. To get these names out
without quotes, while quoting atoms when needed, we have to use a
non-portable trick: see the comments in SHOW.PL.
 
Variables that come from clauses are not given their original names,
because of the risk of clashes. We could use some kind of subscripting
scheme, but I just write them out as _N for '$VAR'(N). This relies
on the fact that Poplog displays '$VAR'(N) as _N. If your Prolog
doesn't, you'll have to change things slightly.
*/
 
 
:- needs
    append / 3,
    ask_yn / 2,
    assertion / 2,
    assertion / 3,
    bug / 1,
    bug / 2,
    findall / 3,
    for_in_list / 3,
    is_mode / 1,
    length / 2,
    member / 2,
    non_binding_call / 1,
/*     numbervars / 3,  - built in to Poplog */
    output / 1,
    question_vs_goal_and_vars / 3,
    show_question / 3.
 
 
/*
Top-level predicates.
---------------------                
*/
 
 
trace_goals( Goals, Varnames, Where ) :-
    append( Goals, [ '$tli'(Varnames) ], GoalsAndTLI ),
    numbervars( Goals, 0, MaxV ),
    and_list( GoalsAndTLI, ['TOP'], bs(Varnames,MaxV,[]),
              [], [],
              we(trace,0,Where),
              AndList
            ).
 
 
why_goals( Goals, Varnames, AndList, SF, Where ) :-
    numbervars( Goals, 0, MaxV ),
    and_list( Goals, ['TOP'], bs(Varnames,MaxV,[]),
              [call(SF=s)], [call(SF=f)],
              we(no_trace,0,Where),
              AndList
            ),
    ( var(SF) -> SF = a ; true ).
    /*  The two call's set SF on success or failure. If still unset
        on exit, we assume execution aborted.
    */                    
 
 
/*
And-or-tree generator and interpreter.
--------------------------------------
 
In these predicates, Bindings is always the bindings in force before
the goals are called. New bindings are passed on by 'success'.   
*/
 
 
/*  and_list( Goals+, Ancestors+, Bindings+,
              CSG+, CP+,
              WE+,
              AndList-
            ):
        AndList is the and-list for Goals.
        First element of Ancestors is the current goal, i.e. that
        one of whose clauses has a tail which is Goals.                 
*/
and_list( [], _, Bindings,
          CSG, CP,
          _,
          []
        ) :-
    success( CSG, CP, Bindings ).
 
and_list( [Goal1|GoalsN], Ancs, Bindings,
          CSG, CP,
          WE,
          [a(AN1,Goal1,SF1,Bindings)|DANsN]
        ) :-
    report_call( Goal1, Bindings, WE ),
    indent( WE, WE_I ),
    and_node( Goal1, [Goal1|Ancs], Bindings,
              [set(SF1),and_list(Goal1,GoalsN,Ancs,Bindings,WE,DANsN)|CSG],
              [fc(Goal1,Bindings,WE)|CP],
              WE_I,
              AN1
            ).
 
 
/*  and_node( Goal+, Ancestors+, Bindings+,
              CSG+, CP+,
              WE+,
              AndNode-
            ):
        AndNode is the and-node (undecorated) for Goal.
        First element of Ancestors is Goal.
*/
and_node( true, _, Bindings,
          CSG, CP,
          WE,
          success(true)
        ) :-
    !,
    success( CSG, CP, Bindings ).
 
and_node( fail, _, Bindings,
          CSG, CP,
          WE,
          fail(fail)
        ) :-
    failure( CP ).
 
and_node( !, Ancs, Bindings,
          CSG, CP0,
          WE,
          success(!)
        ) :-
    cut( CP0, Ancs, CP ),
    /*  Cut choice-points out of CP0 and then continue,
        using the result as the failure continuation.
    */                    
    success( CSG, CP, Bindings ).
 
and_node( '$tli'(Varnames), _, Bindings,
          CSG, CP,
          WE,
          AN
        ) :-
    !,
    is_mode( Mode ),
    and_or_tli( Mode, Varnames, Bindings, CSG, CP, WE, AN ).
 
and_node( SystemCall, Ancs, Bindings,
          CSG, CP,
          WE,
          AN
        ) :-
    system_pred_class( SystemCall, _, _ ),
    !,
    system_call( SystemCall, Ancs, Bindings,
                 CSG, CP,
                 WE,
                 AN
               ).
 
and_node( call(G), Ancs, Bindings,
          CSG, CP,
          WE,
          AN
        ) :-
    !,
    and_node( G, Ancs, Bindings,
              CSG, CP,
              WE,
              AN
            ).
 
and_node( not(G), Ancs, Bindings,
          CSG, CP,
          WE,
          not(AN)
        ) :-
    !,
    and_node( G, [G|Ancs], Bindings,
              [call(SF=s)], [call(SF=f)],
              WE,
              AN
            ),
    (
        SF = f
    ->
        success( CSG, CP, Bindings )
    ;
        failure( CP )
    ).
/*  Here, we call the goal with no success or failure continuations,
    using call() to pass back information on its success or failure.
*/                    
 
and_node( G, Ancs, Bindings,
          CSG, CP,
          WE,
          fail(looping_goal(G))
        ) :-
    no_progress( G, Ancs, Bindings,
                 CSG, CP,
                 WE
               ),
    !.
 
and_node( G, Ancs, bs(Varnames,MaxV,Substs),
          CSG, CP,
          WE,
          N
        ) :-
    clauses_for( WE, G, Clauses ),
    (
        Clauses = error
    ->
        /*  Textbase/database mismatch.  */
        output(  pretty_goal_(G,bs(Varnames,MaxV,Substs))...
                 'has erroneous clauses'~
              ),
        output( 'Tracing aborted'~ ),
        N = fail(clause_error(G))
    ;
        Clauses = []
    ->
        and_or_say( WE, 'There are no clauses for'...pred_(G)~ ),
        N = fail(no_clauses(G)),
        failure( CP )
    ;
        numbervars( Clauses, MaxV, MaxV_ ),
        length( Clauses, HowMany ),
        and_or_say( WE, 'There'...is_are_(HowMany)...count_(HowMany)...
                    number_(s,clause,HowMany)...'for'...pred_(G)~
                  ),
        or_list( Clauses, Ancs, bs(Varnames,MaxV_,Substs),
                 CSG, CP,
                 WE,
                 N
                )
    ).
 
 
/*  or_list( Clauses, Ancestors+, Bindings+,
             CSG+, CP+,
             WE+,
             OrList-
           ):
        OrList is the or-list for Clauses.
        First element of Ancestors is the current goal,
        i.e. the one whose clauses are Clauses.                
*/
or_list( [], [Anc1|_], _,
         CSG, CP,
         WE,
         []
       ) :-
    !,
    and_or_say( WE, 'There are no more clauses for'...pred_(Anc1)~ ),
    failure( CP ).
 
or_list( [Clause1|ClausesN], Ancs, Bindings,
         CSG, CP,
         WE,
         [o(ON1,Clause1,Bindings)|DONsN]
       ) :-
    and_or_say( WE, 'Trying clause'...Clause1~ ),
    or_node( Clause1, Ancs, Bindings,
             [sc(Clause1,WE)|CSG], [or_list( Clause1, ClausesN, Ancs, Bindings, CSG, WE, DONsN )|CP],
             WE,
             ON1
    ).
 
 
/*  or_node( Clause+, Ancestors+, Bindings+,
             CSG+, CP+,
             WE+,
             OrNode-
           ):
        OrNode is the (undecorated) or-node for Clause.
        First element of Ancestors is the current
        goal, i.e. that one of whose clauses is Clause.
 
        NOTE that we completely ignore the variable names belonging
        to this clause, and let them be written out as _numbers. A
        better system would be to use them, but with subscripts
        to distinguish from other variables of the same name.
*/
or_node( clause(Number,H,[],_), [Anc1|_], Bindings,
         CSG, CP,
         WE,
         N
       ) :-
    !,
    assertion( Bindings = bs(Varnames,MaxV,Substs), 'or_node: Bindings' ),
    (
        unify_mc_terms( H, Anc1, Substs, NewSubsts )
    ->
        N = success(unify_with_unconditional_fact(Anc1)),
        success( CSG, CP, bs(Varnames,MaxV,NewSubsts) )
    ;
        N = fail(unify_with_unconditional_fact(Anc1)),
        failure( CP )
    ).
 
or_node( clause(Number,H,T,_), [Anc1|AncsN], Bindings,
         CSG, CP,
         WE,
         N
       ) :-
    !,
    assertion( Bindings = bs(Varnames,MaxV,Substs), 'or_node: Bindings' ),
    (
        unify_mc_terms( H, Anc1, Substs, NewSubsts )
    ->
        and_list( T, [Anc1|AncsN], bs(Varnames,MaxV,NewSubsts),
                  CSG, CP,
                  WE,
                  N
                )
    ;
        N = fail(unify_with_conditional_fact(Anc1)),
        failure( CP )
    ).
 
 
/*
Success and failure.
--------------------
 
These pick the appropriate delayed element off the CSG or CP, and start
executing it.
 
As mentioned under "Miscellaneous data structures", the CSG and CP are
augmented with other elements that provide diagnostics.
 
 
Use of open lists.
------------------
 
To maintain fd-lists and the s-lists in the SF part of a
decorated-and-node, I have to represent these as open lists, i.e. whose
tail is uninstantiated. I append to them using append_to_open. I am
not particularly proud of this trick, as I can't see what it means
declaratively. Anyone got any ideas, or can suggest how to do it more
cleanly?
*/
 
 
/*  success( CSG+, CP+, Bindings_+ ):
        Continue to the next goal on CSG. Bindings_ are those
        in force after the previous goal succeeded; those in force
        before it was called are in the top element of CSG.
        CP is the choice points currently in force.                     
*/
success( [], _, _ ) :- !.
 
success( [and_list(Goal1,GoalsN,Ancs,Bindings,WE,Open)|CSG], CP, Bindings_ ) :-
    !,
    report_exit( Goal1, Bindings, Bindings_, WE ),
    append_to_open( Open, fd(DANsN) ),
    and_list( GoalsN, Ancs, Bindings_, CSG, CP, WE, DANsN ).
 
success( [sc(Clause1,WE)|CSG], CP, Bindings_ ) :-
    !,
    and_or_say( WE, 'Clause'...Clause1...'succeeded'~ ),
    success( CSG, CP, Bindings_ ).
 
success( [call(Goal)|CSG], CP, Bindings_ ) :-
    !,
    assertion( Goal, 'success: goal failed' ),
    success( CSG, CP, Bindings_ ).
 
success( [set(SF)|CSG], CP, Bindings_ ) :-
    append_to_open( SF, s(Bindings_) ),
    success( CSG, CP, Bindings_ ).
 
 
/*  failure( CP+ ):
        Obey the next choice point on CP: return if none.
*/
failure( [] ) :- !.
 
failure( [or_list(Clause1,ClausesN,Ancs,Bindings,CSG,WE,DONsN)|CP] ) :-
    !,
    and_or_say( WE, 'Clause'...Clause1...'failed'~ ),
    assertion( Ancs = [Goal|_], 'failure: no ancestors' ),
    edent( WE, WEE ),
    report_redo( Goal, Bindings, WEE ),
    or_list( ClausesN, Ancs, Bindings, CSG, CP, WE, DONsN ).
 
failure( [fc(Goal1,Bindings,WE)|CP] ) :-
    !,
    report_fail( Goal1, Bindings, WE ),
    failure( CP ).
 
failure( [cut(AfterClause,Goal,Bindings,WE,DONsN)|CP] ) :-
    !,
    report_cut(AfterClause,Goal,Bindings,WE),
    DONsN = cut(AfterClause,Goal),
    failure( CP ).
 
failure( [call(Goal)|CP] ) :-
    Goal,
    failure( CP ).
 
 
/*
Cut.
----
 
We use the list of ancestors to tell us how far down the cut was
called from. Because the choice points also contain information
about their ancestors, we can compare the two, and cut appropriately.
(If you wanted, you could implement other kinds of cut this way, e.g.
cut back to a specified goal).
*/
 
/*  cut( CP0+, Ancs+, CP- ):
        CP is the CP resulting from cutting out of CP0, all those
        choice points affected by a cut whose ancestors were
        the tail of Ancs. (Anc's first element is the cut itself).
 
        When cutting, we must not remove call(), fc() and other
        annotations, since this will affect diagnostics and returned
        results.
*/
cut( [X|CP0], Ancs, [X|CP] ) :-
    functor( X, F, _ ),
    F \= or_list,
    !,
    /*  X is some kind of annotation: ignore it.  */
    cut( CP0, Ancs, CP ).
 
cut( [CP|Rest], Ancs, [CP_|Rest_] ) :-
    !,
    cut_one( CP, Ancs, CP_ ),
    cut( Rest, Ancs, Rest_ ).
 
cut( [], _, [] ).
 
 
cut_one( or_list( Clause1, ClausesN, ClauseAncs, Bindings, CSG, WE, DONsN ),
         [!|CutsAncs],
         cut(Clause1,Goal,Bindings,WE,DONsN)
       ) :-
    ends_in( ClauseAncs, CutsAncs ),
    ClauseAncs = [Goal|_],
    !.
 
cut_one( CP, _, CP ).
 
 
/*  ends_in( List+, Sub+ ):
        Sub is a suffix of List, where Sub and List are both
        lists of ancestors.   
*/
ends_in( ['TOP'], ['TOP'] ) :- !.
 
ends_in( [H|T], [H|T1] ) :-
    ends_in( T, T1 ).
 
ends_in( [_|T], T1 ) :-
    ends_in( T, T1 ).
 
 
/*
System calls.
-------------
 
I can only work out how to trace system predicates which are not
resatisfiable, since I can't see how to preserve the alternative's for
others. Hence I have to abort those.
 
To trace a predicate call, we convert its mc-variables back into Prolog
variables, and call it. This call may have generated some new bindings
for those Prolog variables. We have to convert these back into the mc
representation, and add the result to Bindings. Still-unbound variables
have to be converted back to their mc-equivalents. The call may even
have created some new variables. These must be replaced by new
mc-variables.
 
Put like this, it sounds trivial. But I didn't get it right first time.                   
*/
 
 
/*  system_call( Goal+, Ancs+, Bindings+,
                 CSG+, CP+,
                 WE+,
                 AN-
               ):
        Goal is a system call. If I know how to trace it, do so,
        succeed or fail appropriately, and set AN. Otherwise, abort.
*/
system_call( SystemCall, _, Bindings,
             CSG, CP,
             WE,
             AN
           ) :-
    system_pred_class( SystemCall, 1, _ ),
    /*  If it has only one solution...  */
    !,
    and_or_say( WE, 'Trying a system predicate'~ ),
    assertion( Bindings = bs(Varnames,MaxV0,Substs0), 'and_node: bindings' ),
    mc_term_to_prolog_term( SystemCall, Substs0, SystemCallInProlog, Mc_vs_Prolog ),
    (
        call( SystemCallInProlog )
    ->
        prolog_term_to_mc_term( SystemCallInProlog, Substs0, MaxV0, Mc_vs_Prolog, Substs, MaxV ),
        AN = success(system_call(SystemCallInProlog)),
        success( CSG, CP, bs(Varnames,MaxV,Substs) )
    ;
        AN = fail(system_call(SystemCallInProlog)),
        failure( CP )
    ).
 
system_call( SystemCall, _, Bindings,
             CSG, CP,
             WE,
             fail(untraceable_system_call(SystemCall))
           ) :-
    system_pred_class( SystemCall, _, _ ),
    !,
    output( 'Can\'t trace the built-in predicate'...pred_(SystemCall)~ ),
    output( 'Tracing aborted'~ ).
 
 
/*  mc_term_to_prolog_term( McTerm+, Substs+, PrologTerm-, Mc_vs_Prolog- ):
        Convert mc-term McTerm to PrologTerm, replacing all the
        mc-variables by Prolog ones. Substs gives the variable
        values, which must be inserted in place of any mc-variable
        that has a value.
 
        Mc_vs_Prolog is a list of elements
            N=Var
        where N is an n-variable (the number of an mc-variable), and
        Var is a new uninstantiated variable which takes the
        place of '$VAR'(N) in PrologTerm.
*/
mc_term_to_prolog_term( McTerm, Substs, PrologTerm, Mc_vs_Prolog ) :-
    mc_term_to_prolog_term( McTerm, Substs, PrologTerm, [], Mc_vs_Prolog ).
 
 
mc_term_to_prolog_term( A, _, A, Mc_vs_Prolog, Mc_vs_Prolog ) :-
    atomic(A),
    !.
 
mc_term_to_prolog_term( V, _, _, _, _ ) :-
    var(V),
    !,
    bug( 'mc_term_to_prolog_term: real variable found in goal!' ).
 
mc_term_to_prolog_term( '$VAR'(N), Substs, Value, Mc_vs_Prolog0, Mc_vs_Prolog ) :-
    !,
    deref_mc_term_if_mc_var( '$VAR'(N), Substs, DerefedVar ),
    (
        DerefedVar = '$VAR'(M)
        /*  The mc-variable shares with another one.  */
    ->
        (
            member( M=Value, Mc_vs_Prolog0 )
        ->
            true
            /*  Value is the value already associated with the variable  */
        ;
            Mc_vs_Prolog = [ N=Value | Mc_vs_Prolog0 ]
            /*  Value left unbound, so it will be the new variable we need.  */
        )
    ;
        mc_term_to_prolog_term( DerefedVar, Substs, Value, Mc_vs_Prolog0, Mc_vs_Prolog )
    ).
 
mc_term_to_prolog_term( T, Substs, T_, Mc_vs_Prolog0, Mc_vs_Prolog ) :-
    T =.. [ P | A ],
    mc_term_to_prolog_term_1( A, Substs, A_, Mc_vs_Prolog0, Mc_vs_Prolog ),
    T_ =.. [ P | A_ ].
 
 
mc_term_to_prolog_term_1( [], _, [], Mc_vs_Prolog, Mc_vs_Prolog ) :- !.
 
mc_term_to_prolog_term_1( [H|T], Substs, [H_|T_], Mc_vs_Prolog0, Mc_vs_Prolog ) :-
    mc_term_to_prolog_term( H, Substs, H_, Mc_vs_Prolog0, Mc_vs_Prolog1 ),
    mc_term_to_prolog_term_1( T, Substs, T_, Mc_vs_Prolog1, Mc_vs_Prolog ).
 
 
/*  prolog_term_to_mc_term( PrologTerm+, Substs0+, MaxV0+, Mc_vs_Prolog-, Substs-, MaxV- ):
        This predicate converts PrologTerm to an mc-term.
 
        1) Prolog variables created by the system call (e.g. by a call
           to functor) are replaced by new mc-variables, and MaxV0 is
           incremented appropriately.
 
        2) Prolog variables that were created by mc_term_to_prolog_term
           (i.e. that are in Mc_vs_Prolog) and that have become bound
           are replaced by the corresponding mc-variables, and Substs0
           is updated to reflect the new binding. We do _not_ replace
           these variables by their value in PrologTerm, since this
           would create inconsistencies.
 
        3) Prolog variables that were created by mc_term_to_prolog_term
           (i.e. that are in Mc_vs_Prolog) and that have remained
           unbound are replaced by the corresponding mc-variables.
*/
prolog_term_to_mc_term( PrologTerm, Substs0, MaxV0, Mc_vs_Prolog, Substs, MaxV ) :-
    prolog_term_to_mc_term_1( PrologTerm, Substs0, Mc_vs_Prolog, Substs ),
    numbervars( PrologTerm, MaxV0, MaxV ).
 
 
/*  prolog_term_to_mc_term_1( PrologTerm+, Substs0+, Mc_vs_Prolog-, Substs- ):
        Mc_vs_Prolog is as described for mc_term_to_prolog_term.
        This predicate replaces each Prolog variable occurring in it
        that is still unbound with its corresponding mc-variable.
 
        If the Prolog variable has become bound, we have to add its
        binding to Substs0.
 
        Thus this predicate implements the relation:
            Substs is Substs0
                plus the bindings for those Prolog variables in
                Mc_vs_Prolog that have become bound
        and binds all the other Prolog variables in Mc_vs_Prolog
        to their mc-equivalents in Mc_vs_Prolog. It therefore
        reverses the translation of all variables that existed when
        PrologTerm was an mc-term.
 
        The call to numbervars in the previous predicate deals with
        the rest: new variables that were created by the system call.
        (Many calls wouldn't do this, but a call to, e.g. functor,
        could.)
*/
prolog_term_to_mc_term_1( PrologTerm, Substs, [], Substs ) :- !.
 
prolog_term_to_mc_term_1( PrologTerm, Substs0, [McTerm=PrologTerm|Rest], Substs ) :-
    nonvar( PrologTerm ),
    !,
    unify_mc_terms( '$VAR'(McTerm), PrologTerm, Substs0, Substs1 ),
    prolog_term_to_mc_term_1( PrologTerm, Substs1, Rest, Substs ).
 
prolog_term_to_mc_term_1( PrologTerm, Substs0, [McTerm=PrologTerm|Rest], Substs ) :-
    /*  var(PrologTerm)  */
    PrologTerm = '$VAR'(McTerm),
    prolog_term_to_mc_term_1( PrologTerm, Substs0, Rest, Substs ).
 
 
/*
Reporting at ports.
-------------------
 
Just some convenient output predicates for reporting various ways of
entering/leaving a goal.
 
We do not report the '$tli' goal, and we call and_or_say, which remains
silent if WE is no_trace.                    
*/
 
 
report_call( Goal, Bindings, WE ) :-
    not( functor( Goal, '$tli', _ ) ),
    !,
    and_or_say( WE, 'Calling goal'...pretty_goal_(Goal,Bindings)~ ).
 
report_call( _, _, _ ).
 
 
report_redo( Goal, Bindings, WE ) :-
    not( functor( Goal, '$tli', _ ) ),
    !,
    and_or_say( WE, 'Redoing goal'...pretty_goal_(Goal,Bindings)~ ).
 
report_redo( _, _, _ ).
 
 
report_exit( Goal, Bindings, Bindings_, WE ) :-
    not( functor( Goal, '$tli', _ ) ),
    !,
    and_or_say( WE, 'Goal'...pretty_goal_(Goal,Bindings)...'succeeded' ),
    and_or_say_substs( WE, Goal, Bindings, Bindings_ ),
    /*  Bindings is before the call; Bindings_ is afterwards.  */
    and_or_say( WE, nl_ ).
 
report_exit( _, _, _, _ ).
 
 
report_fail( Goal, Bindings, WE ) :-
    not( functor( Goal, '$tli', _ ) ),
    !,
    and_or_say( WE, 'Goal'...pretty_goal_(Goal,Bindings)...'failed'~ ).
 
report_fail( _, _, _ ).
 
 
report_cut( AfterClause, Goal, Bindings, WE ) :-
    and_or_say( WE, 'Clause(s) following'...AfterClause...'have been cut'~ ).
 
 
/*  and_or_say_substs( WE+, Goal+, BeforeBindings+, AfterBindings+ ):
        If Goal has made some new bindings, list them.
*/
and_or_say_substs( we(no_trace,_,_), Goal, _, _ ) :- !.
 
and_or_say_substs( WE, Goal, bs(Varnames,_,Substs0), bs(_,_,Substs1) ) :-
    new_bindings_from( Goal, Substs0, Substs1, NVs ),
    (
         NVs \= []
    ->
        output( ', and set ' ),  /*  To get indentation  */
        for_in_list( NV=Value,
                     NVs,
                     (
                        and_or_say_subst(NV,Value,Varnames)
                     )
                   )
    ;
        true
    ).
 
 
/*  and_or_say_subst( NVar+, Value+, Varnames+ ):
        NVar is an n-variable with value Value. Output its name
        and value.
*/
and_or_say_subst( NVar, Value, Varnames ) :-
    mc_var_to_name( '$VAR'(NVar), Varnames, Name ),
    output( Name...'='...write_(Value)...'' ).
 
 
/*  new_bindings_from( Goal+, Substs0+, Substs+, New- ):
        New contains bindings that are in Substs but not Substs0,
        and that refer to variables in Goal.
        We use it to write out only that subset of new bindings made
        by a particular goal.
*/
new_bindings_from( Goal, Substs0, Substs, NVs ) :-
    new_bindings_from( Goal, Substs0, Substs, [], NVs ).                 
 
 
new_bindings_from( X, _, _, Bindings, Bindings ) :-
    atomic( X ),
    !.
 
new_bindings_from( X, _, _, Bindings, Bindings ) :-
    var( X ),
    !,
    bug( 'new_bindings_from: real variable found in goal!' ).
 
new_bindings_from( '$VAR'(N), Substs, NewSubsts, Bindings, Bindings ) :-
    member( N=_, Bindings ),
    !.
    /*  Have already encountered this one.  */
 
new_bindings_from( '$VAR'(N), Substs, NewSubsts, Bindings, Bindings ) :-
    n_var_bound_in( N, Substs ),
    !.
    /*  Variable was already bound.  */
 
new_bindings_from( '$VAR'(N), Substs, NewSubsts, Bindings, [N=V|Bindings] ) :-
    n_var_bound_in( N, NewSubsts, V ),
    !.
    /*  Variable is bound in NewSubsts to V, but not
        in Substs
    */
 
new_bindings_from( '$VAR'(N), Substs, NewSubsts, Bindings, Bindings ) :-
    !.
    /*  Not bound in NewSubsts.  */
 
new_bindings_from( T, Substs, NewSubsts, Bindings0, Bindings ) :-
    T =.. [ _ | A ],
    new_bindings_from_l( A, Substs, NewSubsts, Bindings0, Bindings ).
 
 
new_bindings_from_l( [], _, _, Bindings, Bindings ) :- !.
 
new_bindings_from_l( [H|T], Substs, NewSubsts, Bindings0, Bindings ) :-
    new_bindings_from( H, Substs, NewSubsts, Bindings0, Bindings1 ),
    new_bindings_from_l( T, Substs, NewSubsts, Bindings1, Bindings ).
 
 
n_var_bound_in( N, Substs, V ) :-
    deref_n_var( N, Substs, Substs, V ),
    V \= '$VAR'(_),
    !.
 
 
n_var_bound_in( N, Substs ) :-
    n_var_bound_in( N, Substs, _ ).
 
 
/*
Output.
-------
*/
 
 
/*  and_or_say( WE+, X+ ):
        X is any outputtable term. If WE indicates tracing, then
        output X, otherwise do nothing.
 
        and_or_say is used to write messages that should appear
        if the tree-generator is doing a trace, but not if
        it is generating a tree for future analysis (as in the
        'why' command).
*/
and_or_say( we(no_trace,_,_), _ ) :- !.
 
and_or_say( we(trace,M,_), X ) :-
    tab(M), output(X).
 
 
/*  output_and_or( X+ ):
        This is a user-defined hook for outputting clauses and other things
        in particular formats. See OUTPUT.PL for how to define such hooks.
*/
:- add_user_output( output_and_or ).
 
 
output_and_or( clause(Number,Head,_,_) ) :-
    !,
    /*  Output a clause as its predicate and number.  */
    functor( Head, P, _ ),
    output( Number...for...P ).
 
output_and_or( pretty_goal_(Goal,bs(Varnames,_,Substs)) ) :-
    !,
    /*  Output a goal in the same format as a question.  */
    make_mc_term_writeable( Goal, Substs, Varnames, GoalWithVariables ),
    assertion( is_mode( Mode ), 'output_and_or: mode' ),
    question_vs_goal_and_vars( Q, GoalWithVariables, Varnames ),
    show_question( Q, Mode, [] ).
 
output_and_or( pred_(Goal) ) :-
    !,
    /*  Output the predicate of a goal in P/A format.  */
    functor( Goal, F, A ),
    output( F<>'/'<>A ).
 
output_and_or( count_(N) ) :-
    !,
    /*  Output N as 'one' for 1, else as the number.  */
    ( N = 1 -> output( one )
    ;          output( N )
    ).
 
 
/*  indent( WE+, WEI- ):
        WEI is a new write-environment, like WE but indented four
        places more.
*/
indent( we(Tracing,M,Where), we(Tracing,I,Where) ) :-
    I is M+4.
 
 
/*  edent( WE+, WEE- ):
        WEI is a new write-environment, like WE but indented four
        places less.
*/
edent( we(Tracing,M,Where), we(Tracing,I,Where) ) :-
    I is M-4.
 
 
/*
Unification.
------------
*/
 
 
/*  unify_mc_terms( T1+, T2+, Substs+, NewSubsts- ):
        NewSubsts is Substs, plus any new substitutions arising
        from unifying mc-terms T1 and T2 in environment Substs.
 
        Fails if T1 and T2 don't unify.
*/
unify_mc_terms( T1, T2, Substs, NewSubsts ) :-
    deref_mc_term_if_mc_var( T1, Substs, DT1 ),
    deref_mc_term_if_mc_var( T2, Substs, DT2 ),
    unify_canonical_mc_terms( DT1, DT2, Substs, NewSubsts ).
 
 
/*  unify_canonical_mc_terms( T1+, T2+, Substs+, NewSubsts- ):
        NewSubsts is Substs, plus any new substitutions arising
        from unifying mc-terms T1 and T2 in environment Substs.
        If T1 or T2 are mc-variables, then they are guaranteed
        unbound in Substs.
 
        Fails if T1 and T2 don't unify.
*/
unify_canonical_mc_terms( T, '$VAR'(N), Substs, [N=T|Substs] ) :- !.
 
unify_canonical_mc_terms( '$VAR'(N), T, Substs, [N=T|Substs] ) :- !.
 
unify_canonical_mc_terms( T1, T2, Substs, Substs ) :-
    ( atomic( T1 ) ; atomic( T2 ) ),
    !,
    T1 = T2.
    /*  You can omit this clause if your version of 'functor' accepts
        atomic terms (including numbers) as first argument.
    */
 
unify_canonical_mc_terms( T1, T2, Substs, NewSubsts ) :-
    functor( T1, F, N ),
    functor( T2, F, N ),
    unify_mc_terms( N, T1, T2, Substs, NewSubsts ).
 
 
unify_mc_terms( 0, T1, T2, Substs, Substs ) :- !.
 
unify_mc_terms( I, T1, T2, Substs, NewSubsts ) :-
    arg( I, T1, A1 ),
    arg( I, T2, A2 ),
    unify_mc_terms( A1, A2, Substs, MidSubsts ),
    J is I-1,
    unify_mc_terms( J, T1, T2, MidSubsts, NewSubsts ).
 
 
/*
Dereferencing variables.
------------------------
*/
 
 
/*  deref_mc_term_if_mc_var( McTerm+, Substs+, Value- ):
        If Oterm is an mc-variable, then dereference it as far
        as possible, ending up with either a value or an mc-
        variable which is not bound to anything else in Substs.
        Otherwise, Value = McTerm.
*/
deref_mc_term_if_mc_var( '$VAR'(N), Substs, Value ) :-
    !,
    deref_n_var( N, Substs, Substs, Value ).
 
deref_mc_term_if_mc_var( X, S, X ).
 
 
deref_n_var( N, [N=V1|Rest], Substs, V2 ) :-
    !,
    deref_mc_term_if_mc_var( V1, Substs, V2 ).
 
deref_n_var( N, [_|Rest], Substs, V ) :-
    !,
    deref_n_var( N, Rest, Substs, V ).
 
deref_n_var( N, [], _, '$VAR'(N) ).
 
 
/*
Variable names.
---------------
 
These predicates convert between the internal representation of
variables, and the names they have for the user.
*/
 
 
/*  mc_var_to_users_name( McVar+, Varnames+, Name? ):
        Name is the name of mc-variable McVar.
        Fails if McVar does not occur in Varnames.
*/
mc_var_to_users_name( McVar, Varnames, '$NOQUOTE'(Name) ) :-
    member( var(McVar,Name), Varnames ),
    !.
 
 
/*  mc_var_to_name( McVar+, Varnames+, Name? ):
        Name is the name of mc-variable McVar.
        If McVar does not occur in Varnames, uses the internal name.
        (In this version of Prolog, '$VAR'(N) is always written
        out as _N.)
*/
mc_var_to_name( McVar, Varnames, '$NOQUOTE'(Name) ) :-
    member( var(McVar,Name), Varnames ),
    !.
 
mc_var_to_name( McVar, Varnames, McVar ).
 
 
/*  make_mc_term_writeable( Goal+, Substs+, Varnames+, GoalWithVariables- ):
        GoalWithVariables is Goal where each bound mc-variable is
        replaced by its value. Unbound mc-variables are replaced
        by their names, if these are in Varnames, otherwise by
        something which causes variable N to be written out as _N.
*/
make_mc_term_writeable( A, _, _, A ) :-
    atomic(A),
    !.
 
make_mc_term_writeable( V, _, _, _ ) :-
    var(V),
    !,
    bug( 'make_mc_term_writeable: real variable found in goal!' ).
 
make_mc_term_writeable( '$VAR'(N), Substs, Varnames, X ) :-
    !,
    deref_mc_term_if_mc_var( '$VAR'(N), Substs, Value ),
    (
        Value = '$VAR'(M),
        mc_var_to_users_name( '$VAR'(M), Varnames, X )
    ->
        true
    ;
        X = Value
    ).
 
make_mc_term_writeable( T, Substs, Varnames, T_ ) :-
    T =.. [ P | A ],
    make_mc_term_writeable_l( A, Substs, Varnames, A_ ),
    T_ =.. [ P | A_ ].
 
 
make_mc_term_writeable_l( [], _, _ , [] ) :- !.
 
make_mc_term_writeable_l( [H|T], Substs, Varnames, [H_|T_] ) :-
    make_mc_term_writeable( H, Substs, Varnames, H_ ),
    make_mc_term_writeable_l( T, Substs, Varnames, T_ ).
 
 
/*
Top-level interpreters for use in tracing.
------------------------------------------
 
To make the tracer compatible with the Tutor's normal interface, it
must be able to imitate the top-level interpreters, and generate
extra solutions if required. We do this by arranging that when all
the user's original goals have succeeded, a special goal
    and_or_tli( Mode )
is called. This adapts its action depending on Mode.
 
If Mode=logic, it fails, forcing the tracer to find another solution.
This will repeat until all solutions have been found, as in the standard
Logic TLI.
 
If Mode=prolog, it asks the user whether he wants another solution, and
fails if he does.
 
In either mode, the TLI also writes out the bindings found for the
variables in Varnames. These will be just those named when the original
query was given.
 
The user interaction should be as similar as possible to those of the
Tutor's standard TLI's.
 
If the user is not writing to the screen, the TLI displays the bindings
on screen as well as on the printer, and directs its question to
the screen. Otherwise, the user would not see the More (y/n) prompt.
*/
 
 
/*  and_or_tli( Mode+, Varnames+, Bindings+, CSG+, CP+, WE+, AndNode- ):
*/
and_or_tli( prolog, Varnames, Bindings, CSG, CP, we(_,_,Where), AN ) :-
    !,
    assertion( Bindings=bs(_,_,Substs), 'and_node: Bindings' ),
    and_or_write_vars( Varnames, Substs ),
    (
        Where \= screen
    ->
        telling(COS), tell(user), and_or_write_vars( Varnames, Substs )
    ;
        true
    ),
    ask_yn( 'More (y/n)? ', YN ),
    (   Where \= screen
    ->
        tell(COS),
        output( 'More (y/n)?'...YN~ )
    ;
        true
    ),
    (
        YN = yes
    ->
        AN = fail(forced_by_user),
        failure( CP )
    ;
        AN = success(forced_by_user),
        success( CSG, CP, Bindings )
    ).
 
and_or_tli( logic, Varnames, Bindings, CSG, CP, we(_,_,Where), AN ) :-
    assertion( Bindings=bs(_,_,Substs), 'and_or_tli: Bindings' ),
    and_or_write_vars( Varnames, Substs ),
    (
        Where \= screen
    ->
        telling(COS), tell(user), and_or_write_vars( Varnames, Substs ),
        tell( COS )
    ;
        true
    ),
    AN = fail(forced_by_user),
    failure( CP ).
 
 
/*  and_or_write_vars( Varnames+, Substs+ ):
        For each variable whose name appears in Varnames, write
        its binding.
*/
and_or_write_vars( Varnames, Substs ) :-
    for_in_list( E, Varnames, and_or_write_var(E,Substs) ).
 
 
/*  and_or_write_var( Var+, Substs+ ):
        Write the binding for Var, as given by Substs.
*/
and_or_write_var( var(Var,Name), Substs ) :-
    deref_mc_term_if_mc_var( Var, Substs, Value ),
    output( Name...'='...write_(Value)~ ).
 
 
                      
/*
Interface to the editor.
------------------------
*/
 
 
/*  clauses_for( WE+, Goal+, Clauses- ):
        Unify Clauses with a list of clauses for Goal. Each element of
        the list is of the form
            clause( Number, Head, Tail, Varnames )
        where Tail has been converted to a list of goals, Varnames are the
        variable names, and Number is the number in the textbase.
 
        clauses_for checks the textbase against the database. If the
        textbase has _no_ clauses for Goal, it takes them from the database:
        they were probably loaded by "load". In this case, it gives the
        relative position in the database as the clause number.
 
        If there are some in both, but they mismatch, it says so and sets
        Clauses to 'error'.
*/
clauses_for( WE, Goal, Clauses ) :-
    functor( Goal, F, A ),
    functor( Head, F, A ),
    findall( clause(Number,Head,TailList,Varnames),
             ( editor_clause( Number, Head, Tail, Varnames ),
               conj_vs_list( Tail, TailList )
             ),
             TextbaseClauses
           ),
    findall( clause(_,Head,TailList,[]),
             ( clause( Head, Tail ),
               ( Tail \= (fail,'UNDEFINED-PREDICATE') ),
               conj_vs_list( Tail, TailList )
             ),
             DatabaseClauses
           ),
    check_db_tb_clauses( WE, TextbaseClauses, DatabaseClauses, Status ),
    (
        Status = database
    ->
        and_or_say( WE, 'There are no clauses in the textbase: I shall use those from the database'~ ),
        number_database_clauses( DatabaseClauses, Clauses )
    ;
        Status = textbase
    ->
        Clauses = TextbaseClauses
    ;
        Status = error
    ->
        Clauses = error
    ).
 
 
/*  check_db_tb_clauses( WE+, TextbaseClauses+, DatabaseClauses+, Status- ):
        TextbaseClauses and DatabaseClauses are the text- and data-base
        clauses for the same predicate. Check that there are the same
        number of each, and that the Nth textbase clause matches
        the Nth database clause. If not, then use of 'load' (or perhaps
        a bug in the Tutor), has introduced an error.
 
        If there are _no_ textbase clauses at all, we assume that the
        predicate was loaded and that there is no error.
 
        Status becomes one of:
            textbase - if there are the same number of clauses in both,
                       and they match.
            database - if there are database clauses only.
            error    - for anything else.
 
        The predicate gives an error message if there is a mismatch:
        WE controls the indentation of that message.
 
        ??? for why.
*/
check_db_tb_clauses( WE, [], [], textbase ) :- !.
 
check_db_tb_clauses( WE, [], _, database ) :- !.
 
check_db_tb_clauses( WE, TextbaseClauses, DatabaseClauses, Status ) :-
    check_db_tb_clauses_1( WE, TextbaseClauses, DatabaseClauses, Status ).
 
 
check_db_tb_clauses_1( WE, [], [], textbase ) :-
    !.
 
check_db_tb_clauses_1( WE, [], DatabaseClauses, error ) :-
    !,
    and_or_say( WE, 'There are fewer clauses in the textbase than in the database'~ ).
 
check_db_tb_clauses_1( WE, TextbaseClauses, [], error ) :-
    !,
    and_or_say( WE, 'There are fewer clauses in the database than in the textbase'~ ).
 
check_db_tb_clauses_1( WE, [clause(N,TBH,TBT,_)|TBCN], [clause(_,DBH,DBT,_)|DBCN], Status ) :-
    !,
    (
        non_binding_call( TBC1 = DBC1 )
    ->
        check_db_tb_clauses_1( WE, TBCN, DBCN, Status )
    ;
        and_or_say( WE, 'Clause mismatch: database clause'...(DBH:-DBT)...
                        'does not match textbase clause'...N...(TBH:-TBT)~
                  ),
        Status = error
    ).
 
 
/*  number_database_clauses( Clauses+, NumberedClauses- ):
        Clauses is a clause-list, but with the numbers left uninstantiated.
        This predicate instantiates each number to db<>N where N
        is the clause's relative position in the database.
*/
number_database_clauses( DBC, C ) :-
    number_database_clauses( 1, DBC, C ).
 
 
number_database_clauses( _, [], [] ) :- !.
 
number_database_clauses( N, [clause(_,H,T,V)|DBN], [clause(db<>N,H,T,V)|ClausesN] ) :-
    Next is N + 1,
    number_database_clauses( Next, DBN, ClausesN ).
 
 
/*
No-progress check for infinite loops.
-------------------------------------
*/
 
 
/*  no_progress( Goal+, Ancs+, Bindings+,
                 CSG+, CP+,
                 WE+
               ):
        True if the ancestors of Goal show that it is recalling
        itself without making any progress, i.e. without
        creating any new non-variable substitutions.
*/
no_progress( G, Ancs, Bindings,
             CSG, CP,
             WE
           ) :-
    Ancs = [ First | Rest ],
    assertion( First = G, 'no_progress: first element of Ancs not G', [Ancs,G] ),
    member( G0, Rest ),
    unify_mc_terms( G0, G, ['$BARRIER'|Substs], NewSubsts ),
    /* Include '$BARRIER' so that 'progress' knows where to stop.  */
    not( progress( NewSubsts, Substs ) ),
    !,
    output( pretty_goal_(G,bs(Varnames,MaxV,Substs))...
            'is in an infinite loop'~
          ),
    output( 'Tracing aborted'~ ).
 
 
/*  progress( NewSubsts+, Substs+ ):
        NewSubsts and Substs are subst-lists. Substs is those
        in force before a goal was called; NewSubsts is those in force
        afterwards.
 
        If NewSubsts contains no extra bindings (except possibly to
        unbound variables), then the goal that produced it is not
        making any progress, and can be deemed to be in an infinite
        loop.
*/
progress( [], Substs ) :-
    !, fail.
 
progress( [ '$BARRIER' ], Substs ) :-
    !, fail.
 
progress( [N=V|Rest], Substs ) :-
    deref_mc_term_if_mc_var( V, Substs, Value ),
    Value \= '$VAR'(_),
    progress( Rest, Substs ).
 
 
/*
Classifying system predicates.
------------------------------
 
This is non-portable! 
*/
 
 
/*  system_pred_class( Goal?, Resatisfiable?, LogicOrSideEffects? ):
        This predicate supplies details on the properties of system
        predicates.
 
        Goal is a goal, assumed to be a system call.
 
        Resatisfiable indicates whether Goal's system predicate can be
        resatisfied: '1' if not, 'finite' if it can be resatisfied with a
        finite number of solutions; 'infinite' if it has a potentially
        infinite set of solutions.
 
        LogicOrSideEffects is 'logic' for logical predicates,
        'side_effect' for others.
 
        This predicate does not classify
        true,fail,!,call,not,comma,semicolon: these are handled
        specially by the and-or-tree generator.
 
        We also classify add,adda,del. These are provided by the Tutor
        for the students' use, and to the students should look like
        system predicates, i.e. we don't trace inside them.
*/
system_pred_class( <(_,_),      1,        logic ).
system_pred_class( =(_,_),      1,        logic ).
system_pred_class( =..(_,_),    1,        logic ).
system_pred_class( =:=(_,_),    1,        logic ).
system_pred_class( =<(_,_),     1,        logic ).
system_pred_class( ==(_,_),     1,        logic ).
system_pred_class( =\=(_,_),    1,        logic ).
system_pred_class( >(_,_),      1,        logic ).
system_pred_class( >=(_,_),     1,        logic ).
system_pred_class( @<(_,_),     1,        logic ).
system_pred_class( @=<(_,_),    1,        logic ).
system_pred_class( @>(_,_),     1,        logic ).
system_pred_class( @>=(_,_),    1,        logic ).
system_pred_class( \=(_,_),     1,        logic ).
system_pred_class( \==(_,_),    1,        logic ).
system_pred_class( abort,       1,        side_effect ).
system_pred_class( arg(_, _, _),1,        logic ).
system_pred_class( assert(_),   1,        side_effect ).
system_pred_class( asserta(_),  1,        side_effect ).
system_pred_class( assertz(_),  1,        side_effect ).
system_pred_class( atom(_),     1,        logic ).
system_pred_class( atomic(_),   1,        logic ).
system_pred_class( break,       1,        side_effect ).
system_pred_class( clause(_, _),finite,   logic ).
system_pred_class( consult(_),  1,        side_effect ).
system_pred_class( display(_),  1,        side_effect ).
system_pred_class( functor(_, _, _),1,    logic ).
system_pred_class( get(_),      1,        side_effect ).
system_pred_class( get0(_),     1,        side_effect ).
system_pred_class( halt,        1,        side_effect ).
system_pred_class( is(_,_),     1,        logic ).
system_pred_class( listing(_),  1,        side_effect ).
system_pred_class( listing,     1,        side_effect ).
system_pred_class( name(_,_),   1,        logic ).
system_pred_class( nl,          1,        side_effect ).
system_pred_class( nonvar(_),   1,        logic ).
system_pred_class( nospy(_),    1,        side_effect ).
system_pred_class( nospy,       1,        side_effect ).
system_pred_class( numeric(_),  1,        logic ).
system_pred_class( op(_, _, _), 1,        logic ).
system_pred_class( phrase(_,_), 1,        logic ).
system_pred_class( print(_),    1,        side_effect ).
system_pred_class( put(_),      1,        side_effect ).
system_pred_class( read(_),     1,        side_effect ).
system_pred_class( read(_,_),   1,        side_effect ).
system_pred_class( real(_),     1,        logic ).
system_pred_class( reconsult(_),1,        side_effect ).
system_pred_class( repeat,      infinite, logic ).
system_pred_class( retract(_),  finite,   side_effect ).
system_pred_class( retractall(_),1,       side_effect ).
system_pred_class( see(_),      1,        side_effect ).
system_pred_class( seeing(_),   1,        logic ).
system_pred_class( seen,        1,        side_effect ).
system_pred_class( skip(_),     1,        side_effect ).
system_pred_class( spy(_),      1,        side_effect ).
system_pred_class( spy,         1,        side_effect ).
system_pred_class( tab(_),      1,        side_effect ).
system_pred_class( tell(_),     1,        side_effect ).
system_pred_class( telling(_),  1,        logic ).
system_pred_class( told,        1,        side_effect ).
system_pred_class( var(_),      1,        logic ).
system_pred_class( write(_),    1,        side_effect ).
system_pred_class( writeq(_),   1,        side_effect ).
 
system_pred_class( adda(_),     1,        side_effect ).
system_pred_class( add(_),      1,        side_effect ).
system_pred_class( del(_),      finite,   side_effect ).
 
 
/*
Utilities.
----------
*/
 
 
/*  append_to_open( Open, Element+ ):
        Append Element to open-list Open, forming a new uninstantiated
        variables as Open's new tail.              
*/
append_to_open( Var, Elt ) :-
    var( Var ),
    !,
    Var = [ Elt | _ ].
 
append_to_open( [_|T], Elt ) :-
    append_to_open( T, Elt ).
