; -------------------------------------- INTERESTS -------------------------------------- 

(defstruct (instantiated-premise (:print-function print-instantiated-premise) (:conc-name ip-))
    (reason nil)
    (binding nil)  ;; cumulative binding prior to this premise
    (basis nil)
    (premise nil)
    (remaining-premises nil)  ;; premises left to be instantiated
    (instantiations nil)  ;; instantiations of node-variables in previous premises
    (used-premise-variables nil)  ;; premise-variables bound in earlier premises
    (used-variables nil)  ;; conclusion-variables occurring in basis
    (derived-premises nil)  ;; instantiated-premises immediately following this one
    (d-node nil)
    (number 0)
    (clues nil)
     (initial?  nil))   ;; records whether the premise is the initial premise of the reason

(defun print-instantiated-premise (x stream depth)
    (declare (ignore depth))
    (princ "<instantiated-premise " stream) (princ (ip-number x) stream) (princ " for " stream)
    (princ (ip-reason x) stream)
    (princ ">" stream))

(defstruct (interest-scheme (:include instantiated-premise)
                                                    (:print-function print-interest-scheme) (:conc-name is-))
    (target-interest nil)
    (supposition nil)
    (supposition-variables nil)
    (instance-function nil)
    (generating-node nil))

(defun print-interest-scheme (x stream depth)
    (declare (ignore depth))
    (princ "<<interest-scheme " stream) (princ (is-number x) stream) (princ " for " stream)
    (princ (is-target-interest x) stream) (princ " by " stream) (princ (ip-reason x) stream) (princ ">>" stream))

#| This finds the interest-scheme with is-number n. |#
(defunction interest-scheme (n)
    (let ((is nil))
      (some #'(lambda (dn)
                       (find-if #'(lambda (i)
                                         (and (equal (is-number i) n)
                                                  (setf is i)))
                                   (d-node-interest-schemes dn)))
                  *discrimination-net*)
      is))

#| This finds the instantiated-premise with ip-number n. |#
(defunction instantiated-premise (n)
    (let ((ip nil))
      (some #'(lambda (dn)
                       (find-if #'(lambda (i)
                                         (and (equal (ip-number i) n)
                                                  (setf ip i)))
                                   (d-node-forwards-reasons dn)))
                  *discrimination-net*)
      ip))

