#| -*-Scheme-*-

$Id: symbolic-values.scm 2891 2006-04-20 18:19:29Z cph $

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.

|#

;;;; Value model for symbolic algebra using scmutils

(declare (usual-integrations))

;;; The caller must supply a plunk-generator
;;;   if there are units, for example.

(define (algebraic-solver #!optional plunk-chooser)
  (if (default-object? plunk-chooser) (set! plunk-chooser car))
  (let ((*plunked-variables* '())
	(*equations* '())
	(*solved-equations* '()))

    (define (numerical-quantities-equal? x y)
      (let ((x (u:value x)) (y (u:value y)))
	(if (and (number? x) (number? y))
	    (= x y)
	    (let ((z (new-simplify (- x y))))
	      (zero? (expression z))))))

    (define (choose-numerical-quantity ns)
      (or (find-matching-item ns
	    (lambda (x)
	      (number? (expression (u:value x)))))
	  (find-matching-item ns
	    (lambda (x) (symbol? (expression (u:value x)))))
	  (car ns)))

    (define (plunk-connector connector)
      (if (cp:has-value? connector)
	  (error "Connector has a value -- plunk" connector))
      (let* ((units-wrapper
	      (eq-get (cp:connector-value-model connector) 'units-wrapper))
	     (new-var (symbol "x-" (cp:connector-name connector)))
	     (new-variable (if units-wrapper (units-wrapper new-var) new-var)))
	(set! *plunked-variables*
	      (cons (cons new-var connector)
		    *plunked-variables*))
	(cp:assume-value connector new-variable)))

    (define (coincidence-handler connector value justify)
      (let ((old-value (cp:value-of connector))
	    (current-assignment (cp:supported-assignment connector)))
	(let ((residual (expression (u:value (new-simplify (- value old-value))))))
	  (if (number? residual)
	      (if (= residual 0)
		  (justify current-assignment)
		  (cp:set-contradiction connector value justify))
	      #|
	      ;; This replaces the next expression
	      (maybe-post-equation connector value residual justify)
	      |#

	      (substitute-for-knowns
	       (if (quotient? residual) (symb:dividend residual) residual)
	       (lambda (resi substs-used)
		 (if (null? substs-used)
		     (maybe-post-equation connector value residual justify)
		     (let ((inode
			    (tms:make-node (tms:node-tms current-assignment)
					   'linker)))
		       (justify inode)
		       (let ((residual (new-simplify resi))
			     (justify
			      (lambda (node)
				(tms:justify-node node 'residual
						  (cons inode substs-used)))))
			 (if (number? residual)
			     (if (= residual 0)
				 (tms:justify-node current-assignment
						   'tautology
						   (cons inode substs-used))
				 (cp:set-contradiction connector value justify))
			     (maybe-post-equation connector value
						  residual
						  justify)))))))
	      ))))

    (define (maybe-post-equation connector value residual justify)
      (let ((same-equation
	     (find-matching-item *equations*
	       (lambda (eqn)
		 (number?
		  (expression
		   (new-simplify
		    (/ (equation-expression eqn) residual)))))))
	    (current-assignment
	     (cp:supported-assignment connector)))
	(if same-equation
	    (tms:justify-node
	     (car (equation-justifications same-equation))
	     'additional
	     (list (cp:set-justified-value connector value justify)
		   current-assignment))
	    (let ((equation
		   (make-equation
		    residual
		    (list (cp:set-justified-value connector value justify)
			  current-assignment))))
	      (if equation
		  (set! *equations*
			(cons equation *equations*)))))))

    (define (try-to-solve-equations)
      (and (pair? *equations*)
	   (let ((solution
		  (solve-incremental
		   (keep-matching-items *equations* equation-supported?)
		   (unresolved-plunked-variables))))
	     (for-each
	      (lambda (subst)
		(let ((var (substitution-variable subst))
		      (expr (substitution-expression subst))
		      (justs (substitution-justifications subst)))
		  (let* ((connector (plunked-connector var))
			 (units-wrapper
			  (eq-get (cp:connector-value-model connector)
				  'units-wrapper)))
		    (cp:set-justified-value
		     connector
		     (if units-wrapper
			 (units-wrapper
			  (if (numerical-quantity? expr)
			      expr
			      (make-numerical-literal expr)))
			 expr)
		     (lambda (node)
		       (tms:conditional-justification
			node
			'equation-solver
			justs
			(map plunk-assignment
			     (plunked-vars-not-in expr))))))))
	      (substitutions solution))
	     (let ((unsolved
		    (list-intersection *equations*
				       (residual-equations solution))))
	       (set! *solved-equations*
		     (list-union (list-difference *equations* unsolved)
				 *solved-equations*))
	       (set! *equations* unsolved)))))

    (define (post-propagation-processor network)
      (try-to-solve-equations)
      (and *complete-propagation*
	   (let ((unassigned-connectors
		  (delete-matching-items (cp:network-connectors network)
		    cp:has-value?)))
	     (and (pair? unassigned-connectors)
		  (cp:plunk-connector (plunk-chooser unassigned-connectors)))
	     )))

    (define (unresolved-plunked-variables)
      (map car
	   (keep-matching-items *plunked-variables*
	     (lambda (varpair)
	       (eq? (u:value (cp:value-of (cdr varpair)))
		    (car varpair))))))

    (define (plunk-assignment var)
      (find-matching-item
	  (cp:connector-assignments (plunked-connector var))
	(lambda (assignment)
	  (eq? var (u:value (cp:assignment-value assignment))))))

    (define (plunked-connector var)
      (let ((entry (assoc var *plunked-variables*)))
	(if (not entry)
	    (error "Not a plunked variable." var))
	(cdr entry)))

    (define (plunked-vars-in expr)
      (cond ((pair? expression)
	     (list-union (plunked-vars-in (car expression))
			 (plunked-vars-in (cdr expression))))
	    ((assq expression *plunked-variables*) expression)
	    (else '())))

    (define (plunked-vars-not-in expr)
      (list-difference (map car *plunked-variables*)
		       (plunked-vars-in expr)))

    (define (substitute-for-knowns expression continue)
      (let subst ((expr expression) (substs-used '()) (continue continue))
	(cond ((pair? expr)
	       (subst (car expr) substs-used
		      (lambda (x substs-used)
			(subst (cdr expr) substs-used
			       (lambda (y substs-used)
				 (continue (cons x y) substs-used))))))
	      ((assq expr *plunked-variables*)
	       =>
	       (lambda (entry)
		 (if (cp:has-value? (cdr entry))
		     (let ((v (u:value (cp:value-of (cdr entry)))))
		       (if (eq? v (car entry))
			   (continue expr substs-used)
			   (continue v
				     (cons (cp:supported-assignment (cdr entry))
					   substs-used))))
		     (continue expr substs-used))))
	      (else
	       (continue expr substs-used)))))

    (define (value-of connector)
      (if (not (cp:has-value? connector))
	  (error "Connector value not known" connector))
      (substitute-for-knowns (cp:value-of connector)
        (lambda (expr substs-used)
	  (if (pair? substs-used)
	      (let ((ass (cp:supported-assignment connector)))
		(cp:set-justified-value
		 connector
		 expr
		 (lambda (node)
		   (tms:justify-node node 'substitution
				     (cons ass substs-used))))
		expr)
	      (cp:value-of connector)))))

    (lambda (message)
      (case message
	((membership) numerical-quantity?)
	((equality) numerical-quantities-equal?)
	((choose-value) choose-numerical-quantity)
	((coincidence-handler) coincidence-handler)
	((post-propagation-processor) post-propagation-processor)
	((value-model)
	 (cp:make-value-model numerical-quantity?
			      numerical-quantities-equal?
			      choose-numerical-quantity
			      coincidence-handler
			      post-propagation-processor))
	((plunk-connector) plunk-connector)
	((plunked-variables) *plunked-variables*)
	((equations) *equations*)
	((solved-equations) *solved-equations*)
	((value-of) value-of)
	(else (error "algebra: Unknown message:" message))))
    ))

(define *complete-propagation* #f)

(define (equation-supported? equation)
  (for-all? (cadr equation) tms:node-supported?))

(define (algebra:value-of connector)
  (if (cp:has-value? connector)
      (((ckt:algebra (cp:connector-network connector))
	'value-of)
       connector)
      #f))