;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Little Backwards Chainer
; Don Hopkins
; CMSC 421
; November 5 1987
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; general discrimination tree climbing and building

; -----------------------------
; data types and definitions

; a node has three properties ASSOCIATED-ATOM, SEXP and ALIST
(defun node-sexp (node)
   (get node 'sexp))
; set sexp uses ADDPROP, clobber-sexp uses PUTPROP (resets)
(defun node-set-sexp (node sexp)
    (addprop node sexp 'sexp)
    (dirty-node node))
(defun node-clobber-sexp (node sexp)
    (putprop node sexp 'sexp)
    (dirty-node node))
(defun node-reset-sexp (node)
    (putprop node nil 'sexp)
    (dirty-node node))

; node alist accessing functions
(defun node-alist (node)
  (get node 'alist))
(defun node-set-alist (node alist)
  (addprop node alist 'alist)
  (dirty-node node))
(defun node-reset-alist (node)
  (putprop node nil 'alist)
  (dirty-node node))

; node associated atom accessing functions
(defun node-associated-atom (node)
  (get node 'associated-atom))
(defun node-set-associated-atom (node associated-atom)
  (addprop node associated-atom 'associated-atom)
  (dirty-node node))
(defun node-reset-associated-atom (node)
  (putprop node nil 'associated-atom)
  (dirty-node node))

; ---------------------------
;  necessary utilities

; add to last is essentially a destructive append
(defun add-to-last (lst itm)
    (rplacd (last lst) (ncons itm)))

(defun addprop (atm val prop)
   (putprop atm (cons val (get atm prop)) prop))

(defun make-node (sexp alist associated-atom)
 (let ((node-name (newsym 'NODE)))
      (putprop node-name sexp 'sexp)
      (putprop node-name alist 'alist)
      (putprop node-name associated-atom 'associated-atom)
      (dirty-node node)
      node-name))

; -------------------
; Index adds an arbitrary s-expression to a tree
(defun index (sexp node associated-atom)
    (let ((leaf-node (establish-links sexp node)))
	 (node-clobber-sexp leaf-node sexp)
	 (cond ((node-associated-atom leaf-node))   
                	        ; if associated-atom is there return it
	       (t (node-set-associated-atom leaf-node associated-atom)))))
 				; otherwise create one with the called value

; ------------- NOTE THE DOUBLE RECURSION ---------
; -------------                           ---------
(defun establish-links (item node)
    (cond ((null item) (establish-link '*NIL* node))
	  ((atom item)(establish-link item node))
	  ((establish-links 
	       (cdr item)
	       (establish-links 
		   (car item)
		   (establish-link '*CONS* node))))))

(defun establish-link (sexp node)
   (let ((auxil (assoc sexp (node-alist node))))
    (cond (auxil (cadr auxil))
	  (t (let ((new-node (make-node sexp nil nil)))
		  (add-to-alist node new-node sexp)
		  new-node)))))


(defun add-to-alist (node new-node sexp)
     (node-set-alist node (list sexp new-node)))

; Start with an empty rule list.
(setq *RULE-LIST* nil)

; Display each node of a knowledge base
(defun display (node)
  (display-tree node 0))

(defun display-tree (node level)
  (msg (B level) "Node: " node
       " alist: " (node-alist node) N
       (B level) "sexp: " (node-sexp node)
       " associated-atom: " (node-associated-atom node) N)
  (cond
    ((null (node-alist node)) nil)
    (t (mapcar #'(lambda (link)
		   (display-tree (link-node link) (add1 level)))
	       (node-alist node))
       nil)))

; When a node is changed, it is marked as being dirty, so we can later 
; update the copy in the NeWS server.
(defun dirty-node (node)
  (putprop node t 'dirty))

; Write dirty nodes to the NeWS server in PostScript, and mark them as 
; clean.
(defun sweep ()
  (clean-tree '*KB*))

(defun clean-tree (node)
  (cond ((get node 'dirty)
	 (send-node node)
	 (putprop node nil 'dirty)))
  (cond
    ((null (node-alist node)) nil)
    (t (mapcar #'(lambda (link)
		   (clean-tree (link-node link)))
	       (node-alist node))
       nil)))

(defun send-node (node)
  (ps-make-node node (node-sexp node)
    (node-associated-atom node)
    (node-alist node)))

; Magic control characters the PostScript terminal emulator responds to.
(setq StartPS "") ; begin trojan horse
(setq EndPS "") ; end and execute trojan horse

; Write out a NeWS menu definition, with the right control characters to 
; make the PostScript terminal program (SoftTTY) execute it.
(defun ps-make-node (name sexp associated-atom alist)
  (msg "% Sending " name "...")
  (msg StartPS "userdict /" name " [" N)
  (msg "  " (list 'Name= name) " {" (ncons name) " print}" N
       "  " (list 'Sexp= sexp) " {" (ncons sexp) " print}" N
       "  " (list 'Atom= (fact-name associated-atom))
	    " {" (ncons (fact-name associated-atom)) " print}" N)
  (mapcar #'(lambda (link)
	      (msg "  " link " /" (link-node link) " cvx" N))
	  alist)
  (msg "] /new DefaultMenu send put" N)
  (msg name " /Clockwise false put" N)
  (cond ((eq name '*KB*) (msg "/ClientMenu *KB* def" N))) ; kludge
  (msg EndPS N))

; Link accessing functions.
; The node alist is a list of links. 
(defun link-name (link)
  (car link))

(defun link-node (link)
   (cadr link))

; Look up an s-expression in a knowledge base.
; Returns the leaf node if the s-expression is in the base,
; or nil if not.
(defun lookup (sexp node)
    (cond
      ((null node) nil)
      ((null sexp) (find-link '*NIL* node))
      ((atom sexp) (find-link sexp node))
      (t (lookup (cdr sexp)
	         (lookup (car sexp)
			 (find-link '*CONS* node))))))

; Match a pattern against a knowledge base. Returns the first node it 
; finds that matches, of nil if there are none.
(defun match-fetch (sexp rest node)
    (cond
      ((null node) nil)
      ((null sexp)
       (match-rest rest (find-link '*NIL* node)))
      ((atom sexp)
       (match-rest rest (find-link sexp node)))
      ((var-p sexp)
       (match-var-rest (node-alist node) rest node))
      (t (match-fetch (car sexp) (cons (cdr sexp) rest)
		      (find-link '*CONS* node)))))

(defun match-rest (rest node)
  (cond ((null rest) t)
	(t (match-fetch (car rest) (cdr rest) node))))

(defun match-var-rest (alist rest node)
  (cond ((null alist) nil)
	((member (link-name (car alist)) '(*CONS* *NIL*))
	 (match-var-rest (cdr alist) rest node))
	((match-rest rest (link-node (car alist))))
	(t (match-var-rest (cdr alist) rest node))))

; Return the node linked to by name, or nil if none.
(defun find-link (name node)
  (let ((link (assoc name (node-alist node))))
    (cond ((null link) nil)
	  (t (link-node link)))))

; Fetch takes a pattern and a node of a tree. 
; If the pattern is not in the tree, nil is returned.
; If the pattern matches the tree, a list of lists
; is returned. The car of each list if a fact name, 
; and the cdr is a set of variables bindings, or nil if 
; there were no variables.
(defun fetch (pat node)
  (fetch-nodes pat nil node nil))

(defun fetch-nodes (pat rest node bindings)
    (cond
      ((null node) nil) ; ran off the edge
      ((null (node-alist node)) ; at a terminal node!
       (ncons (cons (associated-fact node)
		    bindings)))
      ((null pat) ; follow nil link
       (fetch-nodes (car rest) (cdr rest)
		    (find-link '*NIL* node) bindings))
      ((atom pat) ; follow atom link
       (fetch-nodes (car rest) (cdr rest)
		    (find-link pat node) bindings))
      ((var-p pat) ; follow a variable 
       (cond ((assoc (var-name pat) bindings) ; do we already know this var?
	      (fetch-nodes (car rest) (cdr rest) ; then follow the old value
			   (find-link
			     (binding-val
			       (assoc (var-name pat) bindings))
			     node)
			   bindings))
	     (t ; otherwise, follow every value
	      (mapcan #'(lambda (link)
			  (and (not (member (link-name link)
					    '(*CONS* *NIL*)))
			       (fetch-nodes (car rest) (cdr rest)
					    (link-node link)
					    (cons
					      (list (var-name pat)
						    (link-name link))
					      bindings))))
		      (node-alist node)))))
      (t (fetch-nodes (car pat) (cons (cdr pat) rest) ; follow a cons node
		      (find-link '*CONS* node) bindings))))

; the "official" definition
(defun FETCH (pat)
  (fetch pat '*KB*))

; Just return name of the first fact found that matches sexp, 
; of nil if none.
(defun fetch-fact-name (sexp node)
  (let ((facts (fetch sexp node)))
    (and facts (fact-name (car facts)))))

; Change the associated-atom of the leaf node of an sexp.
(defun change (sexp node atom)
  (let ((leaf-node (lookup sexp node)))
    (cond (leaf-node
	    (node-set-associated-atom leaf-node atom)
	    atom)
          (t
	    nil))))

; Return the first atom of the associated-atom list, the fact name.
(defun associated-fact (node)
  (fact-name (node-associated-atom node)))

; Get the fact name out of a list returned by fetch.
(defun fact-name (fetched-fact)
       (car fetched-fact))

; Get the bindings out of a list returned by fetch.
(defun fact-bindings (fetched-fact)
       (cdr fetched-fact))

; Fact status accessing functions.
(defun get-status (fact)
       (get fact 'STATUS))

(defun set-status (fact status)
       (putprop fact status 'STATUS))

; Assert a fact, putting it into the knowledge base.
(defun ASSERT (fact &optional name)
       (cond ((null name)
	      (setq name (newsym 'FACT)))) ; make up a name if one not supplied
       (index fact '*KB* name)
       (set-status name 'KNOWN)
       name)

; Return the status of a fact, given the fact name or the fact 
; s-expression. 
(defun STATUS (fact)
       (cond ((not (atom fact))
	      (setq fact (fetch-fact-name fact '*KB*))))
       (get-status fact))

; Rule fact and prove accessing functions
(defun rule-set-fact (rule fact)
  (putprop rule fact 'FACT))
(defun rule-fact (rule)
  (get rule 'FACT))
(defun rule-set-prove (rule prove)
  (putprop rule prove 'PROVE))
(defun rule-prove (rule)
  (get rule 'PROVE))

; Assert a rule. Make a rule atom, cons it onto *RULE-LIST*, and set
; it up.
(defun ASSERT-RULE (fact prove)
       (let ((rule-name (newsym 'RULE)))
	 (rule-set-fact rule-name (unabbreviate-rule fact))
	 (rule-set-prove rule-name (unabbreviate-rule prove))
	 (setq *RULE-LIST* (cons rule-name *RULE-LIST*))
	 rule-name))

; Erase the knowledge base and rebuild from by reading the knowledge
; base, given the file name to load.
(defun REBUILD (file)
  (node-reset-sexp '*KB*)
  (node-reset-alist '*KB*)
  (node-reset-associated-atom '*KB*)
  (setq *RULE-LIST* nil)
  (load file))

; Display all the facts in the data base, or just the ones given in the
; optional argument, a list.
(defun SHOW-FACTS (&optional facts)
  (find-facts facts '*KB*))

(defun find-facts (facts node)
  (cond
    ((null (node-alist node))
     (cond
       ((or (not facts) (member (associated-fact node) facts))
	(msg "NAME: " (associated-fact node)
	     ", " (node-sexp node)
	     ", STATUS: " (get-status (associated-fact node)) N)
	nil)))
    (t (mapcar #'(lambda (link)
		   (find-facts facts (link-node link)))
	       (node-alist node))
       nil)))

; Show all the rules in the *RULE-LIST*
(defun SHOW-RULES (&optional rules)
  (mapcar #'(lambda (rule)
	      (msg  rule ": "
		    "I can prove " (abbreviate-rule (rule-fact rule))
		    " if I can prove " (abbreviate-rule (rule-prove rule))
		    "." N))
    (or rules *RULE-LIST*))
  nil)

; Variable pattern accessing functions
(defun var-p (element)
  (and (listp element) (eq (car element) '*VAR*)))

(defun var-name (element)
  (cadr element))

; Change (*VAR* X) into ?x
(defun abbreviate-rule (rule)
  (cond ((null rule)
	 nil)
	((atom rule)
	 rule)
	((var-p rule)
	 (implode (cons '\? (explode (var-name rule)))))
	(t
	 (cons (abbreviate-rule (car rule))
	       (abbreviate-rule (cdr rule))))))

; Change ?x into (*VAR* X)
(defun unabbreviate-rule (rule)
  (cond ((null rule)
	 nil)
	((atom rule)
	 (let ((chars (explode rule)))
	    (cond ((eq (car chars) '?)
		   (list '*VAR* (implode (cdr chars))))
		  (t rule))))
	(t
	 (cons (unabbreviate-rule (car rule))
	       (unabbreviate-rule (cdr rule))))))

; Match two rule patterns together, returning nil if they don't count,
; or a set of variable bindings if they do (or t if there were no
; variables.) 
(defun match-rule (fact-pat fact bindings)
  (cond
    ((and (null fact-pat) (null fact)) (or bindings t))
    ((or (null fact-pat) (null fact)) nil)
    ((var-p fact-pat)
      (add-binding (var-name fact-pat)
		  fact bindings))
    ((atom fact-pat)
     (cond ((eq fact-pat fact) (or bindings t))
	   (t nil)))
    (t (let ((new-bindings (match-rule (car fact-pat) (car fact) bindings)))
	 (cond (new-bindings
		 (match-rule
		   (cdr fact-pat) (cdr fact)
		   (cond ((eq new-bindings t) nil)
			 (t new-bindings))))
	       (t nil))))))

; extract the value from one binding
(defun binding-val (binding)
  (cadr binding))

; Bind a name to a value in a list of bindings if it's not already bound
; to something else. If it's the latter case, then return nil.
(defun add-binding (name val bindings)
  (let ((binding (assoc name bindings)))
    (cond (binding
	   (and (eq (binding-val binding) val)
                bindings))
	  (t (cons (list name val) bindings)))))

; Assert a bunch of facts we know are justified.
; Return a list of all the facts asserted so far this proof.
(defun assert-facts (rule fetched-facts new-facts)
   (cond ((null fetched-facts)
	  new-facts)
	 (t
	  (let ((new-fact
		    (ASSERT (instantiate (rule-fact rule)
					 (fact-bindings
					   (car fetched-facts))))))
	      (set-status new-fact (list 'INFERRED rule))
	      (cons new-fact
		    (assert-facts rule (cdr fetched-facts) new-facts))))))

; Try to prove a guess, and if it succeeds, assert the stuff that can be
; concluded.
; (You're in a little maze of twisting passages, all different.)
(defun try-guess (conjecture new-facts rules fact-bindings guess)
  (let ((result (prove0 guess)))
       (cond
	 (result
	  (prove1 conjecture
		  (assert-facts (car rules)
				(fetch (rule-prove (car rules))
				       '*KB*)
				(append (cond ((eq result 'KNOWN) nil)
					      (t result))
					new-facts))
		  (cdr rules)))
	 (t
	   (prove1 conjecture new-facts (cdr rules))))))

; We found a rule that matches our conjecture, so make a guess
; by instantiating the variables in the prove part of the rule,
; and trying to prove the guess.
; (You're in a little twisting maze of passages, all different.)
(defun prove2 (conjecture new-facts rules fact-bindings)
  (cond
    (fact-bindings
      (try-guess conjecture new-facts rules fact-bindings
		 (instantiate (rule-prove (car rules))
			      fact-bindings)))
    (t
      (prove1 conjecture new-facts (cdr rules)))))

; Match the next rule against the conjecture, and try to chain back 
; to known facts if it matches. If there are no more rules left, return
; any facts that have been proven.
; (You're in a maze of twisting little passages, all different.)
(defun prove1 (conjecture new-facts rules)
  (cond
    (rules
      (prove2 conjecture new-facts rules
	      (match-rule (rule-fact (car rules)) conjecture nil)))
    (t
      new-facts)))

; Check to see if there's something already in the knowledge base 
; that matches the fact we're trying to prove. If so, return KNOWN.
; Otherwise, look for matching rules and try to chain back through
; them.
; (You're an amazingly twisted little ass, always different.)
(defun prove0 (conjecture)
  (cond
    ((match-fetch conjecture () '*KB*)
     'KNOWN) 
    (t (prove1 conjecture nil *RULE-LIST*))))

; The documented prove, which allows the notation ?x for specifying
; variables.
(defun PROVE (conjecture)
  (prove0 (unabbreviate-rule conjecture)))

; Plug the values of variables defined in the bindings into slots of 
; the same name in the pattern. 
(defun instantiate (pat bindings)
  (cond
    ((null pat) nil)
    ((atom pat) pat)
    ((var-p pat)
     (cond ((binding-val (assoc (var-name pat) bindings)))
	   (t pat)))
    (t (cons (instantiate (car pat) bindings)
	     (instantiate (cdr pat) bindings)))))