;;;;-*- Mode:  LISP; Syntax: Common-lisp; Package: USER -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: jtms.lsp
;;;;    System: project
;;;;   Version: 176
;;;;    Author: Kenneth D. Forbus, Northwestern University
;;;;            Johan de Kleer, the Xerox Corportation.
;;;;   Purpose: Justification-based Truth Maintenence System (JTMS)
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Tuesday, January 18, 2005 at 20:20:42 by forbus
;;;; ---------------------------------------------------------------------------

;;; Copyright (c) 1986-1992, Kenneth D. Forbus, Northwestern University,
;;; and Johan de Kleer, 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)

;;; There are three central data structures:
;;;   - The JTMS itself.
;;;   - JTMS nodes, which contain a datum, sets of justifications,
;;;       and rules applicable to that node.
;;;   - Justification links, which link a particular node to 
;;;       a conjunctive set of antecedents.
;;;

(defstruct (jtms (:print-function print-jtms))
  "Justification-based Truth-Maintenance System definition"
  (title nil)                           
  (node-counter 0)             ;; Unique namer for nodes.
  (just-counter 0)             ;; Unique namer for justifications.
  (nodes nil)                  ;; list of all tms nodes.
  (justs nil)                  ;; list of all justifications
  (debugging nil)              ;; Debugging flag
  (contradictions nil)         ;; list of contradiction nodes.
  (assumptions nil)            ;; list of assumption nodes.
  (checking-contradictions t)  ;; For external systems--turns off checking.
  (node-string nil)            ;; Procedure which prints node as string.
  (contradiction-handler nil)  ;; Procedure which handles contradictions.
  (enqueue-procedure nil))     ;; Procedure called when some nodes become in.

(defun print-jtms (jtms stream ignore)
  (declare (ignore ignore))
  (format stream "#<JTMS: ~A>" (jtms-title jtms)))

(defstruct (tms-node (:print-function print-tms-node))
  "Single node within the TMS."
  (index 0)             ;; Unique identifier for node.
  (datum nil)           ;; Pointer to external problem solver
  (label :out)          ;; :in means believed, :out means disbelieved
  (support nil)         ;; Current justification or premise marker
  (justs nil)           ;; Possible justifications
  (consequences nil)    ;; Justifications in which it is an antecedent
  (mark nil)            ;; Marker for sweep algorithms
  (contradictory? nil)  ;; Flag marking it as contradictory
  (assumption? nil)     ;; Flag marking it as an assumption.
  (in-rules nil)        ;; Rules that should be triggered when node goes in
  (out-rules nil)       ;; Rules that should be triggered when node goes out
  (jtms nil))           ;; The JTMS in which this node appears.

(defun print-tms-node (node stream ignore)
  (declare (ignore ignore))
  (format stream "#<Node: ~A>" (node-string node)))

(defstruct (just (:print-function print-just))
  "A justification link within the TMS."
  (index 0)    ;; Unique identifier.
  informant    ;; Description of the justification.
  consequence  ;; Node this justification supports.
  antecedents) ;; Nodes that, if all IN, support this justification.

(defun print-just (just stream ignore)
  (declare (ignore ignore))
  (format stream "#<Just ~D>" (just-index just)))

