;; From issue#93. The change happened in right-hand-side of a rule may also impact output in semi-naive cases
(push)
(function f (i64) i64 :merge (max old new))

(set (f 0) 0)
(set (f 3) 0)

(rule ((= f0 (f 0))) ((set (f 1) f0)))
(rule ((= f1 (f 1))) ((set (f 2) f1)))

;; update f3 some iters later to make sure f(0) is inactive
(rule ((= f2 (f 2))) ((set (f 3) 3)))

(push)

;; This rule should fire and set f(0) to be 3, but because f0 is inactive, 
;; it does not fire (despite that f3 is active now)
(rule ((= f0 (f 0))) ((set (f 0) (f 3))))

(run 100)
(print-function f 100) ;; f0 is expected to have value 3, but has 0 in reality.

(check (= (f 0) 3))
(check (= (f 1) 3))
(check (= (f 2) 3))
(check (= (f 3) 3))

(pop)
(push)

;; variants of the last rule.
(rule ((= f0 (f 0)) (= x 3) (= y x))  ((set (f 0) (f y))))

(run 100)
(check (= (f 0) 3))
(check (= (f 1) 3))
(check (= (f 2) 3))
(check (= (f 3) 3))

(pop)
(push)

;; adding let binding
(rule ((= f0 (f 0))) ((let x 3) (let y x) (set (f 0) (f y))))

(run 100)
(check (= (f 0) 3))
(check (= (f 1) 3))
(check (= (f 2) 3))
(check (= (f 3) 3))

(pop)
(push)

(function g (i64) i64 :merge (max old new))
(set (g 0) 3)

;; bind to another function
(rule ((= f0 (f 0))) ((let x (g 0)) (let y x) (set (f 0) (f y))))

(run 100)
(check (= (f 0) 3))
(check (= (f 1) 3))
(check (= (f 2) 3))
(check (= (f 3) 3))

(pop)
(pop)

;; more complicated case, when the evaluation never finish
;; the semi_naive and naive behavior diverage a bit
(function f (i64) i64 :merge (max old new))

(set (f 0) 0)
(set (f 3) 0)

(rule ((= f0 (f 0))) ((set (f 1) (+ 1 f0))))
(rule ((= f1 (f 1))) ((set (f 2) (+ 1 f1))))

(push)

(rule ((= f2 (f 2))) ((set (f 3) 1)))
(rule ((= f0 (f 0))) ((set (f 0) (f (f 3)))))


(run 100)
(print-function f 100) 
(check (!= 0 (f 0)))
(check (!= 0 (f 1)))
(check (!= 0 (f 2)))

(pop)


;; id function that will set all int values, but need strong induction.
(function g (i64) i64 :merge (max old new))
(set (g 0) 0)
(set (g 1) 1)
(rule ((= x (g x)) (= y (g (- x 1)))) ((set (g (+ x 1)) (+ y 2))))

(run 100)
(print-function g 100) 

(check (= 20 (g 20)))