;; -*- Mode: Lisp; -*-

;;;; Database for Tiny Rule Engine using JTMS
;;;; Last Edited 7/1/92, by KDF

;; Copyright (c) 1989, 1990, 1991 Kenneth D. Forbus, Northwestern University,
;; and Johan de Kleer and the Xerox Corporation.
;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(in-package :cl-user)

;;;; Database structure and contents

(defstruct (dbclass (:print-function jtre-dbclass-printer))
  "Database index class."
  name    ; Corresponding symbol
  jtre    ; JTRE it is part of.
  facts   ; Associated facts
  rules)  ; Associated rules

(defun jtre-dbclass-printer (r st ignore)
   (declare (ignore ignore))
   (format st "<Dbclass ~A>" (dbclass-name r)))

(defstruct (datum (:print-function jtre-datum-printer))
  "Datum or fact in database."
  id                   ; Unique ID for easy lookup
  lisp-form            ; Expression for pattern-matching
  (tms-node nil)       ; Pointer into TMS
  dbclass              ; Dbclass of the corresponding pattern
  (assumption? nil)    ; If non-nil, indicates informant
  (plist nil))         ; Local property list

(defun jtre-datum-printer (d st ignore)
  (declare (ignore ignore))
  (format st "<Datum ~D>" (datum-id d)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Making statements

(defun assert! (fact just &optional (*jtre* *jtre*) &aux datum node)
  "Assert fact into the JTRE."
  (setq datum (referent fact t)      ;; Create datum if needed,
        node (datum-tms-node datum)) ;;   with corresponding node.
  (unless (listp just) (setq just (list just)))
  (debugging-jtre "~%    Asserting ~A via ~A." fact just)
  ;; Create justification link between fact and antecendents.
  (justify-node (car just) node
                (mapcar #'(lambda (f) (datum-tms-node (referent f t)))
                        (cdr just)))
  datum)

(defmacro rassert! (fact just)
  "Assert fact (adding any needed quoting of symbols)."
  `(assert! ,(quotize fact) ,(quotize just)))

(defun quiet-assert! (fact just &optional (*jtre* *jtre*))
  "Assert fact, omitting usual contradiction checking."
  (without-contradiction-check (jtre-jtms *jtre*) (assert! fact just)))

(defun assume! (fact reason &optional (*jtre* *jtre*) &aux datum node)
  "Assume fact and label IN."
  (setq datum (referent fact t)
        node (datum-tms-node datum))
  (cond ((not (datum-assumption? datum))
         (setf (datum-assumption? datum) reason)
         (debugging-jtre "~%    Assuming ~A via ~A." fact reason)
         (assume-node node)
         (enable-assumption node))
        ((eq reason (datum-assumption? datum)))
        (t (error
            "Fact ~A assumed because of ~A assumed again because of ~A"
            (show-datum datum) (datum-assumption? datum) reason)))
  datum)

(defun already-assumed? (fact) 
  "Has given fact already been assumed?"
  (datum-assumption? (referent fact t)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Retraction

(defun retract! (fact &optional (just 'user) (quiet? nil)
                      (*jtre* *jtre*) &aux datum node)
  "Retract fact from JTRE."
  (setq datum (referent fact t)
        node (datum-tms-node datum))
  (cond ((not (tms-node-assumption? node))
         (unless quiet?
           (format t "~%~A isn't an assumption."
                   (show-datum datum))))
        ((not (in-node? node))
         (unless quiet?
           (format t
             "~%The assumption ~A is not currently in."
             fact)))
        ((eq just (datum-assumption? datum))
         (debugging-jtre "~%    Retracting ~A via ~A."
                         fact just)
         (setf (datum-assumption? datum) nil)
         (retract-assumption node))
        ((not quiet?)
         (format t "~%~A not source of assumption for ~A"
                 just fact)))
  node)

(defmacro rretract! (fact &optional (just 'user))
  `(retract! ,(quotize fact) ,(quotize just)))

(defun contradiction (fact &optional (*jtre* *jtre*))
  "Make node for this fact into a contradiction."
  (make-contradiction (datum-tms-node (referent fact t))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Interface and display of data

(defun in? (fact &optional (*jtre* *jtre*) &aux r)
  "Is the given fact labeled IN?"
  (when (setq r (referent fact))
        (in-node? (datum-tms-node r))))

(defun out? (fact &optional (*jtre* *jtre*) &aux r)
  "Is the given fact labeled OUT?"
  (when (setq r (referent fact))
        (out-node? (datum-tms-node r))))
    
(defun why? (fact &optional (*jtre* *jtre*) &aux r)
  "Describe why this node is IN or OUT."
  (when (setq r (referent fact))
        (why-node (datum-tms-node r))))

(defun assumptions-of (fact &optional (*jtre* *jtre*))
  (mapcar #'view-node 
          (assumptions-of-node
           (datum-tms-node (referent fact *jtre* t)))))

(defun fetch (pattern &optional (*jtre* *jtre*) &aux bindings unifiers)
  "Fetch all facts from JTRE database which match <pattern>."
  (dolist (candidate (get-candidates pattern) unifiers)
    (setq bindings (unify pattern (datum-lisp-form candidate)))
    (unless (eq bindings :fail)
      (push (sublis bindings pattern) unifiers))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; More display-intensive procedures

(defun wfs (fact &optional (*jtre* *jtre*))
  "Displays well-founded support for a fact."
  (cond ((out? fact) (format t "~% ~A is OUT." fact))
        (t (do ((queue (list (get-tms-node fact))
                       (nconc (cdr queue) new-antes))
                (so-far (list (get-tms-node fact)))
                (new-antes nil nil))
               ((null queue) (format t "~%--------") fact)
             (why-node (car queue))
             (unless (or (out-node? (car queue))
                         (tms-node-assumption? (car queue)))
               ;; Go down the support
               (dolist (ante (just-antecedents
                              (tms-node-support (car queue))))
                 (unless (member ante so-far)
                   (push ante so-far)
                   (push ante new-antes))))))))

(defun say-datum-belief (pr &optional (*jtre* *jtre*) (indent ""))
  "Print belief state for this fact."
  (format t "~%~A~A: ~A" indent pr
    (if (in-node? (get-tms-node pr *jtre*))
       "IN" "OUT")))

(defun show-justifications (fact &optional (*jtre* *jtre*))
  (format t "~% ~A::" fact)
  (let* ((node (get-tms-node fact *jtre*))
         (justs (tms-node-justs node)))
    (unless justs
            (format t " No justifications.")
            (return-from show-justifications node))
    (dolist (j justs)
            (format t "~% ~A" (just-informant j))
            (cond ((just-antecedents j) 
                   (format t ", on:")
                   (dolist (ante (just-antecedents j))
                           (say-datum-belief
                            (view-node ante) *jtre* "  "))
                   (format t "."))
                  (t (format t "."))))))

(defun show-data (&optional (*jtre* *jtre*)
                            (stream *standard-output*))
  "Display list of facts to stream, along with each fact's belief state."
  (format stream 
          "~%~D facts total." (jtre-datum-counter *jtre*))
  (map-dbclass
   #'(lambda (dbclass)
       (dolist (datum (dbclass-facts dbclass))
               (format stream "~%~A: ~A" (show-datum datum)
                       (if (in-node? (datum-tms-node datum))
                           "IN" "OUT"))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Database system

(defun get-dbclass (fact &optional (*jtre* *jtre*) &aux dbclass)
  "Retrieve or create the DBClass for this fact."
  (cond ((null fact) (error "~% nil can't be a dbclass."))
        ((listp fact) (get-dbclass (car fact) *jtre*))
        ((variable? fact)
         (cond ((boundp fact)
                (get-dbclass (symbol-value fact) *jtre*))
               (t (error "~%Dbclass unbound: ~A" fact))))
        ((symbolp fact)
         (cond ((setq dbclass
                      (gethash fact
                               (jtre-dbclass-table *jtre*)))
                dbclass)
               (t (setq dbclass
                        (make-dbclass :name fact :facts nil
                                    :rules nil :jtre *jtre*))
                  (setf (gethash fact
                         (jtre-dbclass-table *jtre*))
                        dbclass)
                  dbclass)))
        (t (error "Bad dbclass type: ~A" fact))))

(defun referent (fact &optional (virtual? nil) (*jtre* *jtre*))
  "Returns the datum for this fact."
  (if virtual? (insert fact) (referent1 fact)))

(defun referent1 (fact)
  (dolist (candidate (dbclass-facts (get-dbclass fact)))
          (when (equal (datum-lisp-form candidate) fact)
                (return candidate))))

(defun insert (fact &aux datum)
  (setq datum (referent1 fact))
  (cond (datum (values datum t))
        (t (setq datum
                 (make-datum
                  :id (incf (jtre-datum-counter *jtre*))
                  :lisp-form fact
                  :dbclass (get-dbclass fact)))
           (setf (datum-tms-node datum)
                 (tms-create-node (jtre-jtms *jtre*) datum))
           (push datum (dbclass-facts (datum-dbclass datum)))
           (try-rules datum)
           (values datum nil))))
           

(defun get-candidates (pattern)
  "Retrieve set of potentially matching datums."
  (dbclass-facts (get-dbclass pattern)))

(defun map-dbclass (proc &optional (*jtre* *jtre*))
  "Call function on all dbclasses within JTRE."
  (maphash #'(lambda (name dbclass) (declare (ignore name))
               (funcall proc dbclass))
           (jtre-dbclass-table *jtre*)))

(defun get-tms-node (fact &optional (*jtre* *jtre*))
  "Return TMS node for this fact."
  (datum-tms-node (referent fact t)))

(defun view-node (node)
  "Return fact represented by this node."
  (datum-lisp-form (tms-node-datum node)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; More query routines

(defun show-datum (datum)
  (format nil "~A" (datum-lisp-form datum)))

(defun get-datum (num &optional (*jtre* *jtre*))
  "Retrieve datum from database using ID number."
  (map-dbclass
   #'(lambda (dbclass)
       (dolist (datum (dbclass-facts dbclass))
               (when (= (datum-id datum) num)
                     (return-from get-datum datum))))))

(defun get-just (num &optional (*jtre* *jtre*))
  "Retrieve justification link from JTRE using ID number."
  (dolist (just (jtms-justs (jtre-jtms *jtre*)))
    (when (= (just-index just) num)
          (return-from get-just just))))