; -------------------------------------- CONCLUSIONS -------------------------------------- 

(defstruct (d-node (:conc-name nil) (:print-function print-d-node))
    d-node-number
    (d-node-description nil)
    (discrimination-tests nil)
    (d-node-c-lists nil)
    (d-node-i-lists nil)
    (parent-d-node nil)
    (d-node-forwards-reasons nil)  ;; a list of partially-instantiated-premises
    (d-node-backwards-reasons nil)  ;; a list of non-degenerate backwards-reasons
    (d-node-interest-schemes nil)  ;; a list of partially-instantiated-premises
    (d-node-degenerate-backwards-reasons nil)
    )

(defunction print-d-node (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "d-node: " stream)
    (princ (d-node-number x) stream) (princ ">" stream))

(defunction d-node (n)
    (find-if #'(lambda (dn) (eql (d-node-number dn) n)) *discrimination-net*))

(defunction display-d-node (dn depth test)
   ; (setf d dn de depth te test)
    ;; (step (display-d-node d de te))
    (let ((pp *print-pretty*))
      (setf *print-pretty* nil)
      (line-indent depth)
      (princ "--")
      (if test (prinp-test test) (princ dn))
      (princ "   ")
      (terpri)
      (dolist (cl (d-node-c-lists dn)) (line-indent depth) (princ "       ") (princ cl) (terpri))
      (dolist (il (d-node-i-lists dn)) (line-indent depth) (princ "       ") (princ il) (terpri))
      (dolist (ip (d-node-forwards-reasons dn))
          (line-indent depth)
          (cond ((ip-basis ip) (princ "       instantiated-premise ") (princ (ip-number ip)) (princ " for "))
                      (t (princ "       first premise for ")))
          (princ (ip-reason ip))
          (princ ": ")
          (let ((p (match-sublis (ip-binding ip) (fp-formula (ip-premise ip)))))
            (if (and (negationp p) (negationp (negand p))) (setf p (negand (negand p))))
            (prinp p))
          (terpri))
      (dolist (br (d-node-backwards-reasons dn)) (line-indent depth) (princ "       conclusion for ")
                 (princ br) (terpri))
      (dolist (br (d-node-degenerate-backwards-reasons dn)) (line-indent depth) (princ "       conclusion for ")
                 (princ br) (terpri))
      (dolist (is (d-node-interest-schemes dn))
          (line-indent depth)
          (princ "       interest-scheme ") (princ (is-number is)) (princ " for interest ")
          (princ (interest-number (is-target-interest is)))
          (princ " by ")
          (princ (is-reason is))
          (princ ": ")
          (let ((p (match-sublis (is-binding is) (fp-formula (is-premise is)))))
            (if (and (negationp p) (negationp (negand p))) (setf p (negand (negand p))))
            (prinp p))
          (terpri))
      (setf *print-pretty* pp)))

(defunction formula-code (P)
    (setf *quantifier-number* 0)
    (multiple-value-bind (code term-list) (formula-code* P nil)
         (values (reverse code) term-list)))

(defunction formula-code* (P descriptor)
    (cond ((listp P)
                 (let ((description nil) (elt-num 1) (term-list nil))
                    (cond
                      ;; This handles notational variants.
                      ((or (eq (car p) 'all) (eq (car P) 'some))
                        (setf P
                                 (cons (car P) (subst (list 'q-var (incf *quantifier-number*)) (mem2 P) (cddr P)))))
                      ((eq (car P) 'at)
                        (setf term-list (cddr P))
                        (setf P (list (car P) (cadr P))))
                      ((eq (car P) 'throughout)
                        (setf term-list (cdr (mem3 P)))
                        (setf P (list (car P) (cadr P) (list (car (mem3 P))))))
                      ((and (symbolp (car P))
                                 (not (member (car P) *operators*))
                                 (not (member (car P) '(~ & v -> <-> all some ? @))))
                        (setf term-list (cdr P))
                        (setf P (list (car P)))))
                    (dolist (Q P)
                        (let ((Q-descriptor (cons elt-num descriptor)))
                           (cond ((not (listp Q))
                                        (push (cons (reverse Q-descriptor) Q) description))
                                       (t 
                                         (multiple-value-bind (d tl) (formula-code* Q Q-descriptor)
                                              (setf term-list (append tl term-list))
                                              (setf description (append d description))
                                              )))
                           (incf elt-num)))
                    (values description term-list)))
                (t (values (list (cons descriptor P)) nil))))

(defun display-discrimination-net (&optional (nodes *discrimination-net*))
    (setf *callees* nil)
    (setf *blank-line* nil)
    (setf *line-columns* nil)
    (display-discrimination-node *top-d-node* nil 0 t nodes)
    nil)

(defun ddn (&optional (nodes *discrimination-net*)) (display-discrimination-net nodes))

(defun display-discrimination-node (d-node listees depth last? nodes &optional test)
    (when (member d-node nodes)
         (when (null depth)
              (setf depth 0) (setf listees nil))
         (cond ((or (mem d-node listees) (mem d-node *callees*))
                     (line-indent depth)
                     (when (not (mem depth *line-columns*)) (princ "|"))
                     (princ "--") (princ d-node) (princ " .....") (terpri)
                     (setf *blank-line* nil)
                     (cond (last? (pull depth *line-columns*))
                               (t (pushnew depth *line-columns* :test 'eql))))
                   (t
                     (let* ((DC (discrimination-tests d-node))
                               (number (length (discrimination-tests d-node)))
                               (number* (round (/ number 2)))
                               (draw-line?
                                 (or (mem d-node listees)
                                       (mem d-node *callees*)
                                       (some #'(lambda (C) (not (mem c listees))) (discrimination-tests d-node)))))
                       (pushnew d-node listees :test 'equal)
                       (push d-node *callees*)
                       (when (and (not *blank-line*) (> number* 0))
                            (line-indent depth) (terpri) (setf *blank-line* t))
                       (dotimes (n number*)
                           (let ((test (mem1 DC)))
                             (cond
                               ((zerop n)
                                 (display-discrimination-node (cdr test) listees (1+ depth) nil nodes test))
                               ((cdr DC) (display-discrimination-node (cdr test) listees (1+ depth) nil nodes test))
                               (t (display-discrimination-node (cdr test) listees (1+ depth) t nodes test))))
                           (setf DC (cdr DC)))
                       (pushnew depth *line-columns* :test 'eql)
                       (display-d-node d-node depth test)
                       (setf *blank-line* nil)
                       (when last? (pull depth *line-columns*))
                       (when (> number 0) (pushnew (1+ depth) *line-columns* :test 'eql))
                       (dolist (test DC)
                           (cond
                             ((cdr DC)
                               (display-discrimination-node (cdr test) listees (1+ depth) nil nodes test))
                             (t (display-discrimination-node (cdr test) listees (1+ depth) t nodes test)))
                           (setf DC (cdr DC)))
                       (when
                            (and (not *blank-line*) draw-line?)
                            (line-indent depth) (terpri) (setf *blank-line* t))
                       )))))

#| The list of instantiated-premises for a forwards-reason. |#
(defunction reason-ips (reason)
    (let ((ips nil))
      (dolist (dn *discrimination-net*)
          (dolist (ip (d-node-forwards-reasons dn))
              (when (equal (ip-reason ip) reason) (push ip ips))))
      ips))

#| The list of interest-schemes for a backwards-reason. |#
(defunction reason-iss (reason)
    (let ((iss nil))
      (dolist (dn *discrimination-net*)
          (dolist (is (d-node-interest-schemes dn))
              (when (equal (ip-reason is) reason) (push is iss))))
      iss))

(defunction d-node-ancestors (dn)
    (let ((pn (parent-d-node dn)))
      (when pn (cons pn (d-node-ancestors pn)))))

(defunction d-node-descendants (dn)
    (when (discrimination-tests dn)
         (let ((nodes (a-range (discrimination-tests dn))))
           (append nodes (unionmapcar #'d-node-descendants nodes)))))

#| Display the part of the discrimination-net that contains d-node number n. |#
(defunction show-d-node (n)
    (let* ((dn (if (numberp n) (d-node n) n))
              (nodes (cons dn (append (d-node-ancestors dn) (d-node-descendants dn)))))
      (display-discrimination-net nodes)))

(defunction show-interest (n)
    (let* ((in (if (numberp n) (interest n) n))
              (dn (i-list-d-node (interest-i-list in)))
              (nodes (cons dn (append (d-node-ancestors dn) (d-node-descendants dn)))))
      (display-discrimination-net nodes)))

(defunction show-node (n)
    (let* ((node (if (numberp n) (node n) n))
              (dn (c-list-d-node (node-c-list node)))
              (nodes (cons dn (append (d-node-ancestors dn) (d-node-descendants dn)))))
      (display-discrimination-net nodes)))

#| This displays all d-nodes directly relevant to the reason. |#
(defunction show-reason (reason)
    (let ((nodes nil))
      (cond ((forwards-reason-p reason)
                  (dolist (dn *discrimination-net*)
                      (when (some #'(lambda (ip) (equal (ip-reason ip) reason)) (d-node-forwards-reasons dn))
                           (push dn nodes))))
                ((backwards-reason-p reason)
                  (dolist (dn *discrimination-net*)
                      (when
                           (or (member reason (d-node-backwards-reasons dn))
                                 (member reason (d-node-degenerate-backwards-reasons dn))
                                 (some #'(lambda (is) (equal (is-reason is) reason)) (d-node-interest-schemes dn)))
                           (push dn nodes)))))
      (setf nodes
               (unionmapcar+
                 #'(lambda (dn) (cons dn (append (d-node-ancestors dn) (d-node-descendants dn))))
                 nodes))
      (display-discrimination-net nodes)))

(defunction prinp-test (test)
    (princ "(") (princ (caar test)) (princ " . ") (prinp (cdar test)) (princ ") : ") (princ (cdr test)))

(defstruct (c-list (:print-function print-c-list)
                              (:conc-name nil))
    (c-list-formula nil)
    (corresponding-i-lists nil)
    (c-list-nodes nil)
    (c-list-processed-nodes nil)
    (link-defeatees nil)
    (reductio-interests nil)
    (c-list-variables nil)
    (c-list-contradictors nil)
    (c-list-term-list nil)
    (c-list-d-node nil)
    (generated-instantiated-premises nil)
    (supported-interest-schemes nil))

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

(defunction processed-c-list-for (formula)
    (cdr (find-if #'(lambda (cl) (notational-variant formula (car cl))) *processed-conclusions*)))

(defunction notational-variant (p q &optional vars)
    (cond ((null p) (null q))
                ((listp p)
                  (and (listp q)
                            (cond ((and (or (eq (car p) 'some) (eq (car p) 'all))
                                                  (eq (car p) (car q)))
                                                        (notational-variant (cdr p) (cdr q)
                                                                                          (cons (cons (cadr p) (cadr q)) vars)))
                                        ((listp (car q)) (and (notational-variant (car p) (car q) vars)
                                                                    (notational-variant (cdr p) (cdr q) vars)))
                                        ((or (eql (car p) (car q))
                                                (and vars
                                                          (mem (cons (car p) (car q)) vars)))
                                          (notational-variant (cdr p) (cdr q) vars)
                                          ))))
                (t (and (not (listp q))
                             (or (eql p q)
                                   (mem (cons p q) vars))))))

(defunction nodes-for (formula)
    (let ((c-list (c-list-for formula)))
       (if c-list (c-list-nodes c-list))))

(defunction processed-nodes-for (formula)
    (let ((c-list (processed-c-list-for formula)))
       (if c-list (c-list-nodes c-list))))

(defunction display-conclusions ()
    (princ "(") (terpri)
    (princ "================== CONCLUSIONS ===================")
    (let* ((**conclusions**
               (unionmapcar
                 #'(lambda (dn)
                       (unionmapcar
                         #'(lambda (cl) (c-list-nodes cl)) (d-node-c-lists dn)))
                 *discrimination-net*))
              (conclusions
                (order **conclusions**
                            #'(lambda (c1 c2)
                                  (< (inference-number c1) (inference-number c2))))))
       (dolist (conclusion conclusions)
           (display-conclusion conclusion)
           (terpri) (princ "---------------------------------------------------")))
    (princ ")") (terpri))

(defunction display-conclusion (n)
    (terpri) (princ n)
    (when (not (equal (node-kind n) :inference))
         (terpri) (princ "  kind: ") (princ (node-kind n)))
    ; (terpri) (princ "  maximal-degree-of-support: ") (princ (compute-maximal-degree-of-support n))
    (terpri) (princ "  undefeated-degree-of-support: ") (princ (compute-undefeated-degree-of-support n))
    (dolist (Q (answered-queries n))
        (terpri) (princ "  This answers ") (princ Q)))

(defunction display-conclusions-by-supposition ()
    (princ "(") (terpri)
    (let ((suppositions nil))
       (dolist (dn *discrimination-net*)
           (dolist (cl (d-node-c-lists dn))
               (dolist (c (c-list-nodes cl))
                   (pushnew (node-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* ((**conclusions**
                  (unionmapcar
                    #'(lambda (dn)
                          (unionmapcar
                            #'(lambda (cl) (c-list-nodes cl)) (d-node-c-lists dn)))
                    *discrimination-net*)))
          (dolist (sup suppositions)
              (princ "==========================================") (terpri)
              (princ "Conclusions with supposition ") (set-prinp sup) (princ ":") (terpri)
              (let* ((sup-conclusions
                         (subset #'(lambda (c) (== (node-supposition c) sup))
                                        **conclusions**))
                        (conclusions
                          (order sup-conclusions
                                      #'(lambda (c1 c2)
                                            (< (inference-number c1) (inference-number c2))))))
                 (dolist (c conclusions)
                     (when (== (node-supposition c) sup)
                          (princ "    #") (princ (inference-number c)) (princ "  ")
                          (prinp (node-formula c)) (terpri)))))))
    (princ ")") (terpri))

(defunction display-c-lists ()
    (princ "(") (terpri)
    (dolist (dn *discrimination-net*)
        (dolist (cl (d-node-c-lists dn))
            (princ "==========================================") (terpri)
            (princ "c-list-formula: ") (prinp (c-list-formula cl)) (terpri)
            (let ((conclusions
                      (order (c-list-nodes cl)
                                  #'(lambda (c1 c2)
                                        (let ((s1 (node-supposition c1))
                                                (s2 (node-supposition c2)))
                                           (or (< (length s1) (length s2))
                                                 (and (= (length s1) (length s2))
                                                           (lessp s1 s2))))))))
               (dolist (c conclusions)
                   (princ "    #") (princ (inference-number c))
                   (princ "   sup = ") (set-prinp (node-supposition c))
                   (terpri)))))
    (princ ")") (terpri))

(defunction display-processed-c-lists ()
    (princ "(") (terpri)
    (dolist (cl *processed-conclusions*)
        (princ "==========================================") (terpri)
        (princ "c-list-formula: ") (prinp (car cl)) (terpri)
        (let ((conclusions
                  (order (c-list-nodes (cdr cl))
                              #'(lambda (c1 c2)
                                    (let ((s1 (node-supposition c1))
                                            (s2 (node-supposition c2)))
                                       (or (< (length s1) (length s2))
                                             (and (= (length s1) (length s2))
                                                       (lessp s1 s2))))))))
           (dolist (c conclusions)
               (princ "    #") (princ (inference-number c))
               (princ "   sup = ") (set-prinp (node-supposition c))
               (terpri))))
    (princ ")") (terpri))

(defunction ?-variables (formula)
    (cond ((and formula (listp formula))
                (union (?-variables (car formula)) (?-variables (cdr formula))))
              ((atom formula)
                (if (equal (car (explode (write-to-string formula))) "?") (list formula)))))

#| (? formula), where formula can contain variables of the form "?x",  returns a list of all 
known conclusions matching the formula. |#
(defunction ? (formula)
    (when (stringp formula) (setf formula (reform formula)))
    (let* ((d-node (d-node-for formula))
              (nodes (search-d-nodes formula d-node)))
      (cond (nodes
                  (terpri)
                  (princ "The following answers are known for the query (? ") (prinp formula) (princ "):") (terpri)
                  (princ "------------------------------------------------------------------------------------------------------------------------------------------------------------")
                  (terpri)
                   (dolist (node nodes)
                       (princ "    ") (princ (node-formula node)) (princ "    by node #")
                       (princ (inference-number node)) (terpri))
                   (terpri))
                (t 
                  (terpri) (princ "No answers are known for the query (? ") (prinp formula) (princ ").") (terpri)
                  (princ "------------------------------------------------------------------------------------------------------------------------------------------------------------")
                  (terpri)
                  (terpri)))
      nodes))

(defunction search-d-nodes (formula d-node)
    (let ((nodes nil)
            (?-vars (?-variables formula)))
      (dolist (c-list (d-node-c-lists d-node))
          (dolist (node (c-list-nodes c-list))
              (when (and (null (node-supposition node))
                                  (match formula (node-formula node) ?-vars))
                   (push node nodes))))
      (append nodes
                     (unionmapcar #'(lambda (dt) (search-d-nodes formula (cdr dt)))
                                             (discrimination-tests d-node)))))

(defunction ?interests (formula)
    (when (stringp formula) (setf formula (reform formula)))
    (let* ((d-node (d-node-for formula))
              (interests (search-d-node-interests formula d-node)))
      (cond (interests
                  (terpri)
                  (princ "The following interests were adopted for the query (? ") (prinp formula) (princ "):") (terpri)
                  (princ "------------------------------------------------------------------------------------------------------------------------------------------------------------")
                  (terpri)
                   (dolist (interest interests)
                       (princ "    ") (princ (interest-formula interest)) (princ "    by interest #")
                       (princ (interest-number interest)) (terpri))
                   (terpri))
                (t 
                  (terpri) (princ "No interests were adopted for the query (? ") (prinp formula) (princ ").") (terpri)
                  (princ "------------------------------------------------------------------------------------------------------------------------------------------------------------")
                  (terpri)
                  (terpri)))
      interests))

(defunction search-d-node-interests (formula d-node)
    (let ((interests nil)
            (?-vars (?-variables formula)))
      (dolist (i-list (d-node-i-lists d-node))
          (dolist (interest (i-list-interests i-list))
              (when (and (null (node-supposition interest))
                                  (match formula (interest-formula interest) ?-vars))
                   (push interest interests))))
      (append interests
                     (unionmapcar #'(lambda (dt) (search-d-node-interests formula (cdr dt)))
                                             (discrimination-tests d-node)))))