;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: ask-tell.lsp
;;;;    System: FIRE
;;;;   Version: v1
;;;;    Author: Ken Forbus
;;;;   Created: December 8, 2000 17:13:52
;;;;   Purpose: Ask/Tell interface to FIRE reasoners
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Monday, May 31, 2004 at 20:51:22 by Kenneth Forbus
;;;; ---------------------------------------------------------------------------

(in-package :fire)

;;; In ASK, the following parameters are used:
;;; query = the pattern comprising the question.
;;; reasoner = the reasoner the question is being asked of.
;;; context = the scope of microtheories/domain theories to be used
;;; number = how many answers are sought.  Possibilities are:
;;;  A positive integer =  Ask will stop once it has that many solutions.
;;;  :all = Ask will try multiple things to get answers, but if there are cached
;;;         answers in the LTRE, it will assume that those are good enough.
;;;  :exhaustive = Ask will try multiple things to get answers, in addition to 
;;;                including cached solutions in the LTRE.
;;; response = form of output desired.  Possibilities for each answer are
;;;  :bindings = an alist of bindings.
;;;  :pattern = the query, with the bindings substituted in.
;;;  :solution = list of the forms found.
;;;  <anything else> = a pattern that the bindings will be plugged into.
;;; effort = bounds on the amount and type of work that the reasoner should do.
;;;  This will be an alist whose entries will be things like (:depth . 3), 
;;;    (:KB-only . T), (:total-nodes . 200), etc.  Still under contemplation.
;;;    The idea is to keep the language open, so that more controls can be added.

;;; Any results produced by ASK are appropriately justified within the LTRE.

(defmethod ask (query (reasoner reasoner)
                      (context t)
                      (number t)
                      (response t)
                      (effort t))
  "ASK provides programmatic access to the reasoner."
  (with-reasoner reasoner
    (mp:with-process-lock ((lock reasoner))
      (cond ((conjunction? query)
             (let ((solutions 
                    (ask-conjunction (cddr query)
                                     (ask (cadr query) reasoner context number
                                          :bindings effort)
                                     reasoner context number effort)))
               ;; Solutions are sets of binding lists.  Now we need to use the
               ;; response information to return the right things
               (case response
                 (:bindings solutions)
                 (:pattern (mapcar #'(lambda (soln)
                                       (sublis soln query)) solutions))
                 (t (mapcar #'(lambda (soln)
                                (sublis soln response)) solutions)))))
            ((disjunction? query)
             (ask-disjunction (cdr query) reasoner context number response effort))
            ((isa-statement? query)
             (ask-isa (cadr query) (third query) reasoner
                      context number response effort))
            ((genls-statement? query)
             (ask-genls (cadr query) (third query) reasoner
                        context number response effort))
            ((evaluate-statement? query)
             (ask-for-evaluation query reasoner context number response effort))
            ((structural-statement? query)
             (ask-structural-statement query reasoner
                                       context number response effort))
            ((lisp-test-statement? query)
             (ask-lisp-test query reasoner context number response effort))
            ((metaknowledge-statement? query)
             (ask-metaknowledge (car query) (cadr query) reasoner
                                context number response effort))
            ((contextualized-query? query)
             (ask-contextualized query reasoner context number response effort))
            (t (ask-proposition query reasoner context number response effort))))))

;;; Handling connectives (:and and :or)

