#| -*-Scheme-*-

$Id$

Copyright 2006 Massachusetts Institute of Technology

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or (at
your option) any later version.

This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301,
USA.

|#

;;;; Simple truth-maintenance system

(declare (usual-integrations))

(define-record-type <tms>
    (tms:%make name event-handler contradiction)
    tms?
  (name tms:name)
  (event-handler tms:event-handler)
  (contradiction tms:contradiction tms:set-contradiction!))

(define (tms:make name event-handler)
  (let ((tms (tms:%make name event-handler #f)))
    (tms:set-contradiction! tms (tms:make-node tms 'contradiction))
    tms))

(define (tms:signal-event node justification)
  ((tms:event-handler (tms:node-tms node)) node justification))

(define-record-type <tms:node>
    (tms:%make-node tms datum supported? justifications consequents)
    tms:node?
  (tms tms:node-tms)
  (datum tms:node-datum)
  (supported? tms:node-supported? tms:set-node-supported?!)
  (justifications tms:node-justifications tms:set-node-justifications!)
  (consequents tms:node-consequents tms:set-node-consequents!))

(define (tms:make-node tms datum)
  (tms:%make-node tms datum #f '() '()))

(define (tms:node-is-contradiction? node)
  (eq? node (tms:contradiction (tms:node-tms node))))

;;;; Justifications

(define (unary-generic default-method)
  (let ((generic (make-generic-procedure 1)))
    (set-generic-procedure-default-generator!
     generic
     (lambda (procedure tags) default-method))
    generic))

(define (define-unary-record-method generic record-type method)
  (add-generic-procedure-generator
   generic
   (let ((record-tag (record-type-dispatch-tag record-type)))
     (lambda (procedure tags)
       (and (eq? (car tags) record-tag)
	    method)))))

(define tms:justification?
  (unary-generic
   (lambda (object) #f)))

(define tms:justification-consequent
  (unary-generic
   (lambda (object)
     (tms:not-justification object 'tms:justification-consequent))))

(define tms:justification-rule
  (unary-generic
   (lambda (object)
     (tms:not-justification object 'tms:justification-rule))))

(define tms:justification-antecedents
  (unary-generic
   (lambda (object)
     (tms:not-justification object 'tms:justification-antecedents))))

(define tms:justification-supported?
  (unary-generic
   (lambda (object)
     (tms:not-justification object 'tms:justification-supported?))))

(define (tms:not-justification object caller)
  (error:wrong-type-argument object "TMS justification" caller))

(define (tms:attach-justification just)
  (let ((node (tms:justification-consequent just)))
    (for-each (lambda (node)
		(let ((consequents (tms:node-consequents node)))
		  (if (not (memq node consequents))
		      (tms:set-node-consequents! node
						 (cons just consequents)))))
	      (tms:justification-antecedents just))
    (tms:set-node-justifications!
     node
     (cons just (tms:node-justifications node)))
    (if (tms:justification-supported? just)
	(tms:support-node node just))))

;;;; Justification of premises

(define-record-type <tms:premise-justification>
    (tms:make-premise-justification consequent supported?)
    tms:premise-justification?
  (consequent tms:premise-justification-consequent)
  (supported? tms:premise-justification-supported?
	      tms:set-premise-justification-supported?!))

(define (tms:new-premise node)
  (let ((just (tms:make-premise-justification node #t)))
    (tms:attach-justification just)
    just))

(define (tms:premise-justification node)
  (find-matching-item (tms:node-justifications node)
    tms:premise-justification?))

(define-unary-record-method tms:justification?
    <tms:premise-justification>
  (lambda (object) #t))

(define-unary-record-method tms:justification-consequent
    <tms:premise-justification>
  tms:premise-justification-consequent)

(define-unary-record-method tms:justification-rule
    <tms:premise-justification>
  (lambda (just) #f))

(define-unary-record-method tms:justification-antecedents
    <tms:premise-justification>
  (lambda (just) '()))

(define-unary-record-method tms:justification-supported?
    <tms:premise-justification>
  tms:premise-justification-supported?)

;;;; Justification by antecedents

(define-record-type <tms:conjunctive-justification>
    (tms:make-conjunctive-justification consequent rule antecedents)
    tms:conjunctive-justification?
  (consequent tms:conjunctive-justification-consequent)
  (rule tms:conjunctive-justification-rule)
  (antecedents tms:conjunctive-justification-antecedents))

(define (tms:justify-node consequent rule antecedents)
  (tms:attach-justification
   (tms:make-conjunctive-justification consequent rule antecedents)))

(define-unary-record-method tms:justification?
    <tms:conjunctive-justification>
  (lambda (object) #t))

(define-unary-record-method tms:justification-consequent
    <tms:conjunctive-justification>
  tms:conjunctive-justification-consequent)

(define-unary-record-method tms:justification-rule
    <tms:conjunctive-justification>
  tms:conjunctive-justification-rule)

(define-unary-record-method tms:justification-antecedents
    <tms:conjunctive-justification>
  tms:conjunctive-justification-antecedents)

(define-unary-record-method tms:justification-supported?
    <tms:conjunctive-justification>
  (lambda (just)
    (for-all? (tms:conjunctive-justification-antecedents just)
      tms:node-supported?)))

;;;; Adding support

(define (tms:node-assumed? node)
  (let ((just (tms:premise-justification node)))
    (and just
	 (tms:premise-justification-supported? just))))

(define (tms:assume-node node)
  (tms:support-node
   node
   (let ((just (tms:premise-justification node)))
     (if just
	 (begin
	   (tms:set-premise-justification-supported?! just #t)
	   just)
	 (tms:new-premise node)))))

(define (tms:support-node node justification)
  (if (not (tms:node-supported? node))
      (begin
	(tms:set-node-supported?! node #t)
	(tms:signal-event node justification)
	(for-each (lambda (just)
		    (if (tms:justification-supported? just)
			(tms:support-node (tms:justification-consequent just)
					  just)))
		  (tms:node-consequents node)))))

;;;; Removing support

(define (tms:retract-node node)
  (let ((just (tms:premise-justification node)))
    (if (not just)
	(error "Node not assumed, can't retract:" node))
    (tms:set-premise-justification-supported?! just #f)
    (if (tms:node-supported? node)
	(begin
	  (tms:set-node-supported?! node #f)
	  (tms:signal-event node #f)
	  (tms:re-support-nodes (tms:propagate-node-retractions node))))))

(define (tms:propagate-node-retractions node)
  (append-map (lambda (just)
		(if (tms:justification-supported? just)
		    '()
		    (tms:propagate-just-retractions just)))
	      (tms:node-consequents node)))

(define (tms:propagate-just-retractions just)
  (let ((node (tms:justification-consequent just)))
    (if (tms:node-supported? node)
	(begin
	  (tms:set-node-supported?! node #f)
	  (cons node (tms:propagate-node-retractions node)))
	'())))

(define (tms:re-support-nodes retracted)
  (let loop ((nodes retracted) (new-support? #f) (unsupported '()))
    (cond ((pair? nodes)
	   (let ((node (car nodes))
		 (nodes (cdr nodes)))
	     (cond ((tms:node-supported? node)
		    (loop nodes new-support? unsupported))
		   ((there-exists? (tms:node-justifications node)
		      tms:justification-supported?)
		    (tms:re-support-node node)
		    (loop nodes #t unsupported))
		   (else
		    (loop nodes new-support? (cons node unsupported))))))
	  (new-support?
	   (tms:re-support-nodes unsupported))
	  (else
	   (for-each (lambda (node)
		       (tms:signal-event node #f))
		     unsupported)))))

(define (tms:re-support-node node)
  (if (not (tms:node-supported? node))
      (begin
	(tms:set-node-supported?! node #t)
	(for-each (lambda (just)
		    (if (tms:justification-supported? just)
			(tms:re-support-node
			 (tms:justification-consequent just))))
		  (tms:node-consequents node)))))
	   

;;;; Printing proofs

(define (tms:why? node #!optional port)
  (tms:walk-node-support node
    (lambda (consequent just antecedents)
      (tms:write-comment
       (cons (tms:node-name consequent)
	     (cond ((tms:premise-justification? just) '(premise))
		   (else
		    `(<==
		      (,(or (tms:justification-rule just) just)
		       ,@(map tms:node-name antecedents))))))
       port))))

(define (tms:walk-node-support node procedure)
  (let ((n-tree (tms:node-support-tree node)))
    (if (not n-tree)
	(error:bad-range-argument node 'tms:walk-support-proof))
    (let ((queue (make-queue))
	  (seen (make-eq-hash-table)))
      (let ((maybe-enqueue
	     (lambda (n-tree)
	       (hash-table/intern! seen (car n-tree)
		 (lambda ()
		   (enqueue! queue n-tree)
		   #t)))))
	(maybe-enqueue n-tree)
	(do ()
	    ((queue-empty? queue) unspecific)
	  (let ((n-tree (dequeue! queue)))
	    (if (pair? (cdr n-tree))
		(let ((consequent (car n-tree))
		      (j-tree (cadr n-tree)))
		  (if (pair? j-tree)
		      (begin
			(procedure consequent
				   (car j-tree)
				   (map car (cdr j-tree)))
			(for-each maybe-enqueue (cdr j-tree))))))))))))

(define (tms:node-support-tree node)
  (let ((tms (tms:node-tms node)))

    (define (walk-node node seen)
      ;; Returns #F or an n-tree.
      (if (memq node seen)
	  #f
	  (let ((j-trees
		 (delq! #f
			(map (let ((seen (cons node seen)))
			       (lambda (just)
				 (walk-just just seen)))
			     (tms:node-justifications node)))))
	    (and (pair? j-trees)
		 (cons node j-trees)))))

    (define (walk-just just seen)
      ;; Returns #F or a j-tree.
      (if (tms:premise-justification? just)
	  (and (tms:premise-justification-supported? just)
	       (cons just '()))
	  (let ((n-trees
		 (map (lambda (node)
			(walk-node node seen))
		      (tms:justification-antecedents just))))
	    (and (for-all? n-trees (lambda (x) x))
		 (cons just n-trees)))))

    (walk-node node '())))

(define (tms:node-name node)
  (list (symbol 'n (object-hash node))
	'=
	(tms:node-datum node)))

(define (tms:write-comment object #!optional port)
  (write-char #\; port)
  (write object port)
  (newline port))

#|
(define tms
  (tms:make "n"
	    (lambda (node justification)
	      (tms:write-comment
	       `(,(if justification 'supported 'unsupported)
		 ,(tms:node-name node))))))

(define a (tms:make-node tms 'A))
(define b (tms:make-node tms 'B))
(define c (tms:make-node tms 'C))
(define d (tms:make-node tms 'D))
(define e (tms:make-node tms 'E))
(define f (tms:make-node tms 'F))
(define g (tms:make-node tms 'G))
(define h (tms:make-node tms 'H))
(define i (tms:make-node tms 'I))

(tms:justify-node e 'MP (list a b))
(tms:justify-node e 'X (list c))
(tms:justify-node g 'Y (list e))
(tms:justify-node h 'Z (list e f))
(tms:justify-node f 'W (list c d))

(tms:assume-node c)
;(supported (n78 = c))
;(supported (n79 = e))
;(supported (n80 = g))
;Unspecified return value

(tms:node-supported? c)
;Value: #t

(tms:node-supported? e)
;Value: #t

(tms:why? g)
;((n80 = g) <== (y (n79 = e)))
;((n79 = e) <== (x (n78 = c)))
;((n78 = c) premise)
;Unspecified return value

(tms:retract-node c)
;(unsupported (n78 = c))
;(unsupported (n80 = g))
;(unsupported (n79 = e))
;Unspecified return value

(tms:assume-node a)
;(supported (n81 = a))
;Unspecified return value

(tms:assume-node b)
;(supported (n82 = b))
;(supported (n79 = e))
;(supported (n80 = g))
;Unspecified return value

(tms:assume-node c)
;(supported (n78 = c))
;Unspecified return value

(tms:assume-node d)
;(supported (n83 = d))
;(supported (n84 = f))
;(supported (n85 = h))
;Unspecified return value

(tms:retract-node a)
;(unsupported (n81 = a))
;Unspecified return value

(tms:why? h)
;((n85 = h) <== (z (n79 = e) (n84 = f)))
;((n79 = e) <== (x (n78 = c)))
;((n84 = f) <== (w (n78 = c) (n83 = d)))
;((n78 = c) premise)
;((n83 = d) premise)
;Unspecified return value

(tms:retract-node d)
;(unsupported (n83 = d))
;(unsupported (n85 = h))
;(unsupported (n84 = f))
;Unspecified return value

(tms:justify-node i 'U (list f))
;Unspecified return value

(tms:justify-node i 'Q (list g))
;(supported (n86 = i))
;Unspecified return value

(tms:justify-node d 'R (list i))
;(supported (n83 = d))
;(supported (n84 = f))
;(supported (n85 = h))
;Unspecified return value

(tms:why? h)
;((n85 = h) <== (z (n79 = e) (n84 = f)))
;((n79 = e) <== (x (n78 = c)))
;((n84 = f) <== (w (n78 = c) (n83 = d)))
;((n78 = c) premise)
;((n83 = d) <== (r (n86 = i)))
;((n86 = i) <== (q (n80 = g)))
;((n80 = g) <== (y (n79 = e)))
;Unspecified return value

(tms:retract-node c)
;(unsupported (n78 = c))
;(unsupported (n85 = h))
;(unsupported (n84 = f))
;(unsupported (n83 = d))
;(unsupported (n86 = i))
;(unsupported (n80 = g))
;(unsupported (n79 = e))
;Unspecified return value

(tms:assume-node a)
;(supported (n81 = a))
;(supported (n79 = e))
;(supported (n80 = g))
;(supported (n86 = i))
;(supported (n83 = d))
;Unspecified return value

(tms:why? d)
;((n83 = d) <== (r (n86 = i)))
;((n86 = i) <== (q (n80 = g)))
;((n80 = g) <== (y (n79 = e)))
;((n79 = e) <== (mp (n81 = a) (n82 = b)))
;((n81 = a) premise)
;((n82 = b) premise)
;Unspecified return value

(tms:assume-node c)
;(supported (n78 = c))
;(supported (n84 = f))
;(supported (n85 = h))
;Unspecified return value

(tms:retract-node c)
;(unsupported (n78 = c))
;(unsupported (n84 = f))
;(unsupported (n85 = h))
;Unspecified return value

|#

;;; Edwin Variables:
;;; lisp-indent/define-unary-record-method: 2
;;; End: