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

(in-package :rules :use '(lisp util))

(eval-when (compile load eval)
  (in-package 'rules :use '(lisp util)))

(export '(defextender
          assert-internal
	  intern-node
	  intern-node2
	  goto-context

	  ;;macro for defining inference rules
	  defnoticer
	  
	  ;;functions for querying data base
	  query

	  ;;explanation function
	  why
	  justification-for
	  print-justification
	  just-assertion
	  just-rule-name
	  just-subjustifications
	  *record-justifications*
	  value-of
	  up
	  current
	  
	  ;;functions for creating justifications
	  justification
	  create-justification
	  *justification-table*

	  ;;predicates with distinguished meanings
	  production
	  =
	  has-value
	  true
	  false
	  consider!
	  ?justification
	  by-definition

	  clear-data-base
	  node-other-assertions
	  node-binaries-forward
	  node-binaries-backward
	  node-monadic-properties
	  noticers
	  replacement
	  dead?))

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

(defvar *node-limit* 10000)

(defvar *node-counter* 0)

(defvar *intern-table* (make-hash-table :test 'equal))

(defvar *record-justifications* t)

(defvar *justification-table* (make-hash-table :test #'equal))

(defvar *truth-table* (make-hash-table :test #'equal))

(defvar *contradiction* nil)

(defvar *justification-stack* nil)

(defvar *congruence-table* (make-hash-table :test #'equal))

(defvar *value-table* (make-hash-table :test #'equal))

(defvar *frame-stack* nil)

(defvar *assertion-noticers* nil)

(defun clear-data-base ()
  (clear-undo-stack)
  (clrhash *justification-table*)
  (clrhash *truth-table*)
  (clrhash *intern-table*)
  (fill-array *node-table* nil)
  (clrhash *congruence-table*)
  (clrhash *value-table*)
  (setq *contradiction* nil)
  (setq *node-counter* 0)
  (setq *frame-stack* nil)
  (assert-internal '(true) 'by-definition)
  (assert-internal `(has-value ,(intern-node '(true)) true) 'by-definition))

;;properties of rule names

(property-macro antecedent-list)

(property-macro noticers)


;========================================================================
;the node data structure and clear-data-base
;========================================================================

(defstruct (node (:predicate nodep)
		 (:conc-name node-)
		 (:print-function print-node))
  index
  constructor
  args
  dead-flag
  (size 1)
  monadic-properties
  binaries-forward
  binaries-backward
  other-assertions)

(defun kill! (x)
  (setf-undo (node-dead-flag x) t))

(defun dead? (x)
  (and (nodep x)
       (node-dead-flag x)))

(defun print-node (self stream ignore)
  (declare (ignore ignore))
  (format stream "[~s ~s]" (node-index self) (node-expression self)))

(defun node-expression (node)
  (if (nodep node)
      (cons (node-constructor node)
	    (mapcar #'node-expression (node-args node)))
      node))

(defmacro node (n)
  `(aref *node-table* ,n))

(defvar *vag-expand*)

(defun intern-node (exp)
  (intern-node2 (funcall *vag-expand* exp)))

(defun intern-node2 (exp)
  (cond ((nodep exp) exp)
	((symbolp exp)
	 (intern-node2 (list :the-variable (list 'quote exp))))
	((or (numberp exp)
	     (and (consp exp)
		  (eq (car exp) 'quote)))
	 (intern-value exp))
	((and (consp exp)
	      (eq (car exp) 'lambda))
	 (intern-value `(quote ,exp)))
	((consp exp)
	 (intern-app (car exp) (mapcar #'intern-node2 (cdr exp))))
	(t
	 (error "unknown expression type ~s" exp))))

(defun intern-value (exp)
  (or (gethash exp *intern-table*)
      (let ((newnode (make-node)))
	(setf-undo (node-index newnode) (incf-undo *node-counter*))
	(when (< *node-counter* *node-limit*)
	  (setf-undo (aref *node-table* (node-index newnode)) newnode))
	(setf (node-constructor newnode) 'quote)
	(setf-undo (gethash exp *intern-table*) newnode)
	(if (numberp exp)
	    (progn
	      (setf (node-args newnode) (list exp))
	      (assert-internal `(has-value ,newnode ,exp) 'by-definition))
	    (progn (setf (node-args newnode) (cdr exp))
		   (assert-internal `(has-value ,newnode ,(second exp)) 'by-definition)))			 
	newnode)))

(defun intern-app (fun argnodes)
  (let ((key (cons fun argnodes)))
    (or (gethash key *intern-table*)
	(let ((newnode (make-node :constructor fun :args argnodes)))
	  (setf-undo (node-index newnode) (incf-undo *node-counter*))
	  (when (< *node-counter* *node-limit*)
	    (setf-undo (node (node-index newnode)) newnode))
	  (setf-undo (gethash key *intern-table*) newnode)
	  (assert-internal `(production ,newnode ,fun ,@argnodes) 'by-definition)
	  newnode))))



;========================================================================
;justifications and assert-internal
;========================================================================

;;A justification is a triple of a justified fact, a rule name (the rule from
;;which the fact is derived, and a list of subjustifications which are justifications
;;for the antecedents used in the rule.

;; The subjustifications field of this data structure is a "lazy field"
;; This means the value is computed in an "on demand" fasion.

(defstruct (justification (:predicate justificationp)
			  (:conc-name just-)
			  (:print-function short-print-justification))
  rule-name
  assertion-internal
  subjustifications-internal)

(defmacro create-justification (rname subjustifications)
  `(make-justification
    :rule-name ,rname
    :subjustifications-internal (lambda () ,subjustifications)))

(defun just-assertion (just)
  (let ((assert (just-assertion-internal just)))
    (cond ((eq (car assert) 'production)
	   `(= ,(node-expression (second assert))
	     (,(third assert) ,@(mapcar #'node-expression (cdddr assert)))))
	  ((eq (car assert) 'replace!)
	   `(= ,@(mapcar #'node-expression (cdr assert))))
	  (t (cons (car assert) (mapcar #'node-expression (cdr assert)))))))

(defun just-subjustifications (just)
  (funcall (just-subjustifications-internal just)))

(defun short-print-justification (self stream ignore)
  ignore
  (format stream "[Justification from ~s]" (just-rule-name self)))

;;the following function returns a justification.  It can take a numerical argument
;;in which case it can be used to walk the justification tree.

(defvar *traced-assertions* nil)

(defun atrace (symbol)
  (pushnew symbol *traced-assertions*))

(defun auntrace ()
  (setq *traced-assertions* nil))

(defun assert-internal (assertion &optional justification)
  (unless *contradiction*
    (unless (gethash assertion *truth-table*)
      (when (member (car assertion) *traced-assertions*)
	(format t "~%asserting ~s" assertion))
      (when (equal assertion '(false))
	(setf-undo *contradiction* t))
      (setf-undo (gethash assertion *truth-table*) t)
      (cond ((justificationp justification)
	     (setf (just-assertion-internal justification)
		   assertion)
	     (setf (gethash assertion *justification-table*) justification))
	    (t
	     (let ((new-just (create-justification (or justification 'null-justification) nil)))
	       (setf (just-assertion-internal new-just) assertion)
	       (setf (gethash assertion *justification-table*) new-just))))
      (selectmatch assertion
	((:anything) nil)
	((?pred ?arg)
	 (when (nodep ?arg)
	   (push-undo ?pred (node-monadic-properties ?arg))))
	((?pred ?arg1 ?arg2)
	 (when (nodep ?arg1)
	   (push-undo ?arg2 (assoc-value ?pred (node-binaries-forward ?arg1))))
	 (when (nodep ?arg2)
	   (push-undo ?arg1 (assoc-value ?pred (node-binaries-backward ?arg2)))))
	((?pred . ?args)
	 (dolist (arg ?args)
	   (when (nodep arg)
	     (push-undo ?args (assoc-value ?pred (node-other-assertions arg)))))))
      (dolist (noticer (noticers (car assertion)))
	(funcall noticer (cdr assertion)))
      (dolist (noticer *assertion-noticers*)
	(funcall noticer (car assertion) (cdr assertion)))
      (when (member (car assertion) *traced-assertions*)
	(format t "~%finishing ~s" assertion))
      t)))


;========================================================================
;defnoticer for defining inference rules
;========================================================================

(defmacro defnoticer (name antecedents &rest body)
  (selectmatch (first antecedents)
    ((?pred . ?args)
     (unless (and (symbolp ?pred)
		  (listp ?args)
		  (every #'symbolp ?args))
       (error "illegal noticer head ~s" (first antecedents)))
     (let ((arg (gentemp "ARG-")))
       `(eval-when (compile load eval)
	 (setf (noticers (caar (antecedent-list ',name)))
	  (remove ',name (noticers (caar (antecedent-list ',name)))))
	 ,@(when body
	     `((setf (antecedent-list ',name) ',antecedents)
	       (defun ,name (,arg)
		 ,(make-bindings arg ?args nil (lambda (bv) (process-antecedents name (rest antecedents) body bv))))
	       (pushnew ',name (noticers ',?pred)))))))
    (:anything
     (error "illegal noticer head ~s" (first antecedents)))))

(emacs-indent defnoticer 2)

(defun bound? (obj bound-vars)
  (or (not (util:variable? obj))
      (member obj bound-vars)))

(defun add-quote (x)
  (if (util:variable? x)
      x
      `',x))

(defun rule-variables (rname)
  (antecedent-variables (antecedent-list rname) nil))

(defun antecedent-variables (ants bound-vars)
  (if (null ants)
      bound-vars
      (ant-vars (car ants) (cdr ants) bound-vars)))

(defun ant-vars (ant rest bound-vars)
  (cond ((null ant)
	 (antecedent-variables rest bound-vars))
	((bound? (car ant) bound-vars)
	 (ant-vars (cdr ant) rest bound-vars))
	(t
	 (ant-vars (cdr ant) rest (cons (car ant) bound-vars)))))

(defun process-antecedents (rname antecedents body bound-vars)
  (if (null antecedents)
      `	(let ((?justification (when *record-justifications*
				(make-rule-justification ',rname (list ,@bound-vars)))))
	  ,@body)
      (selectmatch (first antecedents)
	((when ?test)
	 `(when ,?test
	   ,(process-antecedents rname (rest antecedents) body bound-vars)))
	((?pred . ?args)
	 (cond ((and (bound? ?pred bound-vars)
		     (every #'(lambda (arg) (bound? arg bound-vars))
			    ?args))		     
		`(when (gethash
			(list ,@(mapcar 'add-quote (cons ?pred ?args)))
			*justification-table*)
		  ,(process-antecedents rname (rest antecedents) body bound-vars)))
	       ((or (null ?args) (null (cdr ?args)))
		(error "insufficiently bound antecedent ~s" (car antecedents)))
	       (t
		(selectmatch ?args
		  ((?arg1 ?arg2)
		   (if (bound? ?pred bound-vars)
		       (if (not (bound? ?arg2 bound-vars))
			   `(dolist (,?arg2 (assoc-value ,(add-quote ?pred ) (node-binaries-forward ,?arg1)))
			     ,(process-antecedents rname (rest antecedents) body (cons ?arg2 bound-vars)))
			   `(dolist (,?arg1 (assoc-value ,(add-quote ?pred ) (node-binaries-backward ,?arg2)))
			     ,(process-antecedents rname (rest antecedents) body (cons ?arg1 bound-vars))))
		       (cond ((and (util:variable? ?arg1)
				   (member ?arg1 bound-vars))
			      (let ((temp (gentemp "TEMP-")))
				`(dolist (,temp (node-binaries-forward ,?arg1))
				  (let (,?pred (car ,temp))
				    (dolist (?arg2 (cdr ,temp))
				      ,(process-antecedents rname (rest antecedents) body (list* ?pred ?arg2 bound-vars)))))))
			     ((and (util:variable? ?arg2)
				   (member ?arg2 bound-vars))
			      (let ((temp (gentemp "TEMP-")))
				`(dolist (,temp (node-binaries-backward ,?arg2))
				  (let (,?pred (car ,temp))
				    (dolist (?arg1 (cdr ,temp))
				      ,(process-antecedents rname (rest antecedents) body (list* ?pred ?arg1 bound-vars)))))))
			     (t
			      (error "insufficiently bound antecedent ~s" (car antecedents))))))
		  (:anything
		   (let ((temp (gentemp "TEMP-"))
			 (arg (first-bound ?args bound-vars)))
		     (unless arg
		       (error "insufficienty bound antecedent ~s" (car antecedents)))
		     (if (bound? ?pred bound-vars)
			 `(dolist (,temp (assoc-value ,(add-quote ?pred) (node-other-assertions ,arg)))
			   ,(make-bindings temp ?args bound-vars (lambda (bvs)
								   (process-antecedents rname
											(rest antecedents)
											body
											bvs))))
			 (let ((pred-list (gentemp "TEMP-")))
			   `(dolist (,pred-list (other-properties ,arg))
			     (let ((?pred (car ,pred-list)))
			       (dolist (,temp (cdr ,pred-list))
				 ,(make-bindings temp ?args (cons ?pred bound-vars)
						 (lambda (bvs)
						   (process-antecedents rname
									(rest antecedents)
									body
									bvs)))))))))))))))))

(defun first-bound (args bound-vars)
  (when args
    (if (and (util:variable? (car args))
	     (member (car args) bound-vars))
	(car args)
	(first-bound (cdr args) bound-vars))))

(defun make-bindings (source args bound-vars cont)
  (if (null args)
      (funcall cont bound-vars)
      (let ((temp (gentemp "TEMP-")))
	`(let ((,temp ,source))
	  (when (consp ,temp)
	  ,(cond ((eq (first args) :anything)
		  (make-bindings `(cdr ,temp) (cdr args) bound-vars cont))
		 ((not (bound? (car args) bound-vars))
		  `(let ((,(first args) (car ,temp)))
		    (unless (dead? ,(first args))
		      ,(make-bindings `(cdr ,temp) (cdr args) (cons (car args) bound-vars) cont))))
		 (t
		  `(when (eq (car ,temp) ,(add-quote (car args)))
		    ,(make-bindings `(cdr ,temp) (cdr args) bound-vars cont)))))))))

(defun make-rule-justification (rname bound-vars)
  (create-justification
      rname
    (let ((bindings (mapcar #'cons
			    (rule-variables rname)
			    bound-vars)))
      (mapcar #'(lambda (ant)
		  (if (eq (car ant) 'when)
		      'by-computation
		      (let ((key (mapcar #'(lambda (var) (if (util:variable? var)
							  (assoc-value var bindings)
							  var))
				      ant)))
			(gethash key *justification-table*))))
	      (antecedent-list rname)))))




;========================================================================
;union-find
;========================================================================

(defnoticer basic-equality-noticer
    ((= ?x ?y))
  (unless (or (eq ?x ?y)
	      (not (nodep ?x))
	      (not (nodep ?y)))
    (if (< (node-index ?x)
	   (node-index ?y))
	(do-replacement ?y ?x ?justification)
	(do-replacement ?x ?y ?justification))))

(defun do-replacement (?x ?y ?justification)
  (kill! ?x)
  (incf (node-size ?y))
  (assert-internal `(replace! ,?x ,?y) ?justification))

(defmacro justification (rname &rest assertions)
  `(when *record-justifications*
    (create-justification ,rname
      (list ,@(mapcar #'(lambda (ass) `(gethash ,ass *justification-table*))
		     assertions)))))

(defun property-transfer (args)
  (unless (and (cdr args)
	       (null (cddr args)))
    (error "wrong number of args to replace!"))
  (let ((?x (car args))
	(?y (second args)))
    (dolist (pred (node-monadic-properties ?x))
      (let ((lex-pred pred))
	(assert-internal `(,pred ,?y) (when *record-justifications*
					(justification 'property-transfer `(replace! ,?x ,?y) `(,lex-pred ,?x))))))
    (dolist (plist (node-binaries-forward ?x))
      (let ((pred (car plist)))
	(unless (eq pred 'replace!)
	  (dolist (?z (cdr plist))
	    (let ((lex-z ?z))
	      (assert-internal (map-assertion pred (list ?x ?z) ?x ?y)
			       (justification 'property-transfer-a `(replace! ,?x ,?y) `(,pred ,?x ,lex-z))))))))
    (dolist (plist (node-binaries-backward ?x))
      (let ((pred (car plist)))
	(unless (eq pred 'replace!)
	  (dolist (?z (cdr plist))
	    (let ((lex-z ?z))
	      (assert-internal (map-assertion pred (list ?z ?x) ?x ?y)
			       (justification 'property-transfer-b `(replace! ,?x ,?y) `(,pred ,lex-z ,?x))))))))
    (dolist (plist (node-other-assertions ?x))
      (let ((pred (car plist)))
	(dolist (?z (cdr plist))
	  (let ((lex-z ?z))
	    (assert-internal (map-assertion pred ?z ?x ?y)
			     (justification 'property-transfer `(replace! ,?x ,?y) (cons pred lex-z)))))))))

(pushnew 'property-transfer (noticers 'replace!))

(defun map-assertion (pred args ?x ?y)
  (cons pred
	(mapcar #'(lambda (arg) (if (eq arg ?x) ?y arg))
		args)))

(defun property-transfer2 (pred args)
  (unless (eq pred 'replace!)
    (dolist (?x args)
      (when (nodep ?x)
	(let ((lex-x ?x))
	  (dolist (?y (assoc-value 'replace! (node-binaries-forward ?x)))
	    (let ((lex-y ?y))
	      (let ((just (justification 'property-transfer2
					       `(replace! ,lex-x ,lex-y)
					       (cons pred args))))
		(assert-internal (map-assertion pred args ?x ?y)
				 just)))))))))

(push 'property-transfer2 *assertion-noticers*)

(defnoticer true-equality ((production ?phi = ?x ?x))
  (assert-internal `(has-value ,?phi true) ?justification))

(defnoticer equality-noticer ((production ?phi = ?x ?y)
			      (has-value ?phi true))
  (assert-internal `(= ,?x ,?y) ?justification))

(defnoticer equality-noticer2 ((has-value ?phi true)
			       (production ?phi = ?x ?y))
  (assert-internal `(= ,?x ,?y) ?justification))


;========================================================================
;congruence-closure
;========================================================================

(push 'congruence-noticer (noticers 'production))

(defun congruence-noticer (?all-args)
  (unless (cdr ?all-args)
    (error "empty production"))
  (let ((?x (car ?all-args)))
    (unless (dead? ?x)
      (let ((key (cdr ?all-args)))
	(let ((cell (gethash key *congruence-table*)))
	  (when (null cell)
	    (setq cell (cons nil nil))
	    (setf-undo (gethash key *congruence-table*) cell))
	  (push-undo ?x (cdr cell))
	  (dolist (?y (cdr cell))
	    (unless (or (eq ?y ?x)
			(dead? ?y))
	      (let ((lex-y ?y))
		(assert-internal `(= ,?x ,?y)
				 (justification 'congruence
						      `(production ,?x ,@key)
						      `(production ,lex-y ,@key)))))))))))

(defnoticer same-value ((has-value ?x ?v))
  ?justification
  (unless (or (eq ?v 'true) (eq ?v 'false))
    (let ((cell (gethash ?v *value-table*)))
      (when (null cell)
	(setq cell (cons nil nil))
	(setf-undo (gethash ?v *value-table*) cell))
      (push-undo ?x (cdr cell))
      (dolist (?y (cdr cell))
	(unless (or (eq ?y ?x)
		    (dead? ?y))
	  (let ((lex-y ?y))
	    (assert-internal `(= ,?x ,?y)
			     (justification 'same-value
					    `(has-value ,?x ,?v)
					    `(has-value ,lex-y ,?v)))))))))

(defnoticer two-values ((has-value ?x ?v1)
			(has-value ?x ?v2))
  (when (not (equal ?v1 ?v2))
    (assert-internal '(false) ?justification)))

(defnoticer two-values2 ((production ?phi = ?x ?y)
			 (has-value ?x ?vx)
			 (has-value ?y ?vy))
  (when (not (equal ?vx ?vy))
    (assert-internal `(has-value ,?phi false) ?justification)))

(defnoticer two-values3 ((has-value ?x ?vx)
			 (production ?phi = ?x ?y)
			 (has-value ?y ?vy))
  (when (not (equal ?vx ?vy))
    (assert-internal `(has-value ,?phi false) ?justification)))

(defnoticer two-values4 ((has-value ?y ?vy)
			 (production ?phi = ?x ?y)
			 (has-value ?x ?vx))
  (when (not (equal ?vx ?vy))
    (assert-internal `(has-value ,?phi false) ?justification)))



;========================================================================
;query and why
;========================================================================
;;This is a simple version of query which operates only on binary predicates
;;and only for computing values of the second argument given the first.
;;Rules can be used to construct appropriate "output relations" which can
;;then be used by query.

(defun query (relname exp)
  (if (eq relname 'replace!)
      (mapcar #'node-expression (remove-if #'dead? (assoc-value relname (node-binaries-forward (intern-node exp)))))
      (mapcar #'node-expression (remove-if #'dead? (assoc-value relname (node-binaries-forward (replacement (intern-node exp))))))))

(defun equivalents (exp)
  (let ((node (intern-node exp)))
    (rprint (mapcan #'(lambda (prod)
			(when (eq (first prod) node)
			  (list (cons (second prod)
				      (mapcar #'node-expression (cddr prod))))))
		    (assoc-value 'production (node-other-assertions node))))))

(defun immediate-replacement (node)
  (car (assoc-value 'replace! (node-binaries-forward node))))

(defun replacement (node)
  (let ((next (immediate-replacement node)))
    (if next
	(replacement next)
	node)))

(defun immediate-replacement-just (node)
  (let ((next (car (assoc-value 'replace! (node-binaries-forward node)))))
    (when next
      (gethash `(replace! ,node ,next) *justification-table*))))

(defun replacement-justs (node)
  (let ((next (immediate-replacement node)))
    (when next
      (cons (immediate-replacement-just node)
	    (replacement-justs next)))))


(defun why (exp)
  (if (command? exp)
      (process-command exp)
      (let ((values (value-of exp)))
	(if (null (second values))
	    (format t "~%~s has no value" exp)
	    (let ((just (justification-for exp)))
	      (if just
		  (print-justification just)
		  (format t "~%~s has no recorded justificaiton" `(has-value ,exp ,(first values)))))))))

(defun value-of (exp)
  (value-from-undo-frame
   (let ((node (intern-node exp)))
     (assert-internal `(consider! ,node) 'value-of-premise)
     (let ((values (assoc-value 'has-value (node-binaries-forward (replacement node)))))
       (if values
	   (list (car values) t)
	   (list nil nil))))))

(defun justification-for (exp)
  (if (equal exp '(false))
      (gethash exp *justification-table*)
      (let ((node (intern-node exp)))
	(assert-internal `(consider! ,node) 'justification-for-premise)
	(let ((node2 (replacement node)))
	  (let ((vals (assoc-value 'has-value (node-binaries-forward node2))))
	    (when vals
	      (let ((just (gethash `(has-value ,node2 ,(car vals)) *justification-table*)))
		(let* ((subjusts (replacement-justs node)))
		  (if (null subjusts)
		      (return-just just)
		      (let ((just2 (create-justification 'replacement (cons just subjusts))))
			(setf (just-assertion-internal just2)
			      `(has-value ,node ,(car vals)))
			(return-just just2)))))))))))

(defun return-just (just)
  (when (justificationp just)
    (setq *justification-stack* (list just)))
  just)

(defun command? (exp)
  (or (integerp exp)
      (member exp `(up current))))

(defun process-command (com)
  (cond ((numberp com)
	 (when *justification-stack*
	   (let ((subjusts (just-subjustifications (car *justification-stack*))))
	     (when (and (>= com 1) (<= com (length subjusts)))
	       (let ((just (nth (1- com) subjusts)))
		 (when (justificationp just)
		   (push just *justification-stack*))
		 (print-justification just))))))
	((eq com 'up)
	 (pop *justification-stack*)
	 (print-justification (car *justification-stack*)))
	((eq com 'current)
	 (print-justification (car *justification-stack*)))))

(defun print-justification (just)
  (when just
    (format t "~%Justification: ~s is justified using ~s from:" (just-assertion just) (just-rule-name just))
    (let ((index 1))
      (dolist (subjust (just-subjustifications just))
	(cond ((not (justificationp subjust))
	       (format t "~%      ~a.   ~s" index subjust))
	      (t
	       (format t "~%      ~a.   ~s ~s" index (just-assertion subjust) (just-rule-name subjust))))
	(incf index))
      nil)))