PROGRAM prolog(input,output);

{ Prolog Interpreter, Martin Nilsson UPMAIL 82-11-15
  Booted on Pascal u-eng LEF 830118
  Ported to N-100 TS 830118

Syntax:         Lisp S-expressions
Toplevel:       READ-PROVE loop
Input:          (prove <goal 1>... <goal N>)
<goal>:         (<functor> <arg 1>... <arg N>)
<functor>:      a predicate name, which is represented as a Lisp symbol
<arg>:          S-expressions in general which may contain variables
<variable>:     Lisp symbol with a leading questionmark
Evaluable predicates: assert, read, writeln
(assert <clause 1>... <clause N>): adds clauses to the database
<clause>:       (<goal 1>... <goal N>). Paraphrased: To prove <goal 1> try to
                prove <goal 2>... <goal N>.
(read ?x):      Write ?x and a new line
Initialization: Starts reading from an INIT file.
Backtracking:   During execution after all the goals in a query have been
                proved, you are asked the question "MORE?". If you answer
                NIL, it will return immediately to the toplevel. Otherwise
                it will backtrack and try to find alternative proofs.       } 

{$I_}

LABEL 1 ;  {error return}

CONST txtlength = 10;
      empty = ';'; 
      emptypname     = ';;;;;;;;;;'; 
      t_pname        = 't;;;;;;;;;';
      nil_pname      = 'nil;;;;;;;';
      b_of_env_pname = 'b_of_env;;';
      prove_pname    = 'prove;;;;;';
      read_pname     = 'read;;;;;;';
      writeln_pname  = 'writeln;;;';
      assert_pname   = 'assert;;;;';
      
      
TYPE txt = PACKED ARRAY [1..txtlength] OF Char;
     celltype = (pair, symbol, number);
     ptr = ^cell;
     cell = RECORD
            CASE ptype : celltype of
            pair: (car : ptr; cdr : ptr);
            symbol: (pname : ^txt);
            number: (val : integer);
     END;
     
     
VAR bufferchar :  Char; endline : Boolean; init : Text;
    global_database, expr, nill, temp : ptr;
    garbage : ^Integer;

{ ---------- Lisp Structure Funs }
PROCEDURE doing_it; FORWARD;

PROCEDURE error(msg : txt); BEGIN
           release(garbage);Writeln(msg); goto 1; END; 

FUNCTION car(x : ptr) : ptr; BEGIN car:=x^.car END;
FUNCTION cdr(x : ptr) : ptr; BEGIN cdr:=x^.cdr END;

FUNCTION cons(x, y : ptr) : ptr;
    VAR p : ptr;
BEGIN new(p); p^.ptype:=pair; p^.car:=x; p^.cdr:=y; cons:=p END;

FUNCTION symbolcons(x : txt) : ptr;
    VAR p : ptr;
BEGIN new(p); p^.ptype:=symbol; new(p^.pname); p^.pname^:=x; symbolcons:=p END;

FUNCTION numbercons(x : Integer) : ptr;
    VAR p : ptr;
BEGIN new(p); p^.ptype:=number; p^.val:=x; numbercons:=p END;

FUNCTION equal(x, y : ptr) : Boolean;
BEGIN IF x=y THEN equal:=True
    ELSE IF x^.ptype<>y^.ptype THEN equal:=False
    ELSE CASE x^.ptype OF
        pair : IF Not equal(car(x), car(y)) THEN equal:=False
            ELSE equal:=equal(cdr(x), cdr(y));
        symbol : equal:=(x^.pname^=y^.pname^);
        number : equal:=(x^.val=y^.val);
    END;
END;

FUNCTION atom(x : ptr) : Boolean; BEGIN atom:=(x^.ptype<>pair) END;

FUNCTION assoc(x, l : ptr) : ptr;
BEGIN IF l=nill THEN assoc:=nill
    ELSE IF equal (x, car(car(l))) THEN assoc:=car(l)
    ELSE assoc:=assoc(x, cdr(l));
END;

FUNCTION append(x, y : ptr) : ptr;
BEGIN IF x=nill THEN append:=y
    ELSE append:=cons(car(X), append(cdr(x), y));
