Prolog Interpreter
Parser.
It is straightforward to write a parser for Prolog and one is given in an appendix. Various lexical symbols are recognised:
1 2 3 4 5 6 7 8
12345678901234567890123456789012345678901234567890123456789012345678901234567890
— need 80-ish characters
{lexical items}
symbol = (LCword, UCword, numeral,
open, close, sqopen, sqclose,
impliedby, notsy, andsy, comma, colon, dot, question,
eofsy
);
{ Lexical Types. }
An upper-case (UC) word begins with a capital letter and stands for a variable.
The parser produces a parse tree defined by the following data types:
tree = ^ node;
SyntaxClass = ( constant, intcon, variable, func,
predicate, negate, rule, progrm,
list );
node = record case tag :SyntaxClass of
constant :( cid :alfa ); { eg. fred }
intcon :( n:integer ); { eg. 99 }
variable :( vid :alfa; index :integer ); { eg. X }
func, predicate
:( id :alfa; params:tree ); { eg. h(1,k(p,X)) }
negate :( l :tree ); { eg. not p(7) }
rule :( lhs, rhs :tree ); { eg. p <= q and r. }
progrm :( facts, query :tree );
list :( hd, tl :tree )
end;
{ Syntactic Types. }
The index field associated with a variable is used in the renaming of variables as defined in detail later. When a rule is used, a copy of the rule is made in which the variables are renamed. This is done by setting the index fields to a new value. A variable name is considered to be an <identifier,index> pair.
Simple routines build and manipulate the tree structure:
function newnode(t:SyntaxClass) :tree;
var n :tree;
begin new(n); n^.tag := t; newnode := n
end;
function cons(h, t :tree) :tree;
var c :tree;
begin c := newnode(list);
c^.hd := h; c^.tl := t;
cons := c
end;
function append( a, b :tree ) :tree;
begin if a=nil then append:=b else append:=cons(a^.hd, append(a^.tl, b))
end;
{ Tree Manipulation. }
An output routine prints a tree by recursive traversal:
procedure printtree(t:tree; e:Env);
var v :tree;
procedure printId(id:alfa);
var i:integer;
begin i:=1;
while i<=10 do
if id[i]=' ' then i:=11 else begin write(id[i]); i:=i+1 end
end;
procedure printTail( t :tree );
begin if t <> nil then
begin write(', '); printtree(t^.hd, e); printTail(t^.tl) end
end;
begin{printtree}
if t<>nil then
case t^.tag of
variable:if bound(t, v, e) then printtree(v, e)
else
begin printId(t^.vid);
if t^.index<>0 then write('_', t^.index:1)
end;
constant:printId(t^.cid);
intcon: write(t^.n:1);
predicate, func:
begin printId(t^.id);
if t^.params<>nil then
begin write('('); printtree(t^.params, e); write(')')
end
end;
negate: begin write(' not '); printtree(t^.l, e) end;
rule: begin printtree(t^.lhs, e);
if t^.rhs<>nil then
begin write(' <= '); printtree(t^.rhs, e)
end;
writeln('.')
end;
list: begin printtree(t^.hd, e); printTail(t^.tl) end;
progrm: begin printtree(t^.facts, e); writeln;
write('?'); printtree(t^.query, e); writeln
end
end{case};
end{printtree};
{ Print a Parse Tree. }
A query may contain variables. If the query is satisfied the routine is used to print it. The routine also substitutes the values of any variables if known. These values are contained in an environment which is described below.
Execution.
The interpreter walks the parse tree of a program and executes it. As it does so values are bound to variables and these bindings are kept in an environment:
Env = ^ Binding;
Binding = record id :alfa; index :integer; v:tree; next:Env end;
{ Environment Type. }
and
function bind( x :tree; val :tree; e :Env ) :Env;
var b :Env;
begin new(b);
b^.id := x^.vid; b^.index := x^.index; b^.v := val;
b^.next := e; bind := b
end;
function bound( x :tree; var val :tree; e :Env ) :boolean;
begin if e=nil then bound := false
else if (e^.id=x^.vid) and (e^.index=x^.index) then
begin val := e^.v; bound := true end
else bound := bound( x, val, e^.next )
end;
{ Manipulate Environments. }
The interpreter attempts to prove or satisfy the query in a program using the given facts. If it fails it prints 'no'. It prints all solutions that it finds, if any.
procedure execute(prog :tree);
type mode = (PrintAll, Silent); {search mode}
var index :integer; { used for renaming }
#include "unify.P" { unify two predicates }
#include "rename.P" { rename variables in a rule }
#include "prove.P" { proof strategy }
begin {execute}
index := 0;
if not Prove(PrintAll, prog^.query, prog^.facts, nil) then
writeln(' no')
end {execute};
{ Interpreter. }
Proof
The proof strategy defined here is a simple top-down left-to-right strategy. It attempts to prove a query by proving each literal in turn. It tries to prove an atom by unifying it with the left hand side of some rule. If unification succeeds, the right hand side of the rule plus the remainder of the query must then be proven. An environment is maintained during this process and unification may add to it. The proof of a negated atom relies on negation by failure; the proof of the (positive) atom must fail. If this is the case, the remainder of the query must then be proven.
function Prove( search:mode; query, facts :tree; e :Env) :boolean;
label 99; {success escape for Silent mode}
var Satisfied :boolean;
procedure ProveList( query, facts :tree; e :Env );
procedure ProveLiteral(p, f :tree; e :Env);
var newe :Env;
begin
if p^.tag = negate then { negated atom eg. not l(...) }
begin {negation by failure: not p(...) succeeds iff p(...) fails}
if not Prove(Silent, cons(p^.l, nil), f, e) then
ProveList(query^.tl, f, e) {rest of query}
{else do nothing at all}
end
else { positive atom eg. p(...) }
if f <> nil then
begin if unify(p, rename(f^.hd^.lhs, index), newe, e) then
ProveList(append(rename(f^.hd^.rhs, index), {RHS of rule}
query^.tl), {plus rest of query}
facts, newe);
ProveLiteral(p, f^.tl, e) {also try for other solutions}
end
end {ProveLiteral};
begin {ProveList}
if query = nil then {nothing more to prove - success}
case search of
PrintAll:{print ALL solutions to query}
begin printtree(prog^.query, e); writeln(' yes'); Satisfied:=true end;
Silent: {esp' for negation by failure, only need one success}
begin Satisfied := true; goto 99 {!!! once is enough} end
end
else
begin index:=index+1; ProveLiteral(query^.hd, facts, e) end
end {ProveList};
begin { Prove }
Satisfied := false;
ProveList( query, facts, e);
99: Prove := Satisfied
end { Prove };
{ Depth-First, Left-to-Right Proof Strategy. }
{ - L. Allison 9/2007 }
{Do not remove: Main.p, env*P, execute.P, unify.P, rename.P, prove.P, lex*P, }
{ syntax*P, tree.P are released under Gnu `copyleft' General Public Licence }
Negation
Negation by failure need only detect a single proof of the atom and need not print it. For this reason the proof strategy operates in one of two modes. In 'PrintAll' mode, all solutions are sought and printed. In 'Silent' mode, one solution is sought and not printed.
Renaming
When a rule is used, a copy containing renamed variables is used so as to prevent name clashes between different instances of the rule. Renaming is based on a recursive tree traversal much like the tree print routine.
function rename(t :tree; index :integer) :tree;
var r :tree;
function copynode :tree;
var c :tree;
begin c:=newnode(t^.tag); c^:=t^; copynode:=c
end;
begin{rename}
if t = nil then r := nil
else
case t^.tag of
variable:begin r:=copynode; r^.index:=index end;
constant:r := t;
intcon: r := t;
predicate, func:
begin r := copynode; r^.params := rename(t^.params, index)
end;
negate: begin r := copynode; r^.l := rename(t^.l, index) end;
rule: begin r := copynode;
r^.lhs := rename(t^.lhs, index);
r^.rhs := rename(t^.rhs, index)
end;
list: begin r := copynode;
r^.hd := rename(t^.hd, index);
r^.tl := rename(t^.tl, index)
end;
end{case};
rename := r
end{rename};
{ Rename Variables in a Tree. }
The unification routine attempts to find bindings for variables so as to make two atoms syntactically identical. It is heavily based on a recursive tree-equality function. For example, two constants are the same if and only if they are the same constant! Two function terms are the same if and only if they have the same function identifier and their parameters are the same.
A variable may be bound or unbound in the current environment. If a variable is bound to a value, the variable unifies with a term if and only if its value unifies with the term. On the other hand, an unbound variable unifies with any term and the variable is bound to the term in an extended environment. In this way the environment can grow. Strictly speaking, a variable should not bind with a term that contains the variable. A test to this effect is known as the occurs check. The occurs check is usually not implemented on efficiency grounds but this may cause the interpreter to loop in some cases.
Unification
If two atoms unify, the set of bindings discovered is known as the most general unifier (MGU) in the sense that any other set of bindings unifying the atoms would be a special case of the MGU.
function unify( a, b :tree; var newenv :Env; oldenv :Env) :boolean;
var e2 :Env; v :tree;
begin {unify}
newenv := oldenv;
if (a = nil) or (b=nil) then unify := a=b
else { a<>nil and b<>nil } if a^.tag = b^.tag then
case a^.tag { = b^.tag } of
variable: if bound(a, v, oldenv) then
unify := unify(v, b, newenv, oldenv)
else if bound(b, v, oldenv) then
unify := unify(a, v, newenv, oldenv)
{both unbound}
else if (a^.vid=b^.vid) and (a^.index=b^.index) then
unify := true
else {2 different, unbound vars}
begin newenv := bind(a, b, oldenv); unify := true
end;
constant: unify := a^.cid = b^.cid; { m : n }
intcon: unify := a^.n = b^.n; { x : y }
func, predicate: { a(...) : b(...) }
if a^.id = b^.id then
unify := unify(a^.params, b^.params, newenv, oldenv)
else unify := false;
{ ahd.atl : bhd.btl }
list: if unify(a^.hd, b^.hd, e2, oldenv) then
unify := unify(a^.tl, b^.tl, newenv, e2)
else unify := false
end {case}
else { a^.tag <> b^.tag } if a^.tag = variable then { X : f(...) }
if bound(a, v, oldenv) then
unify := unify(v, b, newenv, oldenv)
else
begin newenv := bind(a, b, oldenv); unify := true
end
else if b^.tag = variable then { f(...) : X }
unify := unify(b, a, newenv, oldenv)
else unify := false
end {unify};
{ Unification Algorithm. }
{ L. Allison 9/2007 }
{Do not remove: Main.p, env*P, execute.P, unify.P, rename.P, prove.P, lex*P, }
{ syntax*P, tree.P are released under Gnu `copyleft' General Public Licence }
Appendix
We also need ...[Main.P]
and
[syntax.P]
and
[lex.insym.P]