;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: scache-dumper.lsp
;;;;    System: FIRE
;;;;    Author: Ken Forbus
;;;;   Created: December 20, 2003 09:43:08
;;;;   Purpose: Dumping structure caches
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Thursday, April 22, 2004 at 17:50:34 by forbus
;;;; ---------------------------------------------------------------------------

(in-package :fire)

;;;; Dumping and loading structural caches.
;;
;; Interfaces are
;;   (dump-structural-cache &key (kb *kb*)) stores it under the resources directory
;;     of the KB.
;;   (load-structural-cache &key (kb *kb*)) loads this kb's structural cache.
;;
;;; Leo's binary dumper made implementing this straightforward.
;;; Most of the work is in extending the bd-write and bd-read methods to
;;; handle the datastructures in the structural cache.  
;;;
;;; As explained below, the existence of pointer cycles in the structural cache means
;;; that the loader has to be a bit fancier.  This also means that comparing two entries
;;; has to become a litlte more subtle, in that we have to know when to break the cycles
;;; at expression names.  

(defun dump-structural-cache (&key (kb *kb*))
  (let ((resource-path (kb-resource-path kb)))
    (with-kb kb
      (delete-structural-cache-files kb)
      (ensure-directories-exist resource-path)
      (bd-save (structural-cache kb) resource-path "structural-cache")
      (format t "~&Dumping of structural cache complete.")
      kb)))

(defun load-structural-cache (&key (kb *kb*))
  (format t "~&Loading structural cache....~%")
  (with-kb kb
    (trap-error (error
                  (format t "~&WARNING: error -- structural cache not loaded.")
                  nil)
      (let ((cache (bd-load (kb-resource-path *kb*) "structural-cache")))
        (format t "~&Done loading structural cache.~%")
        (cond ((structural-cache? cache) 
               (setf (structural-cache kb) cache)
               cache)
              (t 
               (error "Load failure: Not a structural cache: ~A." cache)))))))

