; --------------------------------------  THE INFERENCE-QUEUE -------------------------------------- 

(defstruct (inference-queue-node (:print-function print-inference-queue-node)
                                                                (:conc-name nil))
   (queue-number 0)
   (enqued-item nil)  ;; either an interest or a conclusion or a query
   (item-kind nil)   ;; this will be :conclusion, :interest, or :query
   (item-complexity 0)
   (discounted-strength 0)
   (degree-of-preference 0))

(defun print-inference-queue-node (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Item " stream)
    (princ (queue-number x) stream) (princ ">" stream))

#| *inference-queue* is ordered by i-preference: |#
(defunction i-preferred (node1 node2)
    (> (degree-of-preference node1) (degree-of-preference node2)))

(defunction complexity (x)
    (cond ((null X) 0)
              ((stringp x) 1)
              ((atom x) 1)
              ((listp x) 
                (cond ((skolem-function (car x))
                            (cond ((null (cdr x)) 1)
                                      ((and (not (listp (cadr x))) (not (eq (cadr x) '=)))
                                        *skolem-multiplier*)
                                      ((and (listp (cadr x)) (skolem-function (caar (cdr x))))
                                        (* *skolem-multiplier* (1+ (complexity (cdr x)))))
                                      (t (apply #'+ (mapcar #'complexity x)))))
                          ;; the following handles functions that occur within their own scopes
                          ((and (not (null (cdr x)))
                                    (symbolp (car x))
                                    (not (member (mem1 x) *logical-constants*))
                                    (occur (car x) (cdr x)))
                            (* *skolem-multiplier* (1+ (complexity (cdr x)))))
                          ((or (u-genp x) (e-genp x)) (* *quantifier-discount* (complexity (q-matrix x))))
                          ((consp (cdr x)) (apply #'+ (mapcar #'complexity x)))
                          (t (+ (complexity (car x)) (complexity (cdr x))))))))

(defunction formula-complexity (formula)
    (cond ((mem formula *skolem-free-suppositions*) 0)
                (t (complexity formula))))

(defunction sequent-complexity (sequent)
    (let ((sup (sequent-supposition sequent))
            (formula (sequent-formula sequent)))
       (let ((complexity
                 (cond (sup
                              (+ (max 1 (formula-complexity formula))
                                   (apply
                                     '+ (mapcar
                                           #'(lambda (P)
                                                 (cond ((mem P *skolem-free-suppositions*) 0)
                                                             (t (complexity P))))
                                           sup))))
                             (t (max 1 (formula-complexity formula))))))
          ;  (when *display?*
          ;       (princ "The complexity of ") (print-sequent sequent) (princ " is ") (princ complexity) (terpri))
          complexity)))

#|
(defunction sequent-complexity (sequent)
    (let ((sup (sequent-supposition sequent))
            (formula (sequent-formula sequent))
            (length 0))
       (let ((complexity
                 (cond (sup
                              (+ (max 1 (formula-complexity formula))
                                   (apply
                                     '+ (mapcar
                                           #'(lambda (P)
                                                 (cond ((mem P *skolem-free-suppositions*) 0)
                                                             (t (incf length) (complexity P))))
                                           sup))))
                             (t (max 1 (formula-complexity formula))))))
          ;  (when *display?*
          ;       (princ "The complexity of ") (print-sequent sequent) (princ " is ") (princ complexity) (terpri))
          (if (> length 2) (* complexity (expt 10 (* length length))) complexity))))
|#

#| This is the default computation of degree-of-preference for premises.  Premises
are triples consisting of a formula, a supposition, and a degree-of-support.
Premises are queued for immediate retrieval. |#
(defunction premise-preference (premise)
    (/ (mem2 premise) (complexity (mem1 premise))))

(defstruct (goal (:print-function print-goal) (:conc-name nil))
    (goal-number 0)
    (goal-formula nil)
    (goal-strength 1)
    (supporting-goal-node nil)  ;; the node supporting this as a suitable goal
    (goal-generating-desire nil)  ;; the desire, if there is on, that generates the goal
    (plans-for nil)  ;; the list of candidate plans that aim at the satisfaction of this goal
    (user-question-asked? nil))

(defunction print-goal (goal stream depth)
    (declare (ignore depth))
    (princ "#<goal: " stream)
    (princ (pretty (goal-formula goal)) stream)
    (princ ">" stream))

(defstruct (desire (:print-function print-desire) (:conc-name nil))
    (desire-number 0)
    (desire-content nil)
    (desire-object nil)  ;; the object of a desire will be a goal
    (desire-strength 0)
    (generated-plans nil)
    (desire-generating-interest nil)  ;; for epistemic-desires
    (desire-inference-node nil))  ;; the inference-node recording the desire

(defunction print-desire (desire stream depth)
    (declare (ignore depth))
    (princ "#<desire: " stream)
    (princ (pretty (desire-content desire)) stream)
    (princ ">" stream))

(defunction goal-generating-interest (goal)
    (let ((desire (goal-generating-desire goal)))
       (when desire (desire-generating-interest desire))))

(defstruct (percept (:print-function print-percept) (:conc-name nil))
    (percept-number 0)
    (percept-content nil)
    (percept-clarity 0)
    (percept-date 0))

(defunction print-percept (percept stream depth)
    (declare (ignore depth))
    (princ "#<percept: " stream)
    (princ (pretty (percept-content percept)) stream)
    (princ ">" stream))

#| This is the default computation of degree-of-preference for desires. |#
(defunction desire-preference (desire)
    (/ (desire-strength desire) (complexity (desire-content desire))))

#| This is the default computation of degree-of-preference for percepts. |#
(defunction percept-preference (percept)
    (/ (percept-clarity percept) (complexity (percept-content percept))))

(defunction discharged? (interest degree)
    (let ((discharged-degree (discharged-degree interest)))
       (and discharged-degree
                 (>= discharged-degree degree))))

#| The following is the default computation of interest-priority for defeaters. |#
(defunction defeater-priority (interest)
    (declare (ignore interest))
    *base-priority*)

#| The following is the default computation of the degree-of-preference for queries. |#
(defunction query-preference (query)
    (let ((complexity (complexity (query-formula query)))
            (strength
              (cond ((member query *permanent-ultimate-epistemic-interests*)
                           (query-strength query))
                          ((answered? query)
                            (* (query-strength query) *answered-discount*))
                          (t (query-strength query)))))
       (/ strength complexity)))

#| This is the default computation of degree-of-preference for an interest, where
priority is the interest-priority and complexity is the complexity of the interest-sequent. |#
(defunction interest-preference (priority complexity)
    (if (zerop complexity) priority (/ priority complexity)))

#| This reverses the default computation of degree-of-preference to compute priority
from preference. |#
(defunction retrieved-interest-priority (preference complexity)
    (* complexity preference))

(defunction interest-link-priority (link interest-priority interest)
    (if (or (link-defeat-status link)
               (let ((rn (resultant-interest link)))
                  (discharged? rn (maximum-degree-of-interest rn)))
               (and interest (discharged? interest (maximum-degree-of-interest interest))))
       *base-priority*
       interest-priority))

#| The following is the default computation of interest-priority for an interest on
the inference-queue that is concluded. |#
(defunction concluded-interest-priority (Q)
    (declare (ignore Q))
    *concluded-interest-priority*)

#| This must recompute reductio-ancestors, non-reductio-suppositions, deductive-only-status,
and apply forwards defeasible reasons. |#
(defunction convert-reductio-supposition (sup discount-factor)
    (setf (reductio-ancestors sup) (list (cons (node-formula sup) sup)))
   ; (setf (non-reductio-supposition sup) nil)
    (setf (non-reductio-supposition? sup) t)
    (let ((Q (node-queue-node sup)))
       (when Q
            (setf (degree-of-preference Q) (* discount-factor (/ 1 (item-complexity Q))))
            (setf *inference-queue*
                     (ordered-insert Q (remove Q *inference-queue*) #'i-preferred))))
    (let ((nodes
              (convert-from-deductive-only sup)))
       (dolist (C nodes)
           (when (deductive-in C sup)
                (let ((nr (find-if #'(lambda (x) (equal (cdr x) sup)) (non-reductio-supposition C))))
                   (when nr
                        (pull nr (non-reductio-supposition C))
                        (push nr (reductio-ancestors C))))))
       (dolist (C nodes)
           (apply-forwards-defeasible-reasons C))))

;======================================================