END;

{ ---------- Lisp Syntax Reader }

PROCEDURE myread(VAR ch : Char);
    BEGIN IF Eof(init) THEN read(ch) ELSE read(init, ch);
          IF ch<' ' then ch:=' '
          ELSE IF ch IN ['A'..'Z'] THEN ch:=chr(ord(ch)+32);END;
PROCEDURE myreadln; BEGIN IF Eof(init) THEN readln ELSE readln(init) END;
FUNCTION myeoln : Boolean;
    BEGIN IF Eof(init) THEN myeoln:=eoln ELSE myeoln:=eoln(init) END;
    
FUNCTION readch : Char;
    VAR ch : Char;
BEGIN IF bufferchar<>empty THEN BEGIN readch:=bufferchar; bufferchar:=empty;
    END ELSE IF endline THEN BEGIN myreadln; endline:=False; readch:=readch;
    END ELSE IF myeoln THEN BEGIN endline:=True; readch:=' ';
    END ELSE
     BEGIN myread(ch); readch:=ch; END;
END;

PROCEDURE ratom(VAR atom : ptr; VAR breakchar : Char);
    VAR ch : Char; i : Integer; pnamestr : txt;
BEGIN pnamestr:=emptypname;
    ch:=readch; WHILE ch=' ' DO ch:=readch; breakchar:=ch;
    IF Not (ch IN ['(',')','.']) THEN BEGIN i:=0;
        REPEAT
            IF i<txtlength THEN BEGIN i:=i+1; pnamestr[i]:=ch END;
            ch:=readch;
        UNTIL ch IN [' ',chr(9),'(',')','.']; 
        IF (i=3) AND (pnamestr[1]='n') AND (pnamestr[2]='i')
            AND (pnamestr[3]='l') THEN atom:=nill
        ELSE atom:=symbolcons(pnamestr);
        bufferchar:=ch;
    END;
END;

FUNCTION readtail(firstelem : Boolean) : ptr; FORWARD;

FUNCTION lread : ptr;
    VAR atom : ptr; breakchar : Char;
BEGIN ratom(atom, breakchar);
    IF breakchar='(' THEN lread:=readtail(True)
    ELSE IF (breakchar=')') OR (breakchar='.') THEN error('Syntax R!!')
    ELSE lread:=atom;
END;

FUNCTION readtail{(firstelem : Boolean) : ptr};
    VAR atom : ptr; breakchar : Char;
BEGIN ratom(atom, breakchar);
    IF breakchar='(' THEN readtail:=cons(readtail(True), readtail(False))
    ELSE IF breakchar=')' THEN readtail:=nill
    ELSE IF (breakchar='.') AND firstelem THEN error('Syntax R!!')
    ELSE IF breakchar='.' THEN BEGIN readtail:=lread;
        ratom(atom, breakchar);
        IF Not (breakchar=')') THEN error('Syntax R!!');
    END ELSE readtail:=cons(atom, readtail(False));
END;

{ ---------- Lisp Syntax Printer }

PROCEDURE printtail(expr : ptr); FORWARD;

PROCEDURE lprint(expr : ptr); 
    VAR i : Integer;
BEGIN IF expr=nill THEN write('nil') ELSE
      CASE expr^.ptype OF
          pair : BEGIN write('('); printtail(expr) END;
          symbol : FOR i:=1 TO txtlength DO
              WITH expr^ DO IF pname^[i]<>empty THEN write(pname^[i]);
          number : write(expr^.val);
      END;
END;

PROCEDURE printtail{(expr : ptr)};
BEGIN IF expr=nill THEN write(')')
      ELSE IF expr^.ptype=pair THEN WITH expr^ DO BEGIN
          lprint(car); IF cdr<>nill THEN write(' '); printtail(cdr);
      END ELSE BEGIN write('. '); lprint(expr); write(')'); END;
END;

{ ---------- Prolog Kernel }

