(in-package :vag)

(declare-sort anything)

(declare-sort boolean)

(declare-sort number)
(declare-sort float)
(declare-sort fixnum)

(subsort float number)
(subsort fixnum number)

(declare-sort expression)



;========================================================================
;constants
;========================================================================

(vagprim true boolean ()
    (true)
  'true)

(vagprim nil (list-of anything) ()
    (true)
  nil)

(vagprim false boolean ()
    (true)
  'false)




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

(vagprim if anything ((test boolean) (x anything) (y anything))
    (true)
  (if (eq test 'true) x y))

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


;========================================================================
;the filter! and compute! properties
;========================================================================

(defnoticer filter!1 ((x (filter!)))
  (add-property x 'compute! nil)
  (dolist (prod (var-productions-from x))
    (propagate-filter! x prod)))

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

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

(defun propagate-filter! (x prod)
  (declare (ignore x))
  (let ((fun (prod-fun prod))
	(args (prod-rhs prod)))
    (unless (eq fun 'if)
      (dolist (arg args)
	(add-property arg 'filter! nil))
      (let ((filter-pred (filter-predicate fun)))
	(when filter-pred
	  (let ((filter-formula (beta-reduction filter-pred args)))
	    (set-value filter-formula 'true)
	    (add-property filter-formula 'filter! nil)))))))

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

(defun compute!2 (prod)
  (let ((x (var-find (prod-lhs prod))))
    (when (assoc-value 'compute! (var-properties x))
      (propagate-compute! x prod))))

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

(defun propagate-compute! (x prod)
  (let ((fun (prod-fun prod))
	(args (prod-rhs prod)))
    (unless (eq fun 'if)
      (dolist (arg args)
	(add-property arg 'compute! nil))
      (let ((def (vag-definition fun)))
	(when def
	  (equate-vars x (beta-reduction def args)))))))


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

(vagprim not boolean ((x boolean))
    (true)
  (negation x))

(defun negation (x)
  (if (eq x 'true) 'false 'true))

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

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

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

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

(vagprim and boolean ((x boolean) (y boolean))
    (true)
  (conjunction x y))

(defun conjunction (x y)
  (if (and (eq x 'true) (eq y 'true))
      'true
      'false))

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

(vagdef or boolean ((x boolean) (y boolean))
    (true)
  (not (and (not x) (not y))))

(vagdef implies boolean ((x boolean) (y boolean))
    (true)
  (or (not x) y))

(vagprim iff boolean ((x boolean) (y boolean))
    (true)
  (disjunction (conjunction x y)
	       (conjunction (negation x) (negation y))))

(defun disjunction (x y)
  (if (or (eq x 'true) (eq y 'true))
      'true
      'false))

(defnoticer iff1 ((production z (iff x y)))
  (check-iff-consistency z x y))

(defnoticer iff2 ((value z val)
		 (production-from z (iff x y)))
  (check-iff-consistency z x y))

(defnoticer iff3 ((value y val)
		 (production-to y z (iff x y)))
  (check-iff-consistency z x y))

(defnoticer iff4 ((value x val)
		 (production-to x z (iff x y)))
  (check-iff-consistency z x y))

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



;========================================================================
;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)))))))

(vagprim + number ((x number) (y number))
    (true)
  (when (and (numberp x) (numberp y))
    (+ x y)))

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

(vagprim - number ((x number) (y number))
    (true)
  (when (and (numberp x) (numberp y))
    (- x y)))

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

(vagprim * number ((x number) (y number))
    (true)
  (when (and (numberp x) (numberp y))
    (* x 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))

(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 y (max xy1 xy2 xy3 xy4))
      (set-lower-bound y (min xy1 xy2 xy3 xy4))))))


(vagprim = boolean ((x number) (y number))
    (true)
  (when (and (numberp x) (numberp y))
    (if (< (abs (- x y)) *infinitetesimal*)
	'true
	'false)))

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

(vagprim / number ((x number) (y number))
    (not (= y 0))
  (when (and (numberp x) (numberp y) (not (= y 0)))
    (/ x y)))

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

(vagprim > boolean ((x number) (y number))
    (true)
  (when (and (numberp x) (numberp y))
    (if (> x y)
	'true
	'false)))

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

(vagprim >= boolean ((x number) (y number))
    (true)
  (when (and (numberp x) (numberp y))
    (if (> x (- y *infinitetesimal*))
	'true
	'false)))

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

(vagdef <= boolean ((x number) (y number))
    (true)
  (>= y x))

(vagdef < boolean ((x number) (y number))
    (true)
  (> y x))


;========================================================================
;GFC
;========================================================================



;========================================================================
;unification
;========================================================================

(vagprim equal boolean ((x anything) (y anything))
    (true)
  (if (equal x y)
      'true
      'false))

(defnoticer equal1 ((production phi (equal x y))
		    (value phi truth))
  (when (eq truth 'true)
    (equate-vars x y)))

(defnoticer equal2 ((value phi truth)
		    (production-from phi (equal x y)))
  (when (eq truth 'true)
    (equate-vars x y)))

(defnoticer equal3 ((production e (equal x y)))
  (equate-vars e (intern-exp `(equal ,y ,x))))

(defnoticer equal4 ((value x xval)
		    (production-to x e (equal x y))
		    (value y yval))
  (when (not (equal xval yval))
    (set-value e 'false)))

(defnoticer equal5 ((production e (equal y x))
		    (value x xval)
		    (value y yval))
  (when (not (equal xval yval))
    (set-value e 'false)))

(vagprim cons anything ((x anything) (y anything))
    (true)
  (cons x y))

(defnoticer equal6 ((production e (equal x y))
		    (production-from x (cons z w))
		    (value y yval))
  (if (consp yval)
      (progn (set-value z (car yval))
	     (set-value w (cdr yval)))
      (set-value e 'false)))

(defnoticer equal7 ((production x (cons z w))
		    (production-to x e (equal x y))
		    (value y yval))
  (if (consp yval)
      (progn (set-value z (car yval))
	     (set-value w (cdr yval)))
      (set-value e 'false)))

(defnoticer equal8 ((value y yval)
		    (production-to y e (equal x y))
		    (production-from x (cons z w)))
  (if (consp yval)
      (progn (set-value z (car yval))
	     (set-value w (cdr yval)))
      (set-value e 'false)))

(vagprim car anything ((x anything))
    (true)
  (when (consp x) (car x)))

(defnoticer car1 ((production z (car c))
		  (production-from c (cons x y)))
  (equate-vars z x))

(defnoticer car2 ((production c (cons x y))
		  (production-to c z (car c)))
  (equate-vars z x))

(vagprim cdr anything ((x anything))
    (true)
  (when (consp x) (cdr x)))

(defnoticer cdr1 ((production z (cdr c))
		  (production-from c (cons x y)))
  (equate-vars z y))

(defnoticer cdr2 ((production c (cons x y))
		  (production-to c z (cdr c)))
  (equate-vars z y))

(defnoticer cons1 ((production c (cons x y))
		   (production-from c (cons z w)))
  (equate-vars x z)
  (equate-vars y w))


;========================================================================
;map
;========================================================================

(declare-function (map anything anything) anything)

(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-exp `(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-exp `(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-exp `(cons ,(beta-reduction fval (list x)) (map ,f ,y)))))