;;; DEDUCE is a deductive retrieval system which uses generators to retrieve one
;;; answer at a time and also generates proofs. It currently supports only
;;; backward chaining.  A depth bound in number of rules can be given.

;;;; Copyright (c) 1988 by Raymond Joseph Mooney. This program may be freely 
;;;; copied, used, or modified provided that this copyright notice is included
;;;; in each copy of this code and parts thereof.

;;; Variables are represented with a leading "?". Backchaining rules are of
;;; the form (<- consequent . antecedents) and are indexed by predicate name
;;; of the consequent (i.e. "CAR indexing").  The function index-brules can be 
;;; used to enter these rules.  Facts are also indexed by predicate and
;;; the function index-facts can be used to enter them.
;;; The file CUP-DOMAIN is an example of a domain file which defines rules and facts
;;; The function clear-facts clears the database  of facts and the function dump-facts
;;; returns all facts in the database. Similar functions (clear-brules dump-brules)
;;; exist for backchaining rules.

;;; After a set of rules and facts have been entered, a request can be retrieved by
;;; calling the function (retrieve <form> <depth-bound>) (e.g. (retrieve '(cup obj1) 3))
;;; Retrieve returns a generated list of answers which should be manipulated using only
;;; the functions gfirst, grest, and gnull which perform the obvious operations on
;;; generated lists.  A generated list computes elements of the list only as they are
;;; needed, this allows the retriever to return one answer at a time like PROLOG.
;;; An answer from retrieve is of the form: (<bindings> <proof>) where <bindings> is a
;;; list of variable bindings which create an answer if applied to <form> using
;;; the function (substitute-vars <form> <bindings>). A <proof> is defined recursively
;;; as either a fact from the database which matches <form> or a proof based on a rule:
;;; (rule-proof <consequent> ((<antecedent> <proof>)(<antecedent> <proof>)...))
;;; where <consequent> and <antecedents>'s constitute a uniquely variablized rule.
;;; Each (<antecdent> <proof>) in a rule-proof is called an ante-proof.
;;; This form of proof constitutes an "explanation structure" and can be easily used to
;;; generate a generalized proof.  A compact version of the specific proof for the given 
;;; answer can be generated by calling the function (specific-proof <answer>).

;------------------------------------------------------------------------------
;                             GENERATORS
;------------------------------------------------------------------------------


;;; Defines the function DELAY to create a generated list and the functions
;;; GFIRST, GREST, and GNULL for getting items from and testing a generated list.
;;; See AI Programming 2nd ed. for details

(defstruct (generator (:print-function print-generator))
  closure
  (value nil)
  (forced-p nil))

(defun print-generator (g stream depth)
  (declare (ignore g depth))
  (format stream "#<Generator...>"))

(defmacro delay (&body body)
  `(make-generator :closure #'(lambda () ,@body)))

(defun force (x)
  (cond ((not (generator-p x)) x)
	((generator-forced-p x)(generator-value x))
	(t (prog1 (setf (generator-value x)
			(funcall (generator-closure x)))
		  (setf (generator-forced-p x) t)))))

(defun normalize (g)
  (cond ((null g) nil)
	((not (generator-p (first g))) g)
	(t (let ((new-g (append (force (first g)) (rest g))))
	     (cond ((null new-g) nil)
		   (t (setf (first g) (first new-g))
		      (setf (rest g) (rest new-g))
		      (normalize g)))))))


(defun gfirst (x) (first (normalize x)))

(defun grest (x) (normalize (rest (normalize x))))

(defun gnull (x) (null (normalize x)))

;------------------------------------------------------------------------------
;                               UNIFICATION 
;------------------------------------------------------------------------------

;;; This section defines the unification pattern matcher. A variable must
;;; begin with a leading "?" which is used by the reader to create a structure.
;;; The unify function takes two patterns and a binding list and unifies the
;;; patterns in the context of the current bindings and returns an updated
;;; binding list.  A binding list is of the form:
;;; (T (<var> <value>)(<var> <value>)...)
;;; The leading T is used to distinguish the empty binding list: (T) from
;;; failure to unify for which NIL is returned.
;;; See AI Programming 2nd ed. for details (slightly different).

(defstruct (pcvar (:print-function print-pcvar)) id)

(defun print-pcvar (var stream depth)
  (declare (ignore depth))
  (format stream "?~S" (PCVAR-ID var)))

(set-macro-character #\?
		     #'(lambda (stream char) (declare (ignore char))
			       (if (member (peek-char nil stream t nil t)
					   '(#\space #\newline #\) #\( #\' #\" #\return #\linefeed #\tab
					     #\` #\# #\,))
				   (quote \?)
				   (make-pcvar :id (read stream t nil t))))
		     t)

(defvar *occur-check* t)  ; Performs an occur check if T
(defvar *use-gensyms* t)  ; Uses gensym to create unique variables if T
                          ; otherwise uses copy-symbol

(defun unify (a b &optional (bindings (list t)))
  ;;; Return a most general binding list which unifies a & b
  (cond ((eql a b) bindings)
	((pcvar-p a) (var-unify a b bindings))
	((pcvar-p b) (var-unify b a bindings))
	((or (atom a)(atom b)) nil)
	((setf bindings (unify (first a)(first b) bindings))
	 (unify (rest a) (rest b) bindings))))

(defun var-unify (var b bindings)
  ;;; Unify a variable with a wff, if must bind variable and *occur-check*
  ;;; flag is set then check for occur-check violation
  (if (and (pcvar-p b) (var-eq var b))
      bindings
      (let ((binding (get-binding var bindings)))
	(cond (binding (unify (second binding) b bindings))
	      ((and (pcvar-p b)(bound-to-p b var bindings)) bindings)
	      ((or (null *occur-check*) (free-in-p var b bindings))
	       (add-binding var b bindings))))))

(defun var-eq (var1 var2)
  ;;; Return T if the two variables are equal
  (eql (pcvar-id var1)(pcvar-id var2)))

(defun get-binding (var bindings)
  ;;; Get the variable binding for var
  (assoc var (rest bindings) :test #'var-eq))

(defun add-binding (var val bindings)
  ;;; Add the binding of var to val to the existing set of bindings
  (setf (rest bindings) (cons (list var val) (rest bindings)))
  bindings)

(defun bound-to-p (var1 var2 bindings)
  ;;; Check if var1 is eventually bound to var2 in the bindings
  (cond ((equalp var1 var2) t)
	((let ((val (second (get-binding var1 bindings))))
	   (and val (pcvar-p val) (bound-to-p val var2 bindings))))))

(defun free-in-p (var b bindings)
  ;;; Return T if var does not occur in wff b
  (cond ((equalp var b) nil)
	((pcvar-p b)
	 (free-in-p var (second (get-binding b bindings)) bindings))
	((atom b) t)
	((and (free-in-p var (first b) bindings)
	      (free-in-p var (rest b) bindings)))))

(defun substitute-vars (form bindings)
  ;;; Substitute the variables in form for their ultimate values specified
  ;;; in the bindings
  (if (rest bindings)
      (substitute1 form bindings)
      form))

(defun substitute1 (form bindings)
  (cond ((null form) nil)
	((pcvar-p form)
	 (let ((binding (get-binding form bindings)))
	   (if binding
	       (substitute1 (second binding) bindings)
	       form)))
	((atom form) form)
	(t (cons (substitute1 (first form) bindings)
		 (substitute1 (rest form) bindings)))))

(defun uniquify-variables (form)
  ;;; Make all the variables in form "unique" gensymed variables
  (let ((new-names (rename-list form nil)))
    (if (null new-names)
	form
	(rename-variables form new-names))))

(defun rename-list (form &optional new-names)
  (cond ((pcvar-p form)
	 (let ((id (pcvar-id form)))
	   (if (assoc id new-names)
	       new-names
	       (cons (list id (make-pcvar :id (if *use-gensyms*
						  (gensym)
						  (copy-symbol id))))
		     new-names))))
	((consp form) (rename-list (rest form)
				   (rename-list (first form) new-names)))
	(t new-names)))

(defun rename-variables (form new-names)
  (cond ((pcvar-p form)
	 (let ((entry (assoc (pcvar-id form) new-names)))
	   (if entry (second entry) form)))
	((atom form) form)
	(t (cons (rename-variables (first form) new-names)
		 (rename-variables (rest form) new-names)))))


;------------------------------------------------------------------------------
;                             DEDUCTIVE RETRIEVER
;------------------------------------------------------------------------------

(defvar *rule-predicates* nil "List of predicates for known rule consequents")

;;; Define access functions for backchaining rules
(defun brule-p (x) (and (consp x) (eq (first x) '<-)))

(defun brule-consequent (brule) (second brule))

(defun brule-antecedents (brule) (cddr brule))

(defun index-brules (rules)
  ;;; Index a list of rules using "car indexing"
  ;;; Like PROLOG, rules are tried in the order presented.
  ;;; Each call to index-brules clears previous rules stored on the consequent
  ;;; predicates.
  
  (setf *rule-predicates* nil)
  (dolist (rule rules)
    (setf rule (uniquify-variables rule))
    (let ((predicate (first (brule-consequent rule))))
      (cond ((member predicate *rule-predicates*)
	     (nconc (get predicate 'brules)(list rule))) 
	    (t (setf (get predicate 'brules) (list rule))
	       (push predicate *rule-predicates*))))))

(defun push-brule (rule)
  ;;; Push a backchain rule onto the front of the rules for that predicate
  ;;; so it is tried first in the future.
  (push rule (get (first (brule-consequent rule)) 'brules)))

(defun dump-brules ()
  ;;; Return a list of all known backchaining rules
  (mapcan #'(lambda (predicate) (copy-list (get predicate 'brules)))
	  *rule-predicates*))

(defun clear-brules ()
  (dolist (predicate *rule-predicates*)
    (setf (get predicate 'brules) nil))
  (setf *rule-predicates* nil))

(defvar *fact-predicates* nil) ; Stores the list of all predicates which have facts
                        ; indexed on their fact properties

(defun index-facts (facts)
  ;;; Add facts to the database using "car indexing"
  (dolist (fact facts) (index-fact fact)))

(defun index-fact (form)
  (let ((existing-facts (get (first form) 'facts)))
    (cond ((and existing-facts (not (member form existing-facts :test #'equal)))
	   (nconc existing-facts (list form)))
	  ((null existing-facts)
	   (setf (get (first form) 'facts) (list form))
	   (push (first form) *fact-predicates*))))
  form)

(defun dump-facts ()
  ;;; Return a list of all facts in the database.
  (mapcan #'(lambda (predicate) (copy-list (get predicate 'facts)))
	  *fact-predicates*))

(defun clear-facts ()
  ;;; Clear the database of facts
  (dolist (predicate *fact-predicates*)
    (setf (get predicate 'facts) nil))
  (setf *fact-predicates* nil))

;;; Fact and rule retrievers are explicitly defined so they can be changed as
;;; needed, e.g. to use a descrimination net instead.

(defvar *fact-indexer*   #'index-fact)

(defvar *brule-retriever* #'(lambda (form) (get (first form) 'brules)))

(defvar *fact-retriever* #'(lambda (form) (get (first form) 'facts)))

(defstruct (rule-proof (:type list) :named)
  consequent
  ante-proofs)


(defun retrieve (form &optional (depth-limit 100))
  ;;; Return a generated list of answers but don't search more than
  ;;; depth-limit rules deep.
  (let ((from-database  (mapcan #'(lambda (pos-answer)
				    (let ((bindings (unify form pos-answer)))
				      (if bindings (list (list bindings
							       pos-answer)))))
				(funcall *fact-retriever* form))))
    (cond ((zerop depth-limit) ; if exhausted depth limit then only try known facts
	                       ; and rules with out antecedents
	   (nconc from-database
		  (list (delay (try-rules form
					  (remove-if #'brule-antecedents
						     (funcall *brule-retriever* form))
					  depth-limit)))))
	  (t (nconc from-database
		    (list (delay (try-rules form (funcall *brule-retriever* form)
					    depth-limit))))))))


(defun try-rules (form rules depth-limit)
  (cond ((null rules) nil)
	((let ((bindings (unify (brule-consequent (first rules)) form)))
	   (if bindings
	       (let ((new-names (rename-list (first rules))))
		 (nconc (backchain (rename-variables (first rules) new-names)
			    (rename-variables bindings new-names) depth-limit)
		       (list (delay (try-rules form (rest rules) depth-limit)))))
	       (try-rules form (rest rules) depth-limit))))))


(defun backchain (rule bindings depth-limit)
  (make-answers rule
		(retrieve-conjuncts (brule-antecedents rule) bindings depth-limit)
		bindings))


(defun make-answers (rule ante-answers bindings)
  (cond ((gnull ante-answers) nil)
	(t (list (list (first (gfirst ante-answers))
		       (make-rule-proof :consequent (brule-consequent rule)
					:ante-proofs (rest (gfirst ante-answers))))
		 (delay (make-answers rule (grest ante-answers) bindings))))))


(defun join-bindings (bindings1 bindings2)
  (append bindings1 (rest bindings2)))



(defun retrieve-conjuncts (conjuncts bindings depth-limit)
  (cond ((null conjuncts) (list (list bindings)))
	(t (try-answers (first conjuncts)
		       (retrieve (substitute-vars (first conjuncts) bindings)
				 (1- depth-limit))
		       (rest conjuncts) bindings depth-limit))))


(defun try-answers (conjunct conj-answers remaining-conjuncts bindings depth-limit)
  (cond ((gnull conj-answers) nil)
	(t (let* ((conj-answer (gfirst conj-answers))
		  (remaining-answers (retrieve-conjuncts remaining-conjuncts
						(join-bindings (first conj-answer)
							       bindings)
						depth-limit)))
	     (nconc (join-answers conjunct conj-answer remaining-answers)
		     (list (delay (try-answers conjunct (grest conj-answers)
					       remaining-conjuncts bindings
					       depth-limit))))))))


(defun join-answers (conjunct conj-answer remaining-answers)
  (cond ((gnull remaining-answers) nil)
	((list (cons (first (gfirst remaining-answers))
		     (cons (list conjunct (second conj-answer))
			   (rest (gfirst remaining-answers))))
	       (delay (join-answers conjunct conj-answer (grest remaining-answers)))))))


(defun specific-proof (answer)
  ;;; Return the specific proof for a particualr answer
  (instantiate-proof (second answer) (first answer)))


(defun instantiate-proof (proof bindings)
  ;;; Return the proof created by instantiating the given proof structure
  ;;; with the given variable bindings
  (cond ((rule-proof-p proof)
	 (cons (substitute-vars (rule-proof-consequent proof) bindings)
	       (mapcar #'(lambda (ante-proof)
			   (if (rule-proof-p (second ante-proof))
			       (instantiate-proof (second ante-proof) bindings)
			       (substitute-vars (first ante-proof) bindings)))
		       (rule-proof-ante-proofs proof))))
	(t (substitute-vars proof bindings))))