% $Id: UnaryTest.oz,v 1.2 2008/12/05 04:51:05 leavens Exp leavens $ \insert 'Unary.oz' \insert 'SolveFirst.oz' \insert 'SolveAll.oz' \insert 'TestingNoStop.oz' {StartTesting 'Count'} {Test {List.take {Solve Count} 3} '==' [z s(z) s(s(z))]} {StartTesting 'LT with all'} {Test {SolveAll proc {$ ?Ack} {LT z z} Ack=ok end} '==' nil} {Test {SolveAll proc {$ ?Ack} {LT z s(z)} Ack=ok end} '==' [ok]} {Test {SolveAll proc {$ ?Ack} {LT s(z) z} Ack=ok end} '==' nil} {Test {SolveAll proc {$ ?Ack} {LT s(z) s(z)} Ack=ok end} '==' nil} {Test {SolveAll proc {$ ?Ack} {LT z s(s(z))} Ack=ok end} '==' [ok]} {StartTesting 'LT backwards'} {Test {SolveAll proc {$ ?V} {LT V s(s(z))} end} '==' [z s(z)]} {Test {SolveAll proc {$ ?V} {LT V s(s(s(s(z))))} end} '==' [z s(z) s(s(z)) s(s(s(z)))]} {StartTesting 'Plus forwards'} {Test {SolveAll proc {$ ?Ans} {Plus z z Ans} end} '==' [z]} {Test {SolveAll proc {$ ?Ans} {Plus s(s(z)) s(z) Ans} end} '==' [s(s(s(z)))]} {StartTesting 'Plus backwards'} {Test {List.take {Solve proc {$ ?Ans} X#Y=Ans in {Plus X Y s(s(s(z)))} end} 4} '==' [z#s(s(s(z))) s(z)#s(s(z)) s(s(z))#s(z) s(s(s(z)))#z]} {StartTesting 'Times forwards'} {Test {SolveFirst proc {$ ?Ans} {Times z _ Ans} end} '==' z} {Test {SolveFirst proc {$ ?Ans} {Times s(z) s(s(s(z))) Ans} end} '==' s(s(s(z)))} {Test {SolveFirst proc {$ ?Ans} {Times s(s(s(z))) s(s(s(z))) Ans} end} '==' s(s(s(s(s(s(s(s(s(z)))))))))} {StartTesting 'Times backwards 1'} {Test {SolveFirst proc {$ ?Ans} X#Y=Ans in {Times X Y s(s(s(z)))} end} '==' s(z)#s(s(s(z)))} {StartTesting 'Times backwards 2'} {Test {List.take {Solve proc {$ ?Ans} X#Y=Ans in {Times X Y s(s(s(s(s(s(z))))))} end} 2} '==' [s(z)#s(s(s(s(s(s(z)))))) s(s(z))#s(s(s(z)))]} {StartTesting 'ToNat'} {Test {SolveFirst proc {$ ?Ans} Ans={ToNat 0} end} '==' z} {Test {SolveFirst proc {$ ?Ans} Ans={ToNat 6} end} '==' s(s(s(s(s(s(z))))))} {Test {SolveFirst proc {$ ?Ans} Ans={ToNat 7} end} '==' s(s(s(s(s(s(s(z)))))))} {StartTesting 'ToInt'} {Test {SolveFirst proc {$ ?Ans} Ans={ToInt z} end} '==' 0} {Test {SolveFirst proc {$ ?Ans} Ans={ToInt s(s(s(s(s(s(z))))))} end} '==' 6} {StartTesting 'Times again'} {Test {SolveFirst proc {$ ?Ans} local XTimesYAsNat X={ToNat 3} Y={ToNat 4} in {Times X Y XTimesYAsNat} Ans={ToInt XTimesYAsNat} end end} '==' 12} {Test {SolveFirst proc {$ ?Ans} local XTimesYAsNat X={ToNat 60} Y={ToNat 7} in {Times X Y XTimesYAsNat} Ans={ToInt XTimesYAsNat} end end} '==' 420}