(defmethod ask-conjunction (conjuncts solutions (reasoner reasoner)
                                      (context t)
                                      (number t)
                                      (effort t))
  ;; We're assuming that users never use a huge number of conjuncts.
  ;; (n.b. the backchainer isn't going to use ask-conjunction!)
  (cond ((null conjuncts) (remove-duplicates solutions :test 'equal))
        (t (ask-conjunction 
            (cdr conjuncts)
            (mapcan
                #'(lambda (solution)
                    (let* ((conjunct (sublis solution
                                             (car conjuncts)))
                           (new-bindings
                            (ask conjunct reasoner context number
                                 :bindings effort)))
                      (delete :fail ;; shouldn't be able to be
                              ;; inconsistent, but be careful
                              (mapcar #'(lambda (new-solution)
                                          (merge-binding-lists solution
                                                               new-solution))
                                new-bindings))))
              solutions)
            reasoner context number effort))))

(defun merge-binding-lists (old-alist new-alist)
  ;; We're assuming we can nuke new-alist but not old-alist
  ;; because it is being used to update lots of new solutions.
  ;; We're going to copy entries rather than sharing them to
  ;; avoid downstream lossage.
  (when (eq old-alist :fail)
    ;; (warn "Old alist in merge-binding-lists is :fail: ~A" new-alist)
    (return-from merge-binding-lists (values nil)))
  (when (eq new-alist :fail)
    ;; (warn "New alist in merge-binding-lists is :fail: ~A" old-alist)
    (return-from merge-binding-lists (values nil)))
  ;; Warnings were removed because when there is a failing query, these cases will
  ;; occur, and it isn't appropriate to whine about it.
  (dolist (entry old-alist new-alist)
    (let ((other (assoc (car entry) new-alist)))
      (cond (other 
             (unless (equal (cdr other) (cdr entry))
               (return-from merge-binding-lists (values :fail))))
            (t (push (cons (car entry) (cdr entry)) new-alist))))))

(defmethod ask-disjunction (disjuncts (reasoner reasoner)
                                      (context t)
                                      (number t)
			              (response t)
                                      (effort t))
  ;;; We'll go serially down the disjunctions, left-to-right order, gathering
  ;;; up solutions until we have enough.  Which means updating the number
  ;;; constraint as new solutions come in
  (let ((solutions nil)
        (n-solutions 0)
        (so-far 0)
        (sought number)
        (results nil))
  (dolist (disjunct disjuncts results)
    (setq solutions (ask disjunct reasoner context sought
                         response effort)
        n-solutions (length solutions))
    (incf so-far n-solutions)
    (setq sought (update-ask-number-constraint number n-solutions)
        results (nconc-new-onto-back results solutions))
    ;; A dab extra consing in this
    ;; order, but it will make the results easier to read.
    (when (check-answer-number-constraint number so-far)
      (return-from ask-disjunction results)))))

(defun nconc-new-onto-back (current maybe-new-stuff)
  (cond ((null current) maybe-new-stuff)
        (t (let ((end-pointer (last current))
                 (new-end nil))
             (dolist (maybe maybe-new-stuff current)
               (unless (member maybe current :test 'equal)
                 (setq new-end (cons maybe nil))
                 (setf (cdr end-pointer) new-end)
                 (setq end-pointer new-end)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Special cases: isa, genls
;;
;; We're treating queries of this form as lookups, rather than
;; something that can invoke chaining, whenever possible.
;; Might not be sufficient, but a decent starting point.

;; 2/13/02: Like the KB results, results from structural queries (genls/isas)
;; also need to be justified.  Need to do this somewhat carefully to save work
;; in the LTRE.  The intricate bit is that we can't just do a wm-retrieve and
;; assume that since we found some we have them all.  The genls cache is
;; cheap, though, so by doing the LTRE justifies only when novel, we should do
;; fine.

(defmethod ask-genls (subclass superclass (reasoner reasoner)
                               (context t)
                               (number t)
		               (response t)
                               (effort t))
  (cond ((ltre:variable? subclass)
         (cond ((ltre:variable? superclass)
                ;; (genls ?x ?y) case
                ;; Best we can do is grab everything
                (ask-proposition (make-genls subclass superclass)
                                 reasoner context number response effort))
               (t ;; (genls ?x <constant>) case
                (let ((results (immediate-specs superclass :kb (kb reasoner))))
                  (dolist (subset results)
                    (justify-kb-result-if-needed
                     (make-genls subset superclass) reasoner))
                  (case response
                    (:bindings (mapcar #'(lambda (result)
                                           (list (cons subclass result)))
                                 results))
                    ((:pattern :solutions)
                     (mapcar #'(lambda (sub)
                                 (make-genls sub superclass))
                       results))
                    (t (mapcar #'(lambda (result)
                                   (sublis (list (cons subclass result)) response))
                         results)))))))
        ((ltre:variable? superclass) ;; (genls <constant> ?x) case
         (let ((results (immediate-genls subclass :kb (kb reasoner))))
           (dolist (super results)
             (justify-kb-result-if-needed (make-genls subclass super) reasoner))
           (case response
             (:bindings (mapcar #'(lambda (result)
                                    (list (cons superclass result)))
                          results))
             ((:pattern :solutions)
              (mapcar #'(lambda (sup) (make-genls subclass sup))
                results))
             (t (mapcar #'(lambda (result)
                            (sublis (list (cons superclass result))
                                    response))
                  results)))))
        (t ;; (genls <constant> <constant>)
         (when (spec-of? subclass superclass :kb (kb reasoner))
           (justify-kb-result-if-needed (make-genls subclass superclass) reasoner)
           (case response
             (:bindings (list nil)) ;; One solution, but no new bindings
             ((:pattern :solutions) (list (make-genls subclass superclass)))
             (t (list (copy-tree response))))))))

(defmethod ask-isa (instance collection (reasoner reasoner)
                               (context t)
                               (number t)
                               (response t)
                               (effort t))
  (cond ((not (ground-term? instance))
         (cond ((not (ground-term? collection)) ;; (isa ?i ?col)
                ;; Whoever did this probably didn't mean it.
                ;; But give'm what they asked for.  At least
                ;; the explictly known ones, NOT the deductive
                ;; closure!  
                (ask-proposition (make-isa instance collection)
                                 reasoner context number response effort))
               (t ;; (isa ?x <constant>)
                ;; Another retrieval case.  We'll do the simple thing and not
                ;; do gathering through the entire sublattice
                (ask-proposition (make-isa instance collection)
                                 reasoner context number response effort))))
        ((not (ground-term? collection))
         ;; (isa <constant> ?collection)
         ;; Tougher to know on this one whether or not to do lattice-walking.
         ;; My bet is no, that we're still thinking in terms of lookup here.
         ;; How often does one the whole lattice at this level of operation?
         ;; If one is really doing that, it ought to be dropped into the level
         ;; of special-purpose code.  Hence we'll stick with lookup here as well.
         (ask-proposition (make-isa instance collection)
                          reasoner context number response effort))
        (t ;;(isa <constant> <constant>)
         ;; This IS a case where we want to crawl up the lattice.
         (cond ((instance-of? instance collection reasoner)
                (justify-kb-result-if-needed
                 (make-isa instance collection) reasoner)
                (case response
                  (:bindings (list nil))
                  ((:solutions :pattern) (list (make-isa instance collection)))
                  (t (list (copy-tree response))))))))) 
    
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; The core of ASK: Handling a proposition
(defmethod ask-proposition (query (reasoner reasoner)
                                  (context t)
                                  (number t)
                                  (response t)
                                  (effort t))
  ;; N.B. This nesting doesn't enable ASK to only look at the KB.  But that's
  ;; okay, since RETRIEVE only looks at the KB.  
  ;; The enough? flag indicates that one shouldn't go on.  This can be because
  ;; the numerical constraints are satisfied, or because the system knows that
  ;; going further wouldn't be useful (i.e., when a source responsible for that
  ;; predicate fails.
  (let* ((use-pragma? (use-pragma? effort))
         (signature (and use-pragma? (binding-signature query)))
         (pragma (and use-pragma? 
                      (eq (car signature) :known)
                      (get-pragma (car query) (kb reasoner))))
         (functional-query? (and use-pragma? 
                                 (is-query-functional? signature pragma)))
         (contextualized? (not (global-context? context)))
         (contextualized-query (if contextualized? (make-case-fact context query)
                                 query)))
    (multiple-value-bind (results enough?)
        (ltre::wm-retrieve contextualized-query (ltre reasoner) number response)
      (cond (enough? (values results t))
            ((and results functional-query?) (values results t))
            ((eq effort :wm-only) (values results t))
            (t (let ((number (update-ask-number-constraint
                              number (length results))))
                 (when (and contextualized? ;; Also try original in global context
                            (not (eq effort :local-only)))
                        ;; ***** Really need to support Mt inheritance structure
                        ;; ***** here, but that can wait for now.
                   (multiple-value-bind (general-results enough?)
                       (ltre::wm-retrieve query (ltre reasoner) number response)
                     (setq results (nunion results general-results
                                           :test 'equal))
                     (setq number (update-ask-number-constraint
                                   number (length general-results)))
                     (when (or enough? 
                               (and results functional-query?))
                       (return-from ask-proposition
                         (values results t)))))
                 (multiple-value-bind (kb-results enough?)
                     (ask-kb query reasoner context number response effort)
                   (let ((results (nunion results kb-results :test 'equal)))
                     (cond (enough? (values results t))
                           ((and results functional-query?) (values results t))
                           ((eq effort :lookup-only) (values results t))
                           (t (let ((number (update-ask-number-constraint
                                             number (length kb-results))))
                                (multiple-value-bind (source-results enough?)
                                    (ask-sources query reasoner context number
                                                 response effort)
                                  (values 
                                   (nunion results source-results :test 'equal) 
                                   enough?)))))))))))))
 
(defun use-pragma? (effort)
  ;; for now we only key off effort, we may need to add other constraints
  ;; in the future
  (not (eq effort :wm-only)))

(defun update-ask-number-constraint (limit so-far)
  (cond ((numberp limit)
         ;; Can comment next line out if trying to squeeze performance.
         (unless (integerp limit)
           (error "Number constraint in Ask must be integer: ~A."
             limit))
         (if (> so-far limit) 0 (- limit so-far)))
        (t limit)))


;;; Changed so that symmetric-retrieve returns a list of (query . bindings)
;;; to support justification
(defun ask-kb (query reasoner context number response effort)
  (let* ((result-pairs (symmetric-retrieve query :kb (kb reasoner) :context context
                                           :number number :response :bindings
                                           :effort effort))
         (n-results (length result-pairs))
         (results nil))
    (dolist (result-pair result-pairs)
      (let* ((q (car result-pair))
             (bindings (cdr result-pair))
             (pattern (sublis bindings query))
             (just-type (if (equal q query) :kb-lookup :kb-symmetric))
             (kb-pattern (if (eq just-type :kb-symmetric)
                           (sublis bindings q) pattern)))
        (justify-kb-result pattern reasoner just-type kb-pattern)
        (case response
          (:bindings (push bindings results))
          (:solutions (push pattern results))
          (:pattern (push pattern results))
          (t (push (sublis bindings response) results)))))        
    (values results (check-answer-number-constraint number n-results))))

(defun justify-kb-result (datum reasoner
                                &optional (justification-type :kb-lookup)
                                kb-datum)
  ;; This provides a link between the working memory and KB.
  ;; Important for maintaining good explanations.
  (let ((asn-form (make-in-kb-statement (or kb-datum datum))))
    (ltre::assume! asn-form justification-type (ltre reasoner))
    (ltre::assert! `(:implies ,asn-form ,datum) :kb (ltre reasoner))
    datum)) 

(defun justify-kb-result-if-needed (kb-datum reasoner)
  ;; justify-kb-result is fine when you know that the answer
  ;; wasn't already in WM, as per ask-kb, which is only called
  ;; when wm-retrieve fails.  This is for those other times, when
  ;; we want to avoid doing extra work in the LTRE.  (John's version
  ;; detects duplicate clauses in any case, but better to not create
  ;; them in the first place!)
  (let ((asn-form (make-in-kb-statement kb-datum)))
    (cond ((ltre::known? asn-form) 
           (unless (ltre::known? kb-datum)
             (ltre::assert! `(:implies ,asn-form ,kb-datum) :kb
                            (ltre reasoner)))
           kb-datum)
          (t (ltre::assume! asn-form :kb-lookup (ltre reasoner))
             (ltre::assert! `(:implies ,asn-form ,kb-datum) :kb
                            (ltre reasoner))
             kb-datum))))

(defun check-answer-number-constraint (limit so-far)
  (cond ((numberp limit)
         ;; Can comment next line out if trying to squeeze performance.
         (unless (integerp limit)
           (error "Number constraint in Ask must be integer: ~A."
             limit))
         (>= so-far limit)) ;; got at least as many as we want
        ((and (not (eq limit :exhaustive)) (> so-far 0)) t)
        (t nil))) ;; can always use more if being exhaustive

;;;; ------------------------------------------------------------------------
;;;; Handling queries that can be directly evaluated

(defun lisp-test-statement? (query)
  (and (listp query) (symbolp (car query))
       (or (eq (car query) 'data::equals)
           (eq (car query) 'data::different)
           (eq (car query) 'data::alphalessp))))

(defmethod predicate-ask-signatures ((pred (eql 'data::equals))
                                     (reasoner reasoner))
  '((:input-only :input-only)))

(defmethod predicate-ask-signatures ((pred (eql 'data::different))
                                     (reasoner reasoner))
  '((:input-only :input-only)))

(defmethod predicate-ask-signatures ((pred (eql 'data::alphalessp))
                                     (reasoner reasoner))
  '((:input-only :input-only)))

(defun ask-lisp-test (query reasoner context number response effort)
  ;; For now we're going to punt if the arguments
  ;; are not both known.
  (declare (ignore context number effort))
  (cond ((or (variable? (cadr query)) (variable? (third query))) nil)
        ((ltre:known? query (ltre reasoner))
         (when (ltre:true? query (ltre reasoner))
           (case response
             (:pattern (list query))
             (:bindings (list nil))
             (t response))))
        ((eq (car query) 'data::equals)
         (cond ((equal (cadr query) (third query))
                (ltre:assert! query :lisp-test (ltre reasoner))
                (case response
                  (:pattern (list query))
                  (:bindings (list nil))
                  (t response)))
               (t (ltre:assert! `(:not ,query) :lisp-test (ltre reasoner))
                  nil)))
        ((eq (car query) 'data::different)
         (cond ((equal (cadr query) (third query))
                (ltre:assert! `(:not ,query) :lisp-test (ltre reasoner))
                nil)
               (t (ltre:assert! query :lisp-test (ltre reasoner))
                  (case response
                    (:pattern (list query))
                    (:bindings (list nil))
                    (t response)))))
        ((eq (car query) 'data::alphalessp)
         (cond ((ltre:alphalessp (cadr query) (third query))
                (ltre:assert! query :lisp-test (ltre reasoner))
                (case response
                  (:pattern (list query))
                  (:bindings (list nil))
                  (t response)))
               (t nil)))))

;;;;;;;;;;;;;
;; Handling contextualized queries

(defun contextualized-query? (form)
  (and (listp form)
       (symbolp (car form))
       ;; Hardwire choices for now.  And forget hypens.
       (case (car form)
         (data::ist-Information t)
         (t nil))))  

(defun parse-contextualized-query (form)
  ;; Assumes type checks out correctly.
  ;; Returns three values: contents, context, predicate
  (ecase (car form)
    (data::ist-Information (values (third form) (second form) (car form)))
;;;    (data::ist (values (third form) (second form) (car form)))
;;;    (data::holdsIn (values (second form) (third form) (car form)))
    ))

(defun make-contextualized-assertion (content context predicate)
  (cond ((case-reference? context)
         (ecase predicate
           (data::ist-Information (list predicate context content))
           (data::ist (list predicate context content))
           (data::holdsIn (list predicate content context))))
        (t content)))

(defun case-reference? (context)
  ;; N.B. This is a heuristic.  Need to improve as part of incorporating
  ;; a better context system into FIRE more generally
  (and (symbolp context)
       (not (keywordp context))))

(defun make-case-assertion (content context)
  (make-contextualized-assertion content context 'data::ist-Information))

(defun ask-contextualized (query reasoner context number response effort)
  (multiple-value-bind (content case predicate)
      (parse-contextualized-query query)
    ;; Now we have to look both at the case contents and the KB.
    ;; In general one can do this sort of thing via backchaining,
    ;; but there are some common special cases that look worth
    ;; hard-wiring.  Specifically, the use of inheritance information.
    (cond ((not (listp query)) (error "Non-statement in context: ~A." query))
          ((consp content)
           (cond ((eq (car content) 'data::isa)
                  (cond ((variable? case)
                         ;; This is a question about potentially all cases.
                         ;; Could be dramatically expensive, so we're going to
                         ;; punt on the expensive stuff.  We'll treat this one
                         ;; as a pure lookup
                         (ask-proposition query reasoner context 
                                          number response effort))
                        (t ;; We'll be willing to do more work given that we know a
                         ;; local context to operate in.
                         (ask-contextualized-isa 
                          content case predicate
                          query reasoner context number response effort))))
                 ((any-sources-for? content reasoner)
                  ;; If it's a source, change the context to be that of the
                  ;; case and ask it.  
                  ;; N.B. Sources must do something appropriate if 
                  ;; the case is a variable,
                  ;; but then again, they'd have to do that anyway.
                  ;; Please see "context reasoning notes.cl" in
                  ;; docs directory for discussion of issues involved.
                  (let* ((contextualized-results
                          (ask-sources content reasoner case :all
                                       :pattern effort))
                         (results (case response
                                    (:bindings 
                                     (mapcar #'(lambda (result)
                                                 (ltre::unify result query))
                                       contextualized-results))
                                    (:pattern contextualized-results)
                                    (t (mapcar 
                                           #'(lambda (result)
                                               (let ((bindings (ltre::unify result query)))
                                                     (sublis bindings response)))
                                         contextualized-results)))))
                    (values results 
                            (check-answer-number-constraint
                             number (length results)))))
                 ;; Fall through to default
                 (t (ask-proposition query reasoner 
                                     context number response effort))))
          (t (ask-proposition query reasoner context number response effort)))))

(defun ask-contextualized-isa (content case predicate query 
                                       reasoner context number response effort)
  ;;
  ;; The content is of the form (isa <espec> <cspec>) where either 
  ;; <espec> or <cspec> or both could be (or contain) variables.
  ;; Suppose <cspec> is a constant.  Then we are asking either if a specific entity
  ;; is in that collection, or for the set of entities that are in that collection,
  ;; according to whether or not <espec> is ground.  So first gather the entities 
  ;; independent of type, and retrieve their types in the context.
  ;; Then see if any of those are subsets of <cspec>, and if so, include that
  ;; entity in the result.
  ;; Suppose <cspec> is a variable (or at least is non-ground).  
  ;; If <espec> is a constant, 
  ;; then we want to augment the bindings of <cspec> with all of the
  ;; supercollections of those known in the context.  
  ;; If <espec> isn't a constant, this seems like a very expensive query where
  ;; we are asking for all entities in the context what collections they are part of.
  ;; So we'll punt on that case for now, treating situations 
  ;; where <cspec> is variable as purely
  ;; local queries.
  ;; ***** We'll also assume that when <espec> or <cspec>
  ;; *****   are non-ground, they are simply variables for now.
  (let ((cspec (third content))
        (espec (second content)))
    (cond ((not (ground-term? cspec))
           ;; Treat as purely localized query
           (ask-proposition query reasoner context number response 
                            (if (eq effort :wm-only) :wm-only :lookup-only)))
          (t ;; cspec being a constant means that we must look both within the context
           ;; but also at known ISA's to see if they are subsets of cspec
           (let ((local-results 
                  (ask-proposition 
                   (sublis (list (cons (third content) '?collection)) query)
                   reasoner context :all (make-isa espec '?collection)
                   (if (eq effort :wm-only) :wm-only :lookup-only)))
                 (real-results nil))
             ;; Unfortunately, there can be a lot of these -- in one of the COA cases, there were 
             ;; a couple of hundred!  Worth doing some pre-sorting, so we only ask once per object.
             (let ((table nil))
               (dolist (result local-results)
                 (let ((entry (assoc (second result) table :test 'equal)))
                   (unless entry
                     (push (setq entry (cons (second result) nil)) table))
                   (push (third result) (cdr entry))))
               (dolist (entry table)
                 (let ((entity (car entry))
                       (known-types (cdr entry)))
                   (cond ((member cspec known-types :test 'equal) ;; Nailed it
                          (push (make-contextualized-assertion
                                 (make-isa entity cspec) case predicate)
                                real-results))
                         (t ;; Might get it via inheritance
                          (dolist (col known-types)
                            ;; Check each in turn, to get dependencies right
                            (cond ((spec-of? col cspec) ;; Got it
                                   (let ((kb-genls-form
                                          (justify-kb-result-if-needed 
                                           (make-genls col cspec) reasoner))
                                         (real-result
                                          (make-contextualized-assertion
                                           (make-isa entity cspec) case predicate)))
                                     (justify-result real-result (list kb-genls-form
                                                                       (make-contextualized-assertion
                                                                        (make-isa entity col)
                                                                        case predicate))
                                                     :contextualized-isa-genls-inheritance)
                                     (push real-result real-results))
                                   (return)))))))))
               (case response  
                 (:bindings
                  (let ((result-pattern (make-contextualized-assertion 
                                         (make-isa espec cspec) case predicate)))
                    (setq real-results (mapcar #'(lambda (result)
                                                   (ltre::unify result-pattern result))
                                         real-results))))
                 (:pattern real-results)
                 (t ;; Some pattern -- need to substitute for the vars
                  (let ((result-pattern (make-contextualized-assertion
                                         (make-isa espec cspec) case predicate)))
                    (setq real-results (mapcar #'(lambda (result)
                                                   (sublis (ltre::unify result-pattern result)
                                                           response)) real-results)))))
               real-results)))))

(defun justify-result (consequence antecedents informant)
  (ltre::assert! `(:implies (:and ,@ antecedents) ,consequence) informant))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Metaknowledge queries
;;
;; Right now the only such predicates are
;; (unknownSentence ?sentence) which is true exactly when ?sentence
;; cannot be found in the WM or KB
;; (uninferredSentence ?sentence) which is true exactly when ?sentence
;; cannot be derived by current means.
;; (consistentThat ?sentence) which is true exactly when ?sentence is not
;; already known to be false

(defun metaknowledge-statement? (query)
  (and (listp query) (metaknowledge-predicate? (car query))))

(defun metaknowledge-predicate? (pred)
  (if (mixed-case?)
    (or (eq pred 'data::unknownSentence)
        (eq pred 'data::uninferredSentence)
        (eq pred 'data::consistentThat))
    (or (eq pred 'data::unknown-sentence)
        (eq pred 'data::uninferred-sentence)
        (eq pred 'data::consistent-that)))) 

;;; We're going to be very cautious in backchaining!
(defmethod predicate-ask-signatures ((pred (eql 'data::unknownSentence))
                                     (reasoner reasoner))
  '((:input-only)))

(defmethod predicate-ask-signatures ((pred (eql 'data::uninferredSentence))
                                     (reasoner reasoner))
  '((:input-only)))

(defmethod predicate-ask-signatures ((pred (eql 'data::consistentThat))
                                     (reasoner reasoner))
  '((:input-only)))

(defun ask-metaknowledge (pred arg reasoner context number response effort)
  (declare (ignore number effort))
  (unless (listp arg)
    (error "Malformed metaknowledge query: ~A, ~A." pred arg))
  (ecase pred
    ((data::unknownSentence data::unknown-sentence)
     (cond ((or (ltre::fetch arg (ltre reasoner))
                (retrieve arg :kb (kb reasoner)))
            nil)
           (t (case response
                (:bindings (list nil))
                (:pattern (list (list pred arg)))
                (t (list response))))))
    ((data::uninferredSentence data::uninferred-sentence)
     (let ((answer (ask arg reasoner context :exhaustive :pattern :every)))
       ;; Exhaustive in case someone does this with a conjunctive query.
       ;; Otherwise a single response would be enough.
       (cond (answer nil)
             (t (case response
                  (:bindings (list nil))
                  (:pattern (list (list pred arg)))
                  (t (list response)))))))
    ((data::consistentThat data::consistent-that)
     (let ((answer (ask arg reasoner context :exhaustive :bindings :every)))
       ;; Exhaustive in case someone does this with a conjunctive query.
       ;; Otherwise a single response would be enough.
       (cond (answer ;; we have it, so you bet it's consistent
              (case response
                (:bindings answer)
                (:pattern (mapcar #'(lambda (alist)
                                      (cons pred (sublis alist arg)))
                            answer))
                (t (mapcar #'(lambda (alist)
                               (sublis alist response))
                     answer))))
             ((ltre::false? arg (ltre reasoner)) nil)
             (t (case response
                  (:bindings (list nil))
                  (:pattern (list (list pred arg)))
                  (t (list response)))))))))

;;;;;;;;;;;;;;
;; Interface to sources

(defun ask-sources (query reasoner context number response effort)
  ;; ***** Ignoring number and effort parameters for the time being.
  ;; ***** Pass everything in so that source handler can deal with it
  ;; Sources are the FIRE means of implementing what in CYC are HL modules
  ;; Important: It is assumed that sources justify their results in the WM LTRE!
  (let ((results nil))
    (dolist (ask-handler (gather-query-ask-handlers query reasoner) results)
      (multiple-value-bind (source query-args)
          (query-ask-arglist query ask-handler)
        (setq results (nunion results 
                              (apply (handler ask-handler)
                                     (nconc (list source context number response
                                                  effort query)
                                            query-args))
                              :test 'equal))))))

;;;;;;;;;;;
;; Tell

;;; Tell is a method because we want to be able to extend it via
;;; methods contributed by particular sources. 

(defmethod tell ((fact list) (reasoner reasoner) (reason t) (context t))
  (mp:with-process-lock ((lock reasoner))
    (ltre::assume! fact reason (ltre reasoner)) ;; install
    (tell-appropriate-sources fact reason context reasoner)))

(defmethod untell ((fact list) (reasoner reasoner) (reason t) (context t))
  (mp:with-process-lock ((lock reasoner))
    (ltre::retract! fact reason (ltre reasoner)) ;; install
    (tell-appropriate-sources fact reason context reasoner)))

(defmethod tell-all ((facts t) (reasoner t) (reason t) (context t)) nil)
(defmethod untell-all ((facts t) (reasoner t) (reason t) (context t)) nil)

(defmethod tell-all ((facts list) (reasoner reasoner) (reason t) (context t))
  (dolist (fact facts)
    (tell fact reasoner reason context)))

(defmethod untell-all ((facts list) (reasoner reasoner) (reason t) (context t))
  (dolist (fact facts)
    (untell fact reasoner reason context)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Debugging hooks

(defun cl-user::trace-ask ()
  (trace ask
         ask-sources
         ask-proposition
         ask-contextualized
         ask-kb
         ask-lisp-test
         ask-structural-statement
         ask-metaknowledge
         ask-for-evaluation
         ask-contextualized-isa
         ltre::wm-retrieve))

(defun cl-user::untrace-ask ()
  (untrace ask
           ask-sources
           ask-proposition
           ask-contextualized
           ask-kb
           ask-lisp-test
           ask-structural-statement
           ask-metaknowledge
           ask-for-evaluation
           ask-contextualized-isa
           ltre::wm-retrieve))
         


;;;; ---------------------------------------------------------------------------
;;; END OF CODE