;;; Prof R. Williams
;;; Artificial Intelligence

(defvar *trace* nil)			; when set to t,
					;   shows how program runs
(defvar *avoid-loops* nil)		; default is to eliminate loop test
					;   for efficiency
(defvar *depth-limit* 10)		; depth limit to search to, used to
					;   avoid possible infinite recursion;
					;   nil means no depth limit

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The macro BC is a backward chainer.  It accepts as input any number of
; formulas which are to be simultaneously satisfied and uses backward
; chaining to find all valid substitutions for the query variables consistent
; with the global database of facts and rules.  It calls "retrieve", which
; in turn calls "extend-path". which recursively explores an appropriate
; tree for all solution paths (loop-free paths if *avoid-loops* is t) within
; search depth *depth-limit* and returns a list of the bindings of all
; variables used in the search.  Then "show-answers" is called to display
; all sets of bindings found for the query variables.  This program is an
; adaptation of a more general-purpose predicate calculus backward chaining
; program.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defmacro bc (&rest formulas)
  `(show-answers (retrieve '(and ,@formulas) *depth-limit*)))

(defun show-answers (answers)
  (cond ((null answers) (format t "Nothing satisfies that query.~%"))
	((equal answers (list nil)) (format t "That query is true."))
	(t (format t "Answers are:~%")
	   (dolist (ans answers 'done) (show-bindings ans)))
	))

(defun show-bindings (bindings)
  (dolist (bind bindings (format t "~%"))
    (format t "  ~a = ~a" (car bind) (cdr bind))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Code from here on down is adapted from a general-purpose predicate
; calculus backward chainer.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defstruct node				; data structure for nodes of tree
  bindings				; a-list of bindings of query variables
  goals					; list of goal formulas
  rule-number				; number of rule currently working on
  )

(defun retrieve (formula depth-limit)
  (let* ((start-node
	   (make-node
	     :bindings nil
	     :goals (goal-list formula)
	     :rule-number nil))
	 (vars (remove-duplicates (get-vars formula)))
	 (result
	   (extend-path start-node (append *facts* *bc-rules*)
			vars nil depth-limit))
	 )
    (remove-duplicates
      (mapcar #'(lambda (bindings)	; arrange in consistent order for
		  (sort-to-match-vars bindings vars)) ; better looking outpu
	      result)
      :test #'equal)
    ))

(defun sort-to-match-vars (subst-alist vars)
  (if (null vars)
      nil
      (cons (assoc (car vars) subst-alist)
	    (sort-to-match-vars subst-alist (cdr vars)))
      ))

(defun goal-list (formula)
  (if (eql (car formula) 'and)
      (cdr formula)
      (list formula)
      ))

(defun get-vars (form)
  (cond ((is-var? form) (list form))
	((atom form) nil)
	(t (append (get-vars (car form)) (get-vars (cdr form))))
	))

(defun extend-path (node database vars path-so-far depth-limit
			 &optional (depth 0)) ;last argument for trace output
  (if *trace* (show-node-data node depth))
  (let ((path-so-far (cons node path-so-far)))
    (cond ((null (node-goals node))	; if no goals left to satisfy
	   (list (node-bindings node)))	; then these bindings are a solution
	  ((not (eql depth-limit 0))	; else if depth limit not reached
	   (apply #'append		; append all results obtained by
		  (mapcar		;   doing this recursively on all
		   #'(lambda (n)	;   children
		       (extend-path n database vars path-so-far
				    (one-less depth-limit) (1+ depth)))
		   (let ((children
			  (if *avoid-loops*
			      (set-difference
			       (successors node database vars)
			       path-so-far
			       :test #'(lambda (n1 n2)
					 (equal-goals n1 n2 vars)))
			       (successors node database vars))))
		     (if (and *trace* (null children))
			 (format t "~a*** Failure ***~%" (indent depth)))
		     children))))
	  (t (if *trace* (format t "~a*** Depth Limit Reached ***~%"
				 (indent depth))))
	  )))
  
(defun one-less (n)
  (if (numberp n) (1- n) n))

(defun show-node-data (node depth)
  (if (node-rule-number node)
      (format t "~aWorking on rule ~a~%"
	      (indent depth)
	      (node-rule-number node)))
  (if (null (node-goals node))
      (format t "~aEmpty goal list =>~%~a*** Solution *** "
	      (indent depth) (indent depth))
    (let ((goals (node-goals node)))
      (format t "~aGoals:  ~a~%" (indent depth) (first goals))
      (dolist (g (rest goals))
	(format t "~a        ~a~%" (indent depth) g))
      (format t "~aBindings:" (indent depth))))
  (show-bindings (node-bindings node))
  )

(defun indent (depth) (make-string (* 2 depth) :initial-element #\space))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This function returns a list of successor nodes of a given node.  Each
; successor is obtained by unifying the top goal in the node with either
; an entire formula in the database or the consequent of an implication
; in the database.  In the first case the resulting successor has as its
; list of goals the cdr of the list obtained from its parent; in the second
; case, the corresponding antecedent is appended to this cdr.
; In both cases, the necessary substitutions are made in all the goal
; formulas.  The bindings in this successor node are obtained by appending
; these new bindings to the existing ones after first removing all bindings
; of variables not specified in the original query.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun successors (node database vars)
  (let* ((bindings (node-bindings node))
	 (goals (node-goals node))
	 (first-goal (first goals))
	 (rest-goals (rest goals))
	 (succ-list nil)
	 mgu
	 form)
    (if (lisp-escape? first-goal)
	(let ((form (lisp-form first-goal))) ;escape to lisp
	  (if (is-true? form)
	      (list (make-node
		     :bindings (node-bindings node)
		     :goals rest-goals
		     :rule-number (node-rule-number node)))
	      nil))
        (dolist (item database (reverse succ-list)) ;try match to database
	  (setq form
		(standardize
		  (if (bc-rule-p item) (bc-rule-formula item) item)))
	  (cond ((listp (setq mgu (unify form first-goal))) ; matches formula
		 (push (make-node
			:bindings (append (query-vars-only mgu vars) bindings)
			:goals (subst-in-forms rest-goals mgu)
			:rule-number (node-rule-number node))
		       succ-list))
		((and (eql (car form) 'if)         ; matches consequent of "if"
		      (listp (setq mgu (unify (third form) first-goal))))
		 (push (make-node
			:bindings (append (query-vars-only mgu vars) bindings)
			:goals (subst-in-forms
				(append (goal-list (second form)) rest-goals)
				mgu)
			:rule-number (bc-rule-number item))
		       succ-list)))
	  ))))

(defun query-vars-only (mgu vars)
  (remove-if-not #'(lambda (binding) (member (car binding) vars)) mgu))

(defun subst-in-forms (form-list subst-alist)
  (mapcar #'(lambda (form) (varsubst form subst-alist)) form-list))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Equal-goals tests whether the goal lists of 2 nodes are the same up to
; renaming of any variables not in vars.  This is done by getting an MGU
; for the 2 lists and checking to see that only variables appear as the
; bindings for variables and that any variables in vars are only bound to
; themselves.  For efficiency, the lengths of the 2 goal lists are checked
; first.  If these are unequal no further testing is necessary.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun equal-goals (node1 node2 vars)
  (let ((goal-list1 (node-goals node1))
	(goal-list2 (node-goals node2)))
    (if (/= (length goal-list1) (length goal-list2))
	nil
        (match-up-to-var-names goal-list1 goal-list2 vars)
	)))

(defun match-up-to-var-names (form1 form2 vars)
  (let ((mgu (unify form1 form2)))
    (and (listp mgu)
	 (dolist (bind mgu t)
	   (if (or (not (is-var? (cdr bind)))
		   (and (member (car bind) vars)
			(not (eq (car bind) (cdr bind)))))
	       (return nil)))
	 )))