#| -*-Scheme-*-

$Id: tms.scm 4171 2007-10-07 04:05:43Z cph $

Copyright (C) 2006,2007 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>
    (%make-tms name event-handler contradiction)
    tms?
  (name tms:name)
  (event-handler tms:event-handler)
  (contradiction tms:contradiction tms:set-contradiction!))

(define-guarantee tms "TMS")

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

(define (%signal-event node supported?)
  ((tms:event-handler (tms:node-tms node)) node supported?))

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

(define-guarantee tms:node "TMS node")

(define (tms:make-node tms #!optional datum)
  (%make-tms-node tms
		  (if (default-object? datum) #f datum)
		  #f
		  (random-byte-vector 8)
		  '()
		  '()
		  'was-f))

(define (tms:assume-node node)
  (if (tms:node-assumed? node)
      (error "Node already assumed:" node))
  (%set-node-assumed! node #t)
  (%invalidate-support-records node))

(define (tms:retract-node node)
  (if (not (tms:node-assumed? node))
      (error "Node not assumed:" node))
  (%set-node-assumed! node #f)
  (%invalidate-support-records node))

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

(define (%node<? n1 n2)
  (string<? (%node-ordinal n1) (%node-ordinal n2)))

;;;; Justifications

(define-record-type <%justification>
    (%make-justification consequent rule expression hypotheses antecedents
			 support)
    tms:justification?
  (consequent tms:justification-consequent)
  (rule tms:justification-rule)
  (expression tms:justification-expression)
  (hypotheses tms:justification-hypotheses)
  (antecedents tms:justification-antecedents)
  (support %just-support %set-just-support!))

(define-guarantee tms:justification "TMS justification")

(define (tms:justify-node consequent rule expression #!optional hypotheses)
  (guarantee-tms:node consequent 'tms:justify-node)
  (guarantee-tms:antecedent-expression expression 'tms:justify-node)
  (let ((expression (%canonicalize-expr expression))
	(hypotheses (if (default-object? hypotheses) '() hypotheses)))
    (guarantee-list-of-type hypotheses tms:node? "list of TMS nodes"
			    'tms:justify-node)
    (or (find (lambda (just)
		(and (equal? (tms:justification-expression just) expression)
		     (eqv-set=? (tms:justification-hypotheses just)
				hypotheses)))
	      (tms:node-justifications consequent))
	(let* ((antecedents (%expr-nodes expression))
	       (just
		(%make-justification consequent
				     rule
				     expression
				     (if (default-object? hypotheses)
					 '()
					 (begin
					   hypotheses))
				     antecedents
				     'unknown)))
	  (for-each (lambda (node)
		      (tms:set-node-consequents!
		       node
		       (cons just (tms:node-consequents node))))
		    antecedents)
	  (tms:set-node-justifications!
	   consequent
	   (cons just (tms:node-justifications consequent)))
	  (%invalidate-support-records consequent)
	  just))))

(define (%eval-just just vals)
  (%eval (tms:justification-expression just)
	 (let ((nodes (tms:justification-antecedents just)))
	   (lambda (node)
	     (let loop ((nodes nodes) (vals vals))
	       (if (not (pair? nodes))
		   (error "Node not an antecedent:" node))
	       (if (eq? (car nodes) node)
		   (car vals)
		   (loop (cdr nodes) (cdr vals))))))))

(define (tms:antecedent-expression? object)
  (cond ((tms:node? object) #t)
	((pair? object)
	 (case (car object)
	   ((not)
	    (and (pair? (cdr object))
		 (tms:antecedent-expression? (cadr object))
		 (null? (cddr object))))
	   ((or and) (list-of-type? (cdr object) tms:antecedent-expression?))
	   (else #f)))
	(else #f)))

(define-guarantee tms:antecedent-expression "TMS antecedent expression")

(define (%expr-nodes expr)
  (let loop ((expr expr) (nodes '()))
    (if (pair? expr)
	(do ((exprs (cdr expr) (cdr exprs))
	     (nodes nodes (loop (car exprs) nodes)))
	    ((not (pair? exprs)) nodes))
	(if (memq expr nodes)
	    nodes
	    (cons expr nodes)))))

(define (%eval expr node-value)
  (let loop ((expr expr))
    (if (pair? expr)
	(case (car expr)
	  ((not) (not (loop (cadr expr))))
	  ((or) (any loop (cdr expr)))
	  ((and) (every loop (cdr expr)))
	  (else (error:not-tms:antecedent-expression expr)))
	(node-value expr))))

;;; This doesn't try to deal with logical equivalences like DeMorgan's
;;; laws and such -- that's too hard and not useful here.

(define (%canonicalize-expr expr)

  (define (loop expr)
    (if (pair? expr)
	(case (car expr)
	  ((not)
	   (let ((subexpr (loop (cadr expr))))
	     (cond ((tagged-with? 'not subexpr) (cadr subexpr))
		   ((equal? subexpr '(and)) '(or))
		   ((equal? subexpr '(or)) '(and))
		   (else (list 'not subexpr)))))
	  ((and) (do-and/or 'and '(or) expr))
	  ((or) (do-and/or 'or '(and) expr))
	  (else (error:not-tms:antecedent-expression expr)))
	expr))

  (define (do-and/or tag override expr)
    (let ((subexprs
	   (sort (append-map (lambda (subexpr)
			       (let ((subexpr (loop subexpr)))
				 (if (tagged-with? tag subexpr)
				     (cdr subexpr)
				     (list subexpr))))
			     (cdr expr))
	     %expr<?)))
      (cond ((and (pair? subexprs)
		  (null? (cdr subexprs)))
	     (car subexprs))
	    ((member override subexprs) override)
	    (else (cons (car expr) subexprs)))))

  (define (tagged-with? tag expr)
    (and (pair? expr)
	 (eq? (car expr) tag)))

  (loop expr))

(define (%expr<? e1 e2)
  (if (pair? e1)
      (and (pair? e2)
	   (cond ((eq? (car e1) 'not) #f)
		 ((eq? (car e2) 'not) #t)
		 ((eq? (car e1) 'or) #f)
		 (else (eq? (car e2) 'or))))
      (or (pair? e2)
	  (%node<? e1 e2))))

;;;; Support

(define (tms:node-supported? node)
  (let ((support (%node-support node)))
    (cond ((or (eq? support #t) (eq? support #f))
	   support)
	  ((eq? support 'computing)
	   #f)
	  (else
	   (%set-node-support! node 'computing)
	   (let ((support*
		  (if (tms:node-assumed? node)
		      #t
		      (any tms:justification-supported?
			   (tms:node-justifications node)))))
	     (%set-node-support! node support*)
	     (if (if support*
		     (eq? support 'was-f)
		     (eq? support 'was-t))
		 (%signal-event node support*))
	     support*)))))

(define (tms:justification-supported? just)
  (let ((support (%just-support just)))
    (cond ((or (eq? support #t) (eq? support #f))
	   support)
	  ((eq? support 'computing)
	   #f)
	  (else
	   (%set-just-support! just 'computing)
	   (let ((support*
		  (%eval-just just
			      (map tms:node-supported?
				   (tms:justification-antecedents just)))))
	     (%set-just-support! just support*)
	     support*)))))

(define (%invalidate-support-records node)
  (let ((k
	 (lambda (support)
	   (%set-node-support! node support)
	   (for-each (lambda (just)
		       (let ((support (%just-support just)))
			 (if (or (eq? support #t) (eq? support #f))
			     (begin
			       (%set-just-support! just 'unknown)
			       (%invalidate-support-records
				(tms:justification-consequent just))))))
		     (tms:node-consequents node)))))
    (case (%node-support node)
      ((#t) (k 'was-t))
      ((#f) (k 'was-f)))))

(define (tms:node-support-tree node)

  (define (walk-node node seen hypotheses)
    (cond ((memq node seen)
	   #f)
	  ((or (tms:node-assumed? node)
	       (memq node hypotheses))
	   (%make-support node (list node) '()))
	  (else
	   (let ((j-trees
		  (filter (lambda (j-tree) j-tree)
			  (map (let ((seen (cons node seen)))
				 (lambda (just)
				   (walk-just just seen hypotheses)))
			       (tms:node-justifications node)))))
	     (and (pair? j-trees)
		  (%make-support node
				 (eqv-union*
				  (map tms:support-assumptions j-trees))
				 j-trees))))))

  (define (walk-just just seen hypotheses)
    (let ((n-trees
	   (map (let ((hypotheses
		       (eqv-union (tms:justification-hypotheses just)
				  hypotheses)))
		  (lambda (node)
		    (walk-node node seen hypotheses)))
		(tms:justification-antecedents just))))
      (and (%eval-just just n-trees)
	   (%make-support just
			  (eqv-union* (map tms:support-assumptions n-trees))
			  n-trees))))

  (walk-node node '() '()))

(define-record-type <%support>
    (%make-support object assumptions antecedents)
    tms:support?
  (object tms:support-object)
  (assumptions tms:support-assumptions)
  (antecedents tms:support-antecedents))

;;;; 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))
	 ,(map tms:node-name 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 (tms:support-object n-tree)
		 (lambda ()
		   (enqueue! queue n-tree)
		   #t)))))
	(maybe-enqueue n-tree)
	(do ()
	    ((queue-empty? queue) unspecific)
	  (let ((n-tree (dequeue! queue)))
	    (let ((j-trees (tms:support-antecedents n-tree)))
	      (if (pair? j-trees)
		  (let ((j-tree (car j-trees)))
		    (procedure (tms:support-object n-tree)
			       (tms:support-object j-tree)
			       (map (lambda (n-tree)
				      (tms:support-object n-tree))
				    (tms:support-antecedents j-tree))
			       (tms:support-assumptions j-tree))
		    (for-each maybe-enqueue
			      (tms:support-antecedents j-tree)))))))))))

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