;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - NFS Share File - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(in-package 'user :use '(lisp))

(export '(cr *null-antecedent-rules* *rules* rule-head rule-body rule-number
	     make-new-rule b add-inference-rule
	     rule-alpha rn copy-rule))


;The function cr is the performance bottleneck of the system.
;Implementing cr requires implementing a theorem prover for the
;the given inference rules.  This implementation uses upsilon
;to convert the given rules into Boolean Horn clauses which can
;then be run in a forward chaining manner very efficiently.

;A node is a data structure that represents an
;expression.  Unlike list-structure repsentations, node representations
;have the property that equal expressions are eq objects.

;Various kinds of nodes need various kinds of slots -- we just include
;all the slots in the basic data structure.

(initable)

(defmacro forward-declare-nondeterministic-functions (&rest symlist)
  `(progn ,@(mapcar (lambda (sym) `(forward-declare-nondeterministic ,sym)) symlist)))

(forward-declare-nondeterministic-functions
  choose-nodes-for-exps
  find-nodes-for-formulas
  find-node-for-formula
  find-subnode
  find-node-if-bound
  find-nodes-for-terms)


(def-inited-var *rules* nil)
(def-inited-var *null-antecedent-rules* nil)

(def-inited-var *rule-count* 0)

(defvar *rule-table* (make-array 10000))

(def-inited-var *alpha* nil)
(def-inited-var *goal* nil)
(def-inited-var *true-formulas* nil)
(def-inited-var *upsilon* nil)
(def-inited-var *label-formula-nodes* nil)
(def-inited-var *nodes-available* nil)

