;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: reify-sme.lsp
;;;;    System: FIRE
;;;;   Version: 1.0
;;;;    Author: Ken Forbus
;;;;   Created: December 28, 2000 18:21:17
;;;;   Purpose: Reification of SME results
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Sunday, February 8, 2004 at 13:16:34 by Kenneth Forbus
;;;; ---------------------------------------------------------------------------

(in-package :fire)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Checking syntax of terms

(defun matcher-fn? (form &optional (kb *kb*))
  (car-is form (if (mixed-case? kb) 
                 'data::MatcherFn
                 'data::matcher-fn)))

(defun mapping-fn? (form &optional (kb *kb*))
  (car-is form (if (mixed-case? kb) 
                 'data::MappingFn
                 'data::mapping-fn)))

(defun mh-fn? (form &optional (kb *kb*))
  (car-is form (if (mixed-case? kb) 
                 'data::MhFn
                 'data::mh-fn)))

(defun ci-fn? (form &optional (kb *kb*))
  (car-is form (if (mixed-case? kb) 
                 'data::CiFn 
                 'data::ci-fn)))


(defun car-is (form constant)
  (cond ((null form) nil)
        ((not (listp form)) nil)
        ((equal (car form) constant) t)
        (t nil)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Retrieving SME datastructures corresponding to FIRE terms

(defgeneric sme-referent (form reasoner-or-analogy-source)
  (:documentation "Given an expression representing some kind of SME-related
                   entity (such as (MatcherFn 25)), returns the actual SME
                   object that the form refers to.  Returns nil if none can
                   be found."))

(defmethod sme-referent (form source)
  ;; default method -- just returns nil
  (declare (ignore form source))
  nil)

(defmethod sme-referent (form (reasoner reasoner))
  (do ((sources (sources reasoner) (cdr sources))
       (result nil))
      ((or result (null sources)) result)
    (when (analogy-source? (car sources))
      (setq result (sme-referent form (car sources))))))

(defmethod sme-referent (form (analogy-source analogy-source))
  (with-kb (kb analogy-source)
    (cond ((matcher-fn? form)
           (lookup-sme (cadr form) analogy-source))
          ((mapping-fn? form)
           (lookup-mapping (cadr form) (third form) analogy-source))
          ((mh-fn? form)
           (lookup-mh (cadr form) (third form) analogy-source))
          ((ci-fn? form)
           (lookup-ci (cadr form) (third form) (fourth form) analogy-source))
          (t nil))))

(defun lookup-sme (id analogy-source)
  (find id (smes analogy-source) :key 'sme::id))

(defun lookup-mapping (mapping-id sme-id analogy-source)
  (let ((sme (lookup-sme sme-id analogy-source)))
    (when (typep sme 'sme::sme)
      (find mapping-id (sme::mappings sme) :key 'sme::id))))

(defun lookup-mh (mh-id sme-id analogy-source)
  (let ((sme (lookup-sme sme-id analogy-source)))
    (when (typep sme 'sme::sme)
      (find mh-id (sme::mhs sme) :key 'sme::id))))

(defun lookup-ci (ci-id mapping-id sme-id analogy-source)
  (let ((m (lookup-mapping mapping-id sme-id analogy-source)))
    (when (typep m 'sme::mapping)
      (find ci-id (sme::inferences m) :key 'sme::id))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Going the other way -- generating terms from SME internals

(defmethod generate-analogy-term ((thing t)) nil)

(defmethod generate-analogy-term ((thing sme::sme))
  (make-sme-reference thing))

(defmethod generate-analogy-term ((thing sme::mapping))
  (make-mapping-reference thing))

(defmethod generate-analogy-term ((thing sme::match-hypothesis))
  (make-mh-reference thing))

(defmethod generate-analogy-term ((thing sme::candidate-inference))
  (make-ci-reference thing))

(defmethod generate-analogy-term ((thing sme::description))
  (sme::name thing))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Reifying SME properties into the working memory
;;; 
;;; We do two things for efficiency:
;;; 1. Most reification of SME results into the FIRE WM happen
;;;    on demand, since matches can get quite large and only a
;;;    small subset of them tends to be interesting in most
;;;    reasoning tasks.
;;; 2. All SME results are now justified by at least one assumption.
;;;    The first assumption is that the given SME is relevant.
;;;    This is actually a piece of control knowledge, designed to
;;;    enable the FIRE-side reifications to be cleaned up if someone
;;;    cleans out the SME from the analogy source, or if an application
;;;    knows that it is no longer relevant.
;;;    This assumption takes the form
;;;    (relevantComparison <matcher> <timestamp>)
;;;    where <timestamp> = universal time at reification.
;;;    This assumption is used for all basic structural information
;;;    and other material that cannot change due to updates.
;;;    The second assumption handles the need for facts to change
;;;    as a match is extended, e.g., by extending the base or the
;;;    target, by adding new match constraints, etc.  
;;;    This assumption takes the form
;;;    (smeTimeclockValue <matcher> <timeclock value>)
;;;    [The value of sme::timeclock is roughly the number of
;;;      transactions involving the base or target.  See SME source
;;;      for details.]
;;;    Examples of information which can change include structural
;;;    evaluation scores of mappings, what correspondences are in
;;;    a mapping, and whether or not something is a candidate inference.

;;; ***** Probably need to reify isa's for analogy terms as they are used,
;;; ***** Or maybe just handle (isa <NAT> <collection>) specially, since we
;;; ***** can use the type information regarding the NAT to do a lot.
;;; ***** Although (MappingFn 1024 2) should be a mapping, if (MatcherFn 2)
;;; ***** only has 20 mappings, oops, it isn't.  So this probably does have to
;;; ***** be a more concrete test.

(defun reify-sme (sme analogy-source)
  (with-kb (kb analogy-source)
    (let* ((r (reasoner analogy-source))
           (relevant-sme-asn (find-or-make-sme-relevance-assumption sme))
           (sme-timeclock-asn (make-current-sme-timeclock-assumption sme)))
      (tell relevant-sme-asn r :analogy :all)
      (tell sme-timeclock-asn r :analogy :all))))

;; On when to use relevance-antecedents versus timeclock-antecedents:
;; Relevance antecedents are a subset of timeclock-antecedents, so that
;;  if something becomes moot, everything associated with it is wiped from
;;  the working memory.
;; Timeclock antecedents are needed when a result might change over time.
;; Old results will remain justified, since they could indeed still be true.
;; What we'll do is filter results for dynamic predicates, only picking
;; the latest value.  (Nice intuition, but implementing it will be a bit
;; tricky.)

(defun make-sme-timeclock-antecedents (thing)
  (let ((sme (if (sme::sme? thing) thing
                (if (sme::mapping? thing) (sme::sme thing)
                  (if (sme::candidate-inference? thing)
                    (sme::sme (sme::mapping thing))
                    (if (sme::mh? thing) (sme::sme thing)))))))
    (when (sme::sme? sme)
      (let ((timeclock-asn (make-current-sme-timeclock-assumption sme))
            (relevance-asn (find-or-make-sme-relevance-assumption sme)))
        (unless (ltre:true? timeclock-asn)
          (tell  timeclock-asn *reasoner* :sme-timeclock-measurement
                :all))
        (unless (ltre::true? relevance-asn) ;; Should be true
          (tell relevance-asn *reasoner* :sme-relevance-asn :all))
        (list timeclock-asn relevance-asn)))))

(defun make-sme-relevance-antecedents (thing)
  (let ((sme (if (sme::sme? thing) thing
               (if (sme::mapping? thing) (sme::sme thing)
                 (if (sme::candidate-inference? thing)
                   (sme::sme (sme::mapping thing))
                   (if (sme::mh? thing) (sme::sme thing)))))))
    (when (sme::sme? sme)
      (let ((relevance-asn (find-or-make-sme-relevance-assumption sme)))
        (unless (ltre::true? relevance-asn) ;; Should be true
          (tell relevance-asn *reasoner* :sme-relevance-asn :all))
        (list relevance-asn)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Reifying MAC/FAC results into the working memory
;;; 

(defun reify-macfac (probe library outputs analogy-source)
  ;; output = ( <score> <dgroup> <match>)
  (with-kb (kb analogy-source)
    (let ((r (reasoner analogy-source))
          (results nil))
      (dolist (triple outputs (nreverse results))
        (let ((reminding (make-reminding probe library 
                                         (sme::name (second triple))
                                         (make-sme-reference (third triple)))))
          (push reminding results)
          (tell reminding r :macfac :all)
          (reify-sme (third triple) analogy-source))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Reification support for dgroups

;; Descriptions (aka dgroups) have timeclocks, too.  These are used to
;; increment the SME's timeclock for those involved in matches.

(defun make-dgroup-timeclock-antecedents (dgroup)
  (let* ((current-asn (make-dgroup-timeclock-assumption
                       dgroup (sme::timeclock dgroup))))
    (unless (ltre::true? current-asn)
      (tell current-asn *reasoner* :dgroup-timeclock-measurement
            :all))
    (list current-asn)))

(defun compute-fire-entities-for-dgroup (dgroup)
  ;; SME's notion of entity is anything that isn't an expression or
  ;; a predicate being used as a predicate.  Thus higher-order mentions
  ;; of predicates are treated by entities as SME.  This is fine for most
  ;; purposes, but we probably want to disentagle for FIRE.
  ;; We leave out collections and relations, just keep constants.
  ;; N.B. After a bit of experimentation, it looks like there isn't any
  ;; value to running sme->fire-expression on the forms of entities.
  ;; This could be incorrect if there is something involving a hairy
  ;; Kappa or Lambda somewhere.
  (let ((fire-entities nil))
    (dolist (entity (sme::entities dgroup) fire-entities)
      (let* ((form (sme::lisp-form entity))
             (sc-entry (find-sc-entry form *kb*)))
        (if (or (and (null sc-entry) ;; Some constant not indexed by structural cache
                     (not (variable? form)))
                (sc-constant? sc-entry))
          (push form fire-entities))))))

(defun dgroup-mentions-fire-predicate? (predicate dgroup &key (kb *kb*))
  (let ((sc-entry (find-sc-entry predicate kb)))
    (when (sc-entry? sc-entry)
      (or (assoc sc-entry (sme::expressions dgroup)) ;; Exploit alist
          (find predicate (sme::entities dgroup)
                :key 'sme::lisp-form
                :test 'equal)))))

(defun compute-fire-predicates-for-dgroup (dgroup)
  (let ((predicates (mapcar #'(lambda (exp-entry)
                                (sc-item (car exp-entry))) 
                      (sme::expressions dgroup))))
    (dolist (entity (sme::entities dgroup) predicates)
      ;; Find higher-order usages
      (let ((entity-form (sme::lisp-form entity)))
        (if (predicate? entity-form)
          (pushnew entity-form predicates :test 'equal))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Other useful FIRE-level SME-hacking utilities

(defun sme-of (thing)
  (if (sme::sme? thing) thing
    (if (sme::mh? thing) (sme::sme thing)
      (if (sme::mapping? thing) (sme::sme thing)
        (if (sme::candidate-inference? thing) (sme::sme thing)
          (error "Not datastructure with SME backpointer: ~A." thing))))))


(defun compute-largest-mapping (mappings)
  (let ((candidate (car mappings)))
    (dolist (other (cdr mappings) candidate)
      (if (> (sme::score other)
             (sme::score candidate))
        (setq candidate other)))))

(defun translate-ci-content (ci)
  (sme->fire-expression
   (subst (if (mixed-case?) 
            'data::AnalogySkolemFn 'data::analogy-skolem-fn)
          :skolem (sme::lisp-form ci))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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