(in-package 'rules :use '(lisp util))

(eval-when (compile load eval)
  (in-package 'rules :use '(lisp util)))


;========================================================================
;test cases
;========================================================================
(defnoticer number-propagator
    ((natnum ?x)
     (prod ?y f ?x))
  (assert-internal `(natnum ,?y) ?justification))

(defnoticer number-propagator2
    ((production ?y f ?x)
     (natnum ?x))
  (assert-internal `(natnum ,?y) ?justification))

(defnoticer number-base-case
    ((production ?y zero))
  (assert-internal `(natnum ,?y) ?justification))

(defun cong-test1 ()
  (clear-frame)
  (assert-exp '(= a b))
  (assert-exp '(= c b))
  (assert-exp '(p b))
  (why '(p c)))

(defun cong-test2 ()
  (clear-frame)
  (assert-exp '(= a b))
  (assert-exp '(p b d))
  (assert-exp '(= c b))
  (why '(p c d)))

(defun cong-test3 ()
  (clear-frame)
  (assert-exp '(= a b))
  (assert-exp '(p d b))
  (assert-exp '(= c b))
  (why '(p d c)))

(defun cong-test4 ()
  (clear-frame)
  (assert-exp '(= a b))
  (assert-exp '(p d1 b d2))
  (assert-exp '(= c b))
  (why '(p d1 c d2)))

(defun cong-test5 ()
  (clear-frame)
  (assert-exp '(= a (f a)))
  (why '(= a (f (f (f (f a)))))))