% File : andor_debug
% Author : Dave Bowen (documented by Paul Wilk)
% Updated: 27 February 1984
% Purpose: Meta-circular interpreter maintaining extended AND/OR tree
% Needs : findall/3 from UTIL:SETOF.PL.
/* MAIN DATA STRUCTURES
A1 =:= A term instantiated to the current argument
of the current goal being unified.
A2 =:= A term instantiated to the current argument
of the current choice being unified.
F =:= The name of the principal functor of the
current goal or current procedure.
N =:= The arity of the current goal.
T1 =:= A term instantiated to current goal
being unified.
T2 =:= A term instantiated to the current choice
being unified.
[AndNodes] =:= This is a list of "and" goals for the parent
goal. When AndNodes instantiates to a list, the
current goal can then be thought of as the
parent goal.
[AndNode] =:= This is a list of one "and" goal and is used
to catch a parent goal with only one goal in
its Body.
[And | RestA] =:= When the parent goal has more than one goal
in the Body, And instantiates to the first
goal in the Body and RestA to to the tail.
And will be used to construct an "or" node
and RestA will be saved in
Choice =:= Choice instantiates to the head of the
list of or_goals.
RestC =:= RestC instantiates to the
tail of the list of or_goals; the choicepoints..
[Clauses] =:= The unordered set of all instances of the
goal-term (Head:-Body); a list.
Cont =:= Cont instantiates to the continuation list
of the parent goal for the current goal.
Note that this is a list the head of which
is the term cont/3 the tail is the rest of
the continuation list.
% [bp(RestC,RestA,Goal,Substs,Cont,ParentFail)|Fail]
Fail =:= Holds a list of records, where each record
contains backtrack information relating to a
current goal, i.e. [bp/9 | Fail]. Each record
bp(RestC,RestA,Goal,Substs,Cont,ParentFail)
Goals =:= Goals consists of a linked list of the goals to
be satisfied
Head =:=
OrNodes =:= OrNodes is a pointer to a pointer tuple, Or and
Rest0.
Or =:= Or points to "or" nodes. "or" nodes consist
of a list called Clauses and a list AndNodes.
% cont(RestG, RestO, Parentfail)
RestG =:= continuation list for the parent goal;
for when all descendant goals have been
resolved.
RestO =:= list of choice points still to be resolved
against the current goal; in case the
current or_goal choice fails.
ParentFail =:= Contains the backtracking information for the
current goal's parent goal; in case the parent
goal fails.
Substs =:= A list of the bindings made during the
unification of the current goal.
MidSubsts =:= MidSubsts is used as a local variable in the
nested call to unify/5 for nested terms.
NewSubsts =:= Note that NewSubsts will contain any new
substitutions made locally in the call to
unify/5.
Rest =:= The rest of the substitution list.
Tree =:= contains the current state of the search tree.
The search tree consists of nodes represented
as terms. There are "and" nodes and "or" nodes
An "and" term consists of two pointers Goals
and OrNodes.
Value =:= The value of a unified term; be it an atom
integer, variable or non-real variable.
% MAIN PROCEDURES
%debug/1
Initialise_Question
The call to numbervars/3 unifies the variables in the initial question
with the special term known as $Var; by convention. These variables
are now referred to as non-real variables. Associated with each
non-real variable is a unique number. This number is used to
in the substitution list, to associate a variable with a value.
Note that Tree is a shared variable occuring as the second and
seventh argument of and_node. The contents of Tree, the current state
of the search tree, are built up until a solution is found for the
initial question, or the question fails. In either case fail/3
will call ask/1 to see if the user wishes to display the search tree.
%and_node/8.
Exit_Parent
If the body of the current goal is empty then the second argument
of and_node, which will usually contain a list of and_goals, will
be empty. Therefore the parent goalf is proven true; so call
continue/5.
Reduce_Goal
If the body of the current goal is NOT empty (i.e. their ARE
continuation points) then solve the next goal.
%do_and/8.
Create_AndNode_with_ChoicePoints
Create an and_node using the current goal, passing forward
continuation information in the term cont/3:
copy the continuation list for the
parent goal; copy the list of choice points which may still
satisfy the current goal. Go and look for continuation
Create_AndNode_without_ChoicePoints
Prune at this and_node after satisfying the current goal;
this is the last continuation for the parent goal.
%do_goal/8.
Cut
The current goal is a cut therefore commit to the choices made
since the parent goal was invoked and discard any choices left
prior to the cut; go to continue to determine if the parent goal
has any remaining continuation points.
Test_ChoicePoints
Invariably the choice points will have been collected together
and Or will be instantiated to this collection.
Find_ChoicePoints
Initially, apart from a cut or system predicate goal, when a new
current goal is chosen, the choice points, in the form of
Clauses will not yet have been collected together, and Or will be
uninstantiated.
Note that Cont instantiates to the continuation list of the
parent goal for the current goal. Also note the head of the list is a
is the term cont/3; the tail is the rest of the
continuation list.
So, clause(Head, Body) searches the program for a clause whose head
matches Head. Body instantiates to the body of this clause.
findall repeats this for all the instances of the term Head.
Clauses is a non-empty, unordered list, containing all clause
instances (Head:-Body) such that clause(Head, Body) is true.
Note that for the last goal in a parent goal:
Clauses == [(Head1:-Body1), (Head2:-Body2),...]
But more generally:
Clauses == [[(Head1:-Body1), (Head1:-Body2),...] |
[(Head2:-Body1), (Head2:-Body2),...]].
where each element of the outer list represents a goal to be satisfied;
collectively they form the current list of and_goals still to be
satisfied.
Each element of the inner lists represents an or_goal
that will match the head of the corresponding and_goal.
Note that N, the arity of the term is determined here. It is used
later as a controlling variabl for the unification of terms.
%or_node/8.
Fail_to_MatchClause
No principal functor of a procedure matched the current goal,
i.e. the list Clauses is empty, so fail back.
Succeed_to_MatchClause
A principal functor of a procedure matched the current goal.
%do_or/9.
Last_Choice
There is only one and_goal still to be satisfied in the scope of the
current goal. We are looking to get a current goal from the list of
or_goals contained in Clauses.
Not_Last_Choice
More than one choice left, so Choice instantiates to the current head
of the list of or_goals and RestC instantiates to the tail.
We will pass forward all the information relating to choice points
using the term bp/9 which will instantiate FAIL.
This information is necessary should the current or_goal choice fail,
because we wont have to backtrack and look for the next or_goal choice
as it can be taken from the head of RestC.
If we backtracked we would loose all the current or_goal choice
bindings which defeats the purpose of this debugger.
When the match for and_node is made in do_choice/9 AndNode will
instantiate to the body of the current or_goal choice.
%do_choice/9.
Unify_Choice
Now take the chosen or goal apart again.
If unification against the head of the current_choice is successful
then this or-goal choice is suitable as an and_goal therefore commit
to it.
We won't backtrack looking for any more or_goal choices because we
collect ALL of them once the first one succeeds.
Pass forward the body of the or-goal chosen. This will be used to
form the next and_node and become the new current goal.
Consequently, this call to and_node/8 will instantiate And to a
term pointer which has as its value the head of the
and_goals for the current or_goal. The current or_goal passed forward
should now be thought of as the new parent goal.
Unify_Failed
The or_choice used as the current goal failed to unify so pass
forward the list of or_goal choices held by Fail (this was
instantiated in do_or) and the current state of the proof tree
held by Tree, to fail/3.
Note that Fail could hold an empty list containing no or_goal
choicepoints.
%continue/5
Proven_Question
If continue/5 is called and the list of continuation points
is empty then a solution has been found. Go and write the
solution to the question. Ask the user if they require a display of
the proof tree.
Note that if another solution is required we
fail back here and call fail/3.
Find_Continuation
Usually when continue/5 is called there will be a list containing
continuation points. The head of the first argument will match with
cont/3, and the tail, which will be an empty list or contain
continuation points, will instantiate Cont to be the current
continuation list. Cont is passed forward to do_and/8.
%fail/3.
Fail
There were no choice points left for the current and_goal therefore
Fail consists of an empty list. Ask the user if they want to print
the proof tree.
Get_ChoicePoint
We have not exhausted the choicepoints for the current and_goal
therefore get the head of Fail which contains all the information
about the next choice point.
Note that the information describing the unresolved, unordered set of
choicepoints is contained in the term list bp/6. So, this is passed
forward to or_goal.
Also, note that the tail of the list bp becomes the new choice-point
list, passed forward in Fail.
%unify/4
Test_for_Dereferencing
The terms to be unified might not be integers or atoms so they may
need dereferencing. Pass the values to unify_drf/3 for unification.
%deref/3
Found_VariableTerm
Dereference the non-real varible term; this will be the current goal
term and the head of the current choice on subsequent calls. Note
that.
Found_Atom
The term is an atom or an integer, so simply return its value;
no dereferencing is required.
%unify_drf/4
Current_Goal_is_RealVariable
The current goal unifying with the current choice is a
real variable as yet uninstantiated. So, bind the real variable
to the variable-number of the non-real variable. Unification of the
particular term is true. If there are no more terms to be unified in
the current goal then go to the next and_node. Add this binding to the
head of the substitution list.
Current_Choice_is_RealVariable
The current choice made for unifying with the current goal is a
real variable as yet uninstantiated. So, bind the real variable
to the number of the non-real variable. Unification of the
particular term is true. If there are no more terms to be unified in
the current goal then go to the next and_node. Add this binding
to the head of the substitution list
Current_Patterns_both_NonVariableTerms
Both the current goal and current choice or non-variable terms.
functor/3 returns the arity and name of the principal functor
of each of the terms. Unification will fail when functor/3 is called
for the second time if the names of the principal functors
instantiating the second argument F, are not the same. Or, if they
are the same, they do not have the same arity.
If the terms have the same principal functor and arity then we need to
call unify/5 to see if the
terms are compound structures, atoms or integers. Note that we
carry forward the substition list.
%unify/5
Unify_Atom
The arity of the term is 0 therefore the term is an integer or an
atom. Or, this the terminal case of a compound structure as we
are using the arity returned by functor as a counter for determining
which current argument we are matching. Note that nothing is added to
the substitution list if this clause succeeds.
Unify_Structure
The structures have the same principal functor and arity
so match the arguments in turn. Note that the arity I
returned by functor/3 can be used to iterate up the argument lists
from right to left. arg/3 is used to take the Ith argument
from the current goal and the current choice. Note that we are
still carrying the substitution list. Also note that to keep
the substitutions in the correct order in dealing with the
further nested structures MidSubsts is used as a local variable
to this nested call to unify/4. Note that on successful return
from unify/4, MidSubsts is passed forward. New substitutions
may or may not have been added. Subsequently, Unify/5 is called
attempting to match the I-1th argument. Note that NewSubsts
will contain any new substitutions made, local to the unify/5 call.
%derefvar/4
Dereference_Head_of_SubstitutionList
N is the number of the variable. Unify this with the number of the
numbered-variable in the head of the substitution list. If
they unify then we have to find the value of the numbered-variable
in the head of the substituion list. We call deref/3 to see if
the binding is to a value or to yet another non-real variable.
Dereference_Tail_of_SubstitutionList
If the numbered variable in the head of the substitution list fails
to unify with the number of the current non-real variable then the
tail of the substitution list is passed to derefvar, referenced by
Rest. Note that the third argument is used to maintain the completeness
of the substitution list while searching for the value of the non-real
variable.
Found_RealVariable
We have emptied the substitution list therefore the variable is
unstantiated. So we pass back the value of the last non-real
variable in the chain as the value to which to bind the
current variable term to.
*/
:- public (debug)/1.
:- op(1050,fy,(debug)).
debug Goals :-
numbervars(Goals,0,N),
and_node(Goals,Tree,[],[],[],[],Tree,N).
and_node(true,true,Substs,Cont,Fail,ParentFail,Tree,N) :- !,
continue(Cont,Substs,Fail,Tree,N).
and_node(Goals,and(Goals,OrNodes),Substs,Cont,Fail,ParentFail,Tree,N) :-
do_and(Goals,OrNodes,Substs,Cont,Fail,ParentFail,Tree,N).
do_and((Goal,RestG),(Or,RestO),Substs,Cont,Fail,ParentFail,Tree,N) :- !,
do_goal(Goal,Or,Substs,[cont(RestG,RestO,ParentFail)|Cont],
Fail,ParentFail,Tree,N).
do_and(Goal,Or,Substs,Cont,Fail,ParentFail,Tree,N) :-
do_goal(Goal,Or,Substs,Cont,Fail,ParentFail,Tree,N).
do_goal(!,true,Substs,Cont,Fail,ParentFail,Tree,N) :- !, % handle cut
continue(Cont,Substs,ParentFail,Tree,N).
do_goal(Goal,Or,Substs,Cont,Fail,ParentFail,Tree,N) :-
nonvar(Or), !, % clauses exist
or_node(Clauses,Or,Goal,Substs,Cont,Fail,Tree,N).
do_goal(Goal,Or,Substs,Cont,Fail,ParentFail,Tree,N0) :-
functor(Goal,F,N), % get clauses
functor(Head,F,N),
findall( (Head:-Body),
clause(Head,Body),
Clauses),
numbervars(Clauses,N0,N1),
or_node(Clauses,Or,Goal,Substs,Cont,Fail,Tree,N1).
or_node([],fail,Goal,Substs,Cont,Fail,Tree,N) :- !, % no clauses
nl, write('Warning: there are no clauses for '),
write(Goal), nl,
fail(Fail,Tree,N).
or_node(Clauses,or(Clauses,AndNodes),Goal,Substs,Cont,Fail,Tree,N) :-
do_or(Clauses,AndNodes,Goal,Substs,Cont,Fail,Fail,Tree,N).
do_or([Choice],[AndNode],Goal,Substs,Cont,Fail,ParentFail,Tree,N) :- !, % last clause
do_choice(Choice,AndNode,Goal,Substs,Cont,Fail,ParentFail,Tree,N).
do_or([Choice|RestC],[And|RestA],Goal,Substs,Cont,Fail,ParentFail,Tree,N) :-
do_choice(Choice,And,Goal,Substs,Cont,
[bp(RestC,RestA,Goal,Substs,Cont,ParentFail)|Fail],
ParentFail,Tree,N).
do_choice((Head:-Body),And,Goal,Substs,Cont,Fail,ParentFail,Tree,N) :-
unify(Goal,Head,Substs,NewSubsts), !,
and_node(Body,And,NewSubsts,Cont,Fail,ParentFail,Tree,N).
do_choice(Choice,And,Goal,Substs,Cont,Fail,ParentFail,Tree,N) :-
fail(Fail,Tree,N).
continue([],Substs,Fail,Tree,N) :- !,
( nl, write_substs(Substs,Tree),
ask('More'), !,
nl, write(yes), nl
; fail(Fail,Tree,N)
).
continue([cont(Goals,OrNodes,ParentFail)|Cont],Substs,Fail,Tree,N) :-
do_and(Goals,OrNodes,Substs,Cont,Fail,ParentFail,Tree,N).
fail([],Tree,N) :- !,
nl, write(no), nl,
( ask('Print tree'), !
; printm(0,[],Tree)
).
fail([bp(RestC,RestA,Goal,Substs,Cont,ParentFail)|Fail],Tree,N) :-
do_or(RestC,RestA,Goal,Substs,Cont,Fail,ParentFail,Tree,N).
unify(T1,T2,Substs,NewSubsts) :-
deref(T1,Substs,DT1),
deref(T2,Substs,DT2),
unify_drf(DT1,DT2,Substs,NewSubsts).
unify_drf(T,'$VAR'(N),Substs,[N=T|Substs]) :- !.
unify_drf('$VAR'(N),T,Substs,[N=T|Substs]) :- !.
unify_drf(T1,T2,Substs,NewSubsts) :-
functor(T1,F,N),
functor(T2,F,N),
unify(N,T1,T2,Substs,NewSubsts).
unify(0,T1,T2,Substs,Substs) :- !.
unify(I,T1,T2,Substs,NewSubsts) :-
arg(I,T1,A1),
arg(I,T2,A2),
unify(A1,A2,Substs,MidSubsts),
J is I-1,
unify(J,T1,T2,MidSubsts,NewSubsts).
deref('$VAR'(N),Substs,Value) :- !,
derefvar(N,Substs,Substs,Value).
deref(X,S,X).
derefvar(N,[N=V1|Rest],Substs,V2) :- !,
deref(V1,Substs,V2).
derefvar(N,[_|Rest],Substs,V) :- !,
derefvar(N,Rest,Substs,V).
derefvar(N,[],_,'$VAR'(N)).
/* Outputting routines */
write_substs(Substs,and(Goals,T)) :-
write('Proved:'), nl,
printm(0,Substs,Goals),
( ask('Print tree'), !
; printm(0,Substs,and(Goals,T))
).
printm(M,_,V) :- var(V), !,
write(V).
printm(M,Substs,or(C,A)) :- !,
N is M+1,
write('or('), printm_nl(N,Substs,C), put(0',),
printm_nl(N,Substs,A), put(0')).
printm(M,Substs,and(G,O)) :- !,
N is M+1,
write('and('), printm_nl(N,Substs,G), put(0',),
printm_nl(N,Substs,O), put(0')).
printm(M,Substs,[X|L]) :- !,
N is M+1,
write('[ '), printm(N,Substs,X),
printml(N,Substs,L), write(' ]').
printm(M,Substs,(X,Y)) :- !,
N is M+1,
write('( '), printm(N,Substs,X), put(0',),
printm_nl(N,Substs,Y), write(' )').
printm(M,Substs,X) :-
dosubsts(X,Substs,V),
print(V).
printm_nl(M,S,X) :- nl, tab(M*2), printm(M,S,X).
printml(_,_,V) :-
var(V), !,
write(' |'), write(V), put(0']).
printml(_,_,[]) :- !.
printml(M,Substs,[X|L]) :-
put(0',), printm_nl(M,Substs,X),
printml(M,Substs,L).
dosubsts(Var,S,Var) :- var(Var), !. % Leave real variable alone
dosubsts('$VAR'(N),S,V) :- !,
derefvar(N,S,S,T),
dosubterms(T,S,V).
dosubsts(T,S,V) :-
functor(T,F,N),
functor(V,F,N),
dosubsts(N,T,S,V).
dosubterms('$VAR'(N),_,'$VAR'(N)) :- !. % unbound variable
dosubterms(T,S,V) :- % substitute values of vars in T
dosubsts(T,S,V).
dosubsts(0,T,S,V) :- !.
dosubsts(I,T,S,V) :-
arg(I,T,Ti),
arg(I,V,Vi),
dosubsts(Ti,S,Vi),
J is I-1,
dosubsts(J,T,S,V).
/* Ask user question and fail if "y" typed */
ask(Question) :-
nl, write(Question),
write(' (y/n)? '),
ttyflush,
get0(C),
skiptonl(C),
C =\= "y".
skiptonl(31) :- !. % DEC-10
skiptonl(10) :- !. % VAX
skiptonl(_) :- get0(C), skiptonl(C).