LA home Computing Logic  Prolog   Intro.   Examples   Syntax   Interp.   Interp. Also see:   λ-calculus

### Parser.

It is straightforward to write a parser for Prolog and one is given in an appendix. Various lexical symbols are recognised:

```
{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. }

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.

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  }

```
-- LA 9/2007

### Appendix.

```
{System dependent} procedure setlinebuffering; external;

program prolog(input, output);

label 99; {error failure; stop}

type alfa = packed array [1..10] of char;

#include "lex.type.P"      {Lexical Types}
#include "syntax.type.P"   {Syntactic Types}
#include "env.type.P"      {Environments}

var prog:tree;

#include "tree.P"          {Manipulate trees and nodes}
#include "syntax.P"        {The Parser}
#include "env.P"           {Manipulate Environments}
#include "syntax.print.P"  {Print a Parse Tree}
#include "execute.P"       {interpreter}

begin setlinebuffering; { system dependent }
prog:=parser;
writeln; writeln(' --- end of parsing --- ');
printtree(prog, nil); writeln; writeln(' --- running --- ');
execute(prog);
99:writeln; writeln(' --- finished --- ')
end.

{ 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. }

function parser:tree;

var lineno :integer;                      { state vars for parser}
ch:char; sy:symbol; theword:alfa; theint:integer;

procedure error(m:alfa);
begin writeln;
writeln('error:', m, ' lineno=', lineno:1,
' ch=<', ch, '>(', ord(ch):1, ') sy=', ord(sy):1,
' last word=<', theword, '>');
writeln; write('skip :');
while not eof do
if eoln then begin readln; writeln; write('skip :') end
goto 99 {error abort}
end{error};

#include "lex.insym.P"  {Lexical Analysis Routines}

procedure check(s:symbol; m:alfa);
begin if sy=s then insymbol else error(m) end;

function syis(s:symbol):boolean;
begin if sy=s then begin syis:=true; insymbol end else syis:=false end;

function sequence( function item:tree; sep :symbol ):tree; { >=1 of }
var s :tree;
function rest:tree;
var r :tree;
begin if syis(sep) then
begin r := cons(item, nil); r^.tl := rest
end
else r:=nil;
rest := r
end  {rest};
begin s := cons(item, nil); s^.tl := rest;
sequence := s
end {sequence};

function prog :tree; { ------------------------- parse a program --------- }
var p :tree;

function Pterm :tree; forward;

function Pterms :tree; { optional  (1, x, Y, g(1,h)) }
var p :tree;
begin if syis(open) then
begin p := sequence(Pterm, comma);
check(close, ') expected')
end
else p:=nil;
Pterms := p
end   {Pterms};

function Pterm { :tree -- forwarded}; { constant `x' or func f(1,g(y)) }
var f :tree; id :alfa;
begin if sy=LCword then
begin id := theword; insymbol;
if sy = open then                                { function }
begin f:=newnode(func); f^.id:=id; f^.params := Pterms
end
else                                             { constant }
begin f:=newnode(constant); f^.cid:=id
end
end

else if sy=UCword then                                 { Variable }
begin f := newnode(variable); f^.vid := theword; f^.index := 0;
insymbol
end

else if sy=numeral then                        { integer constant }
begin f := newnode(intcon); f^.n := theint; insymbol
end

else error('no term   ');
Pterm := f
end   {Pterm};

function Patom :tree; { eg. parent(fred, M, D) }
var p :tree;
begin if sy=LCword then
begin p := newnode(predicate); p^.id:=theword; insymbol;
p^.params := Pterms
end
else error('no predcte');
Patom := p
end   {Patom};

function Pliteral :tree; { eg. not equal(X,Y)  or eg. equal(X,Y) }
var l :tree;
begin if syis(notsy) then
begin l:=newnode(negate); l^.l := Patom end
else l := Patom;
Pliteral := l
end   {Pliteral};

function Prule :tree; { `p<=q and s.'   or   `parents(c,m,d).' }
var r :tree;
begin r := newnode(rule);
r^.lhs := Patom;
if syis(impliedby) then r^.rhs := sequence(Pliteral, andsy)
else r^.rhs := nil;
check(dot, '. expected');
Prule := r
end   {Prule};

function Prules :tree; { optional list of rules }
var r :tree;
begin if sy=LCword then
begin r:=cons(Prule, nil); r^.tl := Prules end
else r:=nil;
Prules := r
end   {Prules};

begin {prog}
p := newnode(progrm);
p^.facts := Prules;
check(question, '? expected');
p^.query := sequence(Pliteral, andsy); check(dot, 'missing . ');
prog := p
end   {prog};

begin {parser}
lineno := 1;
writeln(' Simple Prolog, L.A., 9/2007');
write(lineno:3, ': ');
ch:=' '; theword := '-start----'; theint:=maxint; insymbol;

parser := prog;

check(eofsy, 'prog+junk ');
writeln
end{parser};

{ Parser for Prolog-S. }
{ 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  }

procedure getch;
const tab = 9;
begin if eof then begin ch:='.'; theword:='     ' end
else if eoln then
lineno:=lineno+1; write(lineno:3, ': ')
end
if ord(ch)=tab then ch:=' '
end
end{getch};

procedure insymbol;
const blank='          ';
var len:integer;
begin repeat while ch=' ' do getch;
if ch='{' then  { comment }
begin repeat getch
until (ch='}') or eof;
getch
end
until not( ch in [' ', '{'] );
if eof then sy:=eofsy

else if ch in ['a'..'z', 'A'..'Z'] then                             {xyz}
begin theword:=blank;
len:=0;
while ch in ['a'..'z', 'A'..'Z', '0'..'9'] do
begin len:=len+1;
if len<=10 then theword[len] := ch;
getch
end; {not ch in ['a'..'z', '0'..'9']}
if theword='and       ' then sy:=andsy
else if theword='not       ' then sy:=notsy
else if theword in ['a'..'z'] then sy:=LCword
else sy:=UCword
end{alphanums}

else if ch in ['0'..'9'] then                            {123}
begin theint:=0;
while ch in ['0'..'9'] do
begin theint:=theint*10+ord(ch)-ord('0'); getch
end;
sy:=numeral
end

else if ch in  [ '?', '.', ',', ':', '<', '&', '(', ')', '[', ']' ] then
case ch of
'<': begin getch;
if ch='=' then begin getch; sy:=impliedby end
else error('not <=    ')
end;
':': begin getch;
if ch='-' then begin getch; sy:=impliedby end
else sy:=colon
end;
'?', '.', ',', '(', ')', '[', ']', '&':
begin case ch of
'?': sy:=question;
'.': sy:=dot;    ',': sy:=comma;
'(': sy:=open;   ')': sy:=close;
'[': sy:=sqopen; ']': sy:=sqclose;
'&': sy:=andsy
end{case};
getch
end
end{case}