(defmacro is-derived-interest-schemes (is) `(is-derived-premises ,is))

(defstruct (interest-link (:print-function print-interest-link)
                                           (:conc-name nil))   ; "An interest-graph-link"
    (link-number 0)
    (resultant-interest nil)
    (link-interest nil)
    (link-interest-formula nil)
    (link-interest-condition nil)
    (link-binding nil)
    (link-rule nil)
    (remaining-premises nil)
    (supporting-nodes nil)
    (link-instantiations nil)
    (link-supposition nil)
    (link-defeaters nil)
    (link-defeat-status nil)
    (link-strength 0)  ; maximum-degree-of-interest conveyed
    (link-generating-node nil)
    (discharged-link nil)
    (interest-match nil)
    (interest-reverse-match nil)
    (generating-link nil)
    (link-premise nil)
    (link-clues nil)
    )

(defun print-interest-link (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Link " stream)
    (princ (link-number x) stream)
    (when (resultant-interest x)
      (princ ": for  interest #" stream) (princ (interest-number (resultant-interest x)) stream))
    (princ " by " stream) (princ (link-rule x) stream)
    (princ ">" stream))

(defunction link (n)
    (find-if #'(lambda (node) (equal (link-number node) n)) *interest-links*))

(defunction display-links ()
    (dolist (L *interest-links*) (princ L) (terpri)))

(defunction display-link (L)
    (princ "INTEREST-LINK #") (princ (link-number L)) (terpri)
    (princ "  resultant-interest: ") (princ (resultant-interest L)) (terpri)
    (princ "  supporting-nodes: ") (princ (supporting-nodes L)) (terpri)
    (princ "  link-interest: ") (princ (link-interest L)) (terpri)
    (princ "  remaining-premises: ") (princ (remaining-premises L)) (terpri)
    (princ "  reason: ") (princ (link-rule L)) (terpri)
    (princ "  link-interest: ") (princ-set (link-interest L)) (terpri)
    )

(defstruct (interest (:print-function print-interest)
                                    (:conc-name nil))   ; "An interest-graph-node"
    (interest-number 0)
    (interest-sequent nil)
    (interest-formula nil)
    (interest-supposition nil)
    (right-links nil)
    (left-links nil)
    (degree-of-interest *base-priority*)
    (last-processed-degree-of-interest nil)
    (interest-defeat-status nil)
    (discharged-degree nil)  ;; used in computing priorities
    (deductive-interest nil)
    (cancelled-interest nil)
    (interest-queue-node nil)
    (interest-i-list nil)
    (maximum-degree-of-interest 0)
    (interest-defeatees nil)
    (reductio-interest nil)
    (direct-reductio-interest nil)
    (generated-suppositions nil)
    (generating-nodes nil)
    (interest-priority 0)
    (interest-variables nil)
    (discharge-condition nil)  ;;a function of node, unifier, and interest-link
    (interest-supposition-variables nil)
    (cancelling-node nil)
    (discharging-nodes nil)
    (interest-supposition-nodes nil)
    (generated-interest-schemes nil)
    (defeater-binding nil)
    (generating-defeat-nodes nil)
    (cancelled-left-links nil)
   (non-reductio-interest t)
    (anchored-nodes nil)
    (text-discharge-condition nil)  ;; a text statement of the discharge condition
    (enabled-nodes nil)  ;; the nodes for which this is an enabling-interest
    )

#|
(defun print-interest (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Interest " stream)
    (princ (interest-number x) stream)
    (princ ": " stream) (prinp-sequent (interest-sequent x) stream)
    (princ ">" stream))
|#

(defun print-interest (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Interest " stream)
    (princ (interest-number x) stream)
   ; (princ ": " stream) (prinp-sequent (interest-sequent x) stream)
    (princ ">" stream))

(defunction ifm (n)
    (when (numberp n) (setf n (interest n)))
    (prinp (interest-formula n))
    (interest-formula n))

(defstruct (i-list (:print-function print-i-list)
                              (:conc-name nil))
    (i-list-formula nil)
    (corresponding-c-lists nil)
    (i-list-interests nil)
    (i-list-queries nil)
    (reductio-trigger nil)
    (i-list-reductio-supposition nil)
    (i-list-variables)
    (i-list-term-list nil)
    (i-list-d-node nil))

(defun print-i-list (x stream depth)
    (declare (ignore depth))
    (princ "#<i-list for " stream)
    (prinp (i-list-formula x) stream) (princ ">" stream))

#| This returns three values -- the i-list and the match and its reverse. |#
(defunction i-list-for (formula i-vars)
    (multiple-value-bind (profile term-list) (formula-code formula)
         (let ((d-node (pursue-d-node-for profile *top-d-node*)))
           (when d-node
                (some
                  #'(lambda (il)
                        (multiple-value-bind
                             (match match*)
                             (one-one-match term-list (i-list-term-list il) i-vars (i-list-variables il))
                             (when match
                                  (return-from i-list-for (values il match match*)))))
                  (d-node-i-lists d-node))))))

#| If p and q match one-one, this returns the match and its reverse-match. |#
(defunction one-one-match (p q p-vars q-vars)
    (let* ((match (match p q p-vars))
              (match* (reverse-match match)))
       (when
            (and match
                      (or (eq match t)
                            (and
                              (subsetp (a-range match) q-vars)
                              (equal (match-sublis match* q) p))))
            (values match match*))))

#| This returns two values -- the list of interests, and the match |#
(defunction interests-for (formula i-vars)
    (multiple-value-bind
         (i-list match)
         (i-list-for formula i-vars)
         (if i-list (values (i-list-interests i-list) match))))

#| c-variables is the list of node-variables. |#
(defunction matching-i-lists-for (term-list c-variables d-node)
    (let ((i-lists nil))
       (dolist (il (d-node-i-lists d-node))
           (let ((unifier (unifier term-list (i-list-term-list il) c-variables (i-list-variables il))))
              (if unifier (push (list il unifier) i-lists))))
       i-lists))

#| c-variables is the list of node-variables. |#
(defunction matching-c-lists-for (term-list i-variables d-node)
    (let ((c-lists nil))
       (dolist (cl (d-node-c-lists d-node))
           (let ((unifier (unifier  (c-list-term-list cl) term-list (c-list-variables cl) i-variables)))
              (if unifier (push (list cl unifier) c-lists))))
       c-lists))

(defunction store-interest (interest &optional i-list)
   ; (when (eq (interest-number interest) 11) (setf i interest il i-list) (break))
    ;; (step (store-interest i il))
    (push interest *interests*)
    (cond (i-list
                 (push interest (i-list-interests i-list))
                 (let ((reductio-sup (i-list-reductio-supposition i-list)))
                    (when reductio-sup
                         (push interest  (generating-interests reductio-sup))
                         (push reductio-sup (generated-suppositions interest))))
                 (setf (interest-i-list interest) i-list))
                (t 
                  (multiple-value-bind (profile term-list) (formula-code (interest-formula interest))
                       (index-interest interest profile term-list *top-d-node*)))))

#| (descrimination-tests d-node) is an a-list of pairs (test . dn), where test has the form of the
car of a formula-code, and dn is a d-node. |#
(defunction index-interest (interest profile term-list d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node)))
            (new-profile (cdr profile)))
      (cond (dn
                  (if new-profile (index-interest interest new-profile term-list dn)
                       (store-interest-at-d-node interest term-list dn)))
                (new-profile
                  (index-interest-at-new-nodes interest term-list d-node new-profile (car profile)))
                (t (store-interest-at-new-d-node
                      interest term-list d-node (car profile))))))

(defunction fetch-I-list-for (term-list d-node)
    (find-if #'(lambda (il)
                      (equal term-list (i-list-term-list il)))
                 (d-node-i-lists d-node)))

(defunction store-interest-at-d-node (interest term-list dn)
   ; (when (eq interest (interest 11)) (setf i interest tl term-list d dn) (break))
    ;; (step (store-interest-at-d-node i tl d))
    (let* ((formula (interest-formula interest))
              (i-variables (interest-variables interest))
              (i-list (fetch-i-list-for term-list dn)))
       (cond (i-list
                    (push interest (i-list-interests i-list))
                    (let ((reductio-sup (i-list-reductio-supposition i-list)))
                       (when reductio-sup
                            (push interest  (generating-interests reductio-sup))
                            (push reductio-sup (generated-suppositions interest)))))
                   (t (let ((c-lists (matching-c-lists-for term-list i-variables dn)))
                         (setf i-list (make-i-list
                                            :i-list-formula formula
                                            :corresponding-c-lists c-lists
                                            :i-list-interests (list interest)
                                            :reductio-trigger
                                            (appropriate-for-reductio-supposition formula)
                                            :i-list-variables i-variables
                                            :i-list-term-list term-list
                                            :i-list-d-node dn
                                            ))
                         (push i-list (d-node-i-lists dn))
                         (dolist (cl c-lists)
                             (push (cons i-list (cdr cl)) (corresponding-i-lists (mem1 cl)))))))
       (setf (interest-i-list interest) i-list)))

#| Test is the final member of the formula-profile for the node-formula. |#
(defunction store-interest-at-new-d-node (interest term-list d-node test)
   ; (when (eq interest (interest 7)) (setf i interest tl term-list d d-node ts test) (break))
    ;; (step (store-interest-at-new-node i tl d ts))
    (let* ((i-variables (interest-variables interest))
              (formula (interest-formula interest))
              (dn (make-d-node
                       :d-node-number (incf *d-node-number*)
                       :d-node-description (cons test (d-node-description d-node))
                       :parent-d-node d-node))
              (i-list (make-i-list
                          :i-list-formula formula
                          :i-list-interests (list interest)
                          :reductio-trigger
                          (appropriate-for-reductio-supposition formula)
                          :i-list-variables i-variables
                          :i-list-term-list term-list
                          :i-list-d-node dn
                          )))
       (push dn *discrimination-net*)
       (push (cons test dn) (discrimination-tests d-node))
       (setf (d-node-i-lists dn) (list i-list))
       (setf (interest-i-list interest) i-list)))

(defunction find-matching-i-lists-for (formula variables)
    (multiple-value-bind (profile term-list) (formula-code formula)
         (pursue-i-lists-for formula profile term-list variables *top-d-node*)))
    
(defunction pursue-i-lists-for (formula profile term-list variables d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node))))
       (when dn
            (let ((new-profile (cdr profile)))
               (cond
                 (new-profile (pursue-i-lists-for formula new-profile term-list variables dn))
                 (t (matching-i-lists-for term-list variables dn)))))))

(defunction index-interest-at-new-nodes (interest term-list d-node profile test)
    (let ((dn (make-d-node
                     :d-node-number (incf *d-node-number*)
                     :d-node-description (cons test (d-node-description d-node))
                     :parent-d-node d-node)))
       (push (cons test dn) (discrimination-tests d-node))
       (push dn *discrimination-net*)
       (let ((desc (cdr profile)))
          (cond (desc (index-interest-at-new-nodes interest term-list dn desc (car profile)))
                      (t (store-interest-at-new-d-node interest term-list dn (car profile)))))))

(defunction pursue-d-node-for (profile d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node))))
       (when dn
            (let ((new-profile (cdr profile)))
               (cond
                 (new-profile (pursue-d-node-for new-profile dn))
                 (t dn))))))

(defunction store-interest-with-c-lists (interest c-lists)
  ;  (when (eq (interest-number interest) 25) (setf i interest cl c-lists) (break))
    ;; (step (store-interest-with-c-lists i cl))
    (multiple-value-bind (profile term-list) (formula-code (interest-formula interest))
         (declare (ignore profile))
         (cond
           (c-lists
             (push interest *interests*)
             (let* ((formula (interest-formula interest))
                       (dn (c-list-d-node (caar c-lists)))
                       (i-list (fetch-i-list-for term-list dn))
                       (i-variables (interest-variables interest)))
                (cond (i-list
                             (push interest (i-list-interests i-list))
                             (let ((reductio-sup (i-list-reductio-supposition i-list)))
                                (when reductio-sup
                                     (push interest  (generating-interests reductio-sup))
                                     (push reductio-sup (generated-suppositions interest)))))
                            (t (setf i-list (make-i-list
                                                  :i-list-formula formula
                                                  :corresponding-c-lists c-lists
                                                  :i-list-interests (list interest)
                                                  :reductio-trigger
                                                  (appropriate-for-reductio-supposition formula)
                                                  :i-list-variables i-variables
                                                  :i-list-term-list term-list
                                                  :i-list-d-node dn
                                                  ))
                                (push i-list (d-node-i-lists dn))
                                (dolist (cl c-lists)
                                    (push (cons i-list (cdr cl)) (corresponding-i-lists (mem1 cl))))))
                (setf (interest-i-list interest) i-list)))
           (t (store-interest interest)))))

(defunction appropriate-for-reductio-supposition (formula)
    (and
      (not (conjunctionp formula))
      (not (conditionalp formula))
      (not (biconditionalp formula))
      (not (disjunctionp formula))
      (not (u-genp formula))
      (not (undercutterp formula))
      (or (not (negationp formula))
            (atomic-formula (mem2 formula)))))

(defunction store-inference-node (node formula)
   ; (when (eql (inference-number node) 14) (setf n node f formula) (break))
    ;; (step (store-inference-node n f))
    (multiple-value-bind (profile term-list) (formula-code formula)
         (index-inference-node node profile term-list *top-d-node*)))

#| (descrimination-tests d-node) is an a-list of pairs (test . dn), where test has the form of the
car of a formula-code, and dn is a d-node. |#
(defunction index-inference-node (node profile term-list d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node)))
            (new-profile (cdr profile)))
       (cond (dn
                    (if new-profile (index-inference-node node new-profile term-list dn)
                         (store-inference-node-at-d-node node term-list dn)))
                   (new-profile
                     (index-inference-node-at-new-nodes node term-list d-node new-profile (car profile)))
                   (t
                     (store-inference-node-at-new-d-node
                        node term-list d-node (car profile))))))

(defunction fetch-c-list-for (formula d-node)
    (find-if #'(lambda (cl) (notational-variant formula (c-list-formula cl)))
                 (d-node-c-lists d-node)))

(defunction store-inference-node-at-d-node (node term-list dn)
    (let* ((formula (node-formula node))
              (c-list (fetch-c-list-for formula dn))
              (c-variables (node-variables node)))
       (cond (c-list
                    (if (is-inference node) (push node (c-list-nodes c-list))))
                   (t (let ((i-lists (matching-i-lists-for term-list c-variables dn)))
                         (setf c-list (make-c-list
                                             :c-list-formula formula
                                             :corresponding-i-lists i-lists
                                             :c-list-nodes (if (is-inference node) (list node))
                                             :reductio-interests
                                             (appropriate-for-reductio-interest formula)
                                             :c-list-variables c-variables
                                             :c-list-term-list term-list
                                             :c-list-d-node dn
                                             ))
                         (push c-list (d-node-c-lists dn))
                         (dolist (il i-lists)
                             (push (cons c-list (cdr il)) (corresponding-c-lists (mem1 il)))))
                       (when
                            (appropriate-for-contradictors formula)
                            (setf (c-list-contradictors c-list)
                                     (find-matching-c-lists-for (neg formula) (c-list-variables c-list)))
                            (dolist (cl (c-list-contradictors c-list))
                                (push (list c-list (reverse (mem2 cl)))
                                            (c-list-contradictors (mem1 cl)))))))
       (setf (node-c-list node) c-list)))

#| Test is the final member of the formula-profile for the node-formula. |#
(defunction store-inference-node-at-new-d-node (node term-list d-node test)
    (let* ((c-variables (node-variables node))
              (dn (make-d-node
                       :d-node-number (incf *d-node-number*)
                       :d-node-description (cons test (d-node-description d-node))
                       :parent-d-node d-node))
              (formula (node-formula node))
              (c-list (make-c-list
                          :c-list-formula formula
                          :c-list-nodes (list node)
                          :reductio-interests
                          (appropriate-for-reductio-interest formula)
                          :c-list-variables c-variables
                          :c-list-term-list term-list
                          :c-list-d-node dn
                          )))
       (push dn *discrimination-net*)
       (push (cons test dn) (discrimination-tests d-node))
       (setf (d-node-c-lists dn) (list c-list))
       (when
            (appropriate-for-contradictors formula)
            (setf (c-list-contradictors c-list)
                     (find-matching-c-lists-for (neg formula) (c-list-variables c-list)))
            (dolist (cl (c-list-contradictors c-list))
                (push (list c-list (reverse (mem2 cl)))
                            (c-list-contradictors (mem1 cl)))))
       (setf (node-c-list node) c-list)))

(defunction find-matching-c-lists-for (formula variables)
    (multiple-value-bind (profile term-list) (formula-code formula)
         (pursue-c-lists-for formula profile term-list variables *top-d-node*)))
    
(defunction pursue-c-lists-for (formula profile term-list variables d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node))))
       (when dn
            (let ((new-profile (cdr profile)))
               (cond
                 (new-profile (pursue-c-lists-for formula new-profile term-list variables dn))
                 (t (matching-c-lists-for term-list variables dn)))))))

(defunction index-inference-node-at-new-nodes (node term-list d-node profile test)
    (let ((dn (make-d-node
                     :d-node-number (incf *d-node-number*)
                     :d-node-description (cons test (d-node-description d-node))
                     :parent-d-node d-node)))
       (push (cons test dn) (discrimination-tests d-node))
       (push dn *discrimination-net*)
       (let ((desc (cdr profile)))
          (cond (desc (index-inference-node-at-new-nodes node term-list dn desc (car profile)))
                      (t (store-inference-node-at-new-d-node node term-list dn (car profile)))))))

(defunction d-node-for (formula)
    (let ((profile (formula-code formula)))
         (pursue-d-node-for profile *top-d-node*)))

(defunction c-list-for (formula)
    (let ((d-node (d-node-for formula)))
       (if d-node
          (fetch-c-list-for formula d-node))))

(defunction pursue-c-list-for (formula profile d-node)
    (let ((dn (e-assoc (car profile) (discrimination-tests d-node))))
       (when dn
            (let ((new-profile (cdr profile)))
               (cond
                 (new-profile (pursue-c-list-for formula new-profile dn))
                 (t (fetch-c-list-for formula dn)))))))

(defunction store-inference-node-with-c-list (node formula c-list)
    ; (when (equal *inference-number* 31) (setf c node f formula cl c-list) (break))
    ;; (step (store-inference-node-with-c-list c f cl))
    (cond (c-list
                 (push node (c-list-nodes c-list))
                 (setf (node-c-list node) c-list))
                (t (store-inference-node node formula))))

(defunction appropriate-for-reductio-interest (formula)
    (and
      (not (conjunctionp formula))
      (not (disjunctionp formula))   ;; if we use disj-simp
      (not (biconditionalp formula))
      (or (not (conditionalp formula))                                         ;; these assume:
            (and (not (conjunctionp (antecedent formula)))       ;; exportation
                      (not (disjunctionp (antecedent formula)))        ;; disj-antecedent-simp
                      (not (conditionalp (antecedent formula)))))     ;; cond-antecedent-simp
      (not (u-genp formula))
      (not (e-genp formula))
      (or (not (negationp formula))
            (atomic-formula (negand formula))
            (undercutterp (negand formula)))))

(defunction appropriate-for-contradictors (formula)
    (and
      (not (conjunctionp formula))
      (not (disjunctionp formula))   ;; if we use disj-simp
      (not (biconditionalp formula))
      (not (u-genp formula))
      (not (e-genp formula))
      (or (not (negationp formula))
            (atomic-formula (mem2 formula))
            (undercutterp (mem2 formula))
            (conditionalp (mem2 formula)))))

(defunction cancelled-c-list-for (formula)
    (e-assoc formula *cancelled-c-lists*))

(defunction store-processed-inference-node (node)
    (setf (processed? node) T)
    (push node (c-list-processed-nodes (node-c-list node))))

#| This finds the interest with interest-number n. |#
(defunction interest (n)
    (find-if #'(lambda (i) (eql (interest-number i) n)) *interests*))

#| This returns the degree of interest for either an interest or a query. |#
(defunction degree-of-interest* (n)
    (if (interest-p n) (degree-of-interest n) (query-strength n)))

(defunction interest-sequent* (n)
    (if (interest-p n) (interest-sequent n) (list nil (query-formula n))))

(defunction display-interest (interest)
    (if (numberp interest) (setf interest (interest interest)))
    (princ "                                        # ") (princ (interest-number interest)) (princ "  ")
    (when (deductive-interest interest) (princ "deductive "))
    (when (reductio-interest interest) (princ "reductio "))
    (princ "interest:")
    (terpri)
    (princ "                                           ") (prinp  (interest-formula interest))
    (when (interest-supposition interest)
         (princ "    supposition: ")
         (set-prinp (interest-supposition interest)))
    (terpri)
    (when
         (some #'(lambda (L) (query-p (resultant-interest L)))
                     (right-links interest))
         (princ "                                        This is of ultimate interest") (terpri))
    (let ((L (lastmember (right-links interest))))
      (when (and L (not (query-p (resultant-interest L))))
           (princ "                                        For ")
           (when (reductio-interest (resultant-interest L)) (princ "reductio "))
           (princ "interest ")
           (princ (interest-number (resultant-interest L)))
           (princ " by ") (princ (link-rule L))
           (let ((nodes (supporting-nodes L)))
             (when nodes
                  (cond ((equal (length nodes) 1)
                              (princ " using node ")
                              (princ (inference-number (mem1 nodes))))
                            (t
                              (princ " using nodes ")
                              (print-list (mapcar
                                                #'(lambda (conclusion)
                                                      (inference-number conclusion))
                                                nodes) 40)))))
           (let ((nodes (link-clues L)))
             (when nodes
                  (cond ((equal (length nodes) 1)
                              (princ " with clue ")
                              (princ (inference-number (mem1 nodes))))
                            (t
                              (princ " with clues ")
                              (print-list (mapcar
                                                #'(lambda (conclusion)
                                                      (inference-number conclusion))
                                                nodes) 40)))))
           (terpri))
      (when (discharge-condition interest)
           (princ "                                        Discharge condition: ") (terpri)
           (princ "                                             ")
           (display-discharge-condition interest L) (terpri)))
    (terpri))

(defunction display-discharge-condition (interest link)
    (let ((binding
              (mapcar
                #'(lambda (x) (cons (car x) (if (and (cdr x) (listp (cdr x))) (list 'quote (cdr x)) (cdr x))))
                (link-binding link))))
      (print-pretty  (sublis binding (text-discharge-condition interest)))))

(defunction display-interests ()
    (princ "(") (terpri)
    (princ "================== INTERESTS ===================")
    (terpri)
    (let* ((**interests**
                (unionmapcar
                  #'(lambda (dn)
                        (unionmapcar #'(lambda (il) (i-list-interests il)) (d-node-i-lists dn)))
                  *discrimination-net*))
              (interests
                (order **interests**
                           #'(lambda (c1 c2)
                                 (< (interest-number c1) (interest-number c2))))))
      (dolist (interest interests)
          (princ "#") (princ (interest-number interest))
          (cond ((deductive-interest interest) (princ "  deductive interest: "))
                    ((reductio-interest interest) (princ "  reductio interest: "))
                    (t (princ "  interest: ")))
          (prinp (interest-formula interest))
          (when (interest-supposition interest)
               (princ "    supposition: ")
               (set-prinp (interest-supposition interest)))
          (terpri)
          (when
               (some #'(lambda (L) (query-p (resultant-interest L)))
                           (right-links interest))
               (princ "     This is of ultimate interest") (terpri))
          (dolist (L (right-links interest))
              (when (not (query-p (resultant-interest L)))
                   (princ "     For ")
                   (when (reductio-interest (resultant-interest L)) (princ "reductio "))
                   (princ "interest ")
                   (princ (interest-number (resultant-interest L)))
                   (princ " by ") (princ (link-rule L))
                   (let ((nodes (supporting-nodes L)))
                     (when nodes
                          (cond ((equal (length nodes) 1)
                                      (princ " using node ")
                                      (princ (inference-number (mem1 nodes))))
                                    (t
                                      (princ " using nodes ")
                                      (print-list (mapcar
                                                        #'(lambda (conclusion)
                                                              (inference-number conclusion))
                                                        nodes) 40)))))
                   (let ((nodes (link-clues L)))
                     (when nodes
                          (cond ((equal (length nodes) 1)
                                      (princ " with clue ")
                                      (princ (inference-number (mem1 nodes))))
                                    (t
                                      (princ " with clues ")
                                      (print-list (mapcar
                                                        #'(lambda (conclusion)
                                                              (inference-number conclusion))
                                                        nodes) 40)))))
                   (terpri)))
          (when (interest-defeatees interest)
               (princ "     For the defeat of ")
               (print-list (mapcar #'inference-number (interest-defeatees interest)))
               (terpri))
          (princ "---------------------------------------------------") (terpri)))
    (princ ")") (terpri))

#| This builds chains of inference-ancestors. |#
(defunction interest-ancestor-chains (interest)
    (cond ((interest-p interest)
                 (let ((links (right-links interest)))
                    (cond ((null links) (list (list (list interest))))
                                (t 
                                  (unionmapcar
                                    #'(lambda (L)
                                          (mapcar
                                            #'(lambda (c)
                                                  (cons (list interest L) c))
                                            (interest-ancestor-chains (resultant-interest L))))
                                    links)))))
                (t (list nil))))

#| This is like interest-ancestor-chains, but leaves out the links. |#
(defunction right-branches (interest)
    (if (interest-p interest)
       (let ((links (right-links interest)))
          (cond ((null links) (list (list interest)))
                      (t 
                        (unionmapcar
                          #'(lambda (L)
                                (mapcar
                                  #'(lambda (c)
                                        (cons interest c))
                                  (right-branches (resultant-interest L))))
                           links))))))

(defunction good-interest-ancestor-chains (interest)
    (if (interest-p interest)
       (let ((links (right-links interest)))
          (cond ((null links) (list (list (list interest))))
                      (t 
                        (let ((i-list (interest-i-list interest)))
                        (unionmapcar
                          #'(lambda (L)
                                (remove nil
                                (mapcar
                                  #'(lambda (c)
                                        (when
                                             (and 
                                               (not 
                                                 (and 
                                                   (equal (link-rule L) reductio)
                                                   (or
                                                     (and
                                                       (mem2 (mem1 c))
                                                       (equal (link-rule (mem2 (mem1 c))) reductio))
                                                     (some #'(lambda (x)
                                                                       (and (mem2 x)
                                                                                 (equal (link-rule (mem2 x)) reductio)
                                                                                 (equal (interest-i-list (mem1 x))
                                                                                              i-list)))
                                                                  c)))))
                                             (cons (list interest L) c)))
                                  (good-interest-ancestor-chains (resultant-interest L)))))
                           links)))))))

;(defun display-good-interest-map ()
;    (terpri)
;    (let ((endpoints nil))
;       (dolist (i-list *interests*)
;           (dolist (interest (i-list-interests (cdr i-list)))
;               (when (null (left-links interest))
;                    (push interest endpoints))))
;       (princ "Endpoints of interest map: ")
;       (print-list (mapcar #'interest-number endpoints) 40) (terpri)
;      ; (setf *endpoints* endpoints)
;       (setf *interest-map* nil)
;       (dolist (i endpoints)
;           (princ "==============") (terpri)
;           (let ((chains (good-interest-ancestor-chains i)))
;              (cond (chains
;                           (princ "Chains for ") (princ i) (terpri)
;                           (dolist (c chains)
;                               (push c *interest-map*)
;                               (display-interest-ancestor-chain c)))
;                          (t (princ "No chains for ") (princ i) (terpri))))))
;    (princ "==============") (terpri) (terpri))
;
;(defun circular-chain (c)
;    (some #'(lambda (x)
;                        (some #'(lambda (y)
;                                            (equal (interest-i-list (mem1 x)) (interest-i-list (mem1 y))))
;                                      (cdr (mem x c))))
;                  c))
;
;(defun nested-reductio (c)
;    (some #'(lambda (x)
;                        (and
;                          (mem2 x)
;                          (equal (link-rule (mem2 x)) reductio)
;                          (let ((y (mem2 (car (cdr (mem x c))))))
;                             (and y (equal (link-rule y) reductio)))))
;                  c))
;
;(defun display-interest-ancestor-chain (c)
;    (dolist (n c)
;        (print-sequent (interest-sequent (mem1 n)))
;        (when (mem2 n)
;             (princ " <=") (princ (link-number (mem2 n))) (princ "= ")))
;    (terpri))
;
;(defun display-interest-ancestor-chains (n)
;    (dolist (c (interest-ancestor-chains (interest n)))
;        (display-interest-ancestor-chain c)))
;
;#| This builds chains of interests derived from interest. |#
;(defunction interest-chains (interest)
;    (if (interest-p interest)
;       (let ((links (left-links interest)))
;          (cond ((null links) (list (list (interest-number interest))))
;                      (t (mapcar #'(lambda (c) (cons (interest-number interest) c))
;                                          (unionmapcar=
;                                            #'(lambda (L) (interest-chains (link-interest L)))
;                                            links)))))))
;
;(defun display-interest-chain (c)
;    (print-sequent (interest-sequent (interest (mem1 c))))
;    (dolist (n (cdr c))
;        (princ " => ") (print-sequent (interest-sequent (interest n))))
;    (terpri))
;
;(defun interest-map ()
;    (let ((endpoints nil))
;                     (dolist (i-list *interests*)
;                         (dolist (interest (i-list-interests (cdr i-list)))
;                             (when (null (right-links interest))
;                                  (push interest endpoints))))
;       (unionmapcar #'interest-chains endpoints)))
;
;(defun display-interest-map (&optional n)
;    (terpri)
;    (let ((endpoints nil))
;       (cond (n (setf endpoints (list (interest n))))
;                   (t
;                     (dolist (i-list *interests*)
;                         (dolist (interest (i-list-interests (cdr i-list)))
;                             (when (null (right-links interest))
;                                  (push interest endpoints))))))
;       (cond ((null n)
;                    (princ "Endpoints of interest map: ")
;                    (print-list (mapcar #'interest-number endpoints) 40) (terpri))
;                   (t (princ "Interest-chains for interest #") (princ n) (terpri)))
;       (setf *interest-map* nil)
;       (dolist (i endpoints)
;           (princ "==============") (terpri)
;           (dolist (c (interest-chains i))
;               (push c *interest-map*)
;              ; (display-interest-chain c)
;               )))
;    (princ "==============") (terpri)
;    (terpri))

(defun derived-interests (interest)
    (mapcar #'link-interest (left-links interest)))

(defun print-sequent (S &optional stream)
    (prinp (sequent-formula S) stream) (princ "/" stream) (set-prinp (sequent-supposition S) stream))

(defunction display-interests-by-supposition ()
    (princ "(") (terpri)
    (let ((suppositions nil))
       (dolist (dn *discrimination-net*)
           (dolist (il (d-node-i-lists dn))
               (dolist (c (i-list-interests il))
                   (pushnew (interest-supposition c) suppositions :test '==)
                   (setf suppositions
                            (order suppositions
                                        #'(lambda (s1 s2)
                                              (or (< (length s1) (length s2))
                                                    (and (= (length s1) (length s2))
                                                              (lessp s1 s2)))))))))
       (let* ((**interests**
                  (unionmapcar
                    #'(lambda (dn)
                          (unionmapcar #'(lambda (il) (i-list-interests il)) (d-node-i-lists dn)))
                    *discrimination-net*)))
          (dolist (sup suppositions)
              (princ "==========================================") (terpri)
              (princ "Interests with supposition ") (set-prinp sup) (princ ":") (terpri)
              (let* ((sup-interests
                         (subset #'(lambda (c) (== (interest-supposition c) sup))
                                        **interests**))
                        (interests
                          (order sup-interests
                                      #'(lambda (c1 c2)
                                            (< (interest-number c1) (interest-number c2))))))
                 (dolist (c interests)
                     (when (== (interest-supposition c) sup)
                          (princ "    #") (princ (interest-number c)) (princ "  ")
                          (prinp (interest-formula c)) (princ "     ")
                          (when (reductio-interest c) (princ "reductio "))
                          (princ "for  ") 
                          (print-list
                            (remove-duplicates=
                              (mapcar
                                #'(lambda (L) (interest-number (resultant-interest L)))
                                (right-links c))) 40)
                          (terpri)))))))
    (princ ")") (terpri))

(defunction display-i-lists ()
    (princ "(") (terpri)
    (dolist (dn *discrimination-net*)
        (dolist (il (d-node-i-lists dn))
            (princ "==========================================") (terpri)
            (princ "i-list-formula: ") (prinp (i-list-formula il)) (terpri)
            (let ((interests
                      (order (i-list-interests il)
                                  #'(lambda (c1 c2)
                                        (let ((s1 (interest-supposition c1))
                                                (s2 (interest-supposition c2)))
                                           (or (< (length s1) (length s2))
                                                 (and (= (length s1) (length s2))
                                                           (lessp s1 s2))))))))
               (dolist (c interests)
                   (princ "    #") (princ (interest-number c)) (princ "  ")
                   (princ "   sup = ") (set-prinp (interest-supposition c)) (princ "     ")
                   (when (reductio-interest c) (princ "reductio "))
                   (princ "for  ") 
                   (print-list
                     (remove-duplicates=
                       (mapcar
                         #'(lambda (L) (interest-number (resultant-interest L)))
                         (right-links c))) 40)
                   (let ((derived-interests (derived-interests c)))
                      (when derived-interests
                           (princ "  generates ")
                           (print-list (mapcar #'interest-number derived-interests) 40)))
                   (terpri)))))
    (princ ")") (terpri))