;;; R. Williams
;;; Artificial Intelligence

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; The primary user routine here is FC, which draws all possible forward
;;; chaining conclusions from a set of facts and rules.  These results are
;;; displayed to the user and they are also stored in the list of facts
;;; if the optional argument to FC is given a non-nil value.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defvar *new-facts*)		   ; used to keep track of all derived facts

(defun fc (&optional (cumulative nil))
  (setq *new-facts* nil)
  (let ((saved-fc-db *fc-db*))
    (dolist (fact *facts*)	   ; add facts one at a time and see results
      (add-to-fc-db fact nil))
    (setq *fc-db* saved-fc-db)	   ; eliminate newly added stuff from *fc-db*
    (if cumulative
	(setq *facts* (append *facts* (reverse *new-facts*))))
    'done
    ))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; These 2 functions add an item to the internal forward chaining database
; *fc-db*.  In the process, they also recursively add all resulting forward
; chaining consequences to this database.  As each new fact is generated a
; message to this effect is printed out.  Neither the original rule list
; nor the original fact list are changed. This code is a modified version
; of a more general predicate calculus forward chainer.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun add-to-fc-db (formula from-rule)
  (push (make-fc-db-item :formula formula ; update pc fc database
		      :from-rule from-rule)
	*fc-db*)
  (let (new-conclusion)
    (dolist (item *fc-db*)		; try to combine this formula with
      (setq new-conclusion		; each formula already in the database
	    (combine formula (fc-db-item-formula item)))
      (if new-conclusion		; if there is a new conclusion
	  (add-fc-db-item new-conclusion ; add it recursively
			  (if (rule? formula) ; give it the number
			      from-rule	      ; corresponding to the rule
			      (fc-db-item-from-rule item)))) ; it came from
      )))

(defun add-fc-db-item (formula from-rule)
  (cond ((fact? formula)			; if this is a fact
	 (when (and (not (member formula *facts* ; and if it's truly new
				 :test #'equal))
		    (not (member formula *new-facts*
				 :test #'equal)))
	       (push formula *new-facts*)	; store it on new fact list
	       (format t			; and notify user
		 "Concluding new fact ~a from rule ~a~%" formula from-rule)
	       (add-to-fc-db formula from-rule))) ; and add it to fc database
	((lisp-escape? (second formula)) ;else if escape to lisp
	 (if (is-true? (lisp-form (second formula))) ;and evaluates to non-nil
	     (add-fc-db-item (third formula) from-rule))) ;add consequent
	(t 
	 (add-to-fc-db (standardize formula) from-rule))  ; else not a fact
	))				; so standardize and add to fc db

(defun combine (formula1 formula2)
  ; since we don't know which formula is the implication to use for forward
  ; chaining (they could both be implications!), try it both ways
  (or (fchain1 formula1 formula2)
      (fchain1 formula2 formula1)))

(defun fchain1 (formula if-formula)
  ; returns conclusion if the two formulas can be forward chained
  ; and nil otherwise; assumes the two formulas have already been
  ; standardized apart
  (if (eql (first if-formula) 'if)
      (let* ((antecedent (second if-formula))
	     (consequent (third if-formula))
	     (mgu-alist (unify formula antecedent)))
	(if (not (eql mgu-alist 'no))
	    (varsubst consequent mgu-alist))
	)))