For Debugging 0+1 != 1

staload "sessions.sats"
staload UN = "prelude/SATS/unsafe.sats"

#define C 1
#define S 0


stadef fp (a:t@ype) = lam (p:int->protocol):int->protocol => lam n => pite (n>0, pbrch(C, pmsg(C,a)::p(n+1), pmsg(S,a)::p(n-1)), pmsg(C,a)::p(n+1))
stadef queue (a:t@ype) = pfix2 (fp a)



extern fun empty {a:t@ype} (): chan(C, (queue a) 0)
extern fun elem  {a:t@ype} {n:nat} (chan(C, (queue a) n), a): chan(C, (queue a) (n+1))

implement empty {a} () = let 
	fun server (out: chan(S, (queue a) 0)): void = let 
		val _ = recurse2 {S} {lam (p:int->protocol):int->protocol => lam n => pite (n>0, pbrch(C, pmsg(C,a)::p(n+1), pmsg(S,a)::p(n-1)), pmsg(C,a)::p(n+1))} {0} out 
		val _ = ite_false out
		val x = recv out 
		val tail = empty {a} ()
		val q = elem {a} {0} (tail, x)
	in 	
		cut (q, out)
	end
in 
	create (llam out => server out)
end


implement main0 () = () where {
	val queue = empty {int} ()
	val _ = recurse2 {C} {fp int} {0} queue 
	val _ = ite_false queue 
	val _ = send (queue, 1)

    // This line works
	val _ = recurse2 {C} {fp int} {0+1} queue 
	
	// But this equivalent line doesn't
    // val _ = recurse2 {C} {fp int} {1} queue 
    
    // The constraint is as follows, 
    // eqeq: 
    //   app(app(pfix2; lam(p; lam(n; app(pite; app(>; var(n), 0), app(pbrch; 1, app(pseq; app(pmsg; 1, int), app(var(p); app(+; var(n), 1))), app(pseq; app(pmsg; 0, int), app(var(p); app(-; var(n), 1)))), app(pseq; app(pmsg; 1, int), app(var(p); app(+; var(n), 1))))))); app(+; 0, 1)); 
    //   app(app(pfix2; lam(p; lam(n; app(pite; app(>; var(n), 0), app(pbrch; 1, app(pseq; app(pmsg; 1, int), app(var(p); app(+; var(n), 1))), app(pseq; app(pmsg; 0, int), app(var(p); app(-; var(n), 1)))), app(pseq; app(pmsg; 1, int), app(var(p); app(+; var(n), 1))))))); 1)))
    // 
    // it is saying "0+1 == 1" can not be verified. However, it is obviously true.



	val _ = $UN.cast2void queue

}

////

implement elem {a} (inp, x) = let 
	fun server (out: chan(S,queue(a)), inp: chan(C,queue(a))): void = let 
		val _ = recurse out
		val c = offer out
	in 
		case+ c of 
		| ~Left() => 
			let
				val y = recv out
				val _ = recurse inp
				val _ = choose (inp, Left())
				val _ = send (inp, y) 
			in 
				server (out, inp)
			end
		| ~Right() => 
			let 
				val _ = choose (out, Right())
				val _ = send (out, x)
			in 
				cut (out, inp)
			end
	end
in 
	create (llam out => server (out, inp))
end