;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; File:         prolog.el
; Description:  prolog-style search procedure with continuations
; Author:       Jed Krohnfeldt / Craig Steury, University of Utah
; Created:      5-Aug-86
; Language:     Emacs Lisp
; Package:      FROLIC
; RCS           $Header: /usr/home/baccala/Frolic/RCS/prolog.el,v 1.4 1996/03/02 15:30:56 baccala Exp baccala $
;
; (c) Copyright 1986, 1987, University of Utah, all rights reserved.
;
; Ported to Emacs Lisp, 1996, by Brent Baccala
; Requires Common Lisp library (cl.elc) to be loaded
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; This program combines propositional search and unification to achieve a
; predicate-calculus search capability as in Prolog.
; This version of the program implements backtracking and the cut operator
; using a tail-recursive algorithm, implemented with continuations.
; Continuations capture the current state of a computation in such a form
; that it can be restarted at a later time, such as for backtracking to 
; Prolog choice points.
;
; Prolog rules are created with:  (*- head body body ...) - body may be empty
; Prolog queries are posed with:  (q- goal goal ...)
;
; * logical variables are preceeded with an underscore (_)
; * a lisp predicate in the body of a rule is preceded with up-arrow (^)
;   a lisp predicate succeeds if it returns non-nil, and fails otherwise
; * logical variables may be used in lisp predicates provided they are bound
;   by a prolog clause prior to their use - example (q- (foo _x) ^(equal _x 2))
; * use solve-one, solve-next, solve-rest, solve-all to return prolog
;   bindings to lisp
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(setf *print-circle* t)
(proclaim '(optimize (speed 3)))

(defvar *impossible*          'no "make impossible look nice")
(defvar *solved*             'yes "make solved look nice")
(defvar *interactive*           t "true iff interacting with user")
(defvar *auto-backtrack*      nil "return all solutions if true")
(defvar *last-continuation*   nil "saved state of the system")
(defvar *tracing*             nil "if t, tracing is turned on")
(defvar *debug*               nil "if t, debugging is turned on")
(defvar *questions*           nil "if t, questions are turned on")
(defvar *all-continuations*   nil "list of all continuations")
(defvar *lips*                  0 "logical inferences per second")
(defvar *trail*               nil "the trail, for backtracking")
(defvar *x-env*               nil "env for goals")
(defvar *y-env*               nil "env for rules")
(defvar *top-level-envs*      nil "saves top-level environments")
(defvar *top-level-vars*      nil "saves top-level variable names")
(defvar *num-slots*            -1 "number of logical variables in a query")

(defvar *prolog-rules*  (make-hash-table) "hash table for prolog rule heads")

;; rule selector functions

(defmacro head (rule)
  `(car ,rule))

(defmacro body (rule)
  `(cdr ,rule))

(defmacro functor (term)
  `(cond ((consp ,term) (car ,term))
	 ((vectorp ,term) (aref ,term 1))
	 (t ,term)))

(defmacro principal-functor (rule)
  `(functor (head ,rule)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Contunuations (vector version - faster than defstructs).
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defmacro make-cont (goals rules level back trail trace)
  `(vector 'cont ,goals ,rules ,level ,back ,trail ,trace))

(defmacro cont-goals (cont)
  `(aref ,cont 1))

(defmacro cont-rules (cont)
  `(aref ,cont 2))

(defmacro cont-level (cont)
  `(aref ,cont 3))

(defmacro cont-back (cont)
  `(aref ,cont 4))

(defmacro cont-trail (cont)
  `(aref ,cont 5))

(defmacro cont-trace (cont)
  `(aref ,cont 6))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Molecules - a molecule consists of a skeleton and an environment
; occurences of logical variables in the skeleton point to the environment
; (vector version - faster than defstructs).
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defmacro make-molecule (skel env)
  `(vector 'molecule ,skel ,env))

(defmacro molecule-p (exp)
  `(and (vectorp ,exp)
	(not (stringp ,exp))
	(eq (aref ,exp 0) 'molecule)))

(defmacro mol-skel (molecule)
  `(aref ,molecule 1))

(defmacro mol-env (molecule)
  `(aref ,molecule 2))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Random macros.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Take bindings apart.

(defmacro lhs (binding)
  `(car ,binding))

(defmacro rhs (binding)
  `(cdr ,binding))

;; Predicates for variables, atoms, and failure conditions.

(defmacro is-var-name (x)
  `(char-equal ?_ (aref (symbol-name ,x) 0)))

;; Test for anonymous logical variable - assumes logcial variable

(defmacro is-anon-var-name (x)
  `(char-equal ?_ (aref (symbol-name ,x) 1)))

;; A var looks like (*var* name index env) where name is the logical variable
;; name, and index is the index of the variable's value in the environment
;; (vars are contained in skeletons).

(defmacro is-var (x)
  `(and (consp ,x) (eq (car ,x) '*var*)))

(defmacro var-name (x)
  `(cadr ,x))

(defmacro var-index (x)
  `(caddr ,x))

(defmacro var-env (x)
  `(cadddr ,x))

(defmacro is-anon-var (x)
  `(eq (var-name ,x) '__))

(defmacro lookup-var (var env)
  `(aref ,env (var-index ,var)))

(defmacro make-empty-environment (size)
  `(make-vector ,size 'lisp::*undefined*))

(defmacro is-impossible (env)
  `(eq ,env *impossible*))

(defmacro is-cut (goal)
  `(and (molecule-p ,goal) (eq (functor (mol-skel ,goal)) 'cut)))

(defmacro is-unify (goal)
  `(and (molecule-p ,goal) (eq (functor (mol-skel ,goal)) '=)))

(defmacro is-level-tag (goal)
  `(eq ,goal '*level-tag*))

(defmacro is-pl-bound (x)
  `(not (eq ,x 'lisp::*undefined*)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Binding and the trail.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Bind logical variable x to y and push it on the trail.

(defun pl-bind (x x-env y y-env)
  (or (is-anon-var x)
      (progn
	(push (cons x-env (var-index x)) *trail*)
	(setf (lookup-var x x-env)
	      (if (atom y) y (make-molecule y y-env))))))

;; Undo the trail bindings back to the last choice point (mark).

(defun unbind-var (binding)
  (setf (aref (car binding) (cdr binding)) 'lisp::*undefined*))

(defun untrail (mark)
  (declare (inline unbind-var))
  (loop
    (if (eq *trail* mark)
      (return)
      (unbind-var (pop *trail*)))))

(defmacro rule-head (molecule)
  `(head (mol-skel ,molecule)))

(defmacro rule-body (molecule)
  `(body (mol-skel ,molecule)))

(defmacro rule-env (molecule)
  `(mol-env ,molecule))

(defmacro goal-env (goal)
  `(mol-env ,goal))

(defmacro goal-body (goal)
  `(mol-skel ,goal))

(defmacro goal-functor (goal)
  `(if ,goal (functor (mol-skel ,goal)) ,goal))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Hooks to common lisp.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; This is Common LISP code that alters LISP read syntax to make "^" and "^^"
;; resolve to *lisp-query* and *lisp-hook* forms, respectively.
;;
;; ELISP does not support changing the LISP read syntax, so the code is
;; useless.  ELISP users just have to type out (*lisp-query* ...) when
;; they want to use it.

;; (defun lisp-hook-reader (stream char)
;;   (declare (ignore char))
;;   (let ((c (read-char stream)))
;;     (if (char-equal c ?^)
;;       (list '*lisp-hook* (read stream t nil t))
;;       (progn
;; 	(unread-char c stream)
;; 	(list '*lisp-query* (read stream t nil t))))))
;; 
;; (set-macro-character ?^ 'lisp-hook-reader)



(defmacro is-lisp-hook (goal)
  `(and (consp ,goal) (eq (car ,goal) '*lisp-hook*)))

(defmacro is-lisp-hook-mol (goal)
  `(and (molecule-p ,goal) (is-lisp-hook (mol-skel ,goal))))

(defmacro is-lisp-query (goal)
  `(and (consp ,goal) (eq (car ,goal) '*lisp-query*)))

(defmacro is-lisp-query-mol (goal)
  `(and (molecule-p ,goal) (is-lisp-query (mol-skel ,goal))))

(defmacro is-lisp-requery (goal)
  `(and (consp ,goal) (consp (car ,goal)) (eq (caar ,goal) '*lisp-requery*)))

(defmacro is-lisp-requery-mol (goal)
  `(and (molecule-p ,goal) (is-lisp-requery (mol-skel ,goal))))

(defun make-requery-goal (goal state)
  (and (or (is-lisp-query-mol goal) (is-lisp-requery-mol goal))
       (make-molecule (cons (list '*lisp-requery* state)
			    (cdr (mol-skel goal)))
		      (mol-env goal)) ))

;; Scan the form, replacing all logical variables with their values in the
;; given environment.  The optional variable "query" is true if we are
;; expanding in order to print the top level query solution.  In this case,
;; we don't want to print the internal representation of logical variables.

(defun expand-logical-vars (exp env &optional query)
  (cond ((null exp) nil)
	((is-var exp)
	 (if (is-anon-var exp)
	   '__
	   ; deref in goal environment
	   (let ((val (x-view-var exp env)))
	     (if (eq val exp)
	       (if query
		 ; pretty-print logical vars
		 (cadr exp)
		 exp)
	       ; use new environment
	       (expand-logical-vars val *x-env* query)))))
	((molecule-p exp) (expand-logical-vars (mol-skel exp) (mol-env exp)))
	((stringp exp) exp)
        ;; Horrible nasty hack.  Because structures are also vectors,
        ;; this was causing an infinite loop walking down the vector
        ;; associated with structures.  So, this hack tests to see if
        ;; the type-of the exp is a symbol (possibly denoting a
        ;; structure), and then checks to see if it is a FROB.  That
        ;; way, even if frobs isn't loaded, this will still work.
        ;; Geez, what a hack.
        ((and (symbolp (type-of exp))
              (string= (symbol-name (type-of exp)) "FROB"))
         exp)
	((vectorp exp)
         ;; Added because in debugging mode we get different answers
         ;; than in non debugging mode.
         (if query (setq exp (copy-seq exp)))
	 (dotimes (i (length exp) exp)
	   (setf (aref exp i)
		 (expand-logical-vars (aref exp i) env query))))
	((atom exp) exp)
	(t (cons (expand-logical-vars (car exp) env query)
		 (expand-logical-vars (cdr exp) env query)))))

;; Execute a lisp hook form and return the environment handles multiple
;; values returned from the Lisp expression.

(defun do-lisp-hook (molecule)
  (let* ((skel (mol-skel molecule))
	 (env (mol-env molecule))
	 (expanded-form (expand-logical-vars (cadr skel) env)))
    (if (null (eval expanded-form))
      *impossible*
      t)))

(defun get-lisp-hook-values (hook env)
  (let ((expanded-form (expand-logical-vars (cadr hook) env))
	(values nil))
    (setf values (multiple-value-list (eval expanded-form)))
    (if (member *impossible* values)
      *impossible*
      values)))

;; The REPEAT clause - succeed everytime it is hit during a backtrack
;; The only way to get out of a REPEAT is to use a cut.  Ex:
;;
;; (*- (bwb5) (repeat)
;;            (*lisp-query* (setq x (1+ x)))
;;            (*lisp-query* (> x 10))
;;            (cut) )
;;
;; (setq x 0)
;; 0
;;
;; (qq- (bwb5))
;; yesno
;;
;; x
;; 11

(defmacro is-repeat (goal)
  `(and (molecule-p ,goal) (eq (functor (mol-skel ,goal)) 'repeat)))

;; The IS clause - unification on variables returned from calls to Lisp.
;; The general form is (is _v1 ... _vn ^(lisp-hook)).
;; Binds the _vi variables to the values returned from (lisp-hook).

(defmacro is-is (goal)
  `(and (molecule-p ,goal) (eq (functor (mol-skel ,goal)) 'is)))

(defmacro is-reis (goal)
  `(and (molecule-p ,goal) (eq (functor (functor (mol-skel ,goal))) '*reis*)))

(defun make-reis-goal (goal state)
  (and (or (is-is goal) (is-reis goal))
       (make-molecule (cons (list '*reis* state)
			    (cdr (mol-skel goal)))
		      (mol-env goal)) ))

(defun do-is (molecule)
  (let ((goal (mol-skel molecule))
	(env (mol-env molecule)) 
	(hook nil) (vars nil)
	(retvals nil) (return-env t))
    ; collect all of the logical variables
    (dolist (elt (cdr goal))
      (if (is-lisp-query elt)
	(setf hook elt)
	(push elt vars)))
    ; run the lisp hook function
    (if (is-lisp-query hook)
      (setf retvals (get-lisp-hook-values hook env))
      (error "IS clause must have a Lisp hook (%S)" goal))
    ; unify the results with the IS arguments 
    (cond ((eq *impossible* retvals)
	   (setf return-env *impossible*))
          ((< (length retvals) (length vars))
	   (error "IS: lisp-hook returns too few values (%S)" goal))
	  (t (dolist (var (nreverse vars))
	       (setf return-env (unify var env (pop retvals) env))
	       (if (is-impossible return-env) (return return-env)))))
    return-env))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Continuations - a continuation captures the state of prolog, saving the
; binding environment (env), goal list (goals), rule list (rules),
; unification level (level), the current continuation or choice point (back)
; and the goal trace (trace) for debugging purposes.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Predicates for dealing with functors.

(defmacro get-prolog-rules (functor)
  `(gethash ,functor *prolog-rules*))

(defmacro get-env (functor)
  `(cdr (get ,functor 'environment)))

(defmacro get-env-size (functor)
  `(car (get ,functor 'environment)))

(defmacro set-env (functor env)
  `(setf (get ,functor 'environment) (if ,env (cons (length ,env) ,env))))

(defmacro put-prolog-rules (functor rules)
  `(setf (gethash ,functor *prolog-rules*) ,rules))

(defmacro remove-prolog-rules (functor)
  `(progn
     (remhash ,functor *prolog-rules*)
     (set-env ,functor nil)))

(defmacro all-prolog-rules ()
  `(let ((result nil))
     (maphash '(lambda (key val)
		  (declare (ignore key))
		  (setf result (append val result))) *prolog-rules*)
     result))

(defmacro remove-all-prolog-rules ()
  `(progn
     (maphash '(lambda (key val)
		  (declare (ignore val))
		  (set-env key nil)) *prolog-rules*)
     (clrhash *prolog-rules*)))

;; Rule indexing.

(defun index-rule (skeleton num-vars)
  (let ((func (principal-functor skeleton)))
    (if (symbolp func)
      (add-rule-to-index skeleton func num-vars))))

;; Add a rule to prolog.  Each skeleton is paired with the number of
;; variables in its environment, so new environments can be built easily.

(defun add-rule-to-index (skeleton functor num-vars)
  (put-prolog-rules functor (append (get-prolog-rules functor)
				    (list (cons skeleton num-vars))))
  skeleton)

(defun rule-part (rule-pair) (car rule-pair))
(defun num-vars (rule) (cdr rule))

;; Construct environments for top-level goals.

(defun build-molecule (skeleton)
  (make-molecule (rule-part skeleton)
		  (make-empty-environment (num-vars skeleton))))

(defun make-goals (goals)
  (setf *num-slots* -1)
  (do ((goal-list goals (cdr goal-list))
       (acc-env nil)
       (result nil))
      ((null goal-list)
       (progn
	 (setf *top-level-vars* (nreverse acc-env))
	 (let ((g-env (make-empty-environment (1+ *num-slots*))))
	   (setf *top-level-envs* g-env)
	   (nreverse
	    (mapcar '(lambda (x)
			(make-molecule x g-env))
		    result)))))
      ;; make goal skeleton
      (let* ((env (list acc-env))
	     (skel (calcify (first goal-list) env)))
	(setf acc-env (car env))
	(push skel result))))


;; Attempt to solve a list of goals with respect to rule-base.

(defun pl-solve (goals)
  (setf *all-continuations* nil)
  (setf *top-level-vars* nil)
  (setf *top-level-envs* nil)
  (setf *trail* nil)
  (pl-search (make-goals goals) 0 nil))

;; Search to solve goals in possible environment.

(defun pl-search (goals level back)
  (search-rules goals
    (get-rule-molecules (goal-functor (first goals))) level back))

;; Called when a goal successfully matched a rule or fact in the database
;; (used for I/O and debugging).
;;
;; The commented out "prin1"s don't expand the logical variables.
;; I was hoping this would let me see the original form of the rule,
;; but it doesn't always work.

(defun succeed-trace (goal rule back)
  (if *tracing*
    (progn
      (princ "Goal: ")
;     (prin1 (filter-vars (mol-skel rule)))
      (prin1 (expand-logical-vars (mol-skel goal) (mol-env goal) t))
      (princ "\n")
      (if rule
	(if (molecule-p rule)
	  (progn
	    (princ "Rule: (*- ")
;	    (prin1 (filter-vars (mol-skel rule)))
	    (prin1 (expand-logical-vars (mol-skel rule) (mol-env rule) t))
	    (princ "\n"))
	  (princ "Fact: ")
	  (prin1 rule)
	  (princ "\n")))))
  )
  ;(if (and *questions* back)
  ;  (progn
  ;    (setf (cont-trace back)
  ;	    (append (cont-trace back) (cons goal (if rule rule))))
  ;    (push back *all-continuations*))))

(defun succeed-continue (goal goals rule level back)
  (declare (ignore goal rule))
  (succeed-trace goal rule back)
  ; pop level tags off top of goal stack and adjust level accordingly
  (loop
    (if (is-level-tag (car goals))
      (progn
	(decf level)
	(pop goals))
      (return)))
  (pl-search goals level back))

;; Called when a goal fails to match a rule or fact in the database
;; (used for I/O, debugging).

(defun fail-trace (goal)
  (when *tracing*
    (princ "Goal: ")
    (prin1 (expand-logical-vars (mol-skel goal) (mol-env goal) t))
    (princ " fails...\n")))

(defmacro fail-continue (goal back)
  ;(declare (ignore goal))
  `(progn (fail-trace ,goal)
          (continue-on ,back)))

;; Attempt to match a goal against rules in the database.

(defun search-rules (goals rules level back)
  (declare (inline succeed-continue))
  (let ((goal (first goals)))
    (cond ((null goals) (succeed back))

	  ; goal is a call to unify (=)
	  ((is-unify goal)
	   (if (is-impossible (do-unify goal))
	     (fail-continue goal back)
	     (succeed-continue goal (rest goals) nil level back)))

	  ; goal is a prolog "cut" clause
	  ((is-cut goal)
	   (succeed-continue goal (rest goals) nil level (do-cut back level)))

	  ; goal is a "repeat" clause
	  ((is-repeat goal)
	   (succeed-continue
	    goal (rest goals) nil level
	    (make-cont goals rules level back *trail* nil)))

	  ; goal is a common lisp hook - always succeeds
	  ((is-lisp-hook-mol goal)
	   (do-lisp-hook goal)
	   (succeed-continue goal (rest goals) nil level back))

	  ; goal is a common lisp query
	  ;
	  ; We set the LISP variable *lisp-hook-state* to nil, then check it
	  ; on return.  If it's been changed, we need to make a continuation
	  ; here, save the variable's value, and succeed, leaving a requery
	  ; on the top of that continuation's goal list.  When we
	  ; fail back to here later, we re-invoke the LISP function,
	  ; with *lisp-hook-state* set up, and save it's new value again
	  ; in a new continuation.
	  ; We keep this up until the function returns nil.  Ex:
	  ;
	  ; (*- (bwb9) (*lisp-query*
	  ;             (print (setq *lisp-hook-state*
	  ;                           (cond ((null *lisp-hook-state*) 0)
	  ;				    ((>= *lisp-hook-state* 10) nil)
	  ;				    (t (1+ *lisp-hook-state*))) ))))
	  ; (qq- (bwb9))
	  ; 0
	  ; yes
	  ; 1
	  ; yes
	  ; 2
	  ; ...
	  ; yes
	  ; 10
	  ; yes
	  ; nil
	  ; no

	  ;
	  ; Three cases:
	  ;   - do-lisp-hook fails by returning *impossible*
	  ;     Normal failure
	  ;   - do-lisp-hook succeeds but leaves *lisp-hook-state* nil
	  ;     Normal success
	  ;   - do-lisp-hook succeeds and leaves *lisp-hook-state* non-nil
	  ;     Success with backtracking enabled - make a continuation
	  ;
	  ((is-lisp-query-mol goal)
	   (let ((*lisp-hook-state* nil)
		 (*old-trail* *trail*))
	     (cond ((is-impossible (do-lisp-hook goal))
		    (fail-continue goal back))
		   (*lisp-hook-state*
		    (succeed-continue
		     goal (rest goals) nil level
		     (make-cont (cons
				 (make-requery-goal goal *lisp-hook-state*)
				 (rest goals))
				rules level back *old-trail* nil) ))
		   (t
		    (succeed-continue goal (rest goals) nil level back)))))

	  ; goal is a common lisp requery
	  ;
	  ; a requery is when we backtrack to a continuable LISP query
	  ((is-lisp-requery-mol goal)
	   (let ((*lisp-hook-state* (cadar (mol-skel goal)))
		 (*old-trail* *trail*))
	     (cond ((is-impossible (do-lisp-hook goal))
		    (fail-continue goal back))
		   (*lisp-hook-state*
		    (succeed-continue
		     goal (rest goals) nil level
		     (make-cont (cons
				 (make-requery-goal goal *lisp-hook-state*)
				 (rest goals))
				rules level back *old-trail* nil) ))
		   (t
		    (succeed-continue goal (rest goals) nil level back)))))

	  ; goal is an "is" clause
	  ((is-is goal)
	   (let ((*lisp-hook-state* nil)
		 (*old-trail* *trail*))
	     (cond ((is-impossible (do-is goal))
		    (fail-continue goal back))
		   (*lisp-hook-state*
		    (succeed-continue
		     goal (rest goals) nil level
		     (make-cont (cons
				 (make-reis-goal goal *lisp-hook-state*)
				 (rest goals))
				rules level back *old-trail* nil) ))
		   (t
		    (succeed-continue goal (rest goals) nil level back)))))

	  ; goal is a reis
	  ((is-reis goal)
	   (let ((*lisp-hook-state* (cadar (mol-skel goal)))
		 (*old-trail* *trail*))
	     (cond ((is-impossible (do-is goal))
		    (fail-continue goal back))
		   (*lisp-hook-state*
		    (succeed-continue
		     goal (rest goals) nil level
		     (make-cont (cons
				 (make-reis-goal goal *lisp-hook-state*)
				 (rest goals))
				rules level back *old-trail* nil) ))
		   (t
		    (succeed-continue goal (rest goals) nil level back)))))

          ; goal is a variable, check to see if it is bound to a
          ; molecule and if so, try to solve it instead.
          ; RRK -- I am not sure that this is right.  It makes not
          ; seem to work correctly, but it really seems like an
          ; improper fix.  Oh well.  Hope it doesn't break something
          ; else. 
          ((and (molecule-p goal) (is-var (mol-skel goal)))
           (let ((var-val (lookup-var (mol-skel goal) (mol-env goal))))
             (if (molecule-p var-val)
               (pl-search (cons var-val (cdr goals)) level back)
               (fail-continue goal back))))

	  ; otherwise, goal is a general prolog goal
	  ((match-rule-head goal goals rules level back)))))

;; Match a goal against the pending rules.  NOTE that the result of this
;; function is nconc'ed in match-rule-head.

(defun new-goals (molecule)
  (let ((env (rule-env molecule)))
    (do ((goals (rule-body molecule) (cdr goals))
	 (result nil))
	((null goals) (nreverse result))
      (push (make-molecule (first goals)
			   env)
	    result))))

(defun match-rule-head (goal goals pending-rules level back)
  (declare (inline succeed-continue))
  (do ((rules pending-rules (rest rules))
       (old-trail *trail*))
      ((null rules) (fail-continue goal back))
    (if (not (is-impossible (unify (goal-body goal) (goal-env goal)
				 (rule-head (first rules))
				 (rule-env (first rules)))))
      (let ((new-goals (new-goals (first rules))))
	(incf *lips*)
	(return
	 (succeed-continue
	  goal
	  (nconc new-goals (cons '*level-tag* (rest goals)))
	  (first rules)
	  (1+ level)
	  (make-cont goals		    ; goals
		     (rest rules)	    ; rules
		     level		    ; level
		     back		    ; back
		     old-trail		    ; trail
		     nil)))))))		    ; trace

;; Continue searching with continuation - used to backtrack to a choice
;; point and continue executing.

(defun continue-on (cont)
  (if (null cont)
    *impossible*
    (if (null (cont-goals cont))
      (continue-on (cont-back cont))
      (progn
	; wrap trail back to last choice point, undoing bindings
	(untrail (cont-trail cont))
	; resume search
	(search-rules (cont-goals cont) (cont-rules cont)
		      (cont-level cont) (cont-back cont))))))

;; Remove alternatives from a continuation - used to strip away pending
;; goals when a cut operator is executed.

(defun remove-alternatives (cont level)
  (if cont
    (make-cont (cont-goals cont)	    ; goals
	       nil			    ; rules
	       level			    ; level 
	       (cont-back cont)		    ; back
	       (cont-trail cont)	    ; trail
	       nil)))			    ; trace

;; Perform a cut operation.
;;
;; Skip over all the continuations on the current level, then remove
;; the alternatives from the last continuation on the level before
;; this one.

(defun do-cut (cont level)
  (if cont
    (if (= (- level 1) (cont-level cont))
      (remove-alternatives cont level)
      (do-cut (cont-back cont) level))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Unification functions.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Explicit call to unify (= lhs rhs) - unify lhs with rhs.

(defun do-unify (goal)
  (let* ((skel (mol-skel goal))
	 (env (mol-env goal))
	 (lhs (cadr skel))
	 (rhs (caddr skel)))
    (unify (expand-lisp-hooks lhs env) env (expand-lisp-hooks rhs env) env)))

;; If term is a lisp-query, it is evaluated and its result returned; if not,
;; it is simply returned.

(defun expand-lisp-hooks (term env)
  (if (is-lisp-query term)
    (let ((expanded-form (expand-logical-vars (cadr term) env)))
      (eval expanded-form))
    term))

;; Dereference to find ultimate binding of a logical variable in the goal
;; environment.

(defun x-view-var (x env)
  (cond ((is-var x)
	 (if (is-anon-var x)
	   x
	   (let ((val (lookup-var x env)))
	     (if (is-pl-bound val)
	       (x-view-var val env)
	       x))))
	((molecule-p x)
	 (x-view-var (mol-skel x) (setq *x-env* (mol-env x))))
	(t x)))

(defun y-view-var (y env)
  (cond ((is-var y)
	 (if (is-anon-var y)
	   y
	   (let ((val (lookup-var y env)))
	     (if (is-pl-bound val)
	       (y-view-var val env)
	       y))))
	((molecule-p y)
	 (y-view-var (mol-skel y) (setq *y-env* (mol-env y))))
	(t y)))

;; Unify - unification, returns environment in which x and y are unified.
;; Unify sets up environments and trail, and cleans up on failure.

(defun unify (x x-env y y-env)
  (let ((save-trail *trail*) (ans nil))
    (setf *x-env* x-env)			  ;goal environment
    (setf *y-env* y-env)			  ;rule environment
    (if (is-impossible (setf ans (unify1 x y))) (untrail save-trail))
    ans))

;; Unify1 dereferences variables in their environments.

(defun unify1 (x y)
  (unify2 (x-view-var x *x-env*) (y-view-var y *y-env*)))

;; Unify2 is the main unification routine.

(defun unify2 (x y)
  (declare (inline pl-bind))
  (cond ((is-var x) (pl-bind x *x-env* y *y-env*))
        ; bind variables if distinct
        ((is-var y) (pl-bind y *y-env* x *x-env*))
        ; unify atoms 
        ((atom x) (if (equalp x y) t *impossible*))
        ((atom y) *impossible*)
        ; both terms complex
        ((let ((x-env *x-env*)
	       (y-env *y-env*))
	   (if (is-impossible (unify1 (car x) (car y)))
	     *impossible*
	     (progn
	       (setf *x-env* x-env)
	       (setf *y-env* y-env)
	       (unify1 (cdr x) (cdr y))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Success and failure display functions.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Success - report solutions to user.

(defun succeed (back)
  (when *interactive*
    (show-bindings *top-level-vars*
		   *top-level-envs*))
  (setf *last-continuation* back)
  ; query the user if more
  (if (or *auto-backtrack* (and *interactive* (y-or-n-p "is-More ")))
    ; force failure to get more solutions
    (let* ((save-binding-list
            (build-binding-list *top-level-vars* *top-level-envs*))
           (ans (continue-on back)))
      (if (is-impossible ans)
        (if *interactive* 
          ans
          (list save-binding-list))
        (append (list save-binding-list)
		ans)))
    (if (not *interactive*) 
      (build-binding-list *top-level-vars* *top-level-envs*))))

;; Build a list of the bindings.

(defun build-binding-list (vars env)
  (let ((result nil))
    (mapc '(lambda (x)
	      (push (cons (car x) (expand-logical-vars (cdr x) env t)) result))
	  vars)
    (if result (nreverse result) t)))

;; Show result bindings (bindings of goal variables).

(defun show-bindings (vars envs)
  (let ((bindings (build-binding-list vars envs)))
    (terpri)
    (if (atom bindings)
      (prin1 *solved*)
      (mapc 'show-one-binding bindings))))

(defun show-one-binding (binding)
  (prin1 (lhs binding))
  (princ " = ")
  (prin1 (rhs binding))
  (princ "\n"))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Molecule and skeleton building forms - for rules.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun get-rule-molecules (functor)
  (let ((skeletons (get-prolog-rules functor)))
    (mapcar 'build-molecule skeletons)))

(defmacro add-new-var (var vars)
  `(append ,vars (list (cons ,var (incf *num-slots*)))))


;;; Calcify returns form with all logical variables replaced with a vectorized
;;; representation.  env is destructively modified.  It is expected to be input
;;; in the form ((env-a-list)).  Note that the input environment is not
;;; necessarily nil, as in the case when a series of input goals are calcified
;;; and must share an environment.

(defun calcify (form alist)
  (cond ((null form) nil)
	((symbolp form)
	  (if (is-var-name form)
	    (if (is-anon-var-name form)
	      '(*var* __ -1)
	      (let ((slot (assoc form (car alist))))
		(if (not slot)
		  (let ((nv `(,form . (*var* ,form ,(incf *num-slots*)))))
		    ; destructively modify alist
		    (push nv (car alist))
		    (setf slot nv)))
		; return new rep for var
		(cdr slot)))
	    form))
	((stringp form) form)
	((vectorp form)
	 (dotimes (i (length form) form)
	   (setf (aref form i) (calcify (aref form i) alist))))
	((atom form) form)
	(t (cons (calcify (car form) alist)
		 (calcify (cdr form) alist)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Assert and solve - lisp calls to prolog.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Add a rule to the database.

;; Destructively modify a rule to produce a skeleton rule.  Each logical
;; variable is converted to a pointer into the environment.
;; Calcify returns the environment structure created for the rule.

(defun pl-assert (rule)
  (let ((env (list nil)))
    (setf *num-slots* -1)
    (index-rule (calcify rule env) (1+ *num-slots*))
    rule))

;; Makes sure lisp gets nil on failure instead of *impossible*.

(defmacro filter-no (value)
  `(let ((retval ,value))
     (if (is-impossible retval) nil retval)))

;; Return the first solution to the query, setting *last-continuation* so
;; that subsequent calls to solve-next can get other solutions - the return
;; value is an environment, an alist with (var . binding) pairs.

(defun pl-solve-one (goals)
  (setf *interactive* nil)
  (setf *auto-backtrack* nil)
  (filter-no (pl-solve goals)))

;; Return the next solution, using *last-continuation* (the continuation
;; from the most recent pl-solve-one or pl-solve-cc) or the optional
;; continuation provided.

(defun pl-solve-next (&optional cont)
  (if (null cont) (setq cont '*last-continuation*))
  (setf *interactive* nil)
  (setf *auto-backtrack* nil)
  (filter-no (continue-on cont)))

;; Return the rest of the solutions, using *last-continuation* (the
;; continuation from the most recent pl-solve-one or pl-solve-cc) or the
;; optional continuation provided.

(defun pl-solve-rest (&optional cont)
  (if (null cont) (setq cont '*last-continuation*))
  (setf *interactive* nil)
  (setf *auto-backtrack* t)
  (filter-no (continue-on cont)))

;; Return all solutions to the query - the return value is a list of
;; environments (env env ...) where each environment is a
;; ((var . binding)...) alist.

(defun pl-solve-all (goals)
  (setf *interactive* nil)
  (setf *auto-backtrack* t)
  (filter-no (pl-solve goals)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; User interaction.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Interactive version of assert
;; (used to be called :- but common lisp thinks :- is a keyword).

;;; RRK -- Fixed a problem that the vectors in the body of the rules
;;; were getting allocated into bps space.  Then when a destructive
;;; operation occured, the new items were never traced.  This copies
;;; all of those vectors out into the real heap space (but only the
;;; vectors). 

(defmacro *- (lhs &rest rhs)
  `(let ((rule (cons ',lhs (magic-copy ',rhs))))
     (pl-assert rule)))

;;; Copies the top level sequences.

(defun magic-copy (some-list)
  (mapcar '(lambda (element)
              (if (vectorp element) (copy-seq element) element))
          some-list))

;; Interactive version of pl-solve-one.

(defmacro q- (&rest goals)
  `(progn
     (setf *interactive* t)
     (setf *auto-backtrack* nil)
     (pl-solve ',goals)))

;; Interactive version of pl-solve-all.

(defmacro qq- (&rest goals)
  `(progn
     (setf *interactive* t)
     (setf *auto-backtrack* t)
     (pl-solve ',goals)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Rule and database manipulation and printing.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Remove all rules from the database.

(defun clear-rules (&optional functors)
  (if functors
    (dolist (functor functors)
      (remove-prolog-rules functor))
    ; clear rule index
    (remove-all-prolog-rules))
  t)

;; Print all rules, or rules with the given principal functor.

(defun print-rules (&optional functors)
  (if (null functors)
    (maphash '(lambda (key value)
		 (declare (ignore value))
		 (print-rule key))
	     *prolog-rules*)
    (dolist (functor functors)
      (print-rule functor))))

(defun print-rule (functor)
  (let ((rules (get-prolog-rules functor)))
    (when rules
      (prin1 functor)
      (princ ":\n")
      (dolist (rule rules)
	(pp-rule (car rule))))))

;; Prettyprint a single rule.

(defun pp-rule (rule)
  (let ((head (head rule))
	(body (body rule)))
    (if body
      (progn
       (princ "  (* - ")
       (prin1 (filter-vars head))
       (dolist (form body)
	 (cond ((is-lisp-query form)
		(princ "\n      ^")
		(prin1 (filter-vars (cadr form))))
	       ((is-lisp-hook form)
		(princ "\n      ^^")
		(prin1 (filter-vars (cadr form))))
	       (t
		(princ "\n      ")
		(prin1 (filter-vars form)))))
       (princ ")\n"))
      (princ "  (*- ")
      (prin1 (filter-vars head))
      (princ ")\n") )))

;; Change (*var* _x 0) to _x for rule printing.

(defun filter-vars (exp)
  (cond ((null exp) nil)
	((is-var exp) (cadr exp))
	((stringp exp) exp)
	((vectorp exp)
         (setf exp (copy-seq exp))
	 (dotimes (i (length exp) exp)
	   (setf (aref exp i) (filter-vars (aref exp i)))))
	((atom exp) exp)
	(t (cons (filter-vars (car exp))
		 (filter-vars (cdr exp))))))

;; Explain how the last query was solved.

(defun how ()
  (dolist (continuation (reverse *all-continuations*))
    (let* ((event (cont-trace continuation))
	   (rule (cdr event)))
      (princ "Goal: ")
      (prin1 (car event))
      (princ "\n")
      (if rule
	(if (listp rule)
	  (progn (princ "Rule: ")
		 (prin1 `(*- ,@rule))
		 (princ "\n"))
	  (progn (princ "Fact: ")
		 (prin1 rule)
		 (princ "\n")) )))))

;; End of file.
