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

;;This file uses util, screamer, exp-con, and fc-prover

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

;(shadow '(type-declarations make-declaration gensym-var-of-type))

;(defmacro type-declarations (&body declarations)
;  (let ((decl (gensym "DECL-")))
;    `(dolist (,decl ',declarations)
;       (make-declaration (first ,decl) (second ,decl)))))
;
;(defun make-declaration (symbol type)
;  (screamer::make-declaration symbol type)
;  (unify::make-declaration symbol type))
;
;(defun gensym-var-of-type (type &optional (string "VAR-") (package *package*))
;  (let ((var
;	  (loop
;	    (let ((var-string (format nil "?~s" (gentemp string))))
;	      (when (not (find-symbol var-string package))
;		(return (intern var-string package)))))))
;    (make-declaration var type)
;    var))

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

(forward-declare-nondeterministic-functions
  expand-by-rules
  match-gamma
  nd-remove-if
  an-inward-rule-on
  an-original-rule
  nd-some
  nd-every
  make-null-hypothesis)

(def-inited-var *types* nil)

(def-inited-var *constants* nil)

(defmacro rule (body &body head)
  `(rule-fun ',(car head) ',body))

(defun rule-fun (head body)
  (examine-expression head)
  (mapc #'examine-expression body)
  (unless (and (eq 'b (expression-type head))
	       (every (lambda (ant) (eq 'b (expression-type ant)))
		      body))
    (error "some rule component in ~s ~s is not of type Boolean"
	   body head))
  (selectmatch (list head body)
    ((?head ?body)
     (make-new-rule ?head ?body))))

(defun examine-expression (exp)
  (let ((type (expression-type exp)))
    (pushnew type *types* :test #'equal)
    (when (listp exp)
      (dolist (subexp exp)
	(unless (variables subexp)
	  (pushnew subexp *constants* :test #'equal))
	(examine-expression subexp)))))




(defvar *old-hypotheses*)

(defvar *new-hypotheses*)

(defvar *hypothesis-count* 0)

(defvar *hypothesis-table* (make-array 100000))

(defvar *final-hypothesis-table* (make-array 1000))

(defvar *initial-rule-set* nil)

(defmacro hypotheses-of-rank (r)
  `(aref *final-hypothesis-table* ,r))

(defstruct (hypothesis (:print-function (lambda (hypothesis stream &rest ignore)
					  (format stream "[hypothesis ~s ~s ~s ~s ~s]"
						  (hypothesis-number hypothesis)
						  (hypothesis-alpha hypothesis)
						  (hypothesis-phi hypothesis)
						  (hypothesis-sigma hypothesis)
						  (hypothesis-gamma hypothesis)))))
  number
  rank
  alpha
  phi
  sigma
  gamma
  upsilon
  new-rule
  source-hypothesis)


;The generic formula is included in a closure iff the closure is universal
;(equals all label formulas of Upsilon)

(defvar *generic-formula* (gensym "P-"))
(make-declaration *generic-formula* 'B)

(defun universal? (closure)
  (member *generic-formula* closure))


(defun-nondeterministic make-null-hypothesis (alpha sigma gamma phi)
  (let ((upsilon (long-union-equal *constants*
				   (list *generic-formula*)
				   (subterm-close (when (consp phi) phi))
				   (subterm-close (mapcan 'copy-list sigma))
				   (remove-if #'(lambda (term)
						  (known-equal? alpha term))
					      (subterm-close (mapcan 'copy-list gamma))))))

    (when (member? alpha upsilon)
      (fail))
    (make-hypothesis :number (progn (incf *hypothesis-count*) *hypothesis-count*)
		     :rank -1
		     :alpha alpha
		     :phi phi
		     :sigma sigma
		     :gamma gamma
		     :upsilon upsilon)))


(defun examine-rules ()
  (dotimes (n 100000)
    (setf (aref *hypothesis-table* n) nil))
  (gensym 1)

  (setf *initial-rule-set* (nconc (copy-list *rules*) (copy-list *null-antecedent-rules*)))
  (let ((*hypothesis-count* 0)
	(*old-hypotheses* nil)
	(*new-hypotheses* nil))

    ;initialize *new-hypotheses* to initial hypotheses
    (mapcar
      'notice-new-hypothesis
      (all-values
	(let* ((alpha (create-expression (member-of (mapcar #'gensym-var-of-type *types*))))
	       (irule (an-inward-rule-on alpha))
	       (sigma (nd-remove-if #'(lambda-nondeterministic (formula)
					(member? alpha formula))
				    (rule-body irule)))
	       (gamma (nd-remove-if #'(lambda-nondeterministic (formula)
					(not (member? alpha formula)))
				    (rule-body irule))))
	  (apply-hypothesis-substitution
	    (make-null-hypothesis alpha sigma gamma (rule-head irule))))))

    (iterate-rule-composition)))

(defun-nondeterministic an-original-rule ()
  (create-rule-expression (member-of *initial-rule-set*)))

(defun-nondeterministic an-inward-rule-on (alpha)
  (some-such-that (an-original-rule) ?s
		  (and (not (member? alpha (rule-head ?s)))
		       (nd-some #'(lambda-nondeterministic (ant)
				    (member? alpha ant))
				(rule-body ?s))
		       (determine-matches alpha
					  (top-level-subexpressions ?s)))))


(defun iterate-rule-composition (&aux (rank 0))
  (loop
    (format t "~% Filtering New Hypotheses")
    (format t "~%   --> (There is/are ~s new hypotheses)" (length *new-hypotheses*))
    (let ((filtered-new-hypotheses (remove-if 'provable-from-old-hypotheses
					      *new-hypotheses*)))
      (setf *old-hypotheses* (append *old-hypotheses* filtered-new-hypotheses))
      (mapc (lambda (new-hyp)
	      (setf (hypothesis-new-rule new-hyp)
		    (add-inference-rule (convert-exp-vars (hypothesis-phi new-hyp))
					(convert-exp-vars
					  (append (hypothesis-sigma new-hyp)
						  (hypothesis-gamma new-hyp)))
					(convert-exp-vars
					  (hypothesis-alpha new-hyp))
					:optional t)))
	    filtered-new-hypotheses)
      (if (null filtered-new-hypotheses)
	  (progn
	    (format t "~% ~% There are no hypotheses of rank ~s" rank)
	    (format t "~% The given rules are ~s-bounded local ~%" (1- rank))
	    (return-from iterate-rule-composition))
	  (progn
	    (if (or (> (length filtered-new-hypotheses) 1)
		    (zerop (length filtered-new-hypotheses)))
		(format t "~% ~% There are ~s rank ~s hypotheses:"
			(length filtered-new-hypotheses)
			rank)
		(format t "~% ~% There is ~s rank ~s hypothesis:"
			(length filtered-new-hypotheses)
			rank))
;	    (dolist (h filtered-new-hypotheses)
;	      (format t "~%   ~s" h))
	    (setf (hypotheses-of-rank rank) (copy-list filtered-new-hypotheses))
	    (let ((feedbacks (remove-if-not 'feedback-hypothesis? filtered-new-hypotheses)))
	      (if feedbacks
		  (progn
		    (format t "~% Hypotheses ~s are feedback events"
			    (mapcar 'hypothesis-number feedbacks))
		    (format t "~% The given rules are not local ~%")
		    (return-from iterate-rule-composition))
		  (progn
		    (format t "~% There are no rank ~s feedback events ~%" rank)
		    (setf *new-hypotheses* nil)
		    (process-rules filtered-new-hypotheses)
		    (incf rank)))))))))

(defun provable-from-old-hypotheses (hyp)
  (let ((closure (cr (convert-exp-vars (append (hypothesis-gamma hyp) (hypothesis-sigma hyp)))
		     (convert-exp-vars (hypothesis-upsilon hyp))
		     (convert-exp-vars (hypothesis-alpha hyp))
		     :goal (convert-exp-vars (hypothesis-phi hyp))
		     :optional-rules (when (and (hypothesis-source-hypothesis hyp)
						(hypothesis-new-rule
						  (hypothesis-source-hypothesis hyp)))
				       (list (hypothesis-new-rule
					       (hypothesis-source-hypothesis hyp)))))))
    (format t ".")
    (or (equal-member (convert-exp-vars (hypothesis-phi hyp)) closure)
	(and (universal? closure) (symbolp (convert-exp-vars (hypothesis-phi hyp)))))))


(defun process-rules (new-hypotheses)
  (format t "~% generating new hypotheses")
  (mapcar 'notice-new-hypothesis
	  (all-values
	    (let* ((h (create-hypothesis-expression (member-of new-hypotheses)))
		   (alpha-ant (first (hypothesis-gamma h)))
		   (rule (an-original-rule)))
	      (ensuring (equal? alpha-ant (rule-head rule))
		(ensuring (determine-matches (hypothesis-alpha h)
					     (top-level-subexpressions rule))
		  (expand-by-rules (list rule) h)))))))

;(defun process-rules (new-hypotheses)
;  (format t "~% Generating New Hypotheses")
;  (mapcar 'notice-new-hypothesis
;	  (all-values
;	    (let* ((h (create-hypothesis-expression (member-of new-hypotheses)))
;		   (rules (match-gamma (hypothesis-gamma h) (hypothesis-alpha h))))
;	      (expand-by-rules rules h)))))

(defun-nondeterministic match-gamma (gamma alpha)
  (when gamma
    (let ((alpha-ant (first gamma))
	  (rule (alpha-rename (an-original-rule))))
      (ensuring (equal? alpha-ant (rule-head rule))
	(ensuring (determine-matches alpha
				     (top-level-subexpressions rule))
	  (cons rule (match-gamma (rest gamma) alpha)))))))


(defun top-level-subexpressions (rule)
  (remove-duplicates (append (rule-head rule)
			     (mapcan #'copy-list (rule-body rule)))
		     :test #'equal))

(defun-nondeterministic nd-remove-if (pred list)
  (when list
    (let ((rest-result (nd-remove-if pred (rest list))))
      (if (not (funcall-nondeterministic pred (first list)))
	  (cons (car list) rest-result)
	  rest-result))))

(defmacro hp (n)
  `(aref *hypothesis-table* ,n))

(defun create-hypothesis-expression (hypothesis)
  (let ((hypothesis (copy-hypothesis hypothesis)))
    (selectmatch (create-expression (list (hypothesis-alpha hypothesis)
					  (hypothesis-phi hypothesis)
					  (hypothesis-sigma hypothesis)
					  (hypothesis-gamma hypothesis)
					  (hypothesis-upsilon hypothesis)))
      ((?alpha ?phi ?sigma ?gamma ?upsilon)
       (setf (hypothesis-alpha hypothesis) ?alpha)
       (setf (hypothesis-phi hypothesis) ?phi)
       (setf (hypothesis-sigma hypothesis) ?sigma)
       (setf (hypothesis-gamma hypothesis) ?gamma)
       (setf (hypothesis-upsilon hypothesis) ?upsilon)))
    hypothesis))

(defun apply-hypothesis-substitution (hypothesis)
  (let ((hypothesis (copy-hypothesis hypothesis)))
    (selectmatch (apply-substitution (list (hypothesis-alpha hypothesis)
					   (hypothesis-phi hypothesis)
					   (hypothesis-sigma hypothesis)
					   (hypothesis-gamma hypothesis)
					   (hypothesis-upsilon hypothesis)))
      ((?alpha ?phi ?sigma ?gamma ?upsilon)
       (setf (hypothesis-alpha hypothesis) ?alpha)
       (setf (hypothesis-phi hypothesis) ?phi)
       (setf (hypothesis-sigma hypothesis) ?sigma)
       (setf (hypothesis-gamma hypothesis) ?gamma)
       (setf (hypothesis-upsilon hypothesis) ?upsilon)))
    hypothesis))

(defun apply-hypothesis-substitution-except-to-upsilon (hypothesis)
  (let ((hypothesis (copy-hypothesis hypothesis)))
    (selectmatch (apply-substitution (list (hypothesis-alpha hypothesis)
					   (hypothesis-phi hypothesis)
					   (hypothesis-sigma hypothesis)
					   (hypothesis-gamma hypothesis)))
      ((?alpha ?phi ?sigma ?gamma)
       (setf (hypothesis-alpha hypothesis) ?alpha)
       (setf (hypothesis-phi hypothesis) ?phi)
       (setf (hypothesis-sigma hypothesis) ?sigma)
       (setf (hypothesis-gamma hypothesis) ?gamma)))
    hypothesis))

(defun notice-new-hypothesis (hypothesis)
  (setf (hp (hypothesis-number hypothesis)) hypothesis)
  (push hypothesis *new-hypotheses*))

(defun label-formula? (phi upsilon)
  (or (symbolp phi)
      (every (lambda (arg) (equal-member arg upsilon))
	     phi)))

;;  assumes hypothesis is not PROVABLE-FROM-OLD-HYPOTHESES
;;
(defun feedback-hypothesis? (hypothesis)
  (null (hypothesis-gamma hypothesis)))


(defun-nondeterministic expand-by-rules (rules old-hyp)
  (do-expansion rules
		(hypothesis-alpha old-hyp)
		(hypothesis-phi old-hyp)
		(hypothesis-sigma old-hyp)
		(hypothesis-gamma old-hyp)
		(hypothesis-upsilon old-hyp)
		(hypothesis-rank old-hyp)
		old-hyp))

(defun-nondeterministic do-expansion (rules alpha phi old-sigma old-gamma old-upsilon rank
					    source)
  (if (null rules)
      (make-hypothesis :number (progn (incf *hypothesis-count*)
				      *hypothesis-count*)
		       :rank (1+ rank)
		       :alpha (apply-substitution alpha)
		       :phi (apply-substitution phi)
		       :sigma (remove-duplicates (apply-substitution old-sigma) :test #'equal)
		       :gamma (remove-duplicates (apply-substitution old-gamma) :test #'equal)
		       :upsilon old-upsilon
		       :source-hypothesis source)
      (let ((rule (first rules)))
	(let* ((new-sigma-elts (nd-remove-if #'(lambda-nondeterministic (?ant)
						 (member? alpha ?ant))
					     (rule-body rule)))
	       (new-gamma-elts (nd-remove-if #'(lambda-nondeterministic (?ant)
						 (not (member? alpha
							       ?ant)))
					     (rule-body rule)))
	       (upsilon (remove-duplicates
			  (subterm-close
			    (apply-substitution
			      (append (when (consp alpha) alpha)
				      (mapcan (lambda (psi)
						(when (consp psi) (copy-list psi)))
					      new-sigma-elts)
				      old-upsilon
				      (nd-remove-if #'(lambda-nondeterministic (?term)
							(equal? alpha ?term))
						    (mapcan (lambda (psi)
							      (when (consp psi)
								(copy-list psi)))
							    new-gamma-elts)))))
			  :test 'equal))

	       ;; remove expanded alpha-leaf
	       (gamma (append (rest old-gamma) new-gamma-elts))

	       (sigma (append old-sigma new-sigma-elts)))
	
	  (when (member? (apply-substitution alpha) upsilon) (fail))
	  (do-expansion (rest rules) alpha phi sigma gamma upsilon rank source)))))



;(defun-nondeterministic expand-by-rule (rule old-hyp)
;  (let* ((alpha (hypothesis-alpha old-hyp))
;	 (phi (hypothesis-phi old-hyp))
;	 (new-sigma-elts (nd-remove-if #'(lambda-nondeterministic (?ant)
;					   (member? (hypothesis-alpha old-hyp) ?ant))
;				       (rule-body rule)))
;	 (new-gamma-elts (nd-remove-if #'(lambda-nondeterministic (?ant)
;					   (not (member? (hypothesis-alpha old-hyp) ?ant)))
;				       (rule-body rule)))
;	 (upsilon (remove-duplicates
;		    (subterm-close
;		      (apply-substitution
;			(append (when (consp alpha) alpha)
;				(mapcan (lambda (psi)
;					  (when (consp psi) (copy-list psi)))
;					new-sigma-elts)
;				(hypothesis-upsilon old-hyp)
;				(nd-remove-if #'(lambda-nondeterministic (?term)
;						  (equal? alpha ?term))
;					      (mapcan (lambda (psi)
;							(when (consp psi) (copy-list psi)))
;						      new-gamma-elts)))))
;		    :test 'equal))
;
;	 ;; remove expanded alpha-leaf
;	 (gamma (union (expose-if nil; (= (hypothesis-number old-hyp) 1)
;				  (apply-substitution (rest (hypothesis-gamma old-hyp)))
;				  "Old-Gamma: ")
;		       (expose-if nil; (= (hypothesis-number old-hyp) 1)
;				  (apply-substitution new-gamma-elts)
;				  "New-elst: ")
;		       :test #'equal))
;
;	 (sigma (union (apply-substitution (hypothesis-sigma old-hyp))
;		       (apply-substitution new-sigma-elts)
;		       :test #'equal)))
;;    (when (= (hypothesis-number old-hyp) 1)
;;      (format t "~%~% Alpha: ~s" (apply-substitution alpha))
;;      (format t "~% Phi: ~s" (apply-substitution phi))
;;      (format t "~% Sigma: ~s" (apply-substitution sigma))
;;      (format t "~% Gamma: ~s" (apply-substitution gamma))
;;      (format t "~% Upsilon: ~s" (apply-substitution Upsilon))
;;      )
;    (when (member? (apply-substitution alpha) upsilon) (fail))
;    (let ((new-hypothesis (make-hypothesis :number (progn (incf *hypothesis-count*)
;							  *hypothesis-count*)
;					   :rank (1+ (hypothesis-rank old-hyp))
;					   :alpha (apply-substitution alpha)
;					   :phi (apply-substitution phi)
;					   :sigma sigma
;					   :gamma gamma
;					   :upsilon upsilon
;					   :source-hypothesis old-hyp)))
;      new-hypothesis)))


(defun subterms (term)
  (if (consp term)
      (cons term (mapcan #'subterms (cdr term)))
      (list term)))

(defun subterm-close (terms)
  (remove-duplicates (mapcan 'subterms terms)))

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

;
;Contrapositives
;When using contrapositive type declarations ``not'' and ``false''
;are automatically provided.

(defvar *formulas* nil)

(defmacro contrapositive-type-declarations (&body declarations)
  (let ((*formulas* nil))
    `(progn (type-declarations
	      ,@(mapcan #'make-negation declarations)
	      (false (() B))
	      (not ((B) B))
	      (?p B))
	    ,@(mapcan 'predicate-rules *formulas*))))

(eval-when (compile load eval)
  (defun make-negation (declaration)
    (selectmatch declaration
      ((?constructor (?arg-types ?output-type))
       (if (not (eq ?output-type 'B))
	   (list declaration)
	   (let* ((variable-decls (mapcar (lambda (arg-type)
					    (list (gensym "?X-") arg-type))
					  ?arg-types))
		  (variables (mapcar 'car variable-decls)))
	     (push (cons ?constructor variables) *formulas*)
	     (list* declaration
		    `(,(create-name 'not ?constructor) (,?arg-types ,?output-type))
		    variable-decls))))
      (:anything (list declaration)))))

(eval-when (compile load eval)
  (defun predicate-rules (formula)
    (let ((not-formula `(,(create-name 'not (car formula)) ,@(cdr formula))))
      `((rule ((not ,formula))
	    ,not-formula)
	(rule (,not-formula)
	    (not ,formula))
	(rule (,not-formula
	       ,formula)
	    (false))))))

(defmacro multirule (antecedents &body conclusion)
  (setf conclusion (car conclusion))
  (let ((rule-pairs (cons (cons antecedents conclusion)
			  (mapcar (lambda (ant)
				    (cons (cons `(not ,conclusion)
						(remove ant antecedents))
					  `(not ,ant)))
				  antecedents))))
    `(progn ,@(mapcar 'make-clean-rule rule-pairs))))

(eval-when (compile load eval)
  (defun make-clean-rule (rule-pair)
    (let ((antecedents (mapcar 'remove-nots (car rule-pair)))
	  (conclusion (remove-nots (cdr rule-pair))))
      `(rule ,antecedents
	,conclusion))))

(eval-when (compile load eval)
  (defun remove-nots (formula)
    (selectmatch formula
      ((not (not ?form2))
       (remove-nots ?form2))
      ((not ?form2)
       (cons (create-name 'not (car ?form2)) (cdr ?form2)))
      (:anything
       formula))))



;Examples

(defun prover-test ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (f ((D) D)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ((is ?x ?y))
    (is (f ?x) (f ?y)))

  (cr (list '(is ?x ?y)
	    '(is ?y ?z))
      (list 'is '?x '?y '?z '(f ?x) '(f ?y))))

(defun monotone-test ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (f ((D) D)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ((is ?x ?y))
    (is (f ?x) (f ?y)))

  (examine-rules))

(defun contrapositive-monotone-test ()

  (system-init)

  (contrapositive-type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (f ((D) D)))

  (multirule nil
	     (is ?x ?x))

  (multirule ((is ?x ?y)
	      (is ?y ?z))
	     (is ?x ?z))

  (multirule ((is ?x ?y))
	     (is (f ?x) (f ?y)))

  (examine-rules))

(defun Boolean-test ()

  (system-init)

  (type-declarations
    (?P B)
    (?Q B)
    (F B)
    (or ((B B) B))
    (not ((B) B)))

  (RULE ((NOT (NOT ?P)))
    ?P)

  (RULE (?P)
    (NOT (NOT ?P)))

  (RULE ((OR ?P ?Q)
	 (NOT ?P))
    ?Q)

  (RULE ((OR ?P ?Q)
	 (NOT ?Q))
    ?P)

  (RULE (?P)
    (OR ?P ?Q))

  (RULE (?Q)
    (OR ?P ?Q))

  (RULE ((NOT (OR ?P ?Q)))
    (NOT ?P))

  (RULE ((NOT (OR ?P ?Q)))
    (NOT ?Q))

  (RULE ((NOT ?P)
	 (NOT ?Q))
    (NOT (OR ?P ?Q)))

  (RULE ((NOT ?P)
	 (NOT ?Q))
    (NOT (OR ?Q ?P)))

  (rule (?P (not ?p))
    F)

  (rule (F)
    ?p)

  (examine-rules))

(defun congruence-test ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (?w D)
    (= ((D D) B))
    (?f1 ((D) D))
    (?f2 ((D D) D)))


  (RULE NIL
    (= ?X ?X))

  (RULE ((= ?X ?Y))
    (= ?Y ?X))

  (RULE ((= ?X ?Y)
	 (= ?Y ?Z))
    (= ?X ?Z))

  (RULE ((= ?X ?Y))
    (= (?F1 ?X) (?F1 ?Y)))

  (RULE ((= ?X ?Y)
	 (= ?Z ?W))
    (= (?F2 ?X ?Z) (?F2 ?Y ?W)))
  
  (examine-rules))

(defun tax-test ()

  (system-init)

  (type-declarations
    (?C C)
    (?W C)
    (?Z C)
    (?r ((C) C))
    (fun ((((C) C)) B))
    (det ((C) B))
    (exst ((C) B))
    (is ((C C) B))
    (inter ((C C) B)))

  (rule ()
    (is ?c ?c))

  (rule ((is ?c ?w) (is ?w ?z))
    (is ?c ?z))

  (rule ((exst ?c) (det ?w) (is ?c ?w))
    (is ?w ?c))

  (rule ((is ?c ?w))
    (is (?r ?c) (?r ?w)))

  (rule ((exst ?c) (is ?c ?w))
    (exst ?w))

  (rule ((det ?w) (is ?c ?w))
    (det ?c))

  (rule ((fun ?r) (exst ?c))
    (exst (?r ?c)))

  (rule ((fun ?r) (det ?c))
    (det (?r ?c)))

  (rule ((exst (?r ?c)))
    (exst ?c))

  (rule ((exst ?c))
    (inter ?c ?c))

  (rule ((inter ?c ?w))
    (exst ?c))

  (rule ((inter ?c ?w) (is ?c ?z))
    (inter ?z ?w))

  (rule ((inter ?c ?w) (fun ?r))
    (inter (?r ?c) (?r ?w)))

  (rule ((inter ?c ?w))
    (inter ?w ?c))

  (rule ((inter ?c ?w) (det ?w))
    (is ?w ?c))

  (examine-rules))

(defun montague-test2 ()

  (system-init)

  (type-declarations
    (?x C)
    (?y C)
    (?w C)
    (every ((C) N))
    (some  ((C) N))
    (?R ((N) C))
    (is-every ((C C) B))
    (is-some  ((C C) B)))

  (RULE NIL
    (is-every ?x ?x))

  (RULE ((is-every ?X ?Y)
	 (is-every ?y ?z))
    (is-every ?x ?z))

  (rule ((is-some ?x ?y))
    (is-some ?y ?x))

  (rule ((is-some ?x ?y))
    (is-some ?x ?x))

  (rule ((is-some ?x ?y)
	 (is-every ?y ?z))
    (is-some ?x ?z))

  (RULE ((is-every ?X ?Y))
    (is-every (?R (some ?x)) (?R (some ?y))))

  (RULE ((is-every ?X ?Y))
    (is-every (?R (every ?y)) (?R (every ?x))))

  (RULE ((is-some ?X ?Y))
    (is-every (?R (every ?x)) (?R (some ?y))))

  (examine-rules))

(defun montague-test3 ()

  (system-init)

  (type-declarations
    (?x C)
    (?y C)
    (?w C)
    (every ((C) N))
    (some  ((C) N))
    (?R ((N) C))
    (is-every ((C C) B))
    (is-some  ((C C) B)))

  (RULE NIL
    (is-every ?x ?x))

  (RULE ((is-every ?X ?Y)
	 (is-every ?y ?z))
    (is-every ?x ?z))

  (rule ((is-some ?x ?y))
    (is-some ?x ?x))

  (rule ((is-some ?x ?y)
	 (is-every ?y ?z))
    (is-some ?x ?z))

  (RULE ((is-every ?X ?Y))
    (is-every (?R (some ?x)) (?R (some ?y))))

  (RULE ((is-every ?X ?Y))
    (is-every (?R (every ?y)) (?R (every ?x))))

  (RULE ((is-some ?X ?y)
	 (is-every ?x ?z))
    (is-every (?R (every ?z)) (?R (some ?y))))

  (examine-rules))

(defun montague-test4 ()

  (system-init)

  (type-declarations
    (not ((B) B))
    (or ((B B) B))
    (false (() B))

    (?x C)
    (?y C)
    (?z C)
    (?w C)
    (?p B)

    (thing (() C))
    (every ((C) ((C) B)))
    (some  ((C) ((C) B)))
    (?R ((((C) B)) C))
    (is ((((C) B)) C))
    (is-every ((C C) B))
    (is-some  ((C C) B))
    (determined ((C) B))
    (there-exists-a ((C) B))
    (not-there-exists-a ((C) B)))

  (rule (((every ?x) ?y))
    (is-every ?x ?y))

  (rule ((is-every ?x ?y))
    ((every ?x) ?y))

  (rule ((not (there-exists-a ?x)))
    (not-there-exists-a ?x))

  (rule ((not-there-exists-a ?x))
    (not (there-exists-a ?x)))

  (rule (?p
	  (not ?p))
    (false))

  (rule ((there-exists-a ?x)
	 (not-there-exists-a ?x))
    (false))

;the rules from the paper.

  (rule ()
    (there-exists-a (thing)))

  (rule ()
    (is-every ?x (thing)))

  (rule ((is-every ?x ?y))
    (is-every (?R (some ?x))
	      (?R (some ?y))))

  (rule ((is-every ?x ?y))
    (is-every (?R (every ?y))
	      (?R (every ?x))))

  (rule ((is-every ?x ?y)
	 (determined ?x)
	 (there-exists-a ?x))
    (is-every (is (every ?y))
	      ?x))

  (rule ((is-every ?x ?y)
	 (determined ?y)
	 (there-exists-a ?y))
    (is-every ?y
	      (is (every ?x))))

  (rule ((is-every ?x ?y)
	 (is-every ?y ?z))
    (is-every ?x ?z))

  (rule ()
    (is-every ?x ?x))

  (rule ((there-exists-a (?r (some ?x))))
    (there-exists-a ?x))

  (rule ((there-exists-a ?x)
	 (is-every ?x ?y))
    (there-exists-a ?y))

  (rule ((determined ?x)
	 (is-every ?y ?x))
    (determined ?y))

  (rule ((not (is-every ?x ?y)))
    (there-exists-a ?x))

  (rule ((there-exists-a ?x)
	 (determined ?y)
	 (is-every ?x ?y))
    (is-every ?y ?x))

  (rule ((there-exists-a ?x)
	 (is-every ?x ?y)
	 (is-every ?x ?z))
    (is-every (?r (every ?y))
	      (?r (some ?z))))

  (rule ((there-exists-a ?x)
	 (is-every ?x ?y)
	 (is-every ?x ?z))
    (is-every (is (every ?y)) ?z))

  (rule ((determined ?x)
	 (there-exists-a ?x))
    (is-every ?x (is (every ?x))))

  (rule ((determined ?x)
	 (there-exists-a ?x))
    (is-every (is (every ?x)) ?x))

  (rule ((there-exists-a (is (every ?x)))
	 (there-exists-a ?x))
    (determined ?x))

  (rule ()
    (is-every ?x (is (some ?x))))

  (rule ()
    (is-every (is (some ?x)) ?x))

  (rule ((not-there-exists-a ?x))
    (is-every (thing) (?R (every ?x))))

  (rule ((determined ?y)
	 (is-every ?x ?y)
	 (is-every ?z ?y))
    (is-every (?r (some ?z))
	      (?r (every ?x))))

  (rule ((determined ?y)
	 (is-every ?x ?y)
	 (is-every ?z ?y))
    (is-every ?z (is (every ?x))))

  (rule ((not-there-exists-a ?y)
	 (is-every ?x ?y))
    (not-there-exists-a ?x))


    
  (examine-rules))

(defun montague-test5 ()

  (system-init)

  (contrapositive-type-declarations

    (?x C)
    (?y C)
    (?z C)
    (?w C)
    (?p B)

    (thing (() C))
    (every ((C) NP))
    (some  ((C) NP))
    (?R ((NP) C))
    (is ((NP) C))
    (is-every ((C C) B))
    (is-some  ((C C) B))
    (determined ((C) B))
    (there-exists-a ((C) B))
    (sen ((NP C) B)))

  (multirule ((sen (every ?x) ?y))
    (is-every ?x ?y))

  (multirule ((is-every ?x ?y))
    (sen (every ?x) ?y))

;the multirules from the paper.

  (multirule ()
    (there-exists-a (thing)))

  (multirule ()
    (is-every ?x (thing)))

  (multirule ((is-every ?x ?y))
    (is-every (?R (some ?x))
	      (?R (some ?y))))

  (multirule ((is-every ?x ?y))
    (is-every (?R (every ?y))
	      (?R (every ?x))))

  (multirule ((is-every ?x ?y)
	 (determined ?x)
	 (there-exists-a ?x))
    (is-every (is (every ?y))
	      ?x))

  (multirule ((is-every ?x ?y)
	 (determined ?y)
	 (there-exists-a ?y))
    (is-every ?y
	      (is (every ?x))))

  (multirule ((is-every ?x ?y)
	 (is-every ?y ?z))
    (is-every ?x ?z))

  (multirule ()
    (is-every ?x ?x))

  (multirule ((there-exists-a (?r (some ?x))))
    (there-exists-a ?x))

  (multirule ((there-exists-a ?x)
	 (is-every ?x ?y))
    (there-exists-a ?y))

  (multirule ((determined ?x)
	 (is-every ?y ?x))
    (determined ?y))

  (multirule ((not (is-every ?x ?y)))
    (there-exists-a ?x))

  (multirule ((there-exists-a ?x)
	 (determined ?y)
	 (is-every ?x ?y))
    (is-every ?y ?x))

  (multirule ((there-exists-a ?x)
	 (is-every ?x ?y)
	 (is-every ?x ?z))
    (is-every (?r (every ?y))
	      (?r (some ?z))))

  (multirule ((there-exists-a ?x)
	 (is-every ?x ?y)
	 (is-every ?x ?z))
    (is-every (is (every ?y)) ?z))

  (multirule ((determined ?x)
	 (there-exists-a ?x))
    (is-every ?x (is (every ?x))))

  (multirule ((determined ?x)
	 (there-exists-a ?x))
    (is-every (is (every ?x)) ?x))

  (multirule ((there-exists-a (is (every ?x)))
	 (there-exists-a ?x))
    (determined ?x))

  (multirule ()
    (is-every ?x (is (some ?x))))

  (multirule ()
    (is-every (is (some ?x)) ?x))

  (multirule ((not (there-exists-a ?x)))
    (is-every (thing) (?R (every ?x))))

  (multirule ((determined ?y)
	 (is-every ?x ?y)
	 (is-every ?z ?y))
    (is-every (?r (some ?z))
	      (?r (every ?x))))

  (multirule ((determined ?y)
	 (is-every ?x ?y)
	 (is-every ?z ?y))
    (is-every ?z (is (every ?x))))
    
  (examine-rules))



(defun both-test ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (both ((D D) D)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ()
    (is (both ?x ?y) ?x))

  (rule ()
    (is (both ?x ?y) ?y))

  (rule ((is ?z ?x)
	 (is ?z ?y))

    (is ?z (both ?x ?y)))

  (examine-rules))

(defun either-both-test ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (both ((D D) D))
    (either ((D D) D)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ()
    (is (both ?x ?y) ?x))

  (rule ()
    (is (both ?x ?y) ?y))

  (rule ((is ?z ?x)
	 (is ?z ?y))

    (is ?z (both ?x ?y)))

  (rule ()
    (is ?x (either ?x ?y)))

  (rule ()
    (is ?y (either ?x ?y)))

  (rule ((is ?x ?z)
	 (is ?y ?z))

    (is (either ?x ?y) ?z))

  (examine-rules))

(defun induction-test ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (?R R)
    (apply ((R D) D))
    (apply* ((R D) D))
    (preserves ((R D) B)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ((is ?x ?y))
    (is (apply ?r ?x) (apply ?r ?y)))

  (rule ((is ?x ?y))
    (is (apply* ?r ?x) (apply* ?r ?y)))

  (rule ((is ?x ?y)
	 (is (apply ?r ?y) ?x))
    (preserves ?r ?x))

  (rule ((is ?x ?y)
	 (preserves ?r ?y))
    (is (apply ?r ?x) ?y))

  (rule ((is ?x ?y)
	 (is ?y ?x)
	 (preserves ?r ?x))
    (preserves ?r ?y))

  (rule ()
    (is ?x (apply* ?r ?x)))

  (rule ()
    (preserves ?r (apply* ?r ?x)))

  (rule ((is ?x ?y)
	 (preserves ?r ?y))
    (is (apply* ?r ?x) ?y))

  (examine-rules))

(defun counter-example ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (P ((D D) B))
    (W ((D) B)))


  (rule ((P ?x ?y))
    (W ?x))

  (rule ((P ?x ?y)
	 (is ?x ?z))
    (P ?z ?y))

  (examine-rules))


(defun feedback-test1 ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (f  ((D D) D))
    (is ((D D) B)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ((is ?x ?y))
    (is (f ?x ?z) (f ?y ?z)))

  (rule ((is ?x ?y))
    (is (f ?z ?x) (f ?z ?y)))

  (examine-rules))


(defun feedback-test2 ()

  (system-init)

  (type-declarations
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (?R R)
    (apply ((R D) D))
    (apply* ((R D) D))
    (preserves ((R D) B)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ((is ?x ?y))
    (is (apply ?r ?x) (apply ?r ?y)))

  (rule ((is ?x ?y))
    (is (apply* ?r ?x) (apply* ?r ?y)))

  (rule ((is ?x ?y)
	 (is (apply ?r ?y) ?x))
    (preserves ?r ?x))

  (rule ((is ?x ?y)
	 (preserves ?r ?y))
    (is (apply ?r ?x) ?y))

  (rule ((is ?x ?y)
	 (is ?y ?x)
	 (preserves ?r ?x))
    (preserves ?r ?y))

  (rule ()
    (is ?x (apply* ?r ?x)))

  (rule ()
    (preserves ?r (apply* ?r ?x)))

  (rule ((is ?x ?y)
	 (preserves ?r ?y))
    (is (apply* ?r ?x) ?y))

  (make-declaration '?R1 'R)

  (cr '((IS ?X ?Z)
	(PRESERVES ?R ?X)
	(IS (APPLY ?R1 ?Y) ?X)
	(PRESERVES ?R ?Y)
	(IS (APPLY ?R1 ?Y) ?Y))
      (subterm-close
	'(IS ?X ?Z PRESERVES ?Y
	     (APPLY* ?R (APPLY ?R1 ?Y))
	     (APPLY* ?R1 (APPLY ?R (APPLY ?R1 ?Y))))))
)
;
;((PRESERVES ?R1 ?Y)
; (PRESERVES ?R1 (APPLY ?R1 ?Y))
; (IS (APPLY* ?R1 (APPLY ?R (APPLY ?R1 ?Y))) ?X)
;
;
; (IS (APPLY* ?R1 (APPLY ?R (APPLY ?R1 ?Y))) ?Z)
; (IS (APPLY ?R (APPLY ?R1 ?Y)) ?Y)
; (IS (APPLY* ?R1 (APPLY ?R (APPLY ?R1 ?Y))) ?Y)
; (IS (APPLY* ?R1 (APPLY ?R (APPLY ?R1 ?Y))) (APPLY* ?R (APPLY ?R1 ?Y)))
; (PRESERVES ?R1 (APPLY* ?R (APPLY ?R1 ?Y)))
;
;  (rule ((is ?x ?y)
;	 (is (apply ?r ?y) ?x))
;    (preserves ?r ?x))
;          ||
;	  \/
;  (rule ((is *alpha* ?y)
;	 (is (apply ?r1 ?y) *alpha*))
;    (preserves ?r1 *alpha*))
;
; (IS (APPLY* ?R (APPLY ?R1 ?Y)) ?Y)
; (IS (APPLY ?R1 ?Y) ?Y)
;
; (PRESERVES ?R ?Y)
;
; (IS (APPLY ?R (APPLY ?R1 ?Y)) ?X)
; (IS (APPLY ?R1 ?Y) ?Z)
; (IS (APPLY ?R (APPLY ?R1 ?Y)) ?Z)
; (IS (APPLY* ?R (APPLY ?R1 ?Y)) ?Z)
; (IS (APPLY* ?R (APPLY ?R1 ?Y)) ?X)
; (IS (APPLY ?R1 ?Y) ?X)
;
; (PRESERVES ?R ?X)
;
; (IS ?X ?Z)
;
;
;;; null antecedent consequents:
;
; (IS ?X ?X)
; (IS ?Z ?Z)
; (IS ?Y ?Y)
; (IS (APPLY ?R1 ?Y) (APPLY ?R1 ?Y))
;
; (IS (APPLY ?R (APPLY ?R1 ?Y))
;     (APPLY ?R (APPLY ?R1 ?Y)))
;
; (IS (APPLY ?R (APPLY ?R1 ?Y))
;     (APPLY* ?R (APPLY ?R1 ?Y)))
;
; (IS (APPLY* ?R (APPLY ?R1 ?Y))
;     (APPLY* ?R (APPLY ?R1 ?Y)))
;
; (IS (APPLY ?R1 ?Y)
;     (APPLY* ?R (APPLY ?R1 ?Y)))
;
; (IS (APPLY* ?R1 (APPLY ?R (APPLY ?R1 ?Y)))
;     (APPLY* ?R1 (APPLY ?R (APPLY ?R1 ?Y))))
;
; (IS (APPLY ?R (APPLY ?R1 ?Y))
;     (APPLY* ?R1 (APPLY ?R (APPLY ?R1 ?Y))))
;
; (PRESERVES ?R (APPLY* ?R (APPLY ?R1 ?Y)))
;
; (PRESERVES ?R1 (APPLY* ?R1 (APPLY ?R (APPLY ?R1 ?Y)))))


(defun feedback-test3 ()

  (system-init)

  (type-declarations
    (?w D)
    (?x D)
    (?y D)
    (?z D)
    (is ((D D) B))
    (?R R)
    (apply ((R D) D))
    (apply* ((R D) D))
    (preserves ((R D) B)))

  (rule nil
    (is ?x ?x))

  (rule ((is ?x ?y)
	 (is ?y ?z))
    (is ?x ?z))

  (rule ((is ?x ?y))
    (is (apply ?r ?x) (apply ?r ?y)))

  (rule ((is ?x ?y))
    (is (apply* ?r ?x) (apply* ?r ?y)))

  (rule ((is ?x ?y)
	 (is (apply ?r ?y) ?x))
    (preserves ?r ?x))

  (rule ((is ?x ?y)
	 (preserves ?r ?y))
    (is (apply ?r ?x) ?y))

  (rule ((is ?x ?y)
	 (is ?y ?x)
	 (preserves ?r ?x))
    (preserves ?r ?y))

  (rule ()
    (is ?x (apply* ?r ?x)))

  (rule ()
    (preserves ?r (apply* ?r ?x)))

  (rule ((is ?x ?y)
	 (preserves ?r ?y))
    (is (apply* ?r ?x) ?y))

  (make-declaration '?R1 'R)

;  (cr '((IS ?X ?Y)
;	(IS ?W ?X)
;	(IS ?X ?Z)
;	(IS (APPLY ?R ?Z) ?X))
;      (subterm-close
;	'((APPLY ?R ?Z) ?X
;	  PRESERVES IS (APPLY* ?R (APPLY ?R ?W)) (APPLY ?R ?Y)
;	  (APPLY ?R ?X))))  

  (cr '((IS ?X ?Y)
	(IS ?W ?X)
	(PRESERVES ?R ?X))
      (subterm-close
	'(?X
	  PRESERVES IS (APPLY* ?R (APPLY ?R ?W)) (APPLY ?R ?Y))))
)


;;;((IS (APPLY ?R ?Z) ?Y)
;;; (PRESERVES ?R ?Z)
;;; (IS (APPLY ?R ?Z) ?Z)
;;; (IS (APPLY ?R ?X) ?Y)
;;; (IS (APPLY ?R ?X) ?Z)
;;; (IS (APPLY* ?R (APPLY ?R ?W)) (APPLY ?R ?Y))
;;; (IS (APPLY* ?R (APPLY ?R ?W)) (APPLY ?R ?X))
;;; (PRESERVES ?R (APPLY ?R ?X))
;;; (IS (APPLY ?R ?X) ?X)
;;; (PRESERVES ?R ?X)
;;; (IS (APPLY ?R ?W) ?X)
;;; (IS (APPLY ?R ?W) ?Y)
;;; (IS (APPLY* ?R (APPLY ?R ?W)) ?Y)
;;; (IS (APPLY ?R ?W) ?Z)
;;; (IS (APPLY* ?R (APPLY ?R ?W)) ?Z)
;;; (IS (APPLY* ?R (APPLY ?R ?W)) ?X)
;;; (IS (APPLY* ?R (APPLY ?R ?W)) (APPLY ?R ?Z))
;;; (PRESERVES ?R (APPLY ?R ?Z))
;;; (IS (APPLY ?R ?Z) ?X)
;;;
;;; (IS ?W ?Z)
;;; (IS (APPLY ?R ?W) (APPLY ?R ?Z))
;;; (IS (APPLY ?R ?X) (APPLY ?R ?Z))
;;; (IS ?X ?Z)
;;;
;;; (IS ?W ?Y)
;;; (IS (APPLY ?R ?W) (APPLY ?R ?Y))
;;; (IS (APPLY ?R ?W) (APPLY ?R ?X))
;;; (IS ?W ?X)
;;;
;;; (IS (APPLY ?R ?X) (APPLY ?R ?Y))
;;; (IS ?X ?Y)
;;;
;;; (IS (APPLY ?R ?W) (APPLY* ?R (APPLY ?R ?W)))
;;; (PRESERVES ?R (APPLY* ?R (APPLY ?R ?W))))