FUNCTION first(x : ptr) : ptr; BEGIN first:=car(x) END;
FUNCTION rest(x : ptr) : ptr; BEGIN rest:=cdr(x) END;
FUNCTION level_of(x : ptr) : ptr; BEGIN level_of:=car(x) END;
FUNCTION expr_of(x : ptr) : ptr; BEGIN expr_of:=cdr(x) END; 
FUNCTION second(x : ptr) : ptr; BEGIN second:=car(cdr(x)) END;
FUNCTION functor_of(goal : ptr) : ptr; BEGIN functor_of:=first(goal) END;
FUNCTION goals_of_current_level(to_prove : ptr) : ptr;
    BEGIN goals_of_current_level:=cdr(car(to_prove)) END;
FUNCTION other_level_goals(to_prove : ptr) : ptr;
    BEGIN other_level_goals:=cdr(to_prove) END;
FUNCTION first_goal(to_prove : ptr) : ptr;
    BEGIN first_goal:=car(cdr(car(to_prove))) END;
FUNCTION current_level(to_prove : ptr) : ptr;
    BEGIN current_level:=car(car(to_prove)) END;
FUNCTION but_first_goal(to_prove : ptr) : ptr;
    BEGIN but_first_goal:=cons(cons(car(car(to_prove)),
        cdr(cdr(car(to_prove)))), cdr(to_prove));
    END;
    
FUNCTION prove(goals : ptr) : ptr; FORWARD;
FUNCTION search_database(to_prove, env, level : ptr) : ptr; FORWARD;
FUNCTION unify(levelx, x, levely, y, env : ptr) : ptr; FORWARD;
FUNCTION lookup(x, env : ptr) : ptr; FORWARD;
FUNCTION is_var(x : ptr) : Boolean; FORWARD;
FUNCTION is_eval_predicate(functor : ptr) : Boolean; FORWARD;
FUNCTION apply(functor, to_prove, env, level : ptr) : ptr; FORWARD;
FUNCTION further_bindings(bound, env : ptr) : ptr; FORWARD;

FUNCTION prove{(goals : ptr) : ptr};
BEGIN prove:=search_database(cons(cons(numbercons(0), goals), nill),
    cons(cons(symbolcons(b_of_env_pname), nill), nill), numbercons(1)); 
END;

FUNCTION search_database{(to_prove, env, level : ptr) : ptr};
    VAR database, assertion, new_env, rest_to_prove, returned_val : ptr;
BEGIN IF to_prove=nill THEN BEGIN write('MORE?');
        IF lread=nill THEN search_database:=symbolcons(t_pname)
        ELSE search_database:=nill;
    END ELSE IF goals_of_current_level(to_prove)=nill THEN search_database:=
        search_database(other_level_goals(to_prove), env, level)
    ELSE IF is_eval_predicate(functor_of(first_goal(to_prove))) THEN
        search_database:=
            apply(functor_of(first_goal(to_prove)), to_prove, env, level)
    ELSE BEGIN
        database:=global_database;
        rest_to_prove:=but_first_goal(to_prove);
        returned_val:=nill;
        WHILE (database<>nill) AND (returned_val=nill) DO BEGIN
            assertion:=first(database);
            database:=rest(database);
            new_env:=unify(current_level(to_prove), first_goal(to_prove),
                           level, first(assertion), env);
            IF new_env<>nill THEN returned_val:=
                search_database(cons(cons(level, rest(assertion)),
                    rest_to_prove), new_env, numbercons(level^.val+1))
        END;
        search_database:=returned_val;
    END;
END;

FUNCTION unify{(levelx, x, levely, y, env : ptr) : ptr};
BEGIN
    x:=lookup(cons(levelx, x), env);
    y:=lookup(cons(levely, y), env);
    IF equal(x, y) THEN unify:=env
    ELSE IF is_var(x) THEN unify:=cons(cons(x, y), env)
    ELSE IF is_var(y) THEN unify:=cons(cons(y, x), env)
    ELSE IF atom(expr_of(x)) OR atom(expr_of(y)) THEN BEGIN
        IF equal(expr_of(x), expr_of(y)) THEN unify:=env ELSE unify:=nill;
    END ELSE BEGIN env:=unify(level_of(x), car(expr_of(x)),
                              level_of(y), car(expr_of(y)), env);
        IF env=nill THEN unify:=nill
        ELSE unify:=unify(level_of(x), cdr(expr_of(x)),
                          level_of(y), cdr(expr_of(y)), env);
    END;