(def-inited-var *node-count* 0)
(defvar *node-table* (make-hash-table :test #'equal))


(defmacro rn (n)
  `(aref *rule-table* ,n))

(defstruct (rule (:print-function (lambda (self stream &rest ignore)
				    (format stream "[rule ~s ~s ~s]"
						(rule-number self)
						(rule-body self)
						(rule-head self)))))
  head
  body
  superficial-head
  superficial-body
  number
  alpha
  superficial-alpha
  body-orderings
  covering-expressions)

(defvar *is-alpha* nil)
(defun make-new-rule (head body &optional (alpha nil) &key (optional-rule nil))
  (when alpha
    (setf *is-alpha* (gensym "IS-ALPHA?-"))
    (make-declaration *is-alpha* `((,(expression-type alpha)) B)))
  (let* ((enriched-body (if alpha
			    (cons `(,*is-alpha* ,alpha) body)
			    body))
	 (rule (create-rule-expression-2
		 (make-congruence-rule (make-rule :head head
						  :body enriched-body
						  :number (incf *rule-count*)
						  :alpha alpha)))))
    (when alpha
      (setf (rule-body rule) (remove *is-alpha* body :key #'car))
      (setf (rule-superficial-alpha rule) (second (find *is-alpha*
							(rule-superficial-body rule)
							:key #'car)))
      (setf (rule-superficial-body rule)
	    (remove *is-alpha* (rule-superficial-body rule) :key #'car)))

    (setf (rn (rule-number rule)) rule)
    (unless optional-rule
      (if (null (rule-body rule))
	  (push rule *null-antecedent-rules*)
	  (push rule *rules*)))
    
    (setf (rule-body-orderings rule) (generate-body-orderings (rule-superficial-body rule)
							      (rule-superficial-head rule)))
;;      (compute-covering-expressions rule)
    rule))

(defun generate-body-orderings (body consequent)
  (mapcan (lambda (first-ant)
	    (unless (and (consp first-ant) (eq (car first-ant) '=))
	      (iterate order-rest ((remaining-ants (remove first-ant body))
				   (rev-result (list first-ant))
				   (vars-bound (expression-variables-of first-ant)))
		(if (null remaining-ants)
		    (if (subsetp (expression-variables-of consequent)
				 vars-bound)
			(list (nreverse rev-result))
			(error "Unbound rule consequent: ~s" consequent))
		    (let ((next-ant (find-if (lambda (ant)
					       (some-intersection (expression-variables-of ant)
								  vars-bound))
					     remaining-ants)))
		      (if next-ant
			  (order-rest (remove next-ant remaining-ants)
				      (cons next-ant rev-result)
				      (union (expression-variables-of next-ant) vars-bound))
			  (error "Unthreaded rule antecedents: ~s" body)))))))
	  body))


(defun add-inference-rule (head body alpha &key (optional nil))
  (make-new-rule head body alpha :optional-rule optional))


(defun clear-upsilon ()
  (setf *nodes-available* (nconc *label-formula-nodes*
				 *upsilon*
				 (when *alpha* (list *alpha*))
				 *nodes-available*))
  (setf *alpha* nil)
  (setf *upsilon* nil)
  (setf *label-formula-nodes* nil)
  (setf *true-formulas* nil)
  (clrhash *node-table*))

(defun install-upsilon (upsilon)
  (dolist (exp upsilon)
    (parse-upsilon-exp exp)))

(defun cr (sigma upsilon &optional (alpha nil) &key (goal nil) (optional-rules nil))
  (let ((*rules* *rules*)
	(*null-antecedent-rules* *null-antecedent-rules*))
    (mapc (lambda (rule) (if (null (rule-body rule))
			     (push rule *null-antecedent-rules*)
			     (push rule *rules*)))
	  optional-rules)
    (catch 'goal-asserted
      (clear-upsilon)
      (let ((*goal* (when goal (parse-label goal))))
	(setf *alpha* (when alpha (parse alpha 'parse-upsilon-exp)))
	(install-upsilon upsilon)
	(fire-null-antecedent-rules)
	(dolist (phi sigma)
	  (assert-label (parse-label phi)))
	(nmapcar 'unparse *true-formulas*)))))


(defvar *parsed-nodes* nil)

(defstruct (node (:print-function (lambda (self stream &rest ignore)
				    (format stream "[node ~s]"
						(node-unparse self)))))
  key
  type
  parents
  true-formulas
  unparse
  in-upsilon?
  true?)

(defun parse-label (exp)
  (let* ((*parsed-nodes* nil)
	 (node (parse exp 'parse-upsilon-exp)))
    (setf *label-formula-nodes* (nconc *parsed-nodes* *label-formula-nodes*))
    node))

(defun parse-upsilon-exp (exp)
  (let* ((*parsed-nodes* nil)
	 (node (parse exp 'parse-upsilon-exp)))
    (mapc (lambda (node) (setf (node-in-upsilon? node) t)) *parsed-nodes*)
    (setf *upsilon* (nconc *parsed-nodes* *upsilon*))
    node))

(defun parse (expression recurse-fun &key (freeze-upsilon nil))
  (if (typep expression 'node)
      expression
      (let ((key (if (consp expression)
		     (mapcar recurse-fun expression)
		     expression)))
	(or (gethash key *node-table*)
	    (and (not freeze-upsilon)
		 (let* ((node-list (new-node))
			(node (car node-list)))
		   (setf *parsed-nodes* (nconc *parsed-nodes* node-list))
		   (setf (gethash key *node-table*) node)
		   (setf (node-type node)
			 (if (symbolp key)
			     (expression-type key)
			     (combination-type
			       (mapcar 'node-type key))))
		   (if (consp key)
		       (progn
			 (dolist (child key)
			   (push node (node-parents child)))
			 (setf (node-unparse node) (mapcar 'node-unparse key)))
		       (setf (node-unparse node) key))
		   (setf (node-key node) key)
		   node))))))

(defun unparse (node)
  (node-unparse node))

(defun parse-if-upsilon (exp)
  (let ((node (parse exp 'parse-if-upsilon :freeze-upsilon t)))
    (when (and node
	       (node-in-upsilon? node))
      node)))

(defun new-node ()
  (when *nodes-available*
    (let ((first *nodes-available*))
      (setf *nodes-available* (rest *nodes-available*))
      (setf (rest first) nil)
      (setf (node-parents (first first)) nil)
      (setf (node-true-formulas (first first)) nil)
      (setf (node-true? (first first)) nil)
      (setf (node-in-upsilon? (first first)) nil)
      first))
  (list (make-node)))

(defun fire-null-antecedent-rules ()
  (mapc 'assert-label
	(all-values
	  (let ((null-rule (member-of *null-antecedent-rules*)))
	    (when (and (rule-alpha null-rule)
		       (node-p *alpha*))
	      (when (not (equal? (rule-superficial-alpha null-rule) (node-unparse *alpha*)))
		(fail)))
	    (choose-nodes-for-exps (rule-superficial-head null-rule))
	    (parse-label (apply-substitution (rule-superficial-head null-rule)))))))

;; phi is a label-formula-node
;;
(defun assert-label (phi)
  (when (eq *goal* phi) (throw 'goal-asserted (list (node-unparse phi))))
  (let ((key (node-key phi)))
    (unless (node-true? phi)
      (setf (node-true? phi) t)
      (push phi *true-formulas*)
      (when (consp (node-key phi))
	(dolist (upsilon-exp (rest key))
	  (push phi (node-true-formulas upsilon-exp))))
      (mapc 'assert-label
	    (all-values
	      (let* ((rule (member-of *rules*))
		     (ordering (member-of (rule-body-orderings rule))))
		(when (rule-alpha rule)
		  (ensuring (equal? (node-unparse *alpha*) (rule-superficial-alpha rule))))
		(ensuring (and (equal? (node-unparse phi) (first ordering))
			       (nd-every2 #'(lambda-nondeterministic (subnode subexp)
					      (or (not (eq subnode *alpha*))
						  (equal? subexp
							  (rule-superficial-alpha rule))))
					  (node-key phi)
					  (first ordering)))
		  (find-nodes-for-formulas (rest ordering) (rule-superficial-alpha rule))
		  (let ((consequent (mapcar 'parse-if-upsilon
					    (apply-substitution
					      (rule-superficial-head rule)))))
		    (ensuring (not (some 'null consequent))
		      (parse-label consequent)))))))))
  t)

(defun-nondeterministic find-nodes-for-formulas (formula-list alpha)
  (when formula-list
    (find-node-for-formula (first formula-list) alpha)
    (find-nodes-for-formulas (rest formula-list) alpha)))

(defun-nondeterministic find-node-for-formula (formula alpha)
  (when (consp formula)
    (if (eq (car formula) '=)
	(let ((parent (find-node-if-bound (second formula))))
	  (if parent
	      (ensuring (equal? (node-unparse parent) (third formula)))
	      (let* ((bound-subterm (find-subnode (rest (third formula))))
		     (parent (member-of (node-parents bound-subterm))))
		(ensuring (and (equal? (node-unparse parent) (third formula))
			       (equal? (node-unparse parent) (second formula))
			       (or (not (eq *alpha* parent))
				   (eq alpha (second formula))))))))
	(let ((bound-subterm (find-subnode (rest formula))))
	  (let ((phi (member-of (node-true-formulas bound-subterm))))
	    (ensuring (and (equal? (node-unparse phi) formula)
			   (nd-every2 #'(lambda-nondeterministic (subnode subexp)
					  (or (not (eq subnode *alpha*))
					      (equal? subexp alpha)))
				      (node-key phi)
				      formula))))))))


(defun-nondeterministic find-subnode (term-list)
  (let ((subnode (find-node-if-bound (first term-list))))
    (or subnode
	(find-subnode (rest term-list)))))

(defun-nondeterministic find-node-if-bound (term)
  (if (consp term)
      (let ((subnode (find-subnode (rest term))))
	(let ((parent-term (member-of (node-parents subnode))))
	  (ensuring (equal? (node-unparse parent-term) term)
	    parent-term)))
      (let ((real-term (apply-substitution term)))
	(cond ((consp real-term) (find-node-if-bound real-term))
	      ((null (expression-variables-of real-term))
	       (or (and *alpha* (when (equal real-term (unparse *alpha*)) *alpha*))
		   (parse-if-upsilon real-term)
		   (fail)))
	      (t nil)))))

(defun-nondeterministic choose-nodes-for-exps (exp-list)
  (when exp-list
    (let ((node (member-of *upsilon*)))
      (when (not (equal? (node-unparse node) (first exp-list)))
	(fail)))
    (choose-nodes-for-exps (rest exp-list))))

(defun create-rule-expression-2 (rule)
  (let ((rule (copy-rule rule)))
    (selectmatch (create-expression (list (rule-superficial-alpha rule)
					  (rule-superficial-head rule)
					  (rule-superficial-body rule)))
      ((?alpha ?head ?body)
       (setf (rule-superficial-alpha rule) ?alpha)
       (setf (rule-superficial-head rule) ?head)
       (setf (rule-superficial-body rule) ?body)))
    rule))

(defun apply-rule-substitution (rule)
  (let ((rule (copy-rule rule)))
    (selectmatch (apply-substitution (list (rule-superficial-alpha rule)
					   (rule-superficial-head rule)
					   (rule-superficial-body rule)))
      ((?alpha ?head ?body)
       (setf (rule-superficial-alpha rule) ?alpha)
       (setf (rule-superficial-head rule) ?head)
       (setf (rule-superficial-body rule) ?body)))
    rule))


(defun alpha-rename-rule (rule)
  (let ((rule (copy-rule rule)))
    (selectmatch (alpha-rename (list (rule-superficial-alpha rule)
				     (rule-superficial-head rule)
				     (rule-superficial-body rule)))
      ((?alpha ?head ?body)
       (setf (rule-superficial-alpha rule) ?alpha)
       (setf (rule-superficial-head rule) ?head)
       (setf (rule-superficial-body rule) ?body)))
    rule))

(defun expression-variables-of-rule (rule)
  (union (union (expression-variables-of (rule-superficial-head rule))
		(expression-variables-of (rule-superficial-body rule)) :test #'equal)
	 (expression-variables-of (rule-superficial-alpha rule))
	 :test #'equal))




;congruence conversion

;To describe the output of congruence conversion some new terminology is needed.

;A ``truth slot expression'' is defined to be either a proposition variable
;or an application of a monadic predicate other than NOT.

;A ``binary antecedent'' is an application of a binary predicate other than =.

;After congruence conversion, every antecedent is one of the following.
;
;1. An equation (= ?x (op ?y1 ... ?yn)) where ?x and each ?yi are variables.
;2. A binary antecedent as defined above.
;3. The negation of a truth slot expression.
;4. A truth slot expression.
;

;After congruence conversion, a conclusion is either a an expresion of the
;form (lisp <lisp-form>), an equation between variables, or one of 2, 3, or 4 above.
;

(defun make-congruence-rule (rule)
  (let* ((congruence-formulas (mapcan (lambda (formula)
					(congruence-convert-formula formula))
				      (cons (rule-head rule)
					    (rule-body rule))))
	 (equality-antecedents (remove-if-not (lambda (form)
						(and (consp form)
						     (eq (car form) '=)))
					      (cdr congruence-formulas)))
	 (find-map (congruence-closure equality-antecedents))
	 (antecedents (remove-duplicates
			(sublis find-map (cdr congruence-formulas))
			:test #'equal))
	 (conclusion (sublis find-map (car congruence-formulas))))

    (if (not (null (rule-body rule)))
	(progn (setf (rule-superficial-head rule) conclusion)
	       (setf (rule-superficial-body rule) (remove-if (lambda (ant)
							       (selectmatch ant ((= ?x ?x) t)))
							     antecedents)))
	(progn (setf (rule-superficial-head rule) (rule-head rule))
	       (setf (rule-superficial-body rule) (rule-body rule))))
    rule))

;The following function reduces the given expression to a single variable.

(defun congruence-convert (expression)
  (cond ((variable? expression)
	 (list expression))
	((not (consp expression))
	 (error "Error in rule: constants must be phrase constructors of no arguments"))
	(t
	 (let* ((congruence-args (mapcar (lambda (arg)
					   (congruence-convert arg))
					 (cdr expression)))
		(new-var (gensym "?QVAR-"))
		(new-exp `(,(car expression) ,@(mapcar #'car congruence-args)))
		(new-var-type (expression-type new-exp)))
	   (make-declaration new-var new-var-type)
	   `(,new-var
	     (= ,new-var ,new-exp)
	     ,@(mapcan #'cdr congruence-args))))))

;The following function replaces top level subexpressions by variables.

(defun congruence-convert2 (exp)
  (selectmatch (congruence-convert exp)
    ((?var (= ?var ?exp2) . ?rest)
     `(,?exp2 ,@?rest))
    (?x ?x)))

;The following function normalizes an antecedent.

(defun congruence-convert-formula (formula)
  (selectmatch formula
    ((lisp :anything) (error "Locality tester cannot handle LISP consequents in rules"))
    ((when :anything) (error "Locality tester cannot handle WHEN antecedents in rules"))
    (:anything (congruence-convert2 formula))))


;Whenever the antecedents require to variables ?x and ?y to have the same value
;the rule can be rewritten to use a single variable ?z rather than ?x and ?y.
;A congruence closure procedure is used to determine all forced identities
;between variables in the antecedent set.

;Congruence-convert-formula might return an equation between variables.
;The congruence-closure elimination of redundant variables will eliminate
;all such equations.

;The following procedure assumes that the first argument in each given equation
;is a variable.

(defun congruence-closure (equations)
  (let ((find-alist nil)
	(congruence-alist nil))
    (dolist (equation equations)
      (let ((e1 (second equation))
	    (e2 (third equation)))
	(if (variable? e2)
	    (setq find-alist (alist-union e1 e2 find-alist))
	    (push (cons e2 e1) congruence-alist))))
    (congruence-closure2 find-alist congruence-alist)))

(defun alist-find (var alist)
  (or (cdr (assoc var alist))
      var))

(defun alist-union (var1 var2 alist)
  (let ((v1 (alist-find var1 alist))
	(v2 (alist-find var2 alist)))
    (if (eq v1 v2)
	alist
	(acons v1 v2 (mapcar (lambda (cell)
			       (if (eq (cdr cell) v1)
				   (cons (car cell) v2)
				   cell))
			     alist)))))

(defun congruence-closure2 (find-alist congruence-alist)
  (let ((new-congruence-alist (sublis find-alist congruence-alist)))
    (mvlet (((v1 v2 smaller-congruence-alist) (find-equation new-congruence-alist)))
      (if v1
	  (congruence-closure2 (alist-union v1 v2 find-alist)
			      smaller-congruence-alist)
	  find-alist))))

(defun find-equation (congruence-alist)
  (if (null congruence-alist)
      (values nil nil nil)
      (let* ((first-cell (car congruence-alist))
	     (redundant-cell (assoc (car first-cell)
				    (cdr congruence-alist)
				    :test #'equal)))
	(if redundant-cell
	    (values (cdr first-cell) (cdr redundant-cell) (cdr congruence-alist))
	    (mvlet (((v1 v2 rest-alist) (find-equation (cdr congruence-alist))))
	      (values v1 v2 (cons first-cell rest-alist)))))))