#| -*-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-hypotheses
  (unary-generic
   (lambda (object)
     (tms:not-justification object 'tms:justification-hypotheses))))

(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) 'premise))

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

(define-unary-record-method tms:justification-hypotheses
    <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-hypotheses
    <tms:conjunctive-justification>
  (lambda (just) '()))

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

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

(define (tms:conditional-justification consequent rule antecedents hypotheses)
  (tms:attach-justification
   (tms:make-conditional-justification consequent
				       rule
				       antecedents
				       hypotheses)))

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

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

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

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

(define-unary-record-method tms:justification-hypotheses
    <tms:conditional-justification>
  tms:conditional-justification-hypotheses)

(define-unary-record-method tms:justification-supported?
    <tms:conditional-justification>
  (lambda (just)
    (if (for-all? (tms:conditional-justification-hypotheses just)
	  tms:node-supported?)
	(for-all? (tms:conditional-justification-antecedents just)
	  tms:node-supported?)
	(tms:justification-has-well-founded-support? just))))

;;;; 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)))))

;;;; Analyzing support

(define (tms:node-has-well-founded-support? node)
  (tms:nhwfs? node '() '()))

(define (tms:justification-has-well-founded-support? just)
  (tms:jhwfs? just '() '()))

(define (tms:nhwfs? node seen hypotheses)
  (cond ((memq node seen) #f)
	((memq node hypotheses) #t)
	(else
	 (there-exists? (tms:node-justifications node)
	   (let ((seen (cons node seen)))
	     (lambda (just)
	       (tms:jhwfs? just seen hypotheses)))))))

(define (tms:jhwfs? just seen hypotheses)
  (if (tms:premise-justification? just)
      (tms:premise-justification-supported? just)
      (let ((hypotheses
	     (eqv-union (tms:justification-hypotheses just) hypotheses)))
	(for-all? (tms:justification-antecedents just)
	  (lambda (node)
	    (tms:nhwfs? node seen hypotheses))))))

(define (tms:node-supporting-assumptions node)
  (let ((n-tree (tms:node-support-tree node)))
    (and n-tree
	 (vector-ref n-tree 2))))

(define (tms:node-support-tree node)
  (let ((tms (tms:node-tms node)))

    (define (walk-node node seen)
      ;; Returns #F or an n-tree.
      (let ((seen (cons node seen)))
	(let loop
	    ((justs (tms:node-justifications node))
	     (j-trees '())
	     (support '()))
	  (if (pair? justs)
	      (let* ((just (car justs))
		     (j-tree
		      (if (tms:premise-justification? just)
			  (and (tms:premise-justification-supported? just)
			       (vector just '() (list node)))
			  (walk-just just seen))))
		(if j-tree
		    (loop (cdr justs)
			  (cons j-tree j-trees)
			  (eqv-union-2 (vector-ref j-tree 2) support))
		    (loop (cdr justs)
			  j-trees
			  support)))
	      (and (pair? j-trees)
		   (vector node (reverse! j-trees) support))))))

    (define (walk-just just seen)
      ;; Returns #F or a j-tree.
      (let loop
	  ((nodes (tms:justification-antecedents just))
	   (n-trees '())
	   (support '()))
	(if (pair? nodes)
	    (and (not (memq (car nodes) seen))
		 (let ((n-tree (walk-node (car nodes) seen)))
		   (and n-tree
			(loop (cdr nodes)
			      (cons n-tree n-trees)
			      (eqv-union-2 (vector-ref n-tree 2) support)))))
	    (vector just
		    (reverse! n-trees)
		    (eqv-diff support
			      (tms:justification-hypotheses just))))))

    (walk-node node '())))

(define (eqv-union . lists)
  (eqv-union* lists))

(define (eqv-union* lists)
  (fold-right eqv-union-2 '() lists))

(define (eqv-union-2 a b)
  (let loop ((a a))
    (if (pair? a)
	(if (memv (car a) b)
	    (loop (cdr a))
	    (cons (car a) (loop (cdr a))))
	b)))

(define (eqv-diff s1 s2)
  (cond ((not (pair? s1)) '())
	((not (pair? s2)) s1)
	((memv (car s1) s2) (eqv-diff (cdr s1) s2))
	(else (cons (car s1) (eqv-diff (cdr s1) s2)))))

;;;; Printing proofs

(define (tms:why? node #!optional port)
  (tms:walk-node-support node
    (lambda (consequent just antecedents support)
      (tms:write-comment
       `(,(tms:node-name consequent)
	 <==
	 (,(or (tms:justification-rule just) just)
	  ,@(map tms:node-name antecedents))
	 ,support)
       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-node-support))
    (let ((queue (make-queue))
	  (seen (make-eq-hash-table)))
      (let ((maybe-enqueue
	     (lambda (n-tree)
	       (hash-table/intern! seen (vector-ref n-tree 0)
		 (lambda ()
		   (enqueue! queue n-tree)
		   #t)))))
	(maybe-enqueue n-tree)
	(do ()
	    ((queue-empty? queue) unspecific)
	  (let ((n-tree (dequeue! queue)))
	    (let ((j-trees (vector-ref n-tree 1)))
	      (if (pair? j-trees)
		  (let ((j-tree (car j-trees)))
		    (procedure (vector-ref n-tree 0)
			       (vector-ref j-tree 0)
			       (map (lambda (n-tree)
				      (vector-ref n-tree 0))
				    (vector-ref j-tree 1))
			       (vector-ref j-tree 2))
		    (for-each maybe-enqueue
			      (vector-ref j-tree 1)))))))))))

(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: