ppicl.lisp

;;;  PORTABLE PROLOG INTERPRETER  by  H. Nakashima
;;;               ( Version 2 )        1983.04.09
;;;  Common Lisp Version               1988.11.21

(defvar cue nil "Goals to be executed")
(defvar clause nil "Body of a goal")
(defvar epilog nil "Switch to exit")
(defvar fetched-subst nil "The environment of the value of a variable")
(defvar goal nil "top-level goal")
(defvar new-subst nil "environment of the callee")
(defvar old-subst nil "environment of the caller")
(defvar undo-list nil "variables to be unbound on backtracking")

(defun prolog ()
  (print '(portable prolog (in common lisp)))
      (set-up)
      (loop (terpri)
	    (let ((goal (read))
		  (subst (cons nil nil)))
	      (let ((result
		     (refutes (cons goal nil) subst (cons nil nil) nil)))
		(if result
		    (print (fetch-value result subst))
		  (print nil)))
	      (if epilog (return 'epilog)))))

(defun define-clause (clause)
   (let ((definition (get (caar clause) 'prolog)))
      (cond ((null definition)
	     (setf (get (caar clause) 'prolog)
		   (cons clause nil)))
            (t (nconc definition (cons clause nil))))
      'defined))

(defun refutes (clause old-subst new-subst cue)
   (cond ((null clause)
          (cond ((null cue) goal)
                (t (refutes (car (first cue))
			    (cdr (first cue)) (cons nil nil) (cdr cue)))))
         ((and (var? clause) (assigned? clause old-subst))
          (refutes (fetch-value clause old-subst) fetched-subst new-subst cue))
         ((and (var? (first clause)) (assigned? (first clause) old-subst))
          (refutes
             (cons (fetch-value (first clause) old-subst) nil)
             fetched-subst
             new-subst
             (cons (cons (cdr clause) old-subst) cue)))
         (t (refute clause (get (caar clause) 'prolog)))))

(defun refute (clause definitions)
  (let ((undo-list nil))
    (cond ((null definitions)
	   (cond ((and (try-sys (car clause) old-subst)
		       (refutes (cdr clause) old-subst
				(cons nil nil) cue))
		  goal)
		 (t (undo undo-list))))
	  (t (resolve definitions)))))

(defun resolve (definitions)
   (cond ((null definitions) nil)
         ((and (unify (car clause) old-subst (caar definitions) new-subst)
               (refutes
                  (cdr (first definitions))
                  new-subst
                  (cons nil nil)
                  (cons (cons (cdr clause) old-subst) cue)))
          goal)
         (t (undo undo-list) (resolve (cdr definitions)))))
(defun undo (u)
   (cond ((null u) (setq undo-list nil))
         (t (rplacd (car u) (cddar u)) (undo (cdr u)))))
(defun try-sys (form subst)
   (cond ((get (car form) 'primitive)
          (apply (get (car form) 'primitive) (list (cdr form) subst)))
         (t nil)))
(defun set-up nil
   (setf (get 'assert 'primitive)
	 '(lambda (form subst)
	    (define-clause (fetch-value form subst))))
   (setf (get 'call 'primitive)
	 '(lambda (form subst)
	    (apply (fetch-value (first form) subst)
		   (mapcar '(lambda (x) (fetch-value x subst)) (cdr form)))
	    t))
   (setf (get 'end 'primitive)
	 '(lambda (form subst) (setq epilog t)))
   (setf (get 'eval 'primitive)
      '(lambda (form new-subst)
        (cond ((unify (apply (fetch-value (car (first form)) new-subst)
                             (mapcar '(lambda (x) (fetch-value x new-subst))
                                      (cdr (first form))))
                      new-subst
                      (second form)
                      new-subst)
               t)
              (t nil))))
   (setf (get 'if 'primitive)
      '(lambda (form subst)
        (cond ((refutes (first form) subst (cons nil nil) nil)
               (refutes (second form) subst (cons nil nil) cue))
              (t (refutes (third form) subst (cons nil nil) cue))))))

(defun unify (x x-subst y y-subst)
   (cond ((var? x)
          (cond ((assigned? x x-subst)
		 (unify (fetch x x-subst) fetched-subst y y-subst))
                (t (link x x-subst y y-subst))))
         ((var? y) (unify y y-subst x x-subst))
         ((atom x) (eq x y))
         ((atom y) nil)
         ((unify (car x) x-subst (car y) y-subst)
          (unify (cdr x) x-subst (cdr y) y-subst))
         (t nil)))

(defun var? (x)
  (and (symbolp x)
       (char= (aref (symbol-name x) 0) #\*)))

(defun assigned? (x subst) (assoc x (cdr subst)))
(defun fetch (x subst)
   (setq fetched-subst subst)
   (cond ((var? x)
	  (let ((v (assoc x (cdr subst))))
	    (cond ((null v) x)
		  (t (setq fetched-subst (cddr v))
		     (fetch (second v) (cddr v))))))
	 (t x)))
(defun fetch-value (x subst)
  (cond ((var? x)
	 (let ((v (assoc x (cdr subst))))
	   (cond ((null v) x)
		 (t (fetch-value (second v) (cddr v))))))
	((atom x) x)
	(t (cons (fetch-value (car x) subst) (fetch-value (cdr x) subst))
	   )))
(defun link (x x-subst y y-subst)
  (cond ((and (eq x y) (eq x-subst y-subst)) t)
	(t (setq undo-list 
		 (cons (rplacd x-subst
			       (cons (cons x
					   (cons (fetch y y-subst)
						 fetched-subst))
				     (cdr x-subst)))
		       undo-list)))))

;;; *EOF*