;---------------------------- ULTIMATE-EPISTEMIC-INTERESTS -----------------------------

(defstruct (query (:print-function print-query)
                                (:conc-name nil))
   (query-number 0)
   (query-formula nil)
   (query-strength 0)
   (query-queue-node nil)
   (deductive-query nil)  ;; t if the query is whether the query formula is deductively provable
   (positive-query-instructions nil) ;; a list of functions applicable to an inference-node
   (negative-query-instructions nil) ;; a list of functions applicable to an inference-node
   (query-answers nil)  ;;a list of inference-nodes
   (answered? nil)  ;; t if some answer is justified to degree greater than or equal
                                   ;; to the degree of interest, nil otherwise
   (query-interest nil)   ;; the interest recording the query
   (negative-query-interest nil)  ;; the negative-interest for a whether-query
   (?-constraint nil))  ;; a function which when applied to the ?-vars yields a discharge-condition
                                    ;; for the query-interest, constraining the instantiating terms.

(defun print-query (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Query " stream) (princ (query-number x) stream)
    (princ ": " stream) (princ (pretty (query-formula x)) stream)
    (princ ">" stream))

(defunction query (n)
    (find-if #'(lambda (c) (equal (query-number c) n))
                 *ultimate-epistemic-interests*))

(defunction ?-query-p (Q)
    (and (query-p Q) (?-genp (query-formula Q))))

#| This returns two values: the matrix, and the list of ?-variables. |#
(defunction ?-matrix (p &optional vars)
    (push (q-variable p) vars)
    (let ((formula (q-matrix p)))
       (cond ((?-genp formula) (?-matrix formula vars))
                   (t (values formula vars)))))

(defunction whether-query-p (Q)
    (and (query-p Q) (whether-formula (query-formula Q))))

(defunction query (n)
    (find-if #'(lambda (c) (equal (query-number c) n))
                 *ultimate-epistemic-interests*))

(defunction show-query (Q)
    (if (numberp Q) (setf Q (query Q)))
    (princ Q) (princ ": ")
    (prinp (query-formula Q)) (terpri))

(defunction show-queries ()
    (terpri)
    (princ
      "================== ULTIMATE EPISTEMIC INTERESTS ===================")
    (terpri)
    (dolist (Q *ultimate-epistemic-interests*)
        (show-query Q)))

(defunction inclusive-node-ancestors (node)
    (cons node (node-ancestors node)))

(defunction ancestral-links (node)
    (unionmapcar+ #'support-links (inclusive-node-ancestors node)))

(defunction display-query (Q)
    (princ "  Interest in ") (prinp (query-formula Q)) (terpri)
    (cond ((null (answered? Q))
                 (princ "  is unsatisfied.")
                 (when (null (query-answers Q)) (princ "  NO ARGUMENT WAS FOUND."))
                 (terpri))
                ((or (whether-query-p Q) (?-query-p Q))
                  (dolist (C (query-answers Q))
                      (when (>= (compute-undefeated-degree-of-support C) (query-strength Q))
                           (princ "  is answered by node ")
                           (princ (inference-number C)) (princ ":  ")
                           (princ (pretty (node-formula C))) (terpri)
                           (let ((skolem-functions (skolem-functions (node-formula C))))
                              (when skolem-functions
                                   (let* ((sf (mem1 skolem-functions))
                                             (support-link
                                               (find-if #'(lambda (SL)
                                                                 (and (eq (support-link-rule SL) EI)
                                                                           (occur sf (node-formula (support-link-target SL)))
                                                                           (not (occur sf (node-formula (mem1 (support-link-basis SL)))))))
                                                            (ancestral-links C))))
                                      (when support-link
                                           (let* ((node (mem1 (support-link-basis support-link)))
                                                     (formula (node-formula node))
                                                     (var (q-variable formula)))
                                              (princ "  where ") (princ sf) (princ " is any ") (princ var)
                                              (princ " such that ") (princ (q-matrix formula)) (princ ",") (terpri)
                                              (princ "  and the existence of such")
                                              (if (equal var "x") (princ " an ") (princ " a ")) (princ var)
                                              (princ " is guaranteed by node ") (princ (inference-number node)) (terpri))))))
                           )))
                (t (dolist (C (query-answers Q))
                       (when (>= (compute-undefeated-degree-of-support C) (query-strength Q))
                            (princ "  is answered affirmatively by node ")
                            (princ (inference-number C)) (terpri)))))
    (princ "---------------------------------------------------") (terpri))

(defunction display-queries ()
    (terpri)
    (princ
      "================== ULTIMATE EPISTEMIC INTERESTS ===================")
    (terpri)
    (dolist (Q *ultimate-epistemic-interests*)
        (display-query Q)))

(defunction answers (formula query)
   (let ((query-formula (query-formula query)))
     (if (?-genp query-formula)
       (instance-of formula query-formula)
       (equal formula query-formula))))

#| This assumes that formula2 is indefinite. |#
(defunction instance-of (formula1 formula2)
    (match (mem2 formula2) formula1 (list (mem2 (mem1 formula2)))))

(defunction in-interest (sequent)
    (let ((interests (interests-for (sequent-formula sequent) nil)))
       (when interests
            (some #'(lambda (interest) (null (interest-supposition interest)))
                         interests))))

(defunction adopt-ultimate-interest (query)
    (push query *ultimate-epistemic-interests*)
    (when (not (in-interest (list nil (query-formula query))))
         (queue-query-for-interest query)))

(defunction queue-query-for-interest (query)
    (let ((node
              (make-inference-queue-node
                :queue-number (incf *queue-number*)
                :enqued-item query
                :item-kind :query
                :item-complexity (complexity (query-formula query))
                :discounted-strength (query-strength query)
                :degree-of-preference (query-preference query))))
       (setf (query-queue-node query) node)
       (setf *inference-queue* (ordered-insert node *inference-queue* #'i-preferred))))