END;

FUNCTION lookup{(x, env : ptr) : ptr};
    VAR temp : ptr;
BEGIN IF Not(is_var(x)) THEN lookup:=x
    ELSE BEGIN temp:=further_bindings(assoc(x, env), env);
        IF temp<>nill THEN lookup:=temp ELSE lookup:=x;
    END;
END;

FUNCTION further_bindings{(bound, env : ptr) : ptr};
BEGIN IF bound<>nill THEN further_bindings:=lookup(cdr(bound), env)
    ELSE further_bindings:=nill;
END;

FUNCTION is_var{(x : ptr) : Boolean};
    VAR temp : ptr;
BEGIN temp:=cdr(x);
    IF temp^.ptype<>symbol THEN is_var:=False
    ELSE is_var:=(temp^.pname^[1]='?');
END;

{ ---------- Some Evaluable Predicates (=System Functions) }

FUNCTION instantiate(level, x, env : ptr) : ptr;
BEGIN x:=lookup(cons(level, x), env);
    IF atom(cdr(x)) THEN instantiate:=cdr(x)
    ELSE instantiate:=cons(instantiate(car(x), car(cdr(x)), env),
                           instantiate(car(x), cdr(cdr(x)), env));
END;

FUNCTION pread(to_prove, env, level : ptr) : ptr;
BEGIN env:=unify(current_level(to_prove),
        second(first_goal(to_prove)), level, lread, env);
    IF env<>nill THEN pread:=
        search_database(but_first_goal(to_prove), env,
            numbercons(level^.val+1))
    ELSE pread:=nill;
END;

FUNCTION pwrite(to_prove, env, level : ptr) : ptr;
BEGIN lprint(instantiate(current_level(to_prove),
                         second(first_goal(to_prove)), env));
    writeln;
    pwrite:=search_database(but_first_goal(to_prove), env, level);
END;

FUNCTION assert(to_prove, env, level : ptr) : ptr;
BEGIN global_database:=append(instantiate(current_level(to_prove),
        rest(first_goal(to_prove)), env), global_database);
    mark(garbage);  
    assert:=search_database(but_first_goal(to_prove), env, level); 
END;

FUNCTION is_eval_predicate{(functor : ptr) : Boolean};
BEGIN WITH functor^ DO is_eval_predicate:=
    ((pname^=read_pname) or (pname^=writeln_pname) or (pname^=assert_pname));
END;

FUNCTION apply{(functor, to_prove, env, level : ptr) : ptr}; 
BEGIN IF functor^.pname^=read_pname THEN apply:=pread(to_prove, env, level)
    ELSE IF functor^.pname^=writeln_pname THEN apply:=pwrite(to_prove,env,level)
    ELSE IF functor^.pname^=assert_pname THEN apply:=assert(to_prove,env,level);
END; 

{ ---------- Main Loop }

PROCEDURE doing_it;
BEGIN
    WHILE True DO BEGIN write('Prolog> '); 
        expr:=lread;
        temp:=car(expr);
        IF temp^.pname^=prove_pname THEN temp:=prove(cdr(expr))
            ELSE BEGIN lprint(temp); error('Input R!!!'); END; 
        release(garbage); 
        writeln;
    END;
END;
  


BEGIN 
    connect(init,'(tomas)INIT','PLG','R'); (* N-100 I/O *)
    reset(init);
    endline:=False; bufferchar:=empty;
    nill:=symbolcons(nil_pname);
    global_database:=nill;
    mark(garbage); 
 1: WHILE true DO doing_it ;

END.

{
 (prove (assert
    ((t))
    ((= ?x ?x))
    ((remove ?x (?x . ?l) ?l))
    ((remove ?x (?y . ?l1) (?y . ?l2)) (remove ?x ?l1 ?l2))
    ((append nil ?x ?x))
    ((append (?x . ?y) ?z (?x . ?u))(append ?y ?z ?u))
    ((member ?x (?x . ?y)))
    ((member ?x (?a . ?y))(member ?x ?y)))
    (writeln (V{lkommen till Prolog!))
    (nil))
}