;;; -*- Mode:common-lisp; Package:1user*; Base:10; Fonts:(COURIER TR12I
 COURIER COURIER TR12B) -*-
(in-package 'user)
(proclaim '(optimize (speed 3) (safety 0)))
;1;; DEDUCE is a deductive retrieval system which uses generators to retrieve
 one*
;1;; answer at a time and also generates proofs. It currently supports only*
;1;; backward chaining.  A depth bound in number of rules can be given.*

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

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

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

;1-----------------------------------------------------------------------------
 -*
;1                             GENERATORS*
;1-----------------------------------------------------------------------------
 -*

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

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

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

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


(defun 4force* (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 4normalize* (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 4gfirst* (x) (first (normalize x)))

(defun 4grest* (x) (normalize (rest (normalize x))))

(defun 4gnull* (x) (null (normalize x)))

;1-----------------------------------------------------------------------------
 -*
;1                               UNIFICATION *
;1-----------------------------------------------------------------------------
 -*

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

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

(defun 4print-pcvar* (var stream depth)
  (declare (ignore depth))
  (format stream "3?~A*" (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 4*occur-check** t)  ;1 Performs an occur check if T*
(defvar 4*use-gensyms** t)  ;1 Uses gensym to create unique variables if T*
                          ;1 otherwise uses copy-symbol*

(defun 4unify* (a b &optional (bindings (list t)))
  ;1;; 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 4var-unify* (var b bindings)
  ;1;; Unify a variable with a wff, if must bind variable and *occur-check**
  ;1;; 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 4var-eq* (var1 var2)
  ;1;; Return T if the two variables are equal*
  (eql (pcvar-id var1)(pcvar-id var2)))

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

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

(defun 4bound-to-p* (var1 var2 bindings)
  ;1;; 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 4free-in-p* (var b bindings)
  ;1;; 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 4substitute-vars* (form bindings)
  ;1;; Substitute the variables in form for their ultimate values specified*
  ;1;; in the bindings*
  (if (rest bindings)
      (substitute1 form bindings)
      form))

(defun 4substitute1* (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 4uniquify-variables* (form)
  ;1;; 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 4rename-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 "3G*")
						  (copy-symbol id))))
		     new-names))))
	((consp form) (rename-list (rest form)
				   (rename-list (first form) new-names)))
	(t new-names)))

(defun 4rename-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)))))


;1-----------------------------------------------------------------------------
 -* 1DEDUCTIVE RETRIEVER*
;1-----------------------------------------------------------------------------
 -*

;1D.O. * 12/3/89: This function has been put here to make its definition*
 1appear before its usage in the file.*