(defun tms-node-premise? (node &aux support)
  "Is this node a premise, and not an assumption?"
  (and (setq support (tms-node-support node))
       (not (eq support :enabled-assumption))
       (null (just-antecedents support))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Simple utilities:

(defun node-string (node)
  "Print node as string."
  (funcall (jtms-node-string (tms-node-jtms node)) node))

(defmacro debugging-jtms (jtms msg &optional node &rest args)
  "Print message whenever debugging is turned on in <jtms>."
  `(when (jtms-debugging ,jtms)
     (format *trace-output* ,msg (if ,node (node-string ,node)) ,@args)))

(defun tms-error (string node)
   "Print error message for particular TMS node."
   (error string (node-string node)))

(defun default-node-string (n) (format nil "~A" (tms-node-datum n)))

(defun create-jtms (title &key (node-string 'default-node-string)
                               debugging
                               (checking-contradictions t)
                               (contradiction-handler 'ask-user-handler)
                               enqueue-procedure)
  "Create and return a new JTMS with the given title and fields."
  (make-jtms :title title
             :node-string node-string
             :debugging debugging
             :checking-contradictions checking-contradictions
             :contradiction-handler contradiction-handler
             :enqueue-procedure enqueue-procedure
             ))
             
(defun change-jtms (jtms &key contradiction-handler node-string
                              enqueue-procedure debugging
                              checking-contradictions)
  "Change the settings on the given JTMS."
  (if node-string (setf (jtms-node-string jtms) node-string))
  (if debugging (setf (jtms-debugging jtms) debugging))
  (if checking-contradictions
      (setf (jtms-checking-contradictions jtms) checking-contradictions))
  (if contradiction-handler
      (setf (jtms-contradiction-handler jtms) contradiction-handler))
  (if enqueue-procedure
      (setf (jtms-enqueue-procedure jtms) enqueue-procedure)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Basic inference-engine interface.

(defun in-node? (node) 
   "Non-nil if the given node is labeled in (i.e., true)."
   (eq (tms-node-label node) :in))

(defun out-node? (node) 
   "Non-nil if the given node is labeled out (i.e., false or unknown)."
   (eq (tms-node-label node) :out))

(defun tms-create-node (jtms datum &key assumptionp contradictoryp)
  "Create and return TMS node for fact <datum>."
  (let ((node (make-tms-node :index (incf (jtms-node-counter jtms))
                             :datum datum
                             :assumption? assumptionp
                             :contradictory? contradictoryp
                             :jtms jtms)))
    (if assumptionp (push node (jtms-assumptions jtms)))
    (if contradictoryp (push node (jtms-contradictions jtms)))
    (push node (jtms-nodes jtms))
    node))

(defun assume-node (node &aux (jtms (tms-node-jtms node)))
  "Convert regular node to an assumption and enable it."
  (unless (tms-node-assumption? node)
    (debugging-jtms jtms "~%Converting ~A into an assumption" node)
    (setf (tms-node-assumption? node) t))
  (enable-assumption node))

(defun make-contradiction (node &aux (jtms (tms-node-jtms node)))
  "Mark node as contradiction node."
  (unless (tms-node-contradictory? node)
    (setf (tms-node-contradictory? node) t)
    (push node (jtms-contradictions jtms))
    (check-for-contradictions jtms)))

(defun justify-node (informant consequence antecedents &aux just jtms)
  "Add justification link between given antecedents and a consequent."
  ;; Build a justification object, and use it to link the antecents
  ;;   to the consequent.
  (setq jtms (tms-node-jtms consequence)
        just (make-just :index (incf (jtms-just-counter jtms))
                        :informant informant
                        :consequence consequence
                        :antecedents antecedents))
  (push just (tms-node-justs consequence))
  (dolist (node antecedents) (push just (tms-node-consequences node)))
  (push just (jtms-justs jtms))
  (debugging-jtms jtms
                  "~%Justifying ~A by ~A using ~A."
                  consequence informant (mapcar #'node-string antecedents))
  ;; Install new support structure if needed.
  (if (or antecedents (out-node? consequence))
      (if (check-justification just) (install-support consequence just))
      (setf (tms-node-support consequence) just))
  (check-for-contradictions jtms))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Support for adding justifications

(defun check-justification (just)
  "Returns t if justification can be changed to IN."
  (and (out-node? (just-consequence just))
       (justification-satisfied? just)))

(defun justification-satisfied? (just)
  "Is every antecedent of this justification in?"
  (every #'in-node? (just-antecedents just)))

(defun install-support (conseq just)
  "Make node <conseq> IN, and propagate in-ness to its consequences."
  (make-node-in conseq just)
  (propagate-inness conseq))

(defun propagate-inness (node &aux (jtms (tms-node-jtms node)) (q (list node)))
  "Given newly IN node, progate IN label to consequents that are now
  supported."
  (do () ((null (setq node (pop q))))
    (debugging-jtms jtms "~%   Propagating belief in ~A." node)
    (dolist (justification (tms-node-consequences node))
      (when (check-justification justification)
        (make-node-in (just-consequence justification) justification)
        (push (just-consequence justification) q)))))

(defun make-node-in (conseq reason &aux jtms enqueuef)
  "Make node <conseq> IN for given reason."
  (setq jtms (tms-node-jtms conseq)
        enqueuef (jtms-enqueue-procedure jtms))
  (debugging-jtms jtms "~%     Making ~A in via ~A."
    conseq
    (if (symbolp reason)
       reason
       (cons (just-informant reason)
         (mapcar (jtms-node-string jtms)
           (just-antecedents reason)))))
   (setf (tms-node-label conseq) :in)
   (setf (tms-node-support conseq) reason)
   (when enqueuef
      (dolist (in-rule (tms-node-in-rules conseq))
         (funcall enqueuef in-rule))
      (setf (tms-node-in-rules conseq) nil)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Assumption Manipulation
(defun retract-assumption (node &aux jtms)
  "Retract (assume :out) this assumption node."
  (when (eq (tms-node-support node) :enabled-assumption)
    (setq jtms (tms-node-jtms node))
    (debugging-jtms jtms "~%  Retracting assumption ~A." node)
    (make-node-out node)
    (find-alternative-support jtms (cons node (propagate-outness node jtms)))))

(defun enable-assumption (node &aux (jtms (tms-node-jtms node)))
  "Enable (assume true) the fact in this node."
  (unless (tms-node-assumption? node) 
    (tms-error "Can't enable the non-assumption ~A" node))
  (debugging-jtms jtms "~%  Enabling assumption ~A." node)
  (cond ((out-node? node) (make-node-in node :enabled-assumption)
                          (propagate-inness node))
        ((or (eq (tms-node-support node) :enabled-assumption)
             (null (just-antecedents (tms-node-support node)))))
        (t (setf (tms-node-support node) :enabled-assumption)))
  (check-for-contradictions jtms))

(defun make-node-out (node &aux jtms enqueuef)
  "Label node OUT, remove support, and fire any out-rules."
  (setq jtms (tms-node-jtms node)
        enqueuef (jtms-enqueue-procedure jtms))
  (debugging-jtms jtms "~%     retracting belief in ~a." node)
  (setf (tms-node-support node) nil)
  (setf (tms-node-label node) :out)
  (if enqueuef (dolist (out-rule (tms-node-out-rules node)) 
                 (funcall enqueuef out-rule)))
  (setf (tms-node-out-rules node) nil))

(defun propagate-outness (node jtms &aux out-queue)
  "Given newly retracted node, propagate OUT label to those nodes
  now no longer supported."
  (debugging-jtms jtms "~%   Propagating disbelief in ~A." node)
  (do ((js (tms-node-consequences node) (append (cdr js) new))
       (new nil nil)
       (conseq nil))
      ((null js) out-queue)
    ;;For each justification using the node, check to see if
    ;;it supports some other node.  If so, forget that node,
    ;;queue up the node to look for other support, and recurse
    (setq conseq (just-consequence (car js)))
    (when (eq (tms-node-support conseq) (car js)) 
      (make-node-out conseq)
      (push conseq out-queue)
      (setq new (tms-node-consequences conseq)))))

(defun find-alternative-support (jtms out-queue)
  "Given list out newly OUT nodes, attempt to find alternate support to bring
  back IN.."
  (debugging-jtms jtms "~%   Looking for alternative supports.")
  (dolist (node out-queue)
    (unless (in-node? node)
      (dolist (just (tms-node-justs node))
        (when (check-justification just)
          (install-support (just-consequence just)
                                 just)
          (return just))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Contradiction handling interface
(defun check-for-contradictions (jtms &aux contradictions)
  "Determine if a contradiction is now IN, and fire handler if so."
  (when (jtms-checking-contradictions jtms)
    (dolist (cnode (jtms-contradictions jtms))
      (if (in-node? cnode) (push cnode contradictions)))
    (if contradictions
        (funcall (jtms-contradiction-handler jtms) jtms contradictions))))

(defmacro without-contradiction-check (jtms &body body)
  "Within extent, do not check for contradictions."
  (contradiction-check jtms nil body))

(defmacro with-contradiction-check (jtms &body body)
  "Within extent, check for contradictions." 
  (contradiction-check jtms t body))

(defun contradiction-check (jtms flag body)
  (let ((jtmsv (gensym)) (old-value (gensym)))
    `(let* ((,jtmsv ,jtms)
            (,old-value (jtms-checking-contradictions ,jtmsv)))
       (unwind-protect
           (progn (setf (jtms-checking-contradictions ,jtmsv) ,flag) ,@body)
         (setf (jtms-checking-contradictions ,jtmsv) ,old-value)))))

(defmacro with-contradiction-handler (jtms handler &body body)
  "Within extent, reset contradiction handler to <handler>."
  (let ((jtmsv (gensym)) (old-handler (gensym)))
    `(let* ((,jtmsv ,jtms)
            (,old-handler (jtms-contradiction-handler ,jtmsv)))
     (unwind-protect
         (progn (setf (jtms-contradiction-handler ,jtmsv) ,handler) ,@body)
       (setf (jtms-contradiction-handler ,jtmsv) ,old-handler)))))

(defun default-assumptions (jtms)
  (with-contradiction-check jtms
    (with-contradiction-handler jtms #'(lambda (&rest ignore)
                                         (declare (ignore ignore)) 
                                         (throw 'contradiction t))
      (dolist (assumption (jtms-assumptions jtms))
        (cond ((eq (tms-node-support assumption) :enabled-assumption))
              ((not (eq :default (tms-node-assumption? assumption))))
              ((catch 'contradiction (enable-assumption assumption))
               (retract-assumption assumption)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Well-founded support inqueries
(defun supporting-justification-for-node (node) 
  "Returns either :enabled-assumption if assumption, justification if IN node,
   or nil (if out node)."
  (tms-node-support node))

(defun assumptions-of-node (node &aux assumptions (marker (list :MARK)))
  "Returns the set of enabled assumptions underlying the well-founded
   support for a node."
  (do ((nodes (list node) (append (cdr nodes) new))
       (new nil nil))
      ((null nodes) assumptions)
    (let ((node (car nodes)))
      (cond ((eq (tms-node-mark node) marker))
            ((eq (tms-node-support node) :enabled-assumption)
             (push node assumptions))
            ((in-node? node)
             (setq new (just-antecedents (tms-node-support node)))))
      (setf (tms-node-mark node) marker))))

(defun enabled-assumptions (jtms &aux result)
  "Returns list of all enabled assumptions within the JTMS."
  (dolist (assumption (jtms-assumptions jtms) result)
    (if (eq (tms-node-support assumption) :enabled-assumption)
        (push assumption result))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Inference engine stub to allow this JTMS to be used stand alone
(defun why-node (node &aux justification)
   "Print reason why node is IN to standard output."
   (setq justification (tms-node-support node))
   (cond ((eq justification :enabled-assumption)
          (format t "~%~A is an enabled assumption" (node-string node)))
         (justification
           (format t "~%~A is IN via ~A on" (node-string node)
             (just-informant justification))
           (dolist (anode (just-antecedents justification))
              (format t "~%  ~A" (node-string anode))))
         (t (format t "~%~A is OUT." (node-string node))))
   node)

(defun why-nodes (jtms)
  "Print description of which nodes are IN or OUT, and why."
  (dolist (node (jtms-nodes jtms)) (why-node node)))

(eval-when (:execute :load-toplevel :compile-toplevel)
  (proclaim '(special *contra-assumptions*)))

(defun ask-user-handler (jtms contradictions)
  "Default contradiction handler.  Asks user to resolve contradiction."
  (handle-one-contradiction (car contradictions))
  (check-for-contradictions jtms))

(defun handle-one-contradiction (contra-node
                                 &aux the-answer *contra-assumptions*)
  "Print list of contradictions, and retract one selected by user."
  (setq *contra-assumptions* (assumptions-of-node contra-node))
  (unless *contra-assumptions*
    (tms-error "~%There is a flaw in the universe...~A" contra-node))
  (format t "~%Contradiction found: ~A" (node-string contra-node))
  (print-contra-list *contra-assumptions*)
  (format t "~%Call (tms-answer <number>) to retract assumption.")
  (setq the-answer
        (catch 'tms-contradiction-handler
          (break "JTMS contradiction break")))
  (if (and (integerp the-answer)
           (> the-answer 0)
           (not (> the-answer (length *contra-assumptions*))))
      (retract-assumption (nth (1- the-answer)
                               *contra-assumptions*))))

(defun print-contra-list (nodes)
  (do ((counter 1 (1+ counter))
       (nn nodes (cdr nn)))
      ((null nn))
    (format t "~%~A ~A" counter
            (node-string (car nn)))))

(defun tms-answer (num)
  (if (integerp num)
      (if (> num 0)
          (if (not (> num (length *contra-assumptions*)))
              (throw 'tms-contradiction-handler num)
              (format t "~%Ignoring answer, too big."))
          (format t "~%Ignoring answer, too small"))
      (format t "~%Ignoring answer, must be an integer.")))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun explore-network (node)
  "Allows user to traverse dependency network interactively."
  (unless (in-node? node)
          (format t "~% Sorry, ~A not believed." (node-string node))
          (return-from explore-network node))
  (do ((stack nil)
       (current node)
       (options nil)
       (olen 0)
       (done? nil))
      (done? current)
      (why-node current)
      (setq options (if (typep (tms-node-support current) 'just)
                        (just-antecedents (tms-node-support current))))
      (setq olen (length options))
      (do ((good? nil)
           (choice 0))
          (good? (case good?
                       (q (return-from explore-network current))
                       (0 (if stack
                              (setq current (pop stack))
                              (return-from explore-network current)))
                       (t (push current stack)
                          (setq current (nth (1- good?) options)))))
          (format t "~%>>>")
          (setq choice (read))
          (cond ((or (eq choice 'q)
                     (and (integerp choice)
                          (not (> choice olen))
                          (not (< choice 0))))
                 (setq good? choice))
                (t (format t
                    "~% Must be q or an integer from 0 to ~D."
                    olen))))))