Prolog Interpreter

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  }

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.

{ Prolog Interpreter, Main Program. }
{ 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
            else begin read(ch); write(ch) 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
      begin readln; writeln; ch:=' ';
            lineno:=lineno+1; write(lineno:3, ': ')
      end
      else begin read(ch); write(ch);
                 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[1] 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}

      else error('bad symbol')
end{insymbol};

{ Lexical Analysis. }