;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: kb-tools.lsp
;;;;    System: FIRE
;;;;    Author: Jeff Usher
;;;;   Created: October 18, 2001 08:54:53
;;;;   Purpose: Tools for maintaining the KB.
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Monday, January 26, 2004 at 16:32:09 by usher
;;;; ---------------------------------------------------------------------------

(in-package :fire)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Franz Allegro Stuff

#+(and acl6 (not :runtime-system))
(progn
  (setf (cg:text-edit-indentation 'process-run-function-and-wait) '(4 2))
  (setf (cg:text-edit-indentation 'run-kb-tool) '(4 2)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Queues

(defclass queue ()
  ((start
    :documentation "Pointer to the beginning of the queue."
    :accessor start :accessor queue-start :initarg :start :initform nil)
   (end
    :documentation "Pointer to the end of the queue."
    :accessor end :accessor queue-end :initarg :end :initform nil))
  (:documentation "Basic queue data structure."))


(defun make-queue (&key (type 'queue))
  (make-instance type))

(defun make-queue-from-list (lst &key (type 'queue))
  "Creates and returns a new queue and enqueues the entire list in order."
  (make-instance type
    :start lst
    :end (last lst)))



(defgeneric empty? (queue)
  (:documentation "Returns non-nil iff q is empty."))

(defmethod empty? ((q queue))
   (null (start q)))



(defgeneric reset-queue (queue)
  (:documentation "Removes all the data items from the queue.  
                   Always returns t."))

(defmethod reset-queue ((q queue))
   (setf (start q) nil)
   (setf (end q) nil) ;; allows data to be gc'd
   t)



(defgeneric enqueue (queue item)
  (:documentation "Adds item to the back of the queue."))

(defmethod enqueue ((q queue) item)
   (let ((new-data (cons item nil)))
      (cond ((empty? q)
             (setf (start q) new-data)
             (setf (end q) new-data))
            (t
             (setf (cdr (end q)) new-data)
             (setf (end q) new-data)))))



(defgeneric enqueue-list (queue lst)
  (:documentation "Adds all the items in the list to the back of the queue,
                   in order."))

(defmethod enqueue-list ((q queue) lst)
  (cond ((null lst) nil)
        ((empty? q)
         (setf (start q) lst)
         (setf (end q) (last lst)))
        (t
         (setf (cdr (end q)) lst)
         (setf (end q) (last lst)))))



(defgeneric dequeue (queue)
  (:documentation "Pops the front item off the queue and returns it."))

(defmethod dequeue ((q queue))
   (let ((item (car (start q))))
      (unless (empty? q)
         (setf (start q) (cdr (start q)))
         (when (null (start q))  ;; allow data to be gc'd
            (setf (end q) nil)))
     item))



(defgeneric list-data (queue)
  (:documentation "Returns a list of the data in the queue."))

(defmethod list-data ((q queue))
  (start q))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Globals

(defparameter *kb-checker* nil)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Class Definitions

(defclass kb-checker ()
  ((kb
    :documentation "Pointer to the KB being checked."
    :accessor kb :initarg :kb :initform nil)
   (kb-path
    :documentation "Path to the KB."
    :accessor kb-path :initarg :kb-path :initform nil)
   (kb-name
    :documentation "Name of the KB."
    :accessor kb-name :initarg :kb-name :initform nil)
   (main-win
    :documentation "Pointer to the Kb-Checker's main window."
    :accessor main-win :initarg :main-win :initform nil)
   (logstr
    :documentation "Pointer to the open logfile stream."
    :accessor logstr :initarg :logstr :initform nil))
  (:documentation "The KB Checker is used to grovel over the KB and alert
                   the operator."))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; GUI

(defconstant PBS_SMOOTH 1
  "Windows Common Control constant for type of progress-bar.")



(defclass kb-checker-win ()
  ((kb-checker
    :documentation "Pointer to the kb-checker object running in this window."
    :allocation :class
    :accessor kb-checker :initarg :kb-checker :initform nil))
  (:documentation "All KB Checker windows inherit from this class."))

(defclass kb-checker-main-win (kb-checker-win cg:dialog)
  ((progress-bar
    :documentation "Pointer to the progress bar on the kb-checker's gui."
    :accessor progress-bar :initarg :progress-bar :initform nil)
   (text-output
    :documentation "Pointer to the text output widget -- used for displaying
                    messages about the status of the KB checking operation."
    :accessor text-output :initarg :text-output :initform nil))
  (:documentation "Main window for the KB Checker."))

(defclass kb-checker-bar (cg:progress-indicator)
  ()
  (:documentation "Special class of progress bars."))

(defclass kb-checker-bar-pane (kb-checker-win cg::progress-indicator-pane)
  ()
  (:documentation "Pane to use with a kb-checker-bar"))



(defun make-kb-checker-gui (kb-checker &key (owner (cg:screen cg:*system*)))
  (let ((win (cg:make-window :kb-checker-main-win
               :owner owner
               :device 'kb-checker-main-win
               :title "FIRE KB Consistency Checker"
               :interior (cg:window-to-screen-units owner 
                           (cg:center-box-on-window owner 600 500))
               :border :frame
               :state :shrunk
               :close-button t
               :minimize-button t
               :maximize-button t
               :resizable t
               :scrollbars nil
               :title-bar t
               :toolbar nil
               :pop-up nil
               :overlapped t
               :help-string nil
               :kb-checker kb-checker)))
    (add-kb-checker-widgets win)
    (setf (progress-bar win) (cg:find-component :progress-bar win))
    (setf (text-output win)
      (cg:window (cg:find-component :text-output win)))
    (cg:select-window win)
    (cg:process-pending-events)
    win))

(defun add-kb-checker-widgets (win)
  (let ((w (cg:interior-width win))
        (h (cg:interior-height win)))
    (cg:add-component
     (make-instance 'cg:multi-line-editable-text
       :name :text-output
       :title "text-output"
       :value ""
       :left 4   :width (- w 8)
       :top 4    :height (- h 89)
       :tabstop nil
       :scrollbars :vertical
       :read-only t
       :top-attachment :top
       :bottom-attachment :bottom
       :left-attachment :left
       :right-attachment :right
       :font (cg:make-font-ex :swiss :|ms sans serif| 11 nil)) win)
    (cg:add-component
     (make-instance 'cg:static-text 
       :name :operation-name
       :value ""
       :left 4        :width (- w 128)
       :top (- h 72)  :height 48
       :tabstop nil 
       :top-attachment :bottom
       :bottom-attachment :bottom
       :left-attachment :left
       :right-attachment :right
       :font (cg:make-font-ex :swiss :|ms sans serif| 11 nil)) win)
    (cg:add-component
     (make-instance 'kb-checker-bar
       :name :progress-bar
       :title "progress-bar"
       :left 4        :width (- w 128)
       :top (- h 24)  :height 22
       :value 0
       :range '(0 1000)
       :available t
       :border :static
       :tabstop nil
       :foreground-color #.(cg:make-rgb :red 18 :green 40 :blue 60)
       :top-attachment :bottom
       :bottom-attachment :bottom
       :left-attachment :left
       :right-attachment :right) win)
    (cg:add-component 
     (make-instance 'gui-lib:animation-control
       :name :animation
       :avi-file (qrg:make-full-file-spec 
                  (qrg:make-qrg-path "fire" "v1")
                  "thinking" ".avi")
       :left (- w 120)  :width 116
       :top (- h 82)    :height 81
       :border :plain
       :tabstop nil
       :top-attachment :bottom
       :bottom-attachment :bottom
       :left-attachment :right
       :right-attachment :right) win)
    win))



(defmethod cg:widget-device ((widget kb-checker-bar) win)
  (declare (ignore win))
  'kb-checker-bar-pane)

(defmethod cg::device-open ((widget-pane kb-checker-bar-pane) options)
  ;; note that some of the code in this method uses functions that are not
  ;; exported from Allegro's Common Graphics package and therefore might not
  ;; be portable to new versions of ACL.
  (cg::ensure-common-controls-are-initialized)
  (let* ((widget (cg:dialog-item widget-pane))
         (value (getf options :value)))
    (apply #'cg::open-widget-window widget-pane
           :control-class (cg::control-name widget)
           :id nil 
           :has-title t 
           :style PBS_SMOOTH
           :init-range-p t
           options)
    (when value
      (cg:widget-set-value widget-pane widget value 0 nil))
    widget-pane))

(defun set-kb-checker-bar (kb-checker percent-complete)
  (let* ((main-win (main-win kb-checker))
         (pbar (progress-bar main-win)))
    (when pbar
      (setf (cg:value pbar) (round (* 1000 percent-complete)))
      percent-complete)))



;;;

(defun set-percent-complete (val &optional (kb-checker *kb-checker*))
  (set-kb-checker-bar kb-checker val)
  val)

(defun set-kb-checker-operation-name (name-of-operation 
                                      &optional (kb-checker *kb-checker*))
  (let* ((main-win (main-win kb-checker))
         (opname-widget (cg:find-component :operation-name main-win)))
    (when opname-widget
      (setf (cg:value opname-widget) name-of-operation))
    (cg:process-pending-events)
    name-of-operation))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Some Useful Macros and Utility Functions

(eval-when (:load-toplevel :compile-toplevel :execute)
  (defmacro process-run-function-and-wait ((process-name quantum priority
                                                         fn &rest fn-args)
                                           &body body)
                                           
    (let ((result (gensym "result-"))
          (done? (gensym "done?-")))
      `(let ((,result nil)
             (,done? nil))
         (mp:process-run-function 
          (list :name ,process-name
                :initial-bindings cg:*default-cg-bindings*
                :quantum ,quantum
                :priority ,priority)
          #'(lambda ()
              (setq ,result (funcall ,fn ,@fn-args))
              (setq ,done? t)))
         ,@body
         (mp:process-wait ,process-name #'(lambda () (if ,done? t nil)))
         ,result))))

(eval-when (:load-toplevel :compile-toplevel :execute)
  (defmacro run-kb-tool (tool-desc kb-checker tool-fn &rest tool-args)
    (let ((result (gensym "result-")))
      `(progn
         (cg:process-pending-events)
         (process-run-function-and-wait
             (,tool-desc 
              1 6
              #'(lambda ()
                  (let ((*standard-output* (text-output (main-win ,kb-checker)))
                        (,result nil))
                    (set-kb-checker-operation-name 
                     (format nil "~A ..." ,tool-desc) ,kb-checker)
                    (write-to-kb-checker-log 
                     (format nil "~%~A~%" (make-string 80 :initial-element #\*)))
                    (format t "~%  ~A ..." ,tool-desc)
                    (setq ,result (funcall ,tool-fn ,@tool-args))
                    (format t "~%  Finished ~A.~%" ,tool-desc)
                    ,result))))))))



(defun term->string (term)
  (typecase term
    (symbol (symbol-name term))
    (otherwise (write-to-string term))))
                     
(defun term< (term1 term2)
  "Returns non-nil iff term1 should come before term2 when sorted 
   alphabetically.  This is not the fastest thing in the world."
  (string-lessp (term->string term1) (term->string term2)))



(defun var-skolem-or-nat? (term)
  (or (consp term)
      (and (symbolp term) 
           (char= (char (symbol-name term) 0) #\?))
      (and (symbolp term) 
           (string-equal (subseq (symbol-name term) 0 4) "skf-"))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Main Entry Point

(defun check-kb (kb-path kb-name &key (logfile "c:\\kb-checker-log.txt"))
  (let ((kb-checker (init-kb-checker kb-path kb-name logfile)))
    (when kb-checker
      (let ((*standard-output* (text-output (main-win kb-checker))))
        (format t "~%Starting to check ~A~A ...~%" kb-path kb-name)
        
        ;;; We should make a version of the Grim Fact Reaper that uses this kind of interface.
        ;;; The tests that are in the new structural cache system are a bit more accurate
        ;;; and more exhaustive than these...
;;;        (run-kb-tool 
;;;            #.(format nil "Looking for collections that are lacking a fact ~
;;;                           saying (isa ?foo Collection) {or one of ~
;;;                           Collection's subsets}")
;;;          kb-checker 'find-missing-isas-for-collections (kb kb-checker))
;;;        (run-kb-tool 
;;;            #.(format nil "Looking for collections that are lacking genls ~
;;;                           facts")
;;;          kb-checker 'gather-non-genld-collections (kb kb-checker))
;;;        (run-kb-tool 
;;;            "Looking for isolated trees in the genls heirarchy"
;;;          kb-checker 'find-isolated-ontology-trees (kb kb-checker))
;;;        (run-kb-tool 
;;;            #.(format nil "Looking for relations of arity two that are not ~
;;;                           defined to be some subclass of BinaryRelation")
;;;          kb-checker 'find-missing-binary-defs (kb kb-checker))
;;;        (run-kb-tool
;;;            #.(format nil "Looking for relations missing arity or ~
;;;                           argument type constraints.")
;;;          kb-checker 'check-kb-structural-constraints (kb kb-checker))
        (shutdown-kb-checker kb-checker)
        (format t "~%Finished checking ~A~A.  KB is now closed."
          kb-path kb-name)
        (format t "~%See ~A for more details." logfile)
        kb-checker))))



(defun write-to-kb-checker-log (string &optional (kb-checker *kb-checker*))
  (when (open-stream-p (logstr kb-checker))
    (write-string string (logstr kb-checker))
    (terpri (logstr kb-checker))
    string))

(defun init-kb-checker (kb-path kb-name logfile)
  (let ((kb-checker (make-instance 'kb-checker
                      :kb-path kb-path
                      :kb-name kb-name)))
    (setq *kb-checker* kb-checker)
    (setf (main-win kb-checker) (make-kb-checker-gui kb-checker))
    (when logfile
      (setf (logstr kb-checker)
        (open logfile :direction :output :if-exists :supersede)))
    (process-run-function-and-wait 
        ("Opening KB" 1 8 'open-kb-for-kb-checker kb-checker))
    kb-checker))

(defun open-kb-for-kb-checker (kb-checker)
  (cg:with-hourglass
    (set-kb-checker-operation-name "Opening KB ..." kb-checker)
    (setf (kb kb-checker)
      (make-kb (kb-path kb-checker) (kb-name kb-checker)))))

(defun shutdown-kb-checker (kb-checker)
  (let* ((win (main-win kb-checker))
         (ani-widget (cg:find-component :animation win)))
    (format t "~%Closing the FIRE KB Consistency Checker.  Please wait ...")
    (close-kb (kb kb-checker))
    (when (logstr kb-checker)
      (close (logstr kb-checker)))
    (set-percent-complete 1 kb-checker)
    (gui-lib:stop-animation ani-widget)
    :ok))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Missing (isa ?blah Collection) Definitions

(defun find-missing-isas-for-collections (kb)
  (format t "~%    Calling list-all-collections ....")
  (let* ((all-cols (list-all-collections :kb kb))
         (num-cols (length all-cols))
         (j 0)
         (missing-cols nil))
    (format t "~%    Finding those collections that are not declared to be ~
                     an instance of Collection ...")
    (write-to-kb-checker-log 
     "Collections that had not been declared to be an instance of Collection:")
    (dolist (col all-cols)
      (unless (or (var-skolem-or-nat? col)
                  (instance-of? col 'd::Collection kb))
        (push col missing-cols)
        (store `(data::isa ,col data::Collection) kb))
      (set-percent-complete (/ (incf j) num-cols)))
    (setq missing-cols (sort missing-cols #'term<))
    (dolist (col missing-cols)
      (write-to-kb-checker-log (format nil "  ~A" col)))
    (format t "~%    Finished.  Found ~A Collections not defined to be ~
                     an instance of Collection.  These have now been fixed."
      (length missing-cols))
    (write-to-kb-checker-log
     (format nil "Found ~A collections not defined to be an instance of ~
                  Collection.  These have now been fixed.~%"
       (length missing-cols)))
        missing-cols))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Collections with no genls facts

;;;(defun gather-non-genld-collections (&optional (kb *kb*))
;;;  (set-percent-complete 0)
;;;  (format t "~%    Retrieving all (isa ?x Collection) facts ...")
;;;  (let* ((declared-collections 
;;;          (retrieve '(data::isa ?x data::Collection)  :kb kb :response '?x))
;;;         (subs (direct-subs (genls-cache kb)))
;;;         (genls (direct-genls (genls-cache kb)))
;;;         (ungenld-cols nil)
;;;         (j 0)
;;;         (n (length declared-collections)))
;;;    (write-to-kb-checker-log
;;;     "Collections that have no genls statements whatsoever:")
;;;    (dolist (col declared-collections)
;;;      (unless (or (var-skolem-or-nat? col) 
;;;                  (gethash col genls) (gethash col subs))
;;;        (push col ungenld-cols))
;;;      (set-percent-complete (/ (incf j) n)))
;;;    (setq ungenld-cols (sort ungenld-cols #'term<))
;;;    (dolist (col ungenld-cols)
;;;      (write-to-kb-checker-log (format nil "  ~A" col)))
;;;    (format t "~%    Found ~A collections (out of ~A) that have no genls ~
;;;                     statements whatsoever." 
;;;      (length ungenld-cols) (length declared-collections))
;;;    (write-to-kb-checker-log
;;;     (format nil "Found ~A collections (out of ~A) that have no genls ~
;;;                  statements whatsoever." 
;;;       (length ungenld-cols) (length declared-collections)))
;;;    ungenld-cols))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Isolated trees in the genls hierarchy
;;;
;;; NOTICE - this procedure uses the plist of the symbols.  I know they suck
;;;  but in this case for optimizing it's actually the best way to go.   
;;; This algorithm is linear on the number of collections - starting from 
;;;  each root proceed down their genl hierarchy marking each one as belonging
;;;  to that tree.  

;;; Some Collections are actually NATS - these are expressions
;;;  and have no symbol plist - special case those and store them here
;;;  as a hashtable key'd on the expression, the value will be the tree-id

;;;(defparameter *expressions-hash* (make-hash-table))
;;;
;;;
;;;
;;;(defun find-isolated-ontology-trees (&optional (kb *kb*))
;;;  (write-to-kb-checker-log "Isolated trees in the genls hierachy:")
;;;  (unmark-trees kb)
;;;  (let* ((trees (mark-ontology-trees 
;;;                 (gather-ontology-roots kb) (genls-cache kb)))
;;;         (isolated-roots (sort (mapcar #'car trees) #'term<)))
;;;    (dolist (root isolated-roots)
;;;      (write-to-kb-checker-log (format nil "  ~A" root)))
;;;    (format t "~%    Found ~A isolated trees in the genls hierarchy." 
;;;      (length isolated-roots))
;;;    (write-to-kb-checker-log
;;;     (format nil "~%Found ~A isolated trees in the genls hierarchy." 
;;;       (length isolated-roots)))
;;;    (values isolated-roots trees)))
;;;
;;;
;;;
;;;(defun get-marking (root)
;;;  (if (symbolp root)
;;;    (getf (symbol-plist root) :containing-tree)
;;;    (gethash root *expressions-hash*)))
;;;
;;;(defun set-marking (root tree-id)
;;;  (if (symbolp root)
;;;    (setf (getf (symbol-plist root) :containing-tree) tree-id)
;;;    (setf (gethash root *expressions-hash*) tree-id)))
;;;
;;;(defun clear-hash-marks (hashtable)
;;;  (maphash #'(lambda (key val)
;;;               (declare (ignore val))
;;;               (when (symbolp key)
;;;                 (setf (getf (symbol-plist key) :containing-tree) nil)))
;;;           hashtable))
;;;
;;;(defun unmark-trees (&optional (kb *kb*))
;;;  (clrhash *expressions-hash*)
;;;  (clear-hash-marks (direct-subs (genls-cache kb)))
;;;  (clear-hash-marks (direct-genls (genls-cache kb))))
;;;
;;;
;;;
;;;(defun mark-ontology-trees (tree-roots g-cache)
;;;  (let ((i 0)
;;;        (trees nil))
;;;    (dolist (tree tree-roots)
;;;      (let ((root-id (mark-ontology-tree tree g-cache :tree-id (incf i))))
;;;        (when (= i root-id)
;;;          ;; If i does not equal root-id that meant that that root was
;;;          ;;  found to be part of another tree and not the beginning of 
;;;          ;;  a separate tree.  If they are equal it means it wasn't part
;;;          ;;  of another tree, so push the root with it's id onto our list
;;;          ;;  of separate trees.
;;;          (push (cons tree i) trees))))
;;;    trees))
;;;
;;;(defun mark-ontology-tree (root g-cache &key (tree-id 0))
;;;  (let ((marking (get-marking root)))
;;;    (unless marking
;;;      ;; Mark this symbol
;;;      (set-marking root tree-id)
;;;      ;; Recurse on the children and the parents
;;;      (dolist (genl (gethash root (direct-genls g-cache)))
;;;        (mark-ontology-tree genl g-cache :tree-id tree-id))
;;;      (dolist (spec (gethash root (direct-subs g-cache)))
;;;        (mark-ontology-tree spec g-cache :tree-id tree-id)))
;;;    ;; Return the old marking if it exists, or the tree-id 
;;;    ;;  if it doesn't
;;;    (or marking tree-id)))
;;;
;;;(defun gather-ontology-roots (&optional (kb *kb*))
;;;  (let ((roots nil)
;;;        (genl-c (direct-genls (genls-cache kb))))
;;;    (maphash #'(lambda (key val)
;;;                 (declare (ignore val))
;;;                 ;; Since you will never find a key with a nil value in this 
;;;                 ;; hashtable we can use the first return value as an 
;;;                 ;; indicator of whether the collection has a parent.
;;;                 (unless (or (var-skolem-or-nat? key)
;;;                             (gethash key genl-c))
;;;                   (push key roots)))
;;;             (direct-subs (genls-cache kb)))
;;;    roots))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Missing BinaryPredicate and BinaryFunction Definitions

(defun find-missing-binary-defs (kb)
  (format t "~%    Gathering all predicates of arity two ....")
  (set-percent-complete 0)
  (let* ((all-binaries (retrieve '(data::arity ?pred 2) 
                                 :kb kb :response '?pred
                                 :number :all))
         (missing-bin-fns nil)
         (missing-bin-preds nil)
         (missing-bin-rels nil)
         (j 0)
         (n (length all-binaries)))
    (format t "~%    Finding those relations of arity two that are not defined ~
                     to be some subclass of BinaryRelation  ...")
    (dolist (pred all-binaries)
      (unless (var-skolem-or-nat? pred)
        (case (predicate-type pred kb)
          (:function
           (unless (instance-of? pred 'd::BinaryFunction kb)
             (push pred missing-bin-fns)
             (store `(data::isa ,pred data::BinaryFunction) kb)))
          (:relation
           (unless (instance-of? pred 'd::BinaryPredicate kb)
             (push pred missing-bin-preds)
             (store `(data::isa ,pred data::BinaryPredicate) kb)))
          (otherwise
           (unless (instance-of? pred 'd::BinaryRelation kb)
             (push pred missing-bin-rels)
             (store `(data::isa ,pred data::BinaryRelation) kb)))))
      (set-percent-complete (/ (incf j) n)))
    
    (setq missing-bin-fns (sort missing-bin-fns #'term<))
    (write-to-kb-checker-log 
     (format nil "Functions of arity two that weren't defined as ~
                  BinaryFunctions (~A); these have been fixed:"
       (length missing-bin-fns)))
    (dolist (pred missing-bin-fns)
      (write-to-kb-checker-log (format nil "  ~A" pred)))
    
    (setq missing-bin-preds (sort missing-bin-preds #'term<))
    (write-to-kb-checker-log 
     (format nil "~%Predicates of arity two that weren't defined as ~
                  BinaryPredicates (~A); these have been fixed:"
       (length missing-bin-preds)))
    (dolist (pred missing-bin-preds)
      (write-to-kb-checker-log (format nil "  ~A" pred)))
    
    (setq missing-bin-rels (sort missing-bin-rels #'term<))
    (write-to-kb-checker-log 
     (format nil "~%Relations of arity two that weren't defined as ~
                  BinaryRelations (~A); these have been fixed:"
       (length missing-bin-rels)))
    (dolist (pred missing-bin-rels)
      (write-to-kb-checker-log (format nil "  ~A" pred)))

    (format t "~%    Finished.  Found a total of ~A (of ~A) relations of arity ~
                     two that were not defined to be an instance of ~
                      BinaryRelation."
      (+ (length missing-bin-fns) (length missing-bin-preds) 
         (length missing-bin-rels)) n)
    (values missing-bin-fns missing-bin-preds missing-bin-rels)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Checking structural expression constraints
;;; 
;;; We bundle up arity, argtype, expression type, and expression checks because we
;;; want to be able to suggest repairs based on the way expressions are used.

(defun check-kb-structural-constraints (kb)
  (format t "~%    Gathering all predicates ....")
  (set-percent-complete 0)
  (multiple-value-bind (relations functions connectives other)
      (list-all-predicates :kb kb)
    (let* ((missing-arity nil)
           (missing-argisas nil)
           (missing-resultisas nil)
           (counter 0)
           (n (+ (length relations) (length functions))))
      ;; We're ignoring connectives, under the assumption that those are
      ;; hard-wired correctly from the beginning.  Similarly, the "other"
      ;; category will just be reported straight-up.
      (format t "~%    Checking predicate structural constraints...")
      (dolist (pred relations)
        (multiple-value-bind (new-missing-arity
                              new-missing-argisas
                              new-missing-resultisas)
            (evaluate-predicate-structural-constraints pred :function :kb kb)
          (when new-missing-arity
            (setq missing-arity (nconc new-missing-arity missing-arity)))
          (when new-missing-argisas 
            (setq missing-argisas (nconc new-missing-argisas missing-argisas)))
          (when new-missing-resultisas
            (setq missing-resultisas (nconc new-missing-resultisas missing-resultisas)))
          (set-percent-complete (/ (incf counter) n))))
      (dolist (pred functions)
        (multiple-value-bind (new-missing-arity
                              new-missing-argisas
                              new-missing-resultisas)
            (evaluate-predicate-structural-constraints pred :relation :kb kb)
          (when new-missing-arity
            (setq missing-arity (nconc new-missing-arity missing-arity)))
          (when new-missing-argisas 
            (setq missing-argisas (nconc new-missing-argisas missing-argisas)))
          (when new-missing-resultisas
            (setq missing-resultisas (nconc new-missing-resultisas missing-resultisas)))))
      ;; Output information about missing arity information
      (setq missing-arity (sort missing-arity #'(lambda (x y) (term< (car x) (car y)))))
      (write-to-kb-checker-log 
       (format nil "Relations whose arity is unknown ~
                  (~A); these have been fixed:"
         (length missing-arity)))
      (dolist (pred-entry missing-arity)
        (if (integerp (cadr pred-entry))
          (write-to-kb-checker-log (format nil "  ~A, might be ~D."
                                     (car pred-entry) (cadr pred-entry)))
          (write-to-kb-checker-log (format nil "  ~A" (car pred-entry)))))
      ;; Output information about missing argument type information
      (setq missing-argisas (sort missing-argisas #'(lambda (x y) (term< (car x) (car y)))))
      (write-to-kb-checker-log 
       (format nil "~%Relations whose argument type constraints are not fully specified ~
                  (~A):"
         (length missing-argisas)))
      (dolist (pred-entry missing-argisas)
        (write-to-kb-checker-log (format nil "  ~A: ~A" 
                                   (car pred-entry) (cdr pred-entry))))
      ;; Output information about missing function result types
      (setq missing-resultisas (sort missing-resultisas #'(lambda (x y) (term< x y))))
      (write-to-kb-checker-log
       (format nil "Functions whose result type is unknown (~D):" (length missing-resultisas)))
       (dolist (pred missing-resultisas)
         (write-to-kb-checker-log (format nil " ~A" pred)))
      ;; Output information about miscast predicates
      (setq other (sort other #'(lambda (x y) (term< x y))))
      (cond ((null other)
             (write-to-kb-checker-log (format nil "All predicates are known to be relations, functions, or connectives.")))
            (t (write-to-kb-checker-log (format nil "~D predicates not classified as relation, function, or connective."
                                          (length other)))
               (dolist (o other)
                 (write-to-kb-checker-log 
                  (format nil "  ~A (~A)" o (predicate-type other))))))
      ;; Output information about connectives.
      (setq connectives (sort connectives #'(lambda (x y) (term< x y))))
      (cond ((null connectives)
             (write-to-kb-checker-log (format nil "No logical connectives in this KB!")))
            (t (write-to-kb-checker-log (format nil "~D logical connectives in this KB."
                                          (length connectives)))
               (dolist (c connectives)
                 (write-to-kb-checker-log (format nil "~%  ~A" c)))))
      (values missing-arity missing-argisas missing-resultisas))))
    
(defun evaluate-predicate-structural-constraints (pred pred-type &key (kb *kb*))
  (let ((the-arity (arity pred :kb kb))
        (entry nil)
        (missing-argisas nil)
        (missing-resultisas nil)
        (missing-arity nil))
    (cond ((integerp the-arity)
           (dotimes (arg- the-arity)
             (let* ((arg (1+ arg-))
                    (the-type (arg-isa pred arg :kb kb)))
               (unless (collection? the-type :kb kb)
                 (unless entry
                   (setq entry (list pred nil))
                   (push entry missing-argisas))
                     (push (list arg the-type) (cdr entry))))))
              ((eq the-arity :n-ary)
               (let ((the-type (retrieve (make-args-isa pred '?type)
                                         :kb kb :number 1
                                         :response '?type
                                         :coverage :ground)))
                 (unless (collection? the-type)
                   (push (list pred :n-ary the-type) missing-argisas))))
              (t (let ((max-arg -1))
                   (dotimes (n 6)
                     (let ((arg-type (arg-isa pred (1+ n) :kb kb)))
                       (unless (or (eq arg-type :unknown)
                                   (not (collection? arg-type)))
                         (setq max-arg (1+ n)))))
                   (cond ((> max-arg -1)
                          (push (list pred max-arg) missing-arity))
                         (t (push (list pred nil) missing-arity))))))
    (when (eq pred-type :function)
      ;; Also need to check the result information
      ;; N.B. Cyc sometimes has more than one of these.
      (let ((the-result-types (retrieve (make-result-type pred '?type)
                                       :kb kb :response '?type
                                       :coverage :ground)))
        (unless (some #'(lambda (type) (collection? type))
                      the-result-types)
          (push pred missing-resultisas))))
    (values missing-arity missing-argisas missing-resultisas)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Make saved structural cache

(defun dump-structural-cache-for-kb (kb-path kb-name)
  ;; This function is for building the structural cache on a closed KB; if your
  ;; KB is open and you want to dump the current structural cache, use 
  ;; fire:dump-structural-cache.
  (format t "~%Dumping structural cache for ~A\\~A ..." kb-path kb-name)
  (format t "~%  Opening KB ...")
  (let ((kb (make-kb kb-path kb-name)))
    (unwind-protect
        (progn
          (format t "~%  Making the structural cache ...")
          (recompute-structural-cache :kb kb)
          (make-scache-files-writable kb)
          (dump-structural-cache :kb kb))
      (close-kb kb)
      (format t "~%Finished dumping structural cache for ~A~A." 
        kb-path kb-name)
      (format t "~%KB is closed.")
      :done)))

(defun make-scache-files-writable (kb)
  (let ((cache-files (directory (concatenate 'string (kb-resource-path kb) 
                                  "structural-cache.*"))))
    (dolist (fspec cache-files) 
      (gui-lib:make-file-writable-if-not fspec))
    cache-files))



;;;
;;; make-dumped-genls-cache is now deprecated -- use 
;;; dump-structural-cache-for-kb instead 
;;;
;;;(defun make-dumped-genls-cache (kb-path kb-name &key key-concepts)
;;;  ;; This function is for building the genls cache on a closed KB; if your
;;;  ;; KB is open and you want to dump the current genls-cache, use 
;;;  ;; dump-genls-cache.
;;;  (format t "~%Dumping genls-cache for ~A\\~A ..." kb-path kb-name)
;;;  (format t "~%  Opening KB ...")
;;;  (let ((kb (make-kb kb-path kb-name)))
;;;    (unwind-protect
;;;        (progn
;;;          (format t "~%  Touching the key concepts ...")
;;;          (dolist (col key-concepts)
;;;            (all-genls col :kb kb))
;;;          (format t "~%  Making the dumped cache ...")
;;;          (dump-genls-cache :kb kb))
;;;      (close-kb kb)
;;;      (format t "~%Finished dumping genls-cache for ~A~A." kb-path kb-name)
;;;      (format t "~%KB is closed.")
;;;      :done)))


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