;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: scache-update.lsp
;;;;    System: 
;;;;    Author: Ken Forbus
;;;;   Created: December 18, 2003 09:53:45
;;;;   Purpose: Update methods for structural cache
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Monday, May 31, 2004 at 20:11:57 by Kenneth Forbus
;;;; ---------------------------------------------------------------------------

(in-package :fire)

;;;; Updating the structural cache
;;
;; While structural assertion changes are relatively rare, they do occur,
;; and we want the structural cache to automatically reflect them.
;;
;; There are two operations that we must worry about: kb-add and kb-delete.
;; The methods that will be called for these are:
;;       sc-update-add and sc-update-delete
;; These dispatch on the type of the functor.
;;
;; Also, this is a good place to update context vectors, since we have to look
;; at every statement coming in anyway to see what its structural implications
;; are.  The context vector updates will be implemented later.


(defmacro warn-offline (return-point format-string &rest format-args)
  `(block foo (format t "~%")
     (format t ,format-string ,@ format-args)
     (return-from ,return-point (values nil))))

;;; Error checking

(defmethod sc-update-add ((predicate t) (arguments t) (kb t))
  (warn-offline sc-update-add
                "Bad arguments to sc-update-add: ~A, ~A, ~A."
                predicate arguments kb))

(defmethod sc-update-delete ((predicate t) (arguments t) (kb t))
  (warn-offline sc-update-delete
                "Bad arguments to sc-update-delete: ~A, ~A, ~A."
    predicate arguments kb))

;;; no-op case (i.e., the default)
;; These should call context vector updater when we get to that.

(defmethod sc-update-add ((predicate t) (arguments list) (kb knowledge-base))
  nil) 

(defmethod sc-update-delete ((predicate t) (arguments list) (kb knowledge-base))
  nil)

(defun sc-really-n-ary? (details) 
  (and (sc-n-ary? details)
       (not (eq (sc-n-ary? details) :unknown))))

;;; (isa <entity> <collection>)

(defmethod sc-update-add ((predicate (eql 'data::isa)) (arguments list) (kb knowledge-base))

  (let ((entity (find-or-make-sc-entry (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (pushnew col (sc-isas entity))
    ;; We don't index all of the instances because that takes a lot of storage,
    ;; but we will include a counter so that we can use heuristics in controlling
    ;; search.
    (incf (sc-n-instances (sc-details col)))
    (sc-update-add-specialized-isas (cadr arguments) entity kb)))


(defmethod sc-update-add-specialized-isas ((collection t) (entry t) (kb t)) nil)

(defmethod sc-update-add-specialized-isas ((collection (eql 'data::Collection))
                                           (entry sc-entry)
                                           (kb knowledge-base))
  (cond ((sc-collection? entry) nil)
        ((sc-predicate? entry)
         (warn-offline sc-update-add-specialized-isas
                       "~A can't be a collection in ~A: ~A." 
                       (sc-item entry) kb entry))
        (t (setf (sc-details entry) (make-instance 'sc-collection-details
                                       :sc-entry entry))
           (setf (sc-type entry) :collection)
           entry)))

(defmethod sc-update-add-specialized-isas ((collection (eql 'data::Predicate))
                                           (entry sc-entry)
                                           (kb knowledge-base))
  (cond ((sc-relation? entry) nil)
        ((or (sc-collection? entry)
             (sc-function? entry)
             (sc-logical? entry))
         (warn-offline sc-update-add-specialized-isas
                       "~A can't be a relation in ~A: ~A." 
           (sc-item entry) kb entry))
        ((sc-predicate? entry)
         (coerce-predicate-details entry (sc-details entry) 'sc-relation-details))
        (t (setf (sc-details entry) (make-instance 'sc-relation-details
                                       :sc-entry entry))
           (setf (sc-type entry) :relation)
           entry)))

(defmethod sc-update-add-specialized-isas ((collection (eql 'data::CommutativeRelation))
                                           (entry sc-entry)
                                           (kb knowledge-base))
  (if (sc-predicate? entry)
    (setf (sc-commutative? (sc-details entry)) t)))

(defmethod sc-update-delete-specialized-isas ((collection (eql 'data::CommutativeRelation))
                                              (entry sc-entry)
                                              (kb knowledge-base))
  (if (sc-predicate? entry)
    (setf (sc-commutative? (sc-details entry)) nil)))

(defmethod sc-update-add-specialized-isas ((collection (eql 'data::Function-Denotational))
                                           (entry sc-entry)
                                           (kb knowledge-base))
  (cond ((sc-function? entry) nil)
        ((or (sc-collection? entry)
             (sc-relation? entry)
             (sc-logical? entry))
         (warn-offline sc-update-add-specialized-isas
                       "~A can't be a function in ~A: ~A." 
                       (sc-item entry) kb entry))
        ((sc-predicate? entry)
         (coerce-predicate-details entry (sc-details entry) 'sc-function-details))
        (t (setf (sc-details entry) (make-instance 'sc-function-details
                                       :sc-entry entry))
           (setf (sc-type entry) :function)
           entry)))

(defmethod sc-update-add-specialized-isas ((collection (eql 'data::LogicalConnective))
                                           (entry sc-entry)
                                           (kb knowledge-base))
  (cond ((sc-logical? entry) nil)
        ((or (sc-collection? entry)
             (sc-relation? entry)
             (sc-function? entry))
         (warn-offline sc-update-add-specialized-isas
                       "~A can't be a logical connective in ~A: ~A"
                       (sc-item entry) kb entry))
        ((sc-predicate? entry)
         (coerce-predicate-details entry (sc-details entry) 'sc-logical-details))
        (t (setf (sc-details entry) (make-instance 'sc-logical-details
                                      :sc-entry entry))
           (setf (sc-type entry) :logical)
           entry)))

(defmethod sc-update-add-specialized-isas ((collection (eql 'data::VariableArityRelation))
                                           (entry sc-entry)
                                           (kb knowledge-base))
  ;; Coerce if necessary
  (let* ((predicate (find-or-make-sc-predicate (sc-item entry) kb))
         (details (find-or-make-predicate-details predicate)))
    (cond ((integerp (sc-arity details))
           (warn-offline sc-update-add-specialized-isas
                         "Arity of ~A already ~D, can't be n-ary in ~A. (~A)"
                         (sc-item entry) (sc-arity details) kb entry))
          (t (setf (sc-n-ary? details) t)))))

(defmethod sc-update-add-specialized-isas ((collection (eql 'data::VariableArityFunction))
                                           (entry sc-entry)
                                           (kb knowledge-base))
  ;; Coerce if necessary
  (let* ((predicate (find-or-make-sc-predicate (sc-item entry) kb))
         (details (find-or-make-predicate-details predicate)))
    (cond ((integerp (sc-arity details))
           (warn-offline sc-update-add-specialized-isas
                         "Arity of ~A already ~D, can't be n-ary in ~A. (~A)"
                         (sc-item entry) (sc-arity details) kb entry))
          (t (setf (sc-n-ary? details) t)))))

(defmethod sc-update-add-specialized-isas ((collection (eql 'data::Case))
                                           (entry sc-entry)
                                           (kb knowledge-base))
  ;; Make it a microtheory if not already
  (let ((mt (find-or-make-sc-microtheory (sc-item entry) kb)))
    (cond ((sc-microtheory? mt)) ;; Coercion worked
          (t (warn-offline sc-update-add-specialized-isas
                           "Could not coerce ~A into microtheory: ~A."
                           (sc-item entry) entry)))))
           
(defmethod sc-update-add-specialized-isas ((collection (eql 'data::Microtheory))
                                           (entry sc-entry)
                                           (kb knowledge-base))
  ;; Make it a microtheory if not already
  (let ((mt (find-or-make-sc-microtheory (sc-item entry) kb)))
    (cond ((sc-microtheory? mt)) ;; Coercion worked
          (t (warn-offline sc-update-add-specialized-isas
                           "Could not coerce ~A into microtheory: ~A."
                           (sc-item entry) entry)))))

;;; ***** Interesting question: When can we delete entities from the structural cache?
;;; ***** Declaring that something isn't an mt or case, but a predicate instead, would
;;; ***** potentially require cleaning out the implications of this (e.g., nuking all
;;; ***** ist-Information statements involving it).  Should we do this incrementally?

(defmethod sc-update-delete ((predicate (eql 'data::isa)) (arguments list) (kb knowledge-base))
  (let ((entry (find-sc-entry (car arguments) kb))
        (col (find-sc-collection (cadr arguments) kb)))
    (when (and (sc-entry? entry)
               (sc-collection? col))
      (setf (sc-isas entry) (delete col (sc-isas entry)))
      (decf (sc-n-instances (sc-details col)))
      (sc-update-delete-specialized-isas (cadr arguments) entry kb))))

(defmethod sc-update-delete-specialized-isas ((collection t) (entry t) (knowledge-base t)) nil)

;; Interesting implication: When col here is Collection, this means that entry is a collection also.
;; Similarly for Relation or Function-Denotational.  And for their specs.
;; So what if we find out first that foo is a Mumble-Function, and later discover that Mumble-Function
;; has as a genl Function-Denotational?  We should go through all of the instances of Mumble-Function
;; and coerce them into functions.  That's expensive, unless one stores instances.  Won't handle this for
;; now, since we need to think about it more.
 
;;; (arity <predicate> <number>)

(defmethod sc-update-add ((predicate (eql 'data::arity))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (arity (cadr arguments)))
    (unless (and (integerp arity)
                 (> arity -1))
      (warn-offline sc-update-add 
                    "Arity must be non-negative integer: ~A, for ~A."
        (third arguments) (cadr arguments)))
    (when (sc-predicate? predicate)
      (let ((details (sc-details predicate)))
        (when (sc-really-n-ary? details)
          (warn-offline sc-update-add
                        "~A can't be arity ~D, already n-ary: ~A."
            (sc-item predicate) arity predicate))
        (when (and (integerp (sc-arity details))
                   (not (= arity (sc-arity details))))
          (warn-offline sc-update-add 
                        "Inconsistent arity information for ~A: ~D versus ~D in ~A (~A)."
            (car arguments) arity (sc-arity details) kb predicate))
        (setf (sc-arity (sc-details predicate)) arity)))))

;; Should do error checking about 

(defmethod sc-update-delete ((predicate (eql 'data::arity))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-sc-predicate (car arguments) kb)))
    (when (sc-predicate? predicate)
      (setf (sc-arity (sc-details predicate)) :unknown)
      (unless (sc-n-ary? (sc-details predicate))
        (setf (sc-n-ary? (sc-details predicate)) :unknown)))))

;;; (arityMax <predicate> <number>)
;;; We just call these n-ary for now.
(defmethod sc-update-add ((predicate (eql 'data::arityMax))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb)))
    (when (sc-predicate? predicate)
      (let ((details (sc-details predicate)))
        (cond ((integerp (sc-arity details))
               (warn-offline sc-update-add
                             "Inconsistent arityMax info for ~A: ~D versus ~D."
                             (car arguments) (cadr arguments) (sc-arity details)))
              (t (setf (sc-n-ary? details) t)))))))

(defmethod sc-update-delete ((predicate (eql 'data::arityMax))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-sc-predicate (car arguments) kb)))
    (when (sc-predicate? predicate)
      (unless (integerp (sc-arity (sc-details predicate)))
        (setf (sc-n-ary? (sc-details predicate)) :unknown)))))

;;; (arityMin <predicate> <number>)
;;; We just call these n-ary for now.
(defmethod sc-update-add ((predicate (eql 'data::arityMin))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb)))
    (when (sc-predicate? predicate)
      (let ((details (sc-details predicate)))
        (cond ((integerp (sc-arity details))
               (warn-offline sc-update-add
                             "Inconsistent arityMin info for ~A: ~D versus ~D."
                             (car arguments) (cadr arguments) (sc-arity details)))
              (t (setf (sc-n-ary? details) t)))))))

(defmethod sc-update-delete ((predicate (eql 'data::arityMin))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-sc-predicate (car arguments) kb)))
    (when (sc-predicate? predicate)
      (unless (integerp (sc-arity (sc-details predicate)))
        (setf (sc-n-ary? (sc-details predicate)) :unknown)))))


;;; (argIsa <pred> <n> <col>) indicates that the <n>th argument to <pred>
;;; must be (isa <nth arg> <col>)

(defmethod sc-update-add ((predicate (eql 'data::argIsa))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (n (cadr arguments))
        (col (find-or-make-sc-collection (third arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col)
                 (integerp n)
                 (> n -1))
      ;; N.B. Much to my surprise, 0 is legit, and is used to mean
      ;; all arguments must be a member of the given collection.
      ;; Kind of a kludge IMHO, since arg 0 elsewhere means the functor.
      ;; But as of 12/19/03, there are 497 of them
      ;; in qrg-general.  Most but not all of them are SubLRealNumber
      ;; for the collection, but ExistingObjectType, FirstOrderCollection,
      ;; and a few others make guest appearances.  We'll store it for now
      ;; as zero, and figure out how to apply it later.
      (warn-offline sc-update-add
                    "Invalid ArgIsa constraint on ~A: ~A, ~A.  (~A in ~A)."
        (car arguments)
        (cadr arguments)
        (third arguments)
                    predicate kb))
    ;;; There doesn't seem to be anything in Cyc that precludes this
;;;    (when (or (sc-really-n-ary? (sc-details predicate))
;;;              (and (null (sc-n-ary? (sc-details predicate)))
;;;                   (integerp (sc-arity (sc-details predicate)))
;;;                   (> n (sc-arity (sc-details predicate)))))
;;;      (warn-offline sc-update-add
;;;                    "Can't use argIsa on n-ary predicate: ~A, ~A, ~A.  (~A in ~A)."
;;;        (car arguments) (cadr arguments) (third arguments) predicate kb))
    (add-argisa-constraint predicate n col)))

(defmethod sc-update-delete ((predicate (eql 'data::argIsa))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (n (cadr arguments))
        (col (find-or-make-sc-collection (third arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col)
                 (integerp n)
                 (> n 0))
      (warn-offline sc-update-delete
                    "Invalid ArgIsa constraint deletion on ~A: ~A, ~A.  (~A in ~A)."
        (car arguments)
        (cadr arguments)
        (third arguments)
                    predicate kb))
        ;;; There doesn't seem to be anything in Cyc that precludes this
    
;;;    (when (or (sc-really-n-ary? (sc-details predicate))
;;;              (and (null (sc-n-ary? (sc-details predicate)))
;;;                   (integerp (sc-arity (sc-details predicate)))
;;;                   (> n (sc-arity (sc-details predicate)))))
;;;      (warn-offline sc-update-delete
;;;                    "Can't use argIsa on n-ary predicate: ~A, ~A, ~A.  (~A in ~A)."
;;;        (car arguments) (cadr arguments) (third arguments) predicate kb))
    (remove-argisa-constraint predicate n col)))

;; Now arguments 1-4 for isa's, formats, etc.

(defmethod sc-update-add ((predicate (eql 'data::arg1Isa))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-add "Invalid Arg1Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 1 (sc-arity details)))
        (warn-offline sc-update-add "Invalid Arg1Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
      ;;; There doesn't seem to be anything in Cyc that precludes this
      ;;;      (when (sc-really-n-ary? details)
      ;;;        (warn-offline sc-update-add "Invalid Arg1Isa: ~A is n-ary in ~A. (~A, ~A)."
      ;;;          (car arguments) kb predicate col))
      (add-argisa-constraint predicate 1 col))))

(defmethod sc-update-delete ((predicate (eql 'data::arg1Isa))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-delete "Invalid Arg1Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 1 (sc-arity details)))
        (warn-offline sc-update-delete
                      "Invalid Arg1Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-delete
;;;                      "Invalid Arg1Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;                      (car arguments) kb predicate col))
      (remove-argisa-constraint predicate 1 col))))

;;; Arg2Isa

(defmethod sc-update-add ((predicate (eql 'data::arg2Isa))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-add "Invalid Arg2Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 2 (sc-arity details)))
        (warn-offline sc-update-add "Invalid Arg2Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-add "Invalid Arg2Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (add-argisa-constraint predicate 2 col))))

(defmethod sc-update-delete ((predicate (eql 'data::arg2Isa))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-delete "Invalid Arg2Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 2 (sc-arity details)))
        (warn-offline sc-update-delete "Invalid Arg2Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-delete "Invalid Arg2Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (remove-argisa-constraint predicate 2 col))))
          
;;; Arg3Isa

(defmethod sc-update-add ((predicate (eql 'data::arg3Isa))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-add "Invalid Arg3Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 3 (sc-arity details)))
        (warn-offline sc-update-add "Invalid Arg3Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-add "Invalid Arg3Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (add-argisa-constraint predicate 3 col))))

(defmethod sc-update-delete ((predicate (eql 'data::arg3Isa))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-delete "Invalid Arg3Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 3 (sc-arity details)))
        (warn-offline sc-update-delete "Invalid Arg3Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
      ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-delete "Invalid Arg3Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (remove-argisa-constraint predicate 3 col))))

;;; Arg4Isa

(defmethod sc-update-add ((predicate (eql 'data::arg4Isa))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-add "Invalid Arg4Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 4 (sc-arity details)))
        (warn-offline sc-update-add "Invalid Arg4Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-add "Invalid Arg4Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (add-argisa-constraint predicate 4 col))))

(defmethod sc-update-delete ((predicate (eql 'data::arg4Isa))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-delete "Invalid Arg4Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 4 (sc-arity details)))
        (warn-offline sc-update-delete "Invalid Arg4Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-delete "Invalid Arg4Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (remove-argisa-constraint predicate 4 col))))
    
;;; Arg5Isa

(defmethod sc-update-add ((predicate (eql 'data::arg5Isa))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-add "Invalid Arg5Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 5 (sc-arity details)))
        (warn-offline sc-update-add "Invalid Arg5Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
      ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-add "Invalid Arg5Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (add-argisa-constraint predicate 5 col))))

(defmethod sc-update-delete ((predicate (eql 'data::arg5Isa))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-delete "Invalid Arg5Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 5 (sc-arity details)))
        (warn-offline sc-update-delete "Invalid Arg5Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-delete "Invalid Arg5Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (remove-argisa-constraint predicate 5 col))))

;;; Arg6Isa

(defmethod sc-update-add ((predicate (eql 'data::arg6Isa))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-add "Invalid Arg6Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 6 (sc-arity details)))
        (warn-offline sc-update-add "Invalid Arg6Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-add "Invalid Arg6Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (add-argisa-constraint predicate 6 col))))

(defmethod sc-update-delete ((predicate (eql 'data::arg6Isa))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-delete "Invalid Arg6Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 6 (sc-arity details)))
        (warn-offline sc-update-delete "Invalid Arg6Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-delete "Invalid Arg6Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (remove-argisa-constraint predicate 6 col))))

;;; Arg7Isa


(defmethod sc-update-add ((predicate (eql 'data::arg7Isa))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-add "Invalid Arg7Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 7 (sc-arity details)))
        (warn-offline sc-update-add "Invalid Arg7Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-add "Invalid Arg7Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) kb predicate col))
      (add-argisa-constraint predicate 7 col))))

(defmethod sc-update-delete ((predicate (eql 'data::arg7Isa))
                             (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (col (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? col))
      (warn-offline sc-update-delete "Invalid Arg7Isa: ~A for ~A, in ~A (~A)." 
        (car arguments) (cadr arguments) kb predicate))
    (let ((details (sc-details predicate)))
      (when (and (integerp (sc-arity details))
                 (> 7 (sc-arity details)))
        (warn-offline sc-update-delete "Invalid Arg7Isa: ~A has arity ~D in ~A.  (~A, ~A)."
                      (car arguments) (sc-arity details) kb predicate col))
          ;;; There doesn't seem to be anything in Cyc that precludes this
;;;      (when (sc-really-n-ary? details)
;;;        (warn-offline sc-update-delete "Invalid Arg7Isa: ~A is n-ary in ~A. (~A, ~A)."
;;;          (car arguments) (name kb) predicate col))
      (remove-argisa-constraint predicate 7 col))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Result information

(defmethod sc-update-add ((predicate (eql 'data::resultIsa))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (result-type (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? result-type))
      (warn-offline sc-update-add "Invalid resultIsa: ~A, ~A." (car arguments) (cadr arguments)))
    (let ((details (sc-details predicate)))
      (cond ((eq (sc-result-isa details) :unknown)
             (setf (sc-result-isa details) (list result-type)))
            (t (pushnew result-type (sc-result-isa details)))))))


(defmethod sc-update-delete ((predicate (eql 'data::resultIsa))
                          (arguments list) (kb knowledge-base))
  (let ((predicate (find-or-make-sc-predicate (car arguments) kb))
        (result-type (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-predicate? predicate)
                 (sc-collection? result-type))
      (warn-offline sc-update-delete "Invalid resultIsa: ~A, ~A." (car arguments) (cadr arguments)))
    (let ((details (sc-details predicate)))
      (cond ((eq (sc-result-isa details) :unknown)) ;; Do nothing, already gone
            ((member result-type (sc-result-isa details))
             (setf (sc-result-isa details) (delete result-type (sc-result-isa details)))
             (if (null (sc-result-isa details)) (setf (sc-result-isa details) :unknown)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; lispProcedureImplementing information

(defmethod sc-update-add ((predicate (eql 'data::lispProcedureImplementing))
                          (arguments list) (kb knowledge-base))
  (let ((function (find-or-make-sc-function (car arguments) kb))
        (procedure (cadr arguments)))
    (unless (and (sc-function? function)
                 (not (null procedure))
                 (symbolp procedure)) ;; Very restrictive but probably right
      (warn-offline sc-update-add "Invalid lispProcedureImplementing: ~A, ~A."
                    (car arguments) procedure))
    (let ((details (sc-details function)))
      (setf (sc-lisp-handler details) procedure))))

(defmethod sc-update-delete ((predicate (eql 'data::lispProcedureImplementing))
                             (arguments list) (kb knowledge-base))
  (let ((function (find-or-make-sc-function (car arguments) kb))
        (procedure (cadr arguments)))
    (unless (and (sc-function? function)
                 (not (null procedure))
                 (symbolp procedure)) ;; Very restrictive but probably right
      (warn-offline sc-update-delete "Invalid lispProcedureImplementing: ~A, ~A."
                    (car arguments) procedure))
    (let ((details (sc-details function)))         
      (when (eql (sc-lisp-handler details) procedure)
        (setf (sc-lisp-handler details) nil)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; genls & genlPreds

(defmethod sc-update-add ((predicate (eql 'data::genls))
                          (arguments list) (kb knowledge-base))
  (let ((sub (find-or-make-sc-collection (car arguments) kb))
        (super (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-collection? sub)
                 (sc-collection? super))
      (warn-offline sc-update-add "Invalid genls: ~A (~A), ~A (~A)."
        (car arguments) sub (cadr arguments) super))
    (pushnew sub (sc-specs (sc-details super)))
    (pushnew super (sc-genls (sc-details sub)))))

(defmethod sc-update-delete ((predicate (eql 'data::genls))
                             (arguments list) (kb knowledge-base))
  (let ((sub (find-or-make-sc-collection (car arguments) kb))
        (super (find-or-make-sc-collection (cadr arguments) kb)))
    (unless (and (sc-collection? sub)
                 (sc-collection? super))
      (warn-offline sc-update-delete "Invalid genls: ~A (~A), ~A (~A)."
        (car arguments) sub (cadr arguments) super))
    (setf (sc-specs (sc-details super))
      (delete sub (sc-specs (sc-details super))))
    (setf (sc-genls (sc-details sub))
      (delete super (sc-genls (sc-details sub))))))
             
(defmethod sc-update-add ((predicate (eql 'data::genlPreds)) 
                          (arguments list) (kb knowledge-base))
  (let ((sub (find-or-make-sc-predicate (car arguments) kb))
        (super (find-or-make-sc-predicate (cadr arguments) kb)))
    (unless (and (sc-predicate? sub)
                 (sc-predicate? super)
                 (eq (sc-type sub) (sc-type super)))
      (warn-offline sc-update-add "Invalid genlPreds: ~A (~A), ~A (~A)."
        (car arguments) sub (cadr arguments) super))
    (pushnew sub (sc-specpreds (sc-details super)))
    (pushnew super (sc-genlpreds (sc-details sub)))))

(defmethod sc-update-delete ((predicate (eql 'data::genlPreds))
                             (arguments list) (kb knowledge-base))
  (let ((sub (find-or-make-sc-predicate (car arguments) kb))
        (super (find-or-make-sc-predicate (cadr arguments) kb)))
    (unless (and (sc-predicate? sub)
                 (sc-predicate? super)
                 (eq (sc-type sub) (sc-type super)))
      (warn-offline sc-update-delete "Invalid genlPreds: ~A (~A), ~A (~A)."
        (car arguments) sub (cadr arguments) super))
    (setf (sc-specpreds (sc-details super))
      (delete sub (sc-specpreds (sc-details super))))
    (setf (sc-genlpreds (sc-details sub))
      (delete super (sc-genlpreds (sc-details sub))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; disjointWith

(defmethod sc-update-add ((predicate (eql 'data::disjointWith))
                          (arguments list)
                          (kb knowledge-base))
  (let ((c1 (find-sc-collection (car arguments) kb))
        (c2 (find-sc-collection (cadr arguments) kb)))
    ;; We require the collections to exist.  Otherwise, something
    ;; is wrong, and we won't corrupt the cache with this bogosity.
    (when (and (sc-collection? c1)
               (sc-collection? c2))
      (let ((d1 (sc-details c1))
            (d2 (sc-details c2)))
        (pushnew c2 (sc-disjoints d1))
        (pushnew c1 (sc-disjoints d2))))))

(defmethod sc-update-delete ((predicate (eql 'data::disjointWith))
                             (arguments list)
                             (kb knowledge-base))
  (let ((c1 (find-sc-collection (car arguments) kb))
        (c2 (find-sc-collection (cadr arguments) kb)))
    ;; We require the collections to exist.  Otherwise, something
    ;; is wrong, and we won't corrupt the cache with this bogosity.
    (when (and (sc-collection? c1)
               (sc-collection? c2))
      (let ((d1 (sc-details c1))
            (d2 (sc-details c2)))
        (setf (sc-disjoints d1) (delete c2 (sc-disjoints d1)))
        (setf (sc-disjoints d2) (delete c1 (sc-disjoints d2)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Microtheories

;;; genlMt

(defmethod sc-update-add ((predicate (eql 'data::genlMt))
                          (arguments list)
                          (kb knowledge-base))
  (let ((sub-mt (find-or-make-sc-microtheory (car arguments) kb))
        (super-mt (find-or-make-sc-microtheory (cadr arguments) kb)))
    (when (and (sc-microtheory? sub-mt)
               (sc-microtheory? super-mt)) ;; cautious
      (let ((details-sub-mt (sc-details sub-mt))
            (details-super-mt (sc-details super-mt)))
      (pushnew super-mt (sc-genlmts details-sub-mt))
      (pushnew sub-mt (sc-specmts details-super-mt))))))

(defmethod sc-update-delete ((predicate (eql 'data::genlMt))
                          (arguments list)
                          (kb knowledge-base))
  (let ((sub-mt (find-or-make-sc-microtheory (car arguments) kb))
        (super-mt (find-or-make-sc-microtheory (cadr arguments) kb)))
    (when (and (sc-microtheory? sub-mt)
               (sc-microtheory? super-mt)) ;; cautious
      (let ((details-sub-mt (sc-details sub-mt))
            (details-super-mt (sc-details super-mt)))
        (setf (sc-genlmts details-sub-mt) 
          (delete super-mt (sc-genlmts details-sub-mt)))
        (setf (sc-specmts details-super-mt)
          (delete sub-mt (sc-specmts details-super-mt)))))))

;;; ist-Information

(defmethod sc-update-add ((predicate (eql 'data::ist-Information))
                          (arguments list)
                          (kb knowledge-base))
  (let ((mt (find-or-make-sc-microtheory (cadr arguments) kb)))
    (when (sc-microtheory? mt)
      (let ((details (sc-details mt)))
        (incf (sc-n-facts details)))))) 

(defmethod sc-update-delete ((predicate (eql 'data::ist-Information))
                             (arguments list)
                             (kb knowledge-base))
  (let ((mt (find-or-make-sc-microtheory (cadr arguments) kb)))
    (when (sc-microtheory? mt)
      (let ((details (sc-details mt)))
        (decf (sc-n-facts details))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; chainerContains

;; Need to update the time tag for chainer updates

(defmethod sc-update-add ((predicate (eql 'data::chainerContains))
                          (arguments list)
                          (kb knowledge-base))
  (update-chainer-updated-timestamp (car arguments)))

(defmethod sc-update-delete ((predicate (eql 'data::chainerContains))
                             (arguments list)
                             (kb knowledge-base))
  (update-chainer-updated-timestamp (car arguments)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; End of Code