(defun delete-structural-cache-files (kb)
  (let ((path (concatenate 'string (kb-resource-path kb) "structural-cache.*")))
    (dolist (fspec (directory path)) (delete-file fspec))))

;;; The cache itself

(defmethod bd-write ((thing structural-cache) sout &rest args
                     &key (context nil) &allow-other-keys)
  "BDumper method for storing structural cache."
  (bd-write-token bdt-structural-cache sout)
  (bd-write (table thing) sout :context context)
  (bd-write (updated? thing) sout :context context)
  (bd-write (id-counter thing) sout :context context))

(defmethod bd-read (sin (token (eql bdt-structural-cache))
                        &rest args
                        &key (context nil) &allow-other-keys)
  "BDumper method to loading a structural cache."
  (let ((cache (make-instance 'structural-cache :kb *kb*)))
    (setf (table cache) (bd-read-object sin cache))
    (setf (updated? cache) (bd-read-object sin context))
    (setf (id-counter cache) (bd-read-object sin context))
    (snap-sc-entry-pointers cache)
    cache))

;;; Entries

(defmethod bd-write ((thing sc-entry) sout  &rest args
                     &key (context nil) &allow-other-keys)
  "BDumper method for storing an sc-entry."
  (bd-write-token bdt-sc-entry sout)
  (bd-write (sc-item thing) sout :context context)
  (bd-write (sc-id thing) sout :context context)
  (bd-write (sc-type thing) sout :context context)
  (bd-write (sc-details thing) sout :context context)
  (bd-write (sanitize-sc-entry-list (sc-isas thing))
            sout :context context)
  (bd-write (sc-context-vector thing) sout :context context))

(defmethod bd-read (sin (token (eql bdt-sc-entry))
                        &rest args
                        &key (context nil) &allow-other-keys)
  "BDumper method for reading an sc-entry."
  (let ((entry (make-instance 'sc-entry :sc-item (bd-read-object sin context)
                 :sc-id (bd-read-object sin context))))
    (setf (sc-type entry) (bd-read-object sin context))
    (setf (sc-details entry) (bd-read-object sin entry))
    (setf (sc-isas entry) (bd-read-object sin context))
    (setf (sc-context-vector entry) (bd-read-object sin context))
    entry))

;;; Collection details

(defmethod bd-write ((thing sc-collection-details)  sout  &rest args
                     &key (context nil) &allow-other-keys)
  "BDumper method for writing details of an SC collection"
  (bd-write-token bdt-sc-collection-details sout)
  (bd-write (sanitize-sc-entry-list (sc-genls thing)) sout :context context)
  (bd-write (sanitize-sc-entry-list (sc-specs thing)) sout :context context)
  ;; These are sufficiently quick to compute that we're not going to dump them.
  ;; Chance of bloat is really high
  ;;  (bd-write (sanitize-sc-entry-list (sc-all-genls thing)) sout :context context)
;;  (bd-write (sanitize-sc-entry-list (sc-all-specs thing)) sout :context context)
  (bd-write (sc-n-instances thing) sout :context context)
  (bd-write (sanitize-sc-entry-list (sc-disjoints thing)) sout :context context))

(defmethod bd-read (sin (token (eql bdt-sc-collection-details))
                        &rest args
                        &key (context nil) &allow-other-keys)
  "BDumper method for reading an sc-entry."
  ;; Details always appear in the context of some entry.
  (let ((details (make-instance 'sc-collection-details
                   :sc-entry context)))
    (setf (sc-genls details) (bd-read-object sin context))
    (setf (sc-specs details) (bd-read-object sin context))
    ;; See comment on write
;;;    (setf (sc-all-genls details) (bd-read-object sin context))
;;;    (setf (sc-all-specs details) (bd-read-object sin context))
    (setf (sc-n-instances details) (bd-read-object sin context))
    (setf (sc-disjoints details) (bd-read-object sin context))
    details))

;;; Predicate details

(defmethod bd-write ((thing sc-predicate-details)  sout  &rest args
                     &key (context nil) &allow-other-keys)
  "BDumper method for writing details of an SC predicate"
  (bd-write-predicate-basics thing bdt-sc-predicate-details sout context))

;; We modularize these operations because they are shared amongst several
;; inherited subclasses.  We have to construct the appropriate type of 
;; object when reading it back in, hence the token/instance type arguments
;; on the writing/reading helper procedures.  Subclasses then write/read their
;; appropriate additional information.

(defun bd-write-predicate-basics (thing token sout context)
  (bd-write-token token sout)
  (bd-write (sanitize-sc-entry-list (sc-genlpreds thing)) sout :context context)
  (bd-write (sanitize-sc-entry-list (sc-specpreds thing)) sout :context context)
  (bd-write (sanitize-sc-entry-alist (sc-arg-isas thing)) sout :context context)
  (bd-write (sanitize-sc-entry-list (sc-result-isa thing)) sout :context context)
  (bd-write (sc-n-ary? thing) sout :context context)
  (bd-write (sc-arity thing) sout :context context)
  (bd-write (sc-commutative? thing) sout :context context)
  (bd-write (sc-role-relation-pos thing) sout :context context))

(defmethod bd-read (sin (token (eql bdt-sc-predicate-details))
                        &rest args
                        &key (context nil) &allow-other-keys)
  (bd-read-predicate-basics 'sc-predicate-details sin context))

(defun bd-read-predicate-basics (instance-type sin context)
  (let ((details (make-instance instance-type :sc-entry context)))
    (setf (sc-genlpreds details) (bd-read-object sin context))
    (setf (sc-specpreds details) (bd-read-object sin context))
    (setf (sc-arg-isas details) (bd-read-object sin context))
    (setf (sc-result-isa details) (bd-read-object sin context))
    (setf (sc-n-ary? details) (bd-read-object sin context))
    (setf (sc-arity details) (bd-read-object sin context))
    (setf (sc-commutative? details) (bd-read-object sin context))
    (setf (sc-role-relation-pos details) (bd-read-object sin context))
    details))

;;; Relation details

(defmethod bd-write ((thing sc-relation-details)  sout  &rest args
                     &key (context nil) &allow-other-keys)
  (bd-write-predicate-basics thing bdt-sc-relation-details sout context))

(defmethod bd-read (sin (token (eql bdt-sc-relation-details))
                         &rest args
                        &key (context nil) &allow-other-keys)
  (bd-read-predicate-basics 'sc-relation-details sin context))

;;; Function details
                         
(defmethod bd-write ((thing sc-function-details)  sout  &rest args
                     &key (context nil) &allow-other-keys)
  (bd-write-predicate-basics thing bdt-sc-function-details sout context)
  (bd-write (sc-lisp-handler thing) sout :context context))

(defmethod bd-read (sin (token (eql bdt-sc-function-details))
                         &rest args
                        &key (context nil) &allow-other-keys)
  (let ((details (bd-read-predicate-basics 'sc-function-details sin context)))
    (setf (sc-lisp-handler details) (bd-read-object sin context))
    details))

;;; Logical connective details

(defmethod bd-write ((thing sc-logical-details)  sout  &rest args
                     &key (context nil) &allow-other-keys)
  (bd-write-predicate-basics thing bdt-sc-logical-details sout context))

(defmethod bd-read (sin (token (eql bdt-sc-logical-details))
                         &rest args
                        &key (context nil) &allow-other-keys)
  (bd-read-predicate-basics 'sc-logical-details sin context))

;;;; Microtheory information

(defmethod bd-write ((thing sc-microtheory-details)  sout  &rest args
                     &key (context nil) &allow-other-keys)
  "BDumper method for writing details of an SC predicate"
  (bd-write-microtheory-info thing bdt-sc-microtheory-details sout context))

;; We modularize these operations because they are shared amongst several
;; inherited subclasses.  We have to construct the appropriate type of 
;; object when reading it back in, hence the token/instance type arguments
;; on the writing/reading helper procedures.  Subclasses then write/read their
;; appropriate additional information.

(defun bd-write-microtheory-info (thing token sout context)
  (bd-write-token token sout)
  (bd-write (sanitize-sc-entry-list (sc-genlmts thing)) sout :context context)
  (bd-write (sanitize-sc-entry-list (sc-specmts thing)) sout :context context)
  (bd-write (sc-n-facts thing) sout :context context))

(defmethod bd-read (sin (token (eql bdt-sc-microtheory-details))
                        &rest args
                        &key (context nil) &allow-other-keys)
  (bd-read-microtheory-info 'sc-microtheory-details sin context))

(defun bd-read-microtheory-info (instance-type sin context)
  (let ((details (make-instance instance-type :sc-entry context)))
    (setf (sc-genlmts details) (bd-read-object sin context))
    (setf (sc-specmts details) (bd-read-object sin context))
    (setf (sc-n-facts details) (bd-read-object sin context))
    details))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Sanitizing sc-entries

;;; Classic problem with dumpers/loaders is that there are backpointers and cross-pointers
;;; between them.  Backpointers between an sc-entry and its details are handled by exploiting
;;; their nesting relationship, as per the use of the context parameter above.  However,
;;; sc-entries as well as details have fields which are themselves filled by sc-entries. 
;;; Thus we have a potentially arbitrary amount of same-level cross-pointers.
;;; Consequently, when we dump these fields we "sanitize" them by replacing the sc-entry
;;; with the item it represents.  These are always simple s-expressions, and hence dumpable
;;; without reference to anything else.  On loading, once the entire table is loaded, we
;;; must then map through the table and "snap" these pointers, replacing them by the actual
;;; sc-entry datastructures, in a manner analogous to what dynamic linkers do (hence the
;;; terminology).  

(defun sanitize-sc-entry-list (list-of-entries)
  (if (listp list-of-entries) 
    (mapcar #'sc-item list-of-entries)
    list-of-entries))

(defun sanitize-sc-entry-alist (alist-of-entries)
  ;; We assume these are always of the form (<key ~= sc-entry> . <list of sc-entries>)
  (if (listp alist-of-entries)
    (mapcar #'(lambda (entry)
                (cons (car entry) (sanitize-sc-entry-list (cdr entry))))
      alist-of-entries)
    alist-of-entries))

(defun snap-sc-entry-pointers (cache)
  ;; Snapping the pointers is a bit more annoying, because we have to specialize on
  ;; each type for an entry's details.
  (let ((table (table cache)))
    (maphash #'(lambda (key value)
                 (declare (ignore key))
                 (snap-sc-entry value table)) table)
    cache))

(defun snap-sc-entry (entry table)
  (setf (sc-isas entry) (snap-sc-name-list (sc-isas entry) table))
  (snap-sc-entry-details (sc-details entry) table))

(defun snap-sc-name-list (list-of-names table)
  (if (listp list-of-names)
    (mapcar #'(lambda (name)
                (snap-sc-name name table))
      list-of-names)
    list-of-names))

(defun snap-sc-name-alist (alist-of-names table)
  (mapcar #'(lambda (alist-entry)
              (cons (car alist-entry)
                    (snap-sc-name-list (cdr alist-entry) table)))
    alist-of-names))

(defun snap-sc-name (name table)
  (let ((entry (gethash name table)))
    (unless entry
      (error "No sc-entry for ~A: in ~A."
        name table))
    entry))

;;; Handling the details

(defmethod snap-sc-entry-details ((details t) (table t)) details)
;; Pass-through, unless it is a recognized type of object.

(defmethod snap-sc-entry-details ((details sc-collection-details)
                                  (table hash-table))
  (setf (sc-genls details) (snap-sc-name-list (sc-genls details) table))
  (setf (sc-specs details) (snap-sc-name-list (sc-specs details) table))
  (setf (sc-all-genls details) (snap-sc-name-list (sc-all-genls details) table))
  (setf (sc-all-specs details) (snap-sc-name-list (sc-all-specs details) table))
  (setf (sc-disjoints details) (snap-sc-name-list (sc-disjoints details) table)))

(defmethod snap-sc-entry-details ((details sc-predicate-details)
                                  (table hash-table))
  (snap-predicate-details details table))

(defun snap-predicate-details (details table)
  (setf (sc-genlpreds details) (snap-sc-name-list (sc-genlpreds details) table))
  (setf (sc-specpreds details) (snap-sc-name-list (sc-specpreds details) table))
  (setf (sc-arg-isas details) (snap-sc-name-alist (sc-arg-isas details) table))
  (unless (eq (sc-result-isa details) :unknown)
    (setf (sc-result-isa details) (snap-sc-name-list (sc-result-isa details) table)))
  )

(defmethod snap-sc-entry-details ((details sc-relation-details)
                                  (table hash-table))
  (snap-predicate-details details table))

(defmethod snap-sc-entry-details ((details sc-function-details)
                                  (table hash-table))
  (snap-predicate-details details table)
;;;  (setf (sc-result-isa details) 
;;;    (snap-sc-name-list (sc-result-isa details) table))
  )

(defmethod snap-sc-entry-details ((details sc-logical-details)
                                  (table hash-table))
  (snap-predicate-details details table))

(defmethod snap-sc-entry-details ((details sc-microtheory-details)
                                  (table hash-table))
  (setf (sc-genlmts details) (snap-sc-name-list (sc-genlmts details) table))
  (setf (sc-specmts details) (snap-sc-name-list (sc-specmts details) table)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Debugging

(defun test-structural-cache-dumper (&key (kb *kb*)
                                          (stream *standard-output*))
  (declare (special *old-cache* *new-cache*))
  (setq *old-cache* (structural-cache kb))
  (dump-structural-cache :kb kb)
  (load-structural-cache :kb kb)
  (setq *new-cache* (structural-cache kb))
  (multiple-value-bind (loser? total1 total2)
      (compare-structural-caches *old-cache* *new-cache* stream)
    (declare (ignore total1 total2))
    (cond ((= loser? 0) :ok)
          (t nil))))

(defun compare-structural-caches (cache1 cache2 &optional (stream *standard-output*))
  (let ((table1 (table cache1))
        (table2 (table cache2))
        (loser? 0)
        (total1 0)
        (total2 0))
    (maphash #'(lambda (key value)
                 (incf total1)
                 (let ((other (gethash key table2)))
                   (cond ((not (sc-entry? other))
                          (format stream "~&Bad or missing entry for ~A in 2: ~A.~%" key other)
                          (break "MUMBLE" t)
                          (incf loser?))
                         ((equal-sc? value other))
                         (t (format stream "~&Entries for ~A don't match.~%" key)
                            (break "Foo" t)
                            (incf loser?)))))
             table1)
    (maphash #'(lambda (key value)
                 (declare (ignore value))
                  (incf total2)
                 (let ((other (gethash key table1)))
                   (unless (sc-entry? other)
                     (format stream "~&Bad or missing entry for ~A in 1: ~A.~%" 
                       key other)
                     (break "BAR" t)
                     (incf loser?))))
             table2)
    (values loser? total1 total2)))

(defmethod equal-sc? ((one t) (two t)) (equal one two))
(defmethod equal-sc? ((one cons) (two t)) nil)
(defmethod equal-sc? ((one t) (two cons)) nil)
(defmethod equal-sc? ((one cons) (two cons)) (and (equal-sc? (car one) (car two))
                                                  (equal-sc? (cdr one) (cdr two))))
(defmethod equal-sc? ((one sc-entry) (two t)) nil)
(defmethod equal-sc? ((one t) (two sc-entry)) nil)
(defmethod equal-sc? ((one sc-entry) (two sc-entry))
  (and (equal-sc? (sc-item one) (sc-item two))
       (equal-sc? (sc-type one) (sc-type two))
       (equal-sc? (sc-details one) (sc-details two))
       (equal-sc-entry-list? (sc-isas one) (sc-isas two))))
;; Ignoring cvectors for now.

(defun equal-sc-entry-list? (l1 l2)
  (or (equal l1 l2) ;; Case with :unknown or nil
      (and (listp l1)
           (listp l2)
           (= (length l1) (length l2))
           (every 'sc-entry? l1)
           (every 'sc-entry? l2)
           ;; Must break cycles
           (every #'(lambda (e1 e2) (equal (sc-item e1) (sc-item e2))) l1 l2))))

(defun equal-sc-entry-alist? (al1 al2)
  (every #'(lambda (e1 e2)
             (and (equal (car e1) (car e2))
                  (equal-sc-entry-list? (cdr e1) (cdr e2))))
                al1 al2))

(defmethod equal-sc? ((one sc-collection-details) (two t)) nil)
(defmethod equal-sc? ((one t) (two sc-collection-details)) nil)
(defmethod equal-sc? ((one sc-collection-details) (two sc-collection-details))
  (and (equal-sc-entry-list? (sc-genls one) (sc-genls two))
       (equal-sc-entry-list? (sc-specs one) (sc-specs two))
;;;       (equal-sc-entry-list? (sc-all-genls one) (sc-all-genls two))
;;;       (equal-sc-entry-list? (sc-all-specs one) (sc-all-specs two))
       (= (sc-n-instances one) (sc-n-instances two))))

(defmethod equal-sc? ((one sc-predicate-details) (two t)) nil)
(defmethod equal-sc? ((one t) (two sc-predicate-details)) nil)
(defmethod equal-sc? ((one sc-predicate-details) (two sc-predicate-details))
  (equal-predicate-details? one two))

(defun equal-predicate-details? (one two)
  (and (equal-sc-entry-list? (sc-genlpreds one) (sc-genlpreds two))
       (equal-sc-entry-list? (sc-specpreds one) (sc-specpreds two))
       (equal-sc-entry-alist? (sc-arg-isas one) (sc-arg-isas two))
       (equal (sc-arity one) (sc-arity two))
       (equal (sc-n-ary? one) (sc-n-ary? two))
       
       (equal (sc-commutative? one) (sc-commutative? two))))


(defmethod equal-sc? ((one sc-relation-details) (two t)) nil)
(defmethod equal-sc? ((one t) (two sc-relation-details)) nil)
(defmethod equal-sc? ((one sc-relation-details) (two sc-relation-details))
  (equal-predicate-details? one two))

(defmethod equal-sc? ((one sc-function-details) (two t)) nil)
(defmethod equal-sc? ((one t) (two sc-function-details)) nil)

(defmethod equal-sc? ((one sc-function-details) (two sc-function-details))
  (and (equal-predicate-details? one two)
       (equal (sc-lisp-handler one) (sc-lisp-handler two))
       (equal-sc-entry-list? (sc-result-isa one) (sc-result-isa two))))

(defmethod equal-sc? ((one sc-logical-details) (two t)) nil)
(defmethod equal-sc? ((one t) (two sc-logical-details)) nil)
(defmethod equal-sc? ((one sc-logical-details) (two sc-logical-details))
  (equal-predicate-details? one two))

(defmethod equal-sc? ((one sc-microtheory-details) (two t)) nil)
(defmethod equal-sc? ((one t) (two sc-microtheory-details)) nil)
(defmethod equal-sc? ((one sc-microtheory-details) (two sc-microtheory-details))
  (and (equal-sc-entry-list? (sc-genlmts one) (sc-genlmts two))
       (equal-sc-entry-list? (sc-specmts one) (sc-specmts one))
       (= (sc-n-facts one) (sc-n-facts two))))
  

  

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