X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Flambda2-test.js;fp=code%2Flambda2-test.js;h=09a1b5bc528c358a9d7724c187909dd2c67ea63b;hp=0000000000000000000000000000000000000000;hb=98652627403eaa920f51cedc4d0cc68c1103b972;hpb=904d62aef970037420a9f3e78d9ebc994e524063;ds=sidebyside

diff --git a/code/lambda2-test.js b/code/lambda2-test.js
new file mode 100644
index 00000000..09a1b5bc
--- /dev/null
+++ b/code/lambda2-test.js
@@ -0,0 +1,651 @@
+load("lambda2.js");
+
+
+var g_eta = false;
+var g_cbv = false;
+
+function to_int(expr) {
+	var reduced = reduce(expr, g_eta, g_cbv);
+	if (reduced.to_int) {
+		return reduce(reduced, false, false).to_int(0);
+	} else {
+		return "not a church numeral";
+	}
+}
+
+function to_string(expr) {
+	var reduced = reduce(expr, g_eta, g_cbv);
+	return reduced.to_string();
+}
+
+
+function test() {
+
+	function make_lam2(a, b, aa) {
+		return make_lam(a, make_lam(b, aa));
+	}
+	function make_lam3(a, b, c, aa) {
+		return make_lam(a, make_lam(b, make_lam(c, aa)));
+	}
+	function make_lam4(a, b, c, d, aa) {
+		return make_lam(a, make_lam(b, make_lam(c, make_lam(d, aa))));
+	}
+	function make_lam5(a, b, c, d, e, aa) {
+		return make_lam(a, make_lam(b, make_lam(c, make_lam(d, make_lam(e, aa)))));
+	}
+	function make_app3(aa, bb, cc) {
+		return make_app(make_app(aa, bb), cc);
+	}
+	function make_app4(aa, bb, cc, dd) {
+		return make_app(make_app(make_app(aa, bb), cc), dd);
+	}
+	function make_app5(aa, bb, cc, dd, ee) {
+		return make_app(make_app(make_app(make_app(aa, bb), cc), dd), ee);
+	}
+
+	var s = make_var("s");
+	var z = make_var("z");
+	var m = make_var("m");
+	var n = make_var("n");
+	var u = make_var("u");
+	var v = make_var("v");
+	var d = make_var("d");
+	var ss = new Lambda_var(s);
+	var zz = new Lambda_var(z);
+	var mm = new Lambda_var(m);
+	var nn = new Lambda_var(n);
+	var uu = new Lambda_var(u);
+	var vv = new Lambda_var(v);
+	var dd = new Lambda_var(d);
+	var succ = make_lam3(m, s, z, make_app(ss, make_app3(mm, ss, zz)));
+	var tt = make_lam2(m, n, mm);
+	var ff = make_lam2(m, n, nn);
+	var kk = tt;
+	var get1 = tt;
+	var get2 = ff;
+	var id = make_lam(s, ss);
+	var ww = make_lam(s, make_app(ss, ss));
+	var pair = make_lam3(m, n, s, make_app3(ss, mm, nn));
+	var zero = make_lam2(s, z, zz);
+	var one = make_lam2(s, z, make_app(ss, zz));
+	var two = make_lam2(s, z, make_app(ss, make_app(ss, zz)));
+	var three = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, zz))));
+	var four = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, make_app(ss, zz)))));
+	var five = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, make_app(ss, make_app(ss, zz))))));
+	var iszero = make_lam(m, make_app3(mm, make_lam(s, ff), tt));
+	var add = make_lam2(m, n, make_app3(mm, succ, nn));
+	var mul = make_lam3(m, n, s, make_app(mm, make_app(nn, ss)));
+	var pred1 = make_lam3(n, s, z, make_app4(nn, make_lam2(u, v, make_app(vv, make_app(uu, ss))), make_app(kk, zz), id));
+
+	var shift = make_lam(s, make_app(ss, make_lam2(m, n, make_app3(pair, make_app(succ, mm), mm))));
+	var pred2 = make_lam(n, make_app4(nn, shift, make_app3(pair, zero, zero), get2));
+
+
+	function make_sub() {
+		var mzero = make_app(make_app(pair, zero), id);
+		var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss))))));
+		var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
+		return make_lam(m, make_lam(n, make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1)));
+	}
+	var sub = make_sub();
+
+	var min = make_lam(m, make_lam(n, make_app(make_app(sub, mm), make_app(make_app(sub, mm), nn))));
+	var max = make_lam(m, make_lam(n, make_app(make_app(add, nn), make_app(make_app(sub, mm), nn))));
+
+	function make_lt() {
+		var mzero = make_app(make_app(pair, zero), id);
+		var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss))))));
+		var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
+		return make_lam(n, make_lam(m, make_app(make_app(make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1), make_lam(s, tt)), ff)));
+	}
+	var lt = make_lt();
+
+	function make_leq() {
+		var mzero = make_app(make_app(pair, zero), id);
+		var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss))))));
+		var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
+		return make_lam(m, make_lam(n, make_app(make_app(make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1), make_lam(s, ff)), tt)));
+	}
+	var leq = make_leq();
+
+	function make_eq() {
+		var mzero = make_app(make_app(pair, zero), make_app(kk, make_app(make_app(pair, one), id)));
+		var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss))))));
+		var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
+		return make_lam(m, make_lam(n, make_app(make_app(make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1), make_lam(s, ff)), tt)));
+	}
+	var eq = make_eq();
+
+	function make_divmod() {
+		var triple = make_lam4(m, n, z, s, make_app4(ss, mm, nn, zz));
+		var mzero = make_app4(triple, succ, make_app(kk, zero), id);
+		var msucc = make_lam(u, make_app4(triple, id, succ, make_app(kk, uu)));
+		// mtail is open in d
+		var mtail = make_lam(s, make_app(ss, make_lam5(m, n, u, v, z, make_lam(s, make_app3(zz, dd, make_app3(ss, make_app(uu, mm), make_app(vv, nn)))))));
+		var res = make_lam2(n, u, make_app3(
+				make_lam(d, make_app3(nn, mtail, make_lam(s, make_app(dd, make_app3(ss, zero, zero))))),
+				make_app4(uu, msucc, mzero, make_lam3(m, n, s, make_app(ss, zz))),
+				make_lam5(m, n, u, v, s, make_app3(pair, mm, nn))
+			));
+		return res;
+	}
+	var divmod = make_divmod();
+	var div = make_lam2(n, m, make_app4(divmod, nn, mm, get1));
+	var mod = make_lam2(n, m, make_app4(divmod, nn, mm, get2));
+
+	var yhalf = make_lam(u, make_app(vv, make_app(uu, uu)));
+	var y = make_lam(v, make_app(yhalf, yhalf));
+	var yyhalf = make_lam(u, make_app(vv, make_lam(n, make_app3(uu, uu, nn))))
+	var yy = make_lam(v, make_app(yyhalf, yyhalf));
+
+	var turinghalf = make_lam2(u, v, make_app(vv, make_app3(uu, uu, vv)));
+	var turing = make_app(turinghalf, turinghalf);
+	var tturinghalf = make_lam2(u, v, make_app(vv, make_lam(m, make_app4(uu, uu, vv, mm))));
+	var tturing = make_app(tturinghalf, tturinghalf);
+
+	var ifzero = make_lam(n, make_app4(nn, make_lam2(u, v, make_app(vv, make_app(uu, succ))), make_app(kk, zero), make_lam3(m, s, z, make_app(ss, mm) )));
+
+	var fact1 = make_app(ww, make_lam2(u, n, make_app4(ifzero, nn, make_lam(s, make_app3(mul, nn, make_app3(uu, uu, ss))), one)));
+	function make_fact(y) {
+		return make_app(y, make_lam2(u, n, make_app4(ifzero, nn, make_lam(s, make_app3(mul, nn, make_app(uu, ss))), one)));
+	}
+	var fact2 = make_fact(y);
+	var fact3 = make_fact(yy);
+	var fact4 = make_fact(turing);
+	var fact5 = make_fact(tturing);
+
+	function check(expect, formula) {
+		var i = to_int(formula);
+		print(expect, expect === i);
+	}
+
+	function checkbool(expect, index, formula) {
+		if (expect) {
+			print(index, equal(reduce(formula, g_eta, g_cbv), tt));
+		} else {
+			print(index, equal(reduce(formula, g_eta, g_cbv), ff));
+		}
+	}
+
+	check(0, zero);
+	check(1, one);
+	check(2, two);
+	check(3, three);
+	check(4, four);
+	check(5, five);
+
+	check(1, make_app(succ, zero));
+	check(2, make_app(succ, make_app(succ, zero)));
+	check(3, make_app(succ, make_app(succ, make_app(succ, zero))));
+	check(4, make_app(succ, make_app(succ, make_app(succ, make_app(succ, zero)))));
+	check(5, make_app(succ, make_app(succ, make_app(succ, make_app(succ, make_app(succ, zero))))));
+
+
+	check(2, make_app(succ, one));
+	check(3, make_app(succ, make_app(succ, one)));
+	check(4, make_app(succ, make_app(succ, make_app(succ, one))));
+	check(5, make_app(succ, make_app(succ, make_app(succ, make_app(succ, one)))));
+
+	check(3, make_app(succ, two));
+	check(4, make_app(succ, make_app(succ, two)));
+	check(5, make_app(succ, make_app(succ, make_app(succ, two))));
+
+	print("checking iszero");
+	checkbool(true, 0, make_app(iszero, zero));
+	checkbool(true, 1, make_app(iszero, one));
+	checkbool(true, 2, make_app(iszero, two));
+	checkbool(true, 3, make_app(iszero, three));
+	checkbool(true, 4, make_app(iszero, four));
+	checkbool(true, 5, make_app(iszero, five));
+
+	print("checking add");
+	check(0, make_app(make_app(add, zero), zero));
+	check(1, make_app(make_app(add, zero), one));
+	check(2, make_app(make_app(add, zero), two));
+	check(3, make_app(make_app(add, zero), three));
+	check(4, make_app(make_app(add, zero), four));
+	check(5, make_app(make_app(add, zero), five));
+	check(1, make_app(make_app(add, one), zero));
+	check(2, make_app(make_app(add, one), one));
+	check(3, make_app(make_app(add, one), two));
+	check(4, make_app(make_app(add, one), three));
+	check(5, make_app(make_app(add, one), four));
+	check(6, make_app(make_app(add, one), five));
+	check(2, make_app(make_app(add, two), zero));
+	check(3, make_app(make_app(add, two), one));
+	check(4, make_app(make_app(add, two), two));
+	check(5, make_app(make_app(add, two), three));
+	check(6, make_app(make_app(add, two), four));
+	check(7, make_app(make_app(add, two), five));
+	check(3, make_app(make_app(add, three), zero));
+	check(4, make_app(make_app(add, three), one));
+	check(5, make_app(make_app(add, three), two));
+	check(6, make_app(make_app(add, three), three));
+	check(7, make_app(make_app(add, three), four));
+	check(8, make_app(make_app(add, three), five));
+	check(4, make_app(make_app(add, four), zero));
+	check(5, make_app(make_app(add, four), one));
+	check(6, make_app(make_app(add, four), two));
+	check(7, make_app(make_app(add, four), three));
+	check(8, make_app(make_app(add, four), four));
+	check(9, make_app(make_app(add, four), five));
+
+	print("checking mul");
+	check(0, make_app(make_app(mul, zero), zero));
+	check(0, make_app(make_app(mul, zero), one));
+	check(0, make_app(make_app(mul, zero), two));
+	check(0, make_app(make_app(mul, zero), three));
+	check(0, make_app(make_app(mul, zero), four));
+	check(0, make_app(make_app(mul, zero), five));
+	check(0, make_app(make_app(mul, one), zero));
+	check(1, make_app(make_app(mul, one), one));
+	check(2, make_app(make_app(mul, one), two));
+	check(3, make_app(make_app(mul, one), three));
+	check(4, make_app(make_app(mul, one), four));
+	check(5, make_app(make_app(mul, one), five));
+	check(0, make_app(make_app(mul, two), zero));
+	check(2, make_app(make_app(mul, two), one));
+	check(4, make_app(make_app(mul, two), two));
+	check(6, make_app(make_app(mul, two), three));
+	check(8, make_app(make_app(mul, two), four));
+	check(10, make_app(make_app(mul, two), five));
+	check(0, make_app(make_app(mul, three), zero));
+	check(3, make_app(make_app(mul, three), one));
+	check(6, make_app(make_app(mul, three), two));
+	check(9, make_app(make_app(mul, three), three));
+	check(12, make_app(make_app(mul, three), four));
+	check(15, make_app(make_app(mul, three), five));
+	check(0, make_app(make_app(mul, four), zero));
+	check(4, make_app(make_app(mul, four), one));
+	check(8, make_app(make_app(mul, four), two));
+	check(12, make_app(make_app(mul, four), three));
+	check(16, make_app(make_app(mul, four), four));
+	check(20, make_app(make_app(mul, four), five));
+
+
+	function check_pred(pred) {
+		check(0, make_app(pred, zero));
+		check(0, make_app(pred, make_app(pred, zero)));
+		check(0, make_app(pred, make_app(pred, make_app(pred, zero))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, zero)))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, zero))))));
+
+		check(0, make_app(pred, one));
+		check(0, make_app(pred, make_app(pred, one)));
+		check(0, make_app(pred, make_app(pred, make_app(pred, one))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, one)))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, one))))));
+
+		check(1, make_app(pred, two));
+		check(0, make_app(pred, make_app(pred, two)));
+		check(0, make_app(pred, make_app(pred, make_app(pred, two))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, two)))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, two))))));
+
+		check(2, make_app(pred, three));
+		check(1, make_app(pred, make_app(pred, three)));
+		check(0, make_app(pred, make_app(pred, make_app(pred, three))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, three)))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, three))))));
+
+		check(3, make_app(pred, four));
+		check(2, make_app(pred, make_app(pred, four)));
+		check(1, make_app(pred, make_app(pred, make_app(pred, four))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, four)))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, four))))));
+
+		check(4, make_app(pred, five));
+		check(3, make_app(pred, make_app(pred, five)));
+		check(2, make_app(pred, make_app(pred, make_app(pred, five))));
+		check(1, make_app(pred, make_app(pred, make_app(pred, make_app(pred, five)))));
+		check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, five))))));
+	}
+
+	print("checking pred1");
+	check_pred(pred1);
+
+	print("checking pred2");
+	check_pred(pred2);
+
+	print("checking sub");
+	check(0, make_app(make_app(sub, zero), zero));
+	check(0, make_app(make_app(sub, zero), one));
+	check(0, make_app(make_app(sub, zero), two));
+	check(0, make_app(make_app(sub, zero), three));
+	check(0, make_app(make_app(sub, zero), four));
+	check(0, make_app(make_app(sub, zero), five));
+	check(1, make_app(make_app(sub, one), zero));
+	check(0, make_app(make_app(sub, one), one));
+	check(0, make_app(make_app(sub, one), two));
+	check(0, make_app(make_app(sub, one), three));
+	check(0, make_app(make_app(sub, one), four));
+	check(0, make_app(make_app(sub, one), five));
+	check(2, make_app(make_app(sub, two), zero));
+	check(1, make_app(make_app(sub, two), one));
+	check(0, make_app(make_app(sub, two), two));
+	check(0, make_app(make_app(sub, two), three));
+	check(0, make_app(make_app(sub, two), four));
+	check(0, make_app(make_app(sub, two), five));
+	check(3, make_app(make_app(sub, three), zero));
+	check(2, make_app(make_app(sub, three), one));
+	check(1, make_app(make_app(sub, three), two));
+	check(0, make_app(make_app(sub, three), three));
+	check(0, make_app(make_app(sub, three), four));
+	check(0, make_app(make_app(sub, three), five));
+	check(4, make_app(make_app(sub, four), zero));
+	check(3, make_app(make_app(sub, four), one));
+	check(2, make_app(make_app(sub, four), two));
+	check(1, make_app(make_app(sub, four), three));
+	check(0, make_app(make_app(sub, four), four));
+	check(0, make_app(make_app(sub, four), five));
+	check(5, make_app(make_app(sub, five), zero));
+	check(4, make_app(make_app(sub, five), one));
+	check(3, make_app(make_app(sub, five), two));
+	check(2, make_app(make_app(sub, five), three));
+	check(1, make_app(make_app(sub, five), four));
+	check(0, make_app(make_app(sub, five), five));
+
+	print("checking min");
+	check(0, make_app(make_app(min, zero), zero));
+	check(0, make_app(make_app(min, zero), one));
+	check(0, make_app(make_app(min, zero), two));
+	check(0, make_app(make_app(min, zero), three));
+	check(0, make_app(make_app(min, zero), four));
+	check(0, make_app(make_app(min, zero), five));
+	check(0, make_app(make_app(min, one), zero));
+	check(1, make_app(make_app(min, one), one));
+	check(1, make_app(make_app(min, one), two));
+	check(1, make_app(make_app(min, one), three));
+	check(1, make_app(make_app(min, one), four));
+	check(1, make_app(make_app(min, one), five));
+	check(0, make_app(make_app(min, two), zero));
+	check(1, make_app(make_app(min, two), one));
+	check(2, make_app(make_app(min, two), two));
+	check(2, make_app(make_app(min, two), three));
+	check(2, make_app(make_app(min, two), four));
+	check(2, make_app(make_app(min, two), five));
+	check(0, make_app(make_app(min, three), zero));
+	check(1, make_app(make_app(min, three), one));
+	check(2, make_app(make_app(min, three), two));
+	check(3, make_app(make_app(min, three), three));
+	check(3, make_app(make_app(min, three), four));
+	check(3, make_app(make_app(min, three), five));
+	check(0, make_app(make_app(min, four), zero));
+	check(1, make_app(make_app(min, four), one));
+	check(2, make_app(make_app(min, four), two));
+	check(3, make_app(make_app(min, four), three));
+	check(4, make_app(make_app(min, four), four));
+	check(4, make_app(make_app(min, four), five));
+	check(0, make_app(make_app(min, five), zero));
+	check(1, make_app(make_app(min, five), one));
+	check(2, make_app(make_app(min, five), two));
+	check(3, make_app(make_app(min, five), three));
+	check(4, make_app(make_app(min, five), four));
+	check(5, make_app(make_app(min, five), five));
+
+	print("checking max");
+	check(0, make_app(make_app(max, zero), zero));
+	check(1, make_app(make_app(max, zero), one));
+	check(2, make_app(make_app(max, zero), two));
+	check(3, make_app(make_app(max, zero), three));
+	check(4, make_app(make_app(max, zero), four));
+	check(5, make_app(make_app(max, zero), five));
+	check(1, make_app(make_app(max, one), zero));
+	check(1, make_app(make_app(max, one), one));
+	check(2, make_app(make_app(max, one), two));
+	check(3, make_app(make_app(max, one), three));
+	check(4, make_app(make_app(max, one), four));
+	check(5, make_app(make_app(max, one), five));
+	check(2, make_app(make_app(max, two), zero));
+	check(2, make_app(make_app(max, two), one));
+	check(2, make_app(make_app(max, two), two));
+	check(3, make_app(make_app(max, two), three));
+	check(4, make_app(make_app(max, two), four));
+	check(5, make_app(make_app(max, two), five));
+	check(3, make_app(make_app(max, three), zero));
+	check(3, make_app(make_app(max, three), one));
+	check(3, make_app(make_app(max, three), two));
+	check(3, make_app(make_app(max, three), three));
+	check(4, make_app(make_app(max, three), four));
+	check(5, make_app(make_app(max, three), five));
+	check(4, make_app(make_app(max, four), zero));
+	check(4, make_app(make_app(max, four), one));
+	check(4, make_app(make_app(max, four), two));
+	check(4, make_app(make_app(max, four), three));
+	check(4, make_app(make_app(max, four), four));
+	check(5, make_app(make_app(max, four), five));
+	check(5, make_app(make_app(max, five), zero));
+	check(5, make_app(make_app(max, five), one));
+	check(5, make_app(make_app(max, five), two));
+	check(5, make_app(make_app(max, five), three));
+	check(5, make_app(make_app(max, five), four));
+	check(5, make_app(make_app(max, five), five));
+
+	print("checking lt");
+	checkbool(false, 0, make_app(make_app(lt, zero), zero));
+	checkbool(true, 0, make_app(make_app(lt, zero), one));
+	checkbool(true, 0, make_app(make_app(lt, zero), two));
+	checkbool(true, 0, make_app(make_app(lt, zero), three));
+	checkbool(true, 0, make_app(make_app(lt, zero), four));
+	checkbool(true, 0, make_app(make_app(lt, zero), five));
+	checkbool(false, 1, make_app(make_app(lt, one), zero));
+	checkbool(false, 1, make_app(make_app(lt, one), one));
+	checkbool(true, 1, make_app(make_app(lt, one), two));
+	checkbool(true, 1, make_app(make_app(lt, one), three));
+	checkbool(true, 1, make_app(make_app(lt, one), four));
+	checkbool(true, 1, make_app(make_app(lt, one), five));
+	checkbool(false, 2, make_app(make_app(lt, two), zero));
+	checkbool(false, 2, make_app(make_app(lt, two), one));
+	checkbool(false, 2, make_app(make_app(lt, two), two));
+	checkbool(true, 2, make_app(make_app(lt, two), three));
+	checkbool(true, 2, make_app(make_app(lt, two), four));
+	checkbool(true, 2, make_app(make_app(lt, two), five));
+	checkbool(false, 3, make_app(make_app(lt, three), zero));
+	checkbool(false, 3, make_app(make_app(lt, three), one));
+	checkbool(false, 3, make_app(make_app(lt, three), two));
+	checkbool(false, 3, make_app(make_app(lt, three), three));
+	checkbool(true, 3, make_app(make_app(lt, three), four));
+	checkbool(true, 3, make_app(make_app(lt, three), five));
+	checkbool(false, 4, make_app(make_app(lt, four), zero));
+	checkbool(false, 4, make_app(make_app(lt, four), one));
+	checkbool(false, 4, make_app(make_app(lt, four), two));
+	checkbool(false, 4, make_app(make_app(lt, four), three));
+	checkbool(false, 4, make_app(make_app(lt, four), four));
+	checkbool(true, 4, make_app(make_app(lt, four), five));
+	checkbool(false, 5, make_app(make_app(lt, five), zero));
+	checkbool(false, 5, make_app(make_app(lt, five), one));
+	checkbool(false, 5, make_app(make_app(lt, five), two));
+	checkbool(false, 5, make_app(make_app(lt, five), three));
+	checkbool(false, 5, make_app(make_app(lt, five), four));
+	checkbool(false, 5, make_app(make_app(lt, five), five));
+
+	print("checking leq");
+	checkbool(true, 0, make_app(make_app(leq, zero), zero));
+	checkbool(true, 0, make_app(make_app(leq, zero), one));
+	checkbool(true, 0, make_app(make_app(leq, zero), two));
+	checkbool(true, 0, make_app(make_app(leq, zero), three));
+	checkbool(true, 0, make_app(make_app(leq, zero), four));
+	checkbool(true, 0, make_app(make_app(leq, zero), five));
+	checkbool(false, 1, make_app(make_app(leq, one), zero));
+	checkbool(true, 1, make_app(make_app(leq, one), one));
+	checkbool(true, 1, make_app(make_app(leq, one), two));
+	checkbool(true, 1, make_app(make_app(leq, one), three));
+	checkbool(true, 1, make_app(make_app(leq, one), four));
+	checkbool(true, 1, make_app(make_app(leq, one), five));
+	checkbool(false, 2, make_app(make_app(leq, two), zero));
+	checkbool(false, 2, make_app(make_app(leq, two), one));
+	checkbool(true, 2, make_app(make_app(leq, two), two));
+	checkbool(true, 2, make_app(make_app(leq, two), three));
+	checkbool(true, 2, make_app(make_app(leq, two), four));
+	checkbool(true, 2, make_app(make_app(leq, two), five));
+	checkbool(false, 3, make_app(make_app(leq, three), zero));
+	checkbool(false, 3, make_app(make_app(leq, three), one));
+	checkbool(false, 3, make_app(make_app(leq, three), two));
+	checkbool(true, 3, make_app(make_app(leq, three), three));
+	checkbool(true, 3, make_app(make_app(leq, three), four));
+	checkbool(true, 3, make_app(make_app(leq, three), five));
+	checkbool(false, 4, make_app(make_app(leq, four), zero));
+	checkbool(false, 4, make_app(make_app(leq, four), one));
+	checkbool(false, 4, make_app(make_app(leq, four), two));
+	checkbool(false, 4, make_app(make_app(leq, four), three));
+	checkbool(true, 4, make_app(make_app(leq, four), four));
+	checkbool(true, 4, make_app(make_app(leq, four), five));
+	checkbool(false, 5, make_app(make_app(leq, five), zero));
+	checkbool(false, 5, make_app(make_app(leq, five), one));
+	checkbool(false, 5, make_app(make_app(leq, five), two));
+	checkbool(false, 5, make_app(make_app(leq, five), three));
+	checkbool(false, 5, make_app(make_app(leq, five), four));
+	checkbool(true, 5, make_app(make_app(leq, five), five));
+
+	print("checking eq");
+	checkbool(true, 0, make_app(make_app(eq, zero), zero));
+	checkbool(false, 0, make_app(make_app(eq, zero), one));
+	checkbool(false, 0, make_app(make_app(eq, zero), two));
+	checkbool(false, 0, make_app(make_app(eq, zero), three));
+	checkbool(false, 0, make_app(make_app(eq, zero), four));
+	checkbool(false, 0, make_app(make_app(eq, zero), five));
+	checkbool(false, 1, make_app(make_app(eq, one), zero));
+	checkbool(true, 1, make_app(make_app(eq, one), one));
+	checkbool(false, 1, make_app(make_app(eq, one), two));
+	checkbool(false, 1, make_app(make_app(eq, one), three));
+	checkbool(false, 1, make_app(make_app(eq, one), four));
+	checkbool(false, 1, make_app(make_app(eq, one), five));
+	checkbool(false, 2, make_app(make_app(eq, two), zero));
+	checkbool(false, 2, make_app(make_app(eq, two), one));
+	checkbool(true, 2, make_app(make_app(eq, two), two));
+	checkbool(false, 2, make_app(make_app(eq, two), three));
+	checkbool(false, 2, make_app(make_app(eq, two), four));
+	checkbool(false, 2, make_app(make_app(eq, two), five));
+	checkbool(false, 3, make_app(make_app(eq, three), zero));
+	checkbool(false, 3, make_app(make_app(eq, three), one));
+	checkbool(false, 3, make_app(make_app(eq, three), two));
+	checkbool(true, 3, make_app(make_app(eq, three), three));
+	checkbool(false, 3, make_app(make_app(eq, three), four));
+	checkbool(false, 3, make_app(make_app(eq, three), five));
+	checkbool(false, 4, make_app(make_app(eq, four), zero));
+	checkbool(false, 4, make_app(make_app(eq, four), one));
+	checkbool(false, 4, make_app(make_app(eq, four), two));
+	checkbool(false, 4, make_app(make_app(eq, four), three));
+	checkbool(true, 4, make_app(make_app(eq, four), four));
+	checkbool(false, 4, make_app(make_app(eq, four), five));
+	checkbool(false, 5, make_app(make_app(eq, five), zero));
+	checkbool(false, 5, make_app(make_app(eq, five), one));
+	checkbool(false, 5, make_app(make_app(eq, five), two));
+	checkbool(false, 5, make_app(make_app(eq, five), three));
+	checkbool(false, 5, make_app(make_app(eq, five), four));
+	checkbool(true, 5, make_app(make_app(eq, five), five));
+
+	print("checking div");
+	check(0, make_app(make_app(div, zero), one));
+	check(0, make_app(make_app(div, zero), two));
+	check(0, make_app(make_app(div, zero), three));
+	check(0, make_app(make_app(div, zero), four));
+	check(0, make_app(make_app(div, zero), five));
+	check(1, make_app(make_app(div, one), one));
+	check(0, make_app(make_app(div, one), two));
+	check(0, make_app(make_app(div, one), three));
+	check(0, make_app(make_app(div, one), four));
+	check(0, make_app(make_app(div, one), five));
+	check(2, make_app(make_app(div, two), one));
+	check(1, make_app(make_app(div, two), two));
+	check(0, make_app(make_app(div, two), three));
+	check(0, make_app(make_app(div, two), four));
+	check(0, make_app(make_app(div, two), five));
+	check(3, make_app(make_app(div, three), one));
+	check(1, make_app(make_app(div, three), two));
+	check(1, make_app(make_app(div, three), three));
+	check(0, make_app(make_app(div, three), four));
+	check(0, make_app(make_app(div, three), five));
+	check(4, make_app(make_app(div, four), one));
+	check(2, make_app(make_app(div, four), two));
+	check(1, make_app(make_app(div, four), three));
+	check(1, make_app(make_app(div, four), four));
+	check(0, make_app(make_app(div, four), five));
+	check(5, make_app(make_app(div, five), one));
+	check(2, make_app(make_app(div, five), two));
+	check(1, make_app(make_app(div, five), three));
+	check(1, make_app(make_app(div, five), four));
+	check(1, make_app(make_app(div, five), five));
+
+	print("checking mod");
+	check(0, make_app(make_app(mod, zero), one));
+	check(0, make_app(make_app(mod, zero), two));
+	check(0, make_app(make_app(mod, zero), three));
+	check(0, make_app(make_app(mod, zero), four));
+	check(0, make_app(make_app(mod, zero), five));
+	check(0, make_app(make_app(mod, one), one));
+	check(1, make_app(make_app(mod, one), two));
+	check(1, make_app(make_app(mod, one), three));
+	check(1, make_app(make_app(mod, one), four));
+	check(1, make_app(make_app(mod, one), five));
+	check(0, make_app(make_app(mod, two), one));
+	check(0, make_app(make_app(mod, two), two));
+	check(2, make_app(make_app(mod, two), three));
+	check(2, make_app(make_app(mod, two), four));
+	check(2, make_app(make_app(mod, two), five));
+	check(0, make_app(make_app(mod, three), one));
+	check(1, make_app(make_app(mod, three), two));
+	check(0, make_app(make_app(mod, three), three));
+	check(3, make_app(make_app(mod, three), four));
+	check(3, make_app(make_app(mod, three), five));
+	check(0, make_app(make_app(mod, four), one));
+	check(0, make_app(make_app(mod, four), two));
+	check(1, make_app(make_app(mod, four), three));
+	check(0, make_app(make_app(mod, four), four));
+	check(4, make_app(make_app(mod, four), five));
+	check(0, make_app(make_app(mod, five), one));
+	check(1, make_app(make_app(mod, five), two));
+	check(2, make_app(make_app(mod, five), three));
+	check(1, make_app(make_app(mod, five), four));
+	check(0, make_app(make_app(mod, five), five));
+
+	if (!g_cbv) {
+		print("checking fact1");
+		check(1, make_app(fact1, zero));
+		check(1, make_app(fact1, one));
+		check(2, make_app(fact1, two));
+		check(6, make_app(fact1, three));
+		check(24, make_app(fact1, four));
+	}
+
+	if (!g_cbv) {
+		print("checking fact2");
+		check(1, make_app(fact2, zero));
+		check(1, make_app(fact2, one));
+		check(2, make_app(fact2, two));
+		check(6, make_app(fact2, three));
+		check(24, make_app(fact2, four));
+	}
+
+	if (g_cbv<2) {
+		print("checking fact3");
+		check(1, make_app(fact3, zero));
+		check(1, make_app(fact3, one));
+		check(2, make_app(fact3, two));
+		check(6, make_app(fact3, three));
+		check(24, make_app(fact3, four));
+	}
+
+	if (!g_cbv) {
+		print("checking fact4");
+		check(1, make_app(fact4, zero));
+		check(1, make_app(fact4, one));
+		check(2, make_app(fact4, two));
+		check(6, make_app(fact4, three));
+		check(24, make_app(fact4, four));
+	}
+
+	if (g_cbv<2) {
+		print("checking fact5");
+		check(1, make_app(fact5, zero));
+		check(1, make_app(fact5, one));
+		check(2, make_app(fact5, two));
+		check(6, make_app(fact5, three));
+		check(24, make_app(fact5, four));
+	}
+
+}
+
+
+test();
+