(in-package :vag)


;========================================================================
;consider!
;========================================================================

(defnoticer consider!1 ((x (consider!)))
  (dolist (prod (var-productions-from x))
    (propagate-consider! x prod)))

(defun consider!2 (prod)
  (let ((x (var-find (prod-lhs prod))))
    (when (member '(consider! nil) (var-properties x) :test 'equal)
      (propagate-consider! x prod))))

(push 'consider!2 *production-noticers*)

(defun propagate-consider! (x prod)
  (declare (ignore x))
  (let ((fun (prod-fun prod))
	(args (prod-rhs prod)))
    (if (eq fun 'if)
	(add-property (car args) 'consider! nil)
	(progn
	  (dolist (arg args)
	    (add-property arg 'consider! nil))
	  (assert-predicate (filter-predicate fun) args)
	  (let ((sort (output-sort-cache fun)))
	    (when (and sort (symbolp sort))
	      (assert-sort x sort)))
	  (let ((def (vag-definition fun)))
	    (when def
	      (equate-vars x (beta-reduction def args))))))))

(defun assert-predicate (pred args)
  (when pred
    (let ((formula (beta-reduction pred args)))
      (set-value formula 'true)
      (add-property formula 'consider! nil))))

(defun assert-sort (x sort)
  (add-property x 'has-type (list sort))
  (let ((next (parent-sort sort)))
    (when next
      (assert-sort x next))))

(defun type-noticer (x args)
  (let ((sort (car args)))
    (when (and sort (symbolp sort))
      (assert-predicate (sort-constraint sort) (list x)))))

(pushnew 'type-noticer (noticers 'has-type))
			 


;========================================================================
;conditionals
;========================================================================

(defnoticer if-noticer1 ((production z (if phi x y))
			 (value phi truth))
  (if (eq truth 'true)
      (equate-vars z x)
      (equate-vars z y)))

(defnoticer if-noticer2 ((value phi truth)
			 (production-to phi z (if phi x y)))
  (if (eq truth 'true)
      (equate-vars z x)
      (equate-vars z y)))


;========================================================================
;BCP
;========================================================================

(defnoticer not1 ((production y (not x))
		  (value y val))
  (set-value x (negation val)))

(defnoticer not2 ((value y val)
		  (production-from y (not x)))
  (set-value x (negation val)))

(defnoticer and1 ((production z (and x y)))
  (check-and-consistency z x y))

(defnoticer and2 ((value z val)
		  (production-from z (and x y)))
  (check-and-consistency z x y))

(defnoticer and3 ((value y val)
		  (production-to y z (and x y)))
  (check-and-consistency z x y))

(defnoticer and4 ((value x val)
		  (production-to x z (and x y)))
  (check-and-consistency z x y))

(defun check-and-consistency (z x y)
  (let ((zval (var-value z))
	(xval (var-value x))
	(yval (var-value y)))
    (cond ((eq zval 'true)
	   (set-value x 'true)
	   (set-value y 'true))
	  ((eq zval 'false)
	   (when (eq xval 'true)
	     (set-value y 'false))
	   (when (eq yval 'true)
	     (set-value x 'false)))
	  ((eq xval 'false)
	   (set-value z 'false))
	  ((eq yval 'false)
	   (set-value z 'false)))))


(defnoticer or1 ((production z (or x y)))
  (check-or-consistency z x y))

(defnoticer or2 ((value z val)
		  (production-from z (or x y)))
  (check-or-consistency z x y))

(defnoticer or3 ((value y val)
		  (production-to y z (or x y)))
  (check-or-consistency z x y))

(defnoticer or4 ((value x val)
		  (production-to x z (or x y)))
  (check-or-consistency z x y))

(defun check-or-consistency (z x y)
  (let ((zval (var-value z))
	(xval (var-value x))
	(yval (var-value y)))
    (cond ((eq zval 'false)
	   (set-value x 'false)
	   (set-value y 'false))
	  ((eq zval 'true)
	   (when (eq xval 'false)
	     (set-value y 'true))
	   (when (eq yval 'false)
	     (set-value x 'true)))
	  ((eq xval 'true)
	   (set-value z 'true))
	  ((eq yval 'true)
	   (set-value z 'true)))))


;========================================================================
;structure equality cons, car, cdr, and null?
;========================================================================

;There is a subtle bug motivating the use of consider! in the following rules.
;consider
;(define (numbers-between x y)
;  (if (> x y)
;      nil
;      (cons x (numbers-between (+ x 1) y))))
;
;and (consider! (numbers-between x y)) where x and y are variables.
;
;we get (consider! x) and we get that (cons x (numbers-between (+ x 1) y)) is interned.
;If we equate (car (cons x (numbers-between ...))) to x then we get (consider! (car (cons x ...)))
;which gives us (consider! (numbers-between (+ x 1) y)).  This gives an infinite loop.

(defnoticer cons1 ((production z (cons x y))
		   (production-to z w (car z))
		   (w (consider!)))
  (equate-vars w x))

(defnoticer cons2 ((production w (car z))
		   (w (consider!))
		   (production-from z (cons x y)))
  (equate-vars w x))

(defnoticer cons3 ((w (consider!))
		   (production-from w (car z))
		   (production-from z (cons x y)))
  (equate-vars w x))

(defnoticer cons4 ((production z (cons x y))
		   (production-to z w (cdr z))
		   (w (consider!)))
  (equate-vars w y))

(defnoticer cons5 ((production w (cdr z))
		   (w (consider!))
		   (production-from z (cons x y)))
  (equate-vars w y))

(defnoticer cons6 ((w (consider!))
		   (production-from w (cdr z))
		   (production-from z (cons x y)))
  (equate-vars w y))

(defnoticer null1 ((production z (cons x y)))
  (set-value (intern-exp2 `(null? ,z)) 'false))

(defnoticer null2 ((production y (nil)))
  (set-value (intern-exp2 `(null? ,y)) 'true))

(defnoticer equal1 ((production phi (= x y)))
  (when (eq x y)
    (set-value phi 'true)))

(defnoticer equal1.1 ((production phi (= x y))
		      (value phi v))
  (when (eq v 'true)
    (equate-vars x y)))

(defnoticer equal1.2 ((value phi v)
		      (production-from phi (= x y)))
  (when (eq v 'true)
    (equate-vars x y)))

(defnoticer equal2 ((production phi (= x y))
		    (value x xval)
		    (value y yval))
  (check-equality phi xval yval))

(defnoticer equal3 ((value x xval)
		    (production-to x phi (= x y))
		    (value y yval))
  (check-equality phi xval yval))

(defnoticer equal4 ((value y yval)
		    (production-to y phi (= x y))
		    (value x xval))
  (check-equality phi xval yval))

(defun check-equality (phi xval yval)
  (cond ((symbolp xval)
	 (cond ((symbolp yval)
		(if (eq xval yval)
		    (set-value phi 'true)
		    (set-value phi 'false)))
	       ((not (symbolp yval))
		(set-value phi 'false))))
	((not (symbolp xval))
	 (when (symbolp yval)
	   (set-value phi 'false)))))



;========================================================================
;member?, append, and map
;========================================================================

(setf (vag-definition 'member?)
      '(lambda (x y)
	(if (null? y)
	    (false)
	    (if (= x (car y))
		(true)
		(member? x (cdr y))))))

(setf (vag-definition 'append)
      '(lambda (x y)
	(if (null? x)
	    y
	    (cons (car x) (append (cdr x) y)))))

;map can not be handled with a definition because lambda expressions are
;not first class.

(defnoticer map1 ((production l2 (map f l1))
		  (production-from l1 (nil)))
  (equate-vars l1 l2))

(defnoticer map2 ((production l1 (nil))
		  (production-to l1 l2 (map f l1)))
  (equate-vars l1 l2))

(defnoticer map3 ((production l1 (cons x y))
		  (production-to l1 l2 (map f l1))
		  (value f fval))
  (equate-vars l2 (intern-exp2 `(cons ,(beta-reduction fval (list x)) (map ,f ,y)))))

(defnoticer map4 ((production l2 (map f l1))
		  (production-from l1 (cons x y))
		  (value f fval))
  (equate-vars l2 (intern-exp2 `(cons ,(beta-reduction fval (list x)) (map ,f ,y)))))

(defnoticer map5 ((value f fval)
		  (production-to f l2 (map f l1))
		  (production-from l1 (cons x y)))
  (equate-vars l2 (intern-exp2 `(cons ,(beta-reduction fval (list x)) (map ,f ,y)))))



;========================================================================
;bounds propagation
;========================================================================

(defnoticer value-to-bound1 ((value var val))
  (check-bound-consistency var))

(defnoticer value-to-bound2 ((upper-bound var bound))
  (check-bound-consistency var))

(defnoticer value-to-bound3 ((lower-bound var bound))
  (check-bound-consistency var))

(defun check-bound-consistency (var)
  (let ((val (var-value var)))
    (if (and val (numberp val))
	(if (or (> val (var-upper-bound var))
		(< val (var-lower-bound var)))
	    (declare-contradiction)
	    (progn (set-lower-bound var val)
		   (set-upper-bound var val)))
	(let ((ub (var-upper-bound var))
	      (lb (var-lower-bound var)))
	  (when (< (abs (- ub lb)) (* 5 *infinitetesimal*))
	    (set-value var (/ (+ ub lb) 2)))))))

(defnoticer +noticer1
    ((production x (+ y z)))
  (+-check x y z))

(defnoticer +noticer2
    ((lower-bound x xlb)
     (production-from x (+ y z)))
  (+-check x y z))

(defnoticer +noticer3
    ((lower-bound y ylb)
     (production-to y x (+ y z)))
  (+-check x y z))

(defnoticer +noticer4
    ((lower-bound y ylb)
     (production-to y x (+ z y)))
  (+-check x y z))

(defnoticer +noticer5
    ((upper-bound x xub)
     (production-from x (+ y z)))
  (+-check x y z))

(defnoticer +noticer6
    ((upper-bound y yub)
     (production-to y x (+ y z)))
  (+-check x y z))

(defnoticer +noticer7
    ((upper-bound y yub)
     (production-to y x (+ z y)))
  (+-check x y z))

(defun +-check (x y z) ;x=y+z.
  (let ((ylb (var-lower-bound y))
	(zlb (var-lower-bound z))
	(yub (var-upper-bound y))
	(zub (var-upper-bound z))
	(xlb (var-lower-bound x))
	(xub (var-upper-bound x)))
  (set-lower-bound x (+ ylb zlb))
  (set-upper-bound x (+ yub zub))
  (set-lower-bound y (- xlb zub))
  (set-upper-bound y (- xub zlb))
  (set-lower-bound z (- xlb yub))
  (set-upper-bound z (- xub ylb))))

(defnoticer -noticer1 ((production z (- x y)))
  (equate-vars x (intern-exp2 `(+ ,z ,y))))

(defnoticer *noticer1 ((production x (* y z)))
  (*-consistency-check x y z))

(defnoticer *noticer2 ((upper-bound x xub)
		       (production-from x (* y z)))
  (*-consistency-check x y z))

(defnoticer *noticer3 ((upper-bound y xub)
		       (production-to y x (* y z)))
  (*-consistency-check x y z))

(defnoticer *noticer4 ((upper-bound z xub)
		       (production-to z x (* y z)))
  (*-consistency-check x y z))

(defnoticer *noticer5 ((lower-bound x xub)
		       (production-from x (* y z)))
  (*-consistency-check x y z))

(defnoticer *noticer6 ((lower-bound y xub)
		       (production-to y x (* y z)))
  (*-consistency-check x y z))

(defnoticer *noticer7 ((lower-bound z xub)
		       (production-to z x (* y z)))
  (*-consistency-check x y z))

;in the following x = y*z

(defun *-consistency-check (x y z)
  (let ((xub (var-upper-bound x))
	(xlb (var-lower-bound x))
	(yub (var-upper-bound y))
	(ylb (var-lower-bound y))
	(zub (var-upper-bound z))
	(zlb (var-lower-bound z)))
    (let ((yz1 (* yub zub))
	  (yz2 (* yub zlb))
	  (yz3 (* ylb zub))
	  (yz4 (* ylb zlb)))
      (set-upper-bound x (max yz1 yz2 yz3 yz4))
      (set-lower-bound x (min yz1 yz2 yz3 yz4)))
    (when (or (and (> zlb 0) (> zub 0))
	      (and (< zub 0) (< zlb 0)))
      (let ((xz1 (/ xub zub))
	    (xz2 (/ xub zlb))
	    (xz3 (/ xlb zub))
	    (xz4 (/ xlb zlb)))
	(set-upper-bound y (max xz1 xz2 xz3 xz4))
	(set-lower-bound y (min xz1 xz2 xz3 xz4))))
    (when  (or (and (> ylb 0) (> yub 0))
	       (and (< yub 0) (< ylb 0)))
    (let ((xy1 (/ xub yub))
	  (xy2 (/ xub ylb))
	  (xy3 (/ xlb yub))
	  (xy4 (/ xlb ylb)))
      (set-upper-bound z (max xy1 xy2 xy3 xy4))
      (set-lower-bound z (min xy1 xy2 xy3 xy4))))))


(defnoticer =noticer1 ((production phi (= x y)))
  (check-=-consistency phi x y))

(defnoticer =noticer2 ((value phi ignore)
		       (production-from phi (= x y)))
  (check-=-consistency phi x y))

(defnoticer =noticer3 ((upper-bound x ignore)
		       (production-to x phi (= x y)))
  (check-=-consistency phi x y))

(defnoticer =noticer4 ((upper-bound y ignore)
		       (production-to y phi (= x y)))
  (check-=-consistency phi x y))

(defnoticer =noticer5 ((lower-bound x ignore)
		       (production-to x phi (= x y)))
  (check-=-consistency phi x y))

(defnoticer =noticer6 ((lower-bound y ignore)
		       (production-to y phi (= x y)))
  (check-=-consistency phi x y))


(defun check-=-consistency (phi x y)
  (when (> (var-lower-bound x) (+ (var-upper-bound y) *infinitetesimal*))
    (set-value phi 'false))
  (when (> (var-lower-bound y) (+ (var-upper-bound x) *infinitetesimal*))
    (set-value phi 'false))
  (when (eq (var-value phi) 'true)
    (set-upper-bound x (+ (var-upper-bound y) *infinitetesimal*))
    (set-lower-bound x (- (var-lower-bound y) *infinitetesimal*))
    (set-lower-bound y (- (var-lower-bound x) *infinitetesimal*))
    (set-upper-bound y (+ (var-upper-bound x) *infinitetesimal*))))

(defnoticer /-noticer1 ((production z (/ x y)))
  (equate-vars x (intern-exp2 `(* ,z ,y))))

(defnoticer >noticer1 ((production phi (> x y)))
  (check->-consistency phi x y))

(defnoticer >noticer2 ((value phi ignore)
		       (production-from phi (> x y)))
  (check->-consistency phi x y))

(defnoticer >noticer3 ((upper-bound x ignore)
		       (production-to x phi (> x y)))
  (check->-consistency phi x y))

(defnoticer >noticer4 ((upper-bound y ignore)
		       (production-to y phi (> x y)))
  (check->-consistency phi x y))

(defnoticer >noticer5 ((lower-bound x ignore)
		       (production-to x phi (> x y)))
  (check->-consistency phi x y))

(defnoticer >noticer6 ((lower-bound y ignore)
		       (production-to y phi (> x y)))
  (check->-consistency phi x y))

(defun check->-consistency (phi x y)
  (when (> (var-lower-bound x) (var-upper-bound y))
    (set-value phi 'true))
  (when (>= (var-lower-bound y) (var-upper-bound x))
    (set-value phi 'false))
  (when (eq (var-value phi) 'true)
    (set-lower-bound x (var-lower-bound y))
    (set-upper-bound y (var-lower-bound x)))  
  (when (eq (var-value phi) 'false)
    (set-lower-bound y (var-lower-bound x))
    (set-upper-bound x (var-upper-bound y))))

(defnoticer >=noticer1 ((production phi (>= x y)))
  (check->=-consistency phi x y))

(defnoticer >=noticer2 ((value phi ignore)
		       (production-from phi (>= x y)))
  (check->=-consistency phi x y))

(defnoticer >=noticer3 ((upper-bound x ignore)
		       (production-to x phi (>= x y)))
  (check->=-consistency phi x y))

(defnoticer >=noticer4 ((upper-bound y ignore)
		       (production-to y phi (>= x y)))
  (check->=-consistency phi x y))

(defnoticer >=noticer5 ((lower-bound x ignore)
		       (production-to x phi (>= x y)))
  (check->=-consistency phi x y))

(defnoticer >=noticer6 ((lower-bound y ignore)
			(production-to y phi (>= x y)))
  (check->=-consistency phi x y))

(defun check->=-consistency (phi x y)
  (when (> (var-lower-bound x) (- (var-upper-bound y) *infinitetesimal*))
    (set-value phi 'true))
  (when (> (var-lower-bound y) (+ (var-upper-bound x) *infinitetesimal*))
    (set-value phi 'false))
  (when (eq (var-value phi) 'true)
    (set-lower-bound x (- (var-lower-bound y) *infinitetesimal*))
    (set-upper-bound y (+ (var-upper-bound x) *infinitetesimal*)))
  (when (eq (var-value phi) 'false)
    (set-lower-bound y (+ (var-lower-bound x) *infinitetesimal*))
    (set-upper-bound x (- (var-upper-bound x) *infinitetesimal*))))