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

;;;; LTRE definitions  
;;;; Last edited 1/29/93, by KDF

;;; Copyright 1986, 1989, 1990, 1991 Kenneth D. Forbus, 
;;; Nortwestern University, and Johan de Kleer, 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)

(defstruct (ltre (:print-function ltre-print-procedure))
  title                   ; Pretty name
  ltms                    ; Pointer to its LTMS
  (dbclass-table nil)       ; Hash table of dbclasses
  (datum-counter 0)       ; Unique ID for asserts
  (rule-counter 0)        ; Unique ID for rules
  (debugging nil)         ; Show basic operations
  (queue nil)             ; Queue for rules
  (rules-run 0))          ; Statistics

;; The RULES field of LTREs has been eliminated, since the same
;; information can be reconstructed from the dbclass tables.

(defun ltre-print-procedure (l st ignore)
  (declare (ignore ignore))
  (format st "<LTRE: ~A>" (ltre-title l)))

(defvar *ltre* nil) ;; Default LTRE
;;; The binding of this symbol is used inside rules and various
;;; macros to specify which LTRE a rule or fact should be stored in.
;;; The next few procedures encapsulate this choice

(defmacro with-ltre (ltre &rest forms)
  `(let ((*ltre* ,ltre)) ,@ forms))

(defun in-ltre (ltre) (setq *ltre* ltre)) ;; Analogy with in-package

(defmacro debugging-ltre (msg &rest args)
  `(when (ltre-debugging *ltre*) (format t ,msg  ,@args)))

(defun create-ltre (title &key debugging)
   (let ((l (make-ltre :title title 
               :ltms (create-ltms (list :ltms-OF title) 
                        :node-string 'make-node-string
                        :cache-datums? nil)
	   :dbclass-table (make-hash-table)
	   :debugging debugging)))
   (change-ltms (ltre-ltms l)
		:enqueue-procedure
		#'(lambda (pair) (enqueue pair l)))
   (setq *ltre* l)))

(defun change-ltre (ltre &key (debugging nil debugging?))
  (if debugging? (setf (ltre-debugging ltre) debugging)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Running LTRE

(defun uassert! (fact &optional (just 'user) (*ltre* *ltre*))
  (assert! fact just) ;; Do internal operation
  (run-rules *ltre*))        ;; Run the rules

(defun uassume! (fact reason &optional (*ltre* *ltre*)) 
  (assume! fact reason)
  (run-rules *ltre*))

(defun run-forms (forms &optional (*ltre* *ltre*))
  (dolist (form forms) (eval form) (run-rules *ltre*)))

(defun run (&optional (*ltre* *ltre*)) ;; Toplevel driver function
    (format t "~%>>")
    (do ((form (read) (read)))
        ((member form '(quit stop exit abort)) nil)
        (format t "~%~A" (eval form))
        (run-rules)
        (format t "~%>>")))

(defun show (&optional (*ltre* *ltre*) (stream *standard-output*))
  (format stream "For LTRE ~A:" (ltre-title *ltre*)) 
  (show-data *ltre* stream) (show-rules *ltre* stream))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Some debugging stuff

(defun show-by-informant (informant &optional (*ltre* *ltre*)
				    &aux (count 0))
  (dolist (clause (ltms-clauses (ltre-ltms *ltre*)) count)
	  (when (if (listp (clause-informant clause))
		    (eq (third (clause-informant clause)) informant)
		  (eq (clause-informant clause) informant))
		(incf count)
		(pprint (view-clause clause)))))

(defun view-clause (cl)
  (cons 'or (mapcar #'(lambda (x)
			 (if (eq (cdr x) :false) `(not ,(view-node (car x)))
			   (view-node (car x))))
		    (clause-literals cl))))