(defun 4index-fact* (form)
  "2Add a form to the fact database.*"
  (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)
           (push (first form) *database*)
	   (setf (get (first form) 'facts) (list form)))))
  form)

(defvar 4*database**        nil
   "2Stores the list of all predicates which have facts indexed on their fact
 properties.*")
(defvar 4*seen-predicates** nil
   "2The stored consequent predicates*")
(defvar 4*procedurally-defined-predicates** '(< > <= >= =)
   "2Procedurally-defined predicates.*")
(defvar 4*functions** '(+ - * / max min)
   "2Functions that are procedurally evaluated.*")

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


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

(defun 4brule-consequent* (brule) (second brule))

(defun 4brule-antecedents* (brule) (cddr brule))

;1;; Changed index-brules back to its old form so that I could use
 clear-rulebase.*

(defun 4index-brules* (rules)
  "2Index 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.*"
  ;; 11/3/90: modified to handle structured rules
  (dolist (rule rules)
    (setf *seen-predicates* (delete (first (brule-consequent rule))
				    *seen-predicates*)))
  (dolist (rule rules)
    (index-brule rule)))

(defun 4index-brule* (rule &aux (uniq-rule (uniquify-variables rule)))
  "2Index a rule using 'car indexing.'  This new rule will be
   tried AFTER previously-defined rules with the same consequent.*"
   (let ((predicate (first (brule-consequent uniq-rule))))
        (cond ((member predicate *seen-predicates*)
               (nconc (get predicate 'brules)(list uniq-rule)))
              (t (setf (get predicate 'brules) (list uniq-rule))
                 (push predicate *seen-predicates*)))))



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

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

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

(defun 4index-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) *database*))))
  form)

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

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

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

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

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

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

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

(defun 4clear-rulebase* ()
  "2Clear the rule database.*"
  (dolist (predicate *seen-predicates*)
	(remprop predicate 'brules))
  (setf *seen-predicates* nil))

(defun 4dump-rulebase* ()
  "2Report the rules stored.*"
  (format t "3~%~%Rules Stored~%*")
  (dolist (predicate *seen-predicates*)
	  (dolist (rule (get predicate 'brules)) (format t "3~A~%*" rule))
	  (terpri)))

;1 changes made to do consistency check*
;1 also changes made to handle procedurally evaluated form*
;1;; 3-29-90: added negation.*
(defun 4retrieve *(form &optional (depth-limit 10))
  ;1;; Return a generated list of answers but don't search more than*
  ;1;; depth-limit rules deep.*
  (if (eq (first form) 'not)
      ;1;  First check to see if there are any facts in the database explicitly
 of the form
         *;1;  "(not a)". If there aren't any then check to see if "a" is
 provable. If it isn't return
         *;1;  t. *
      (or (mapcan #'(lambda (pos-answer)
		      (let ((bindings (unify form pos-answer)))
			(if bindings
			    (list (list bindings pos-answer)))))
		  (funcall *fact-retriever* form))
	  (when (not (gfirst (retrieve (second form) depth-limit)))
	    `(((t) ,form))))
  (if (evaluable-procedural-form? form)
      (if (apply (first form) (rest form))
	  `(((t) ,form)))
      (let ((from-database
	      (mapcan #'(lambda (pos-answer)
			  (let ((bindings (unify form pos-answer)))
			    (if bindings
				(list (list bindings pos-answer)))))
		      (append (funcall *fact-retriever* form)
			      *assumptions*))))	;1 use of global variable here*
	(cond ((zerop depth-limit) from-database)
	      (t (nconc from-database
			(list (delay (try-rules form (funcall *brule-retriever* form)
						depth-limit))))))))))

;1;; Old retrieve: does not include assumptions or observations as facts.*

(defun 4old-retrieve* (form &optional (depth-limit 10))
  ;1;; Return a generated list of answers but don't search more than*
  ;1;; depth-limit rules deep.*
  (if (evaluable-procedural-form? form)
      (if (apply (first form) (rest form))
	  `(((t) ,form)))
      (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) from-database)
	      (t (nconc from-database
			(list (delay (try-rules form (funcall *brule-retriever* form)
						depth-limit)))))))))

(defun 4try-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 4backchain* (rule bindings depth-limit)
  (make-answers rule
		(retrieve-conjuncts (brule-antecedents rule) bindings depth-limit)
		bindings))


(defun 4make-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 4join-bindings* (bindings1 bindings2)
  (append bindings1 (rest bindings2)))



(defun 4retrieve-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 4try-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 4join-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 4specific-proof* (answer)
  ;1;; Return the specific proof for a particualr answer*
  (instantiate-proof (second answer) (first answer)))


(defun 4instantiate-proof* (proof bindings)
  ;1;; Return the proof created by instantiating the given proof structure*
  ;1;; 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))))

;1Changes by D.O.*
(defun proof-chain (proof )
  ;;; return the proof obtained from the specific proof in the format used by
  ;;; abduce but with the variables left intact.
  (cond ((rule-proof-p proof)
	 (cons (rule-proof-consequent proof)
	       (mapcar #'(lambda (ante-proof)
			   (if (rule-proof-p (second ante-proof))
			       (proof-chain (second ante-proof) )
			       (first ante-proof)))
		       (rule-proof-ante-proofs proof))))
	(t proof)))

;1 changes (by htng)*



(defun 4evaluable-procedural-form?* (form &optional (check-variables t))
  (and (consp form)
       (member (first form) *procedurally-defined-predicates*)
       (or (not check-variables)
	   (not (contains-variables? form)))))


;1 Determine if this form contains any variables*

(defun 4contains-variables?* (form)
  (cond ((pcvar-p form) t)
        ((atom form) nil)
        ((or (contains-variables? (first form))
             (contains-variables? (rest  form))))))