posted assignment4
[lambda.git] / code / lambda-test.js
1 load("lambda.js");
2
3
4 var g_eta = false;
5 var g_cbv = false;
6
7 function to_int(expr) {
8         var reduced = reduce(expr, g_eta, g_cbv);
9         if (reduced.to_int) {
10                 return reduce(reduced, false, false).to_int(0);
11         } else {
12                 return "not a church numeral";
13         }
14 }
15
16 function to_string(expr) {
17         var reduced = reduce(expr, g_eta, g_cbv);
18         return reduced.to_string();
19 }
20
21
22 function test() {
23
24         function make_lam2(a, b, aa) {
25                 return make_lam(a, make_lam(b, aa));
26         }
27         function make_lam3(a, b, c, aa) {
28                 return make_lam(a, make_lam(b, make_lam(c, aa)));
29         }
30         function make_lam4(a, b, c, d, aa) {
31                 return make_lam(a, make_lam(b, make_lam(c, make_lam(d, aa))));
32         }
33         function make_lam5(a, b, c, d, e, aa) {
34                 return make_lam(a, make_lam(b, make_lam(c, make_lam(d, make_lam(e, aa)))));
35         }
36         function make_app3(aa, bb, cc) {
37                 return make_app(make_app(aa, bb), cc);
38         }
39         function make_app4(aa, bb, cc, dd) {
40                 return make_app(make_app(make_app(aa, bb), cc), dd);
41         }
42         function make_app5(aa, bb, cc, dd, ee) {
43                 return make_app(make_app(make_app(make_app(aa, bb), cc), dd), ee);
44         }
45
46         var s = make_var("s");
47         var z = make_var("z");
48         var m = make_var("m");
49         var n = make_var("n");
50         var u = make_var("u");
51         var v = make_var("v");
52         var d = make_var("d");
53         var ss = new Lambda_var(s);
54         var zz = new Lambda_var(z);
55         var mm = new Lambda_var(m);
56         var nn = new Lambda_var(n);
57         var uu = new Lambda_var(u);
58         var vv = new Lambda_var(v);
59         var dd = new Lambda_var(d);
60         var succ = make_lam3(m, s, z, make_app(ss, make_app3(mm, ss, zz)));
61         var tt = make_lam2(m, n, mm);
62         var ff = make_lam2(m, n, nn);
63         var kk = tt;
64         var get1 = tt;
65         var get2 = ff;
66         var id = make_lam(s, ss);
67         var ww = make_lam(s, make_app(ss, ss));
68         var pair = make_lam3(m, n, s, make_app3(ss, mm, nn));
69         var zero = make_lam2(s, z, zz);
70         var one = make_lam2(s, z, make_app(ss, zz));
71         var two = make_lam2(s, z, make_app(ss, make_app(ss, zz)));
72         var three = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, zz))));
73         var four = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, make_app(ss, zz)))));
74         var five = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, make_app(ss, make_app(ss, zz))))));
75         var iszero = make_lam(m, make_app3(mm, make_lam(s, ff), tt));
76         var add = make_lam2(m, n, make_app3(mm, succ, nn));
77         var mul = make_lam3(m, n, s, make_app(mm, make_app(nn, ss)));
78         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));
79
80         var shift = make_lam(s, make_app(ss, make_lam2(m, n, make_app3(pair, make_app(succ, mm), mm))));
81         var pred2 = make_lam(n, make_app4(nn, shift, make_app3(pair, zero, zero), get2));
82
83
84         function make_sub() {
85                 var mzero = make_app(make_app(pair, zero), id);
86                 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))))));
87                 var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
88                 return make_lam(m, make_lam(n, make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1)));
89         }
90         var sub = make_sub();
91
92         var min = make_lam(m, make_lam(n, make_app(make_app(sub, mm), make_app(make_app(sub, mm), nn))));
93         var max = make_lam(m, make_lam(n, make_app(make_app(add, nn), make_app(make_app(sub, mm), nn))));
94
95         function make_lt() {
96                 var mzero = make_app(make_app(pair, zero), id);
97                 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))))));
98                 var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
99                 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)));
100         }
101         var lt = make_lt();
102
103         function make_leq() {
104                 var mzero = make_app(make_app(pair, zero), id);
105                 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))))));
106                 var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
107                 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)));
108         }
109         var leq = make_leq();
110
111         function make_eq() {
112                 var mzero = make_app(make_app(pair, zero), make_app(kk, make_app(make_app(pair, one), id)));
113                 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))))));
114                 var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
115                 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)));
116         }
117         var eq = make_eq();
118
119         function make_divmod() {
120                 var triple = make_lam4(m, n, z, s, make_app4(ss, mm, nn, zz));
121                 var mzero = make_app4(triple, succ, make_app(kk, zero), id);
122                 var msucc = make_lam(u, make_app4(triple, id, succ, make_app(kk, uu)));
123                 // mtail is open in d
124                 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)))))));
125                 var res = make_lam2(n, u, make_app3(
126                                 make_lam(d, make_app3(nn, mtail, make_lam(s, make_app(dd, make_app3(ss, zero, zero))))),
127                                 make_app4(uu, msucc, mzero, make_lam3(m, n, s, make_app(ss, zz))),
128                                 make_lam5(m, n, u, v, s, make_app3(pair, mm, nn))
129                         ));
130                 return res;
131         }
132         var divmod = make_divmod();
133         var div = make_lam2(n, m, make_app4(divmod, nn, mm, get1));
134         var mod = make_lam2(n, m, make_app4(divmod, nn, mm, get2));
135
136         var yhalf = make_lam(u, make_app(vv, make_app(uu, uu)));
137         var y = make_lam(v, make_app(yhalf, yhalf));
138         var yyhalf = make_lam(u, make_app(vv, make_lam(n, make_app3(uu, uu, nn))))
139         var yy = make_lam(v, make_app(yyhalf, yyhalf));
140
141         var turinghalf = make_lam2(u, v, make_app(vv, make_app3(uu, uu, vv)));
142         var turing = make_app(turinghalf, turinghalf);
143         var tturinghalf = make_lam2(u, v, make_app(vv, make_lam(m, make_app4(uu, uu, vv, mm))));
144         var tturing = make_app(tturinghalf, tturinghalf);
145
146         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) )));
147
148         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)));
149         function make_fact(y) {
150                 return make_app(y, make_lam2(u, n, make_app4(ifzero, nn, make_lam(s, make_app3(mul, nn, make_app(uu, ss))), one)));
151         }
152         var fact2 = make_fact(y);
153         var fact3 = make_fact(yy);
154         var fact4 = make_fact(turing);
155         var fact5 = make_fact(tturing);
156
157         function check(expect, formula) {
158                 var i = to_int(formula);
159                 print(expect, expect === i);
160         }
161
162         function checkbool(expect, index, formula) {
163                 if (expect) {
164                         print(index, equal(reduce(formula, g_eta, g_cbv), tt));
165                 } else {
166                         print(index, equal(reduce(formula, g_eta, g_cbv), ff));
167                 }
168         }
169
170         check(0, zero);
171         check(1, one);
172         check(2, two);
173         check(3, three);
174         check(4, four);
175         check(5, five);
176
177         check(1, make_app(succ, zero));
178         check(2, make_app(succ, make_app(succ, zero)));
179         check(3, make_app(succ, make_app(succ, make_app(succ, zero))));
180         check(4, make_app(succ, make_app(succ, make_app(succ, make_app(succ, zero)))));
181         check(5, make_app(succ, make_app(succ, make_app(succ, make_app(succ, make_app(succ, zero))))));
182
183
184         check(2, make_app(succ, one));
185         check(3, make_app(succ, make_app(succ, one)));
186         check(4, make_app(succ, make_app(succ, make_app(succ, one))));
187         check(5, make_app(succ, make_app(succ, make_app(succ, make_app(succ, one)))));
188
189         check(3, make_app(succ, two));
190         check(4, make_app(succ, make_app(succ, two)));
191         check(5, make_app(succ, make_app(succ, make_app(succ, two))));
192
193         print("checking iszero");
194         checkbool(true, 0, make_app(iszero, zero));
195         checkbool(true, 1, make_app(iszero, one));
196         checkbool(true, 2, make_app(iszero, two));
197         checkbool(true, 3, make_app(iszero, three));
198         checkbool(true, 4, make_app(iszero, four));
199         checkbool(true, 5, make_app(iszero, five));
200
201         print("checking add");
202         check(0, make_app(make_app(add, zero), zero));
203         check(1, make_app(make_app(add, zero), one));
204         check(2, make_app(make_app(add, zero), two));
205         check(3, make_app(make_app(add, zero), three));
206         check(4, make_app(make_app(add, zero), four));
207         check(5, make_app(make_app(add, zero), five));
208         check(1, make_app(make_app(add, one), zero));
209         check(2, make_app(make_app(add, one), one));
210         check(3, make_app(make_app(add, one), two));
211         check(4, make_app(make_app(add, one), three));
212         check(5, make_app(make_app(add, one), four));
213         check(6, make_app(make_app(add, one), five));
214         check(2, make_app(make_app(add, two), zero));
215         check(3, make_app(make_app(add, two), one));
216         check(4, make_app(make_app(add, two), two));
217         check(5, make_app(make_app(add, two), three));
218         check(6, make_app(make_app(add, two), four));
219         check(7, make_app(make_app(add, two), five));
220         check(3, make_app(make_app(add, three), zero));
221         check(4, make_app(make_app(add, three), one));
222         check(5, make_app(make_app(add, three), two));
223         check(6, make_app(make_app(add, three), three));
224         check(7, make_app(make_app(add, three), four));
225         check(8, make_app(make_app(add, three), five));
226         check(4, make_app(make_app(add, four), zero));
227         check(5, make_app(make_app(add, four), one));
228         check(6, make_app(make_app(add, four), two));
229         check(7, make_app(make_app(add, four), three));
230         check(8, make_app(make_app(add, four), four));
231         check(9, make_app(make_app(add, four), five));
232
233         print("checking mul");
234         check(0, make_app(make_app(mul, zero), zero));
235         check(0, make_app(make_app(mul, zero), one));
236         check(0, make_app(make_app(mul, zero), two));
237         check(0, make_app(make_app(mul, zero), three));
238         check(0, make_app(make_app(mul, zero), four));
239         check(0, make_app(make_app(mul, zero), five));
240         check(0, make_app(make_app(mul, one), zero));
241         check(1, make_app(make_app(mul, one), one));
242         check(2, make_app(make_app(mul, one), two));
243         check(3, make_app(make_app(mul, one), three));
244         check(4, make_app(make_app(mul, one), four));
245         check(5, make_app(make_app(mul, one), five));
246         check(0, make_app(make_app(mul, two), zero));
247         check(2, make_app(make_app(mul, two), one));
248         check(4, make_app(make_app(mul, two), two));
249         check(6, make_app(make_app(mul, two), three));
250         check(8, make_app(make_app(mul, two), four));
251         check(10, make_app(make_app(mul, two), five));
252         check(0, make_app(make_app(mul, three), zero));
253         check(3, make_app(make_app(mul, three), one));
254         check(6, make_app(make_app(mul, three), two));
255         check(9, make_app(make_app(mul, three), three));
256         check(12, make_app(make_app(mul, three), four));
257         check(15, make_app(make_app(mul, three), five));
258         check(0, make_app(make_app(mul, four), zero));
259         check(4, make_app(make_app(mul, four), one));
260         check(8, make_app(make_app(mul, four), two));
261         check(12, make_app(make_app(mul, four), three));
262         check(16, make_app(make_app(mul, four), four));
263         check(20, make_app(make_app(mul, four), five));
264
265
266         function check_pred(pred) {
267                 check(0, make_app(pred, zero));
268                 check(0, make_app(pred, make_app(pred, zero)));
269                 check(0, make_app(pred, make_app(pred, make_app(pred, zero))));
270                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, zero)))));
271                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, zero))))));
272
273                 check(0, make_app(pred, one));
274                 check(0, make_app(pred, make_app(pred, one)));
275                 check(0, make_app(pred, make_app(pred, make_app(pred, one))));
276                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, one)))));
277                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, one))))));
278
279                 check(1, make_app(pred, two));
280                 check(0, make_app(pred, make_app(pred, two)));
281                 check(0, make_app(pred, make_app(pred, make_app(pred, two))));
282                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, two)))));
283                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, two))))));
284
285                 check(2, make_app(pred, three));
286                 check(1, make_app(pred, make_app(pred, three)));
287                 check(0, make_app(pred, make_app(pred, make_app(pred, three))));
288                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, three)))));
289                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, three))))));
290
291                 check(3, make_app(pred, four));
292                 check(2, make_app(pred, make_app(pred, four)));
293                 check(1, make_app(pred, make_app(pred, make_app(pred, four))));
294                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, four)))));
295                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, four))))));
296
297                 check(4, make_app(pred, five));
298                 check(3, make_app(pred, make_app(pred, five)));
299                 check(2, make_app(pred, make_app(pred, make_app(pred, five))));
300                 check(1, make_app(pred, make_app(pred, make_app(pred, make_app(pred, five)))));
301                 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, five))))));
302         }
303
304         print("checking pred1");
305         check_pred(pred1);
306
307         print("checking pred2");
308         check_pred(pred2);
309
310         print("checking sub");
311         check(0, make_app(make_app(sub, zero), zero));
312         check(0, make_app(make_app(sub, zero), one));
313         check(0, make_app(make_app(sub, zero), two));
314         check(0, make_app(make_app(sub, zero), three));
315         check(0, make_app(make_app(sub, zero), four));
316         check(0, make_app(make_app(sub, zero), five));
317         check(1, make_app(make_app(sub, one), zero));
318         check(0, make_app(make_app(sub, one), one));
319         check(0, make_app(make_app(sub, one), two));
320         check(0, make_app(make_app(sub, one), three));
321         check(0, make_app(make_app(sub, one), four));
322         check(0, make_app(make_app(sub, one), five));
323         check(2, make_app(make_app(sub, two), zero));
324         check(1, make_app(make_app(sub, two), one));
325         check(0, make_app(make_app(sub, two), two));
326         check(0, make_app(make_app(sub, two), three));
327         check(0, make_app(make_app(sub, two), four));
328         check(0, make_app(make_app(sub, two), five));
329         check(3, make_app(make_app(sub, three), zero));
330         check(2, make_app(make_app(sub, three), one));
331         check(1, make_app(make_app(sub, three), two));
332         check(0, make_app(make_app(sub, three), three));
333         check(0, make_app(make_app(sub, three), four));
334         check(0, make_app(make_app(sub, three), five));
335         check(4, make_app(make_app(sub, four), zero));
336         check(3, make_app(make_app(sub, four), one));
337         check(2, make_app(make_app(sub, four), two));
338         check(1, make_app(make_app(sub, four), three));
339         check(0, make_app(make_app(sub, four), four));
340         check(0, make_app(make_app(sub, four), five));
341         check(5, make_app(make_app(sub, five), zero));
342         check(4, make_app(make_app(sub, five), one));
343         check(3, make_app(make_app(sub, five), two));
344         check(2, make_app(make_app(sub, five), three));
345         check(1, make_app(make_app(sub, five), four));
346         check(0, make_app(make_app(sub, five), five));
347
348         print("checking min");
349         check(0, make_app(make_app(min, zero), zero));
350         check(0, make_app(make_app(min, zero), one));
351         check(0, make_app(make_app(min, zero), two));
352         check(0, make_app(make_app(min, zero), three));
353         check(0, make_app(make_app(min, zero), four));
354         check(0, make_app(make_app(min, zero), five));
355         check(0, make_app(make_app(min, one), zero));
356         check(1, make_app(make_app(min, one), one));
357         check(1, make_app(make_app(min, one), two));
358         check(1, make_app(make_app(min, one), three));
359         check(1, make_app(make_app(min, one), four));
360         check(1, make_app(make_app(min, one), five));
361         check(0, make_app(make_app(min, two), zero));
362         check(1, make_app(make_app(min, two), one));
363         check(2, make_app(make_app(min, two), two));
364         check(2, make_app(make_app(min, two), three));
365         check(2, make_app(make_app(min, two), four));
366         check(2, make_app(make_app(min, two), five));
367         check(0, make_app(make_app(min, three), zero));
368         check(1, make_app(make_app(min, three), one));
369         check(2, make_app(make_app(min, three), two));
370         check(3, make_app(make_app(min, three), three));
371         check(3, make_app(make_app(min, three), four));
372         check(3, make_app(make_app(min, three), five));
373         check(0, make_app(make_app(min, four), zero));
374         check(1, make_app(make_app(min, four), one));
375         check(2, make_app(make_app(min, four), two));
376         check(3, make_app(make_app(min, four), three));
377         check(4, make_app(make_app(min, four), four));
378         check(4, make_app(make_app(min, four), five));
379         check(0, make_app(make_app(min, five), zero));
380         check(1, make_app(make_app(min, five), one));
381         check(2, make_app(make_app(min, five), two));
382         check(3, make_app(make_app(min, five), three));
383         check(4, make_app(make_app(min, five), four));
384         check(5, make_app(make_app(min, five), five));
385
386         print("checking max");
387         check(0, make_app(make_app(max, zero), zero));
388         check(1, make_app(make_app(max, zero), one));
389         check(2, make_app(make_app(max, zero), two));
390         check(3, make_app(make_app(max, zero), three));
391         check(4, make_app(make_app(max, zero), four));
392         check(5, make_app(make_app(max, zero), five));
393         check(1, make_app(make_app(max, one), zero));
394         check(1, make_app(make_app(max, one), one));
395         check(2, make_app(make_app(max, one), two));
396         check(3, make_app(make_app(max, one), three));
397         check(4, make_app(make_app(max, one), four));
398         check(5, make_app(make_app(max, one), five));
399         check(2, make_app(make_app(max, two), zero));
400         check(2, make_app(make_app(max, two), one));
401         check(2, make_app(make_app(max, two), two));
402         check(3, make_app(make_app(max, two), three));
403         check(4, make_app(make_app(max, two), four));
404         check(5, make_app(make_app(max, two), five));
405         check(3, make_app(make_app(max, three), zero));
406         check(3, make_app(make_app(max, three), one));
407         check(3, make_app(make_app(max, three), two));
408         check(3, make_app(make_app(max, three), three));
409         check(4, make_app(make_app(max, three), four));
410         check(5, make_app(make_app(max, three), five));
411         check(4, make_app(make_app(max, four), zero));
412         check(4, make_app(make_app(max, four), one));
413         check(4, make_app(make_app(max, four), two));
414         check(4, make_app(make_app(max, four), three));
415         check(4, make_app(make_app(max, four), four));
416         check(5, make_app(make_app(max, four), five));
417         check(5, make_app(make_app(max, five), zero));
418         check(5, make_app(make_app(max, five), one));
419         check(5, make_app(make_app(max, five), two));
420         check(5, make_app(make_app(max, five), three));
421         check(5, make_app(make_app(max, five), four));
422         check(5, make_app(make_app(max, five), five));
423
424         print("checking lt");
425         checkbool(false, 0, make_app(make_app(lt, zero), zero));
426         checkbool(true, 0, make_app(make_app(lt, zero), one));
427         checkbool(true, 0, make_app(make_app(lt, zero), two));
428         checkbool(true, 0, make_app(make_app(lt, zero), three));
429         checkbool(true, 0, make_app(make_app(lt, zero), four));
430         checkbool(true, 0, make_app(make_app(lt, zero), five));
431         checkbool(false, 1, make_app(make_app(lt, one), zero));
432         checkbool(false, 1, make_app(make_app(lt, one), one));
433         checkbool(true, 1, make_app(make_app(lt, one), two));
434         checkbool(true, 1, make_app(make_app(lt, one), three));
435         checkbool(true, 1, make_app(make_app(lt, one), four));
436         checkbool(true, 1, make_app(make_app(lt, one), five));
437         checkbool(false, 2, make_app(make_app(lt, two), zero));
438         checkbool(false, 2, make_app(make_app(lt, two), one));
439         checkbool(false, 2, make_app(make_app(lt, two), two));
440         checkbool(true, 2, make_app(make_app(lt, two), three));
441         checkbool(true, 2, make_app(make_app(lt, two), four));
442         checkbool(true, 2, make_app(make_app(lt, two), five));
443         checkbool(false, 3, make_app(make_app(lt, three), zero));
444         checkbool(false, 3, make_app(make_app(lt, three), one));
445         checkbool(false, 3, make_app(make_app(lt, three), two));
446         checkbool(false, 3, make_app(make_app(lt, three), three));
447         checkbool(true, 3, make_app(make_app(lt, three), four));
448         checkbool(true, 3, make_app(make_app(lt, three), five));
449         checkbool(false, 4, make_app(make_app(lt, four), zero));
450         checkbool(false, 4, make_app(make_app(lt, four), one));
451         checkbool(false, 4, make_app(make_app(lt, four), two));
452         checkbool(false, 4, make_app(make_app(lt, four), three));
453         checkbool(false, 4, make_app(make_app(lt, four), four));
454         checkbool(true, 4, make_app(make_app(lt, four), five));
455         checkbool(false, 5, make_app(make_app(lt, five), zero));
456         checkbool(false, 5, make_app(make_app(lt, five), one));
457         checkbool(false, 5, make_app(make_app(lt, five), two));
458         checkbool(false, 5, make_app(make_app(lt, five), three));
459         checkbool(false, 5, make_app(make_app(lt, five), four));
460         checkbool(false, 5, make_app(make_app(lt, five), five));
461
462         print("checking leq");
463         checkbool(true, 0, make_app(make_app(leq, zero), zero));
464         checkbool(true, 0, make_app(make_app(leq, zero), one));
465         checkbool(true, 0, make_app(make_app(leq, zero), two));
466         checkbool(true, 0, make_app(make_app(leq, zero), three));
467         checkbool(true, 0, make_app(make_app(leq, zero), four));
468         checkbool(true, 0, make_app(make_app(leq, zero), five));
469         checkbool(false, 1, make_app(make_app(leq, one), zero));
470         checkbool(true, 1, make_app(make_app(leq, one), one));
471         checkbool(true, 1, make_app(make_app(leq, one), two));
472         checkbool(true, 1, make_app(make_app(leq, one), three));
473         checkbool(true, 1, make_app(make_app(leq, one), four));
474         checkbool(true, 1, make_app(make_app(leq, one), five));
475         checkbool(false, 2, make_app(make_app(leq, two), zero));
476         checkbool(false, 2, make_app(make_app(leq, two), one));
477         checkbool(true, 2, make_app(make_app(leq, two), two));
478         checkbool(true, 2, make_app(make_app(leq, two), three));
479         checkbool(true, 2, make_app(make_app(leq, two), four));
480         checkbool(true, 2, make_app(make_app(leq, two), five));
481         checkbool(false, 3, make_app(make_app(leq, three), zero));
482         checkbool(false, 3, make_app(make_app(leq, three), one));
483         checkbool(false, 3, make_app(make_app(leq, three), two));
484         checkbool(true, 3, make_app(make_app(leq, three), three));
485         checkbool(true, 3, make_app(make_app(leq, three), four));
486         checkbool(true, 3, make_app(make_app(leq, three), five));
487         checkbool(false, 4, make_app(make_app(leq, four), zero));
488         checkbool(false, 4, make_app(make_app(leq, four), one));
489         checkbool(false, 4, make_app(make_app(leq, four), two));
490         checkbool(false, 4, make_app(make_app(leq, four), three));
491         checkbool(true, 4, make_app(make_app(leq, four), four));
492         checkbool(true, 4, make_app(make_app(leq, four), five));
493         checkbool(false, 5, make_app(make_app(leq, five), zero));
494         checkbool(false, 5, make_app(make_app(leq, five), one));
495         checkbool(false, 5, make_app(make_app(leq, five), two));
496         checkbool(false, 5, make_app(make_app(leq, five), three));
497         checkbool(false, 5, make_app(make_app(leq, five), four));
498         checkbool(true, 5, make_app(make_app(leq, five), five));
499
500         print("checking eq");
501         checkbool(true, 0, make_app(make_app(eq, zero), zero));
502         checkbool(false, 0, make_app(make_app(eq, zero), one));
503         checkbool(false, 0, make_app(make_app(eq, zero), two));
504         checkbool(false, 0, make_app(make_app(eq, zero), three));
505         checkbool(false, 0, make_app(make_app(eq, zero), four));
506         checkbool(false, 0, make_app(make_app(eq, zero), five));
507         checkbool(false, 1, make_app(make_app(eq, one), zero));
508         checkbool(true, 1, make_app(make_app(eq, one), one));
509         checkbool(false, 1, make_app(make_app(eq, one), two));
510         checkbool(false, 1, make_app(make_app(eq, one), three));
511         checkbool(false, 1, make_app(make_app(eq, one), four));
512         checkbool(false, 1, make_app(make_app(eq, one), five));
513         checkbool(false, 2, make_app(make_app(eq, two), zero));
514         checkbool(false, 2, make_app(make_app(eq, two), one));
515         checkbool(true, 2, make_app(make_app(eq, two), two));
516         checkbool(false, 2, make_app(make_app(eq, two), three));
517         checkbool(false, 2, make_app(make_app(eq, two), four));
518         checkbool(false, 2, make_app(make_app(eq, two), five));
519         checkbool(false, 3, make_app(make_app(eq, three), zero));
520         checkbool(false, 3, make_app(make_app(eq, three), one));
521         checkbool(false, 3, make_app(make_app(eq, three), two));
522         checkbool(true, 3, make_app(make_app(eq, three), three));
523         checkbool(false, 3, make_app(make_app(eq, three), four));
524         checkbool(false, 3, make_app(make_app(eq, three), five));
525         checkbool(false, 4, make_app(make_app(eq, four), zero));
526         checkbool(false, 4, make_app(make_app(eq, four), one));
527         checkbool(false, 4, make_app(make_app(eq, four), two));
528         checkbool(false, 4, make_app(make_app(eq, four), three));
529         checkbool(true, 4, make_app(make_app(eq, four), four));
530         checkbool(false, 4, make_app(make_app(eq, four), five));
531         checkbool(false, 5, make_app(make_app(eq, five), zero));
532         checkbool(false, 5, make_app(make_app(eq, five), one));
533         checkbool(false, 5, make_app(make_app(eq, five), two));
534         checkbool(false, 5, make_app(make_app(eq, five), three));
535         checkbool(false, 5, make_app(make_app(eq, five), four));
536         checkbool(true, 5, make_app(make_app(eq, five), five));
537
538         print("checking div");
539         check(0, make_app(make_app(div, zero), one));
540         check(0, make_app(make_app(div, zero), two));
541         check(0, make_app(make_app(div, zero), three));
542         check(0, make_app(make_app(div, zero), four));
543         check(0, make_app(make_app(div, zero), five));
544         check(1, make_app(make_app(div, one), one));
545         check(0, make_app(make_app(div, one), two));
546         check(0, make_app(make_app(div, one), three));
547         check(0, make_app(make_app(div, one), four));
548         check(0, make_app(make_app(div, one), five));
549         check(2, make_app(make_app(div, two), one));
550         check(1, make_app(make_app(div, two), two));
551         check(0, make_app(make_app(div, two), three));
552         check(0, make_app(make_app(div, two), four));
553         check(0, make_app(make_app(div, two), five));
554         check(3, make_app(make_app(div, three), one));
555         check(1, make_app(make_app(div, three), two));
556         check(1, make_app(make_app(div, three), three));
557         check(0, make_app(make_app(div, three), four));
558         check(0, make_app(make_app(div, three), five));
559         check(4, make_app(make_app(div, four), one));
560         check(2, make_app(make_app(div, four), two));
561         check(1, make_app(make_app(div, four), three));
562         check(1, make_app(make_app(div, four), four));
563         check(0, make_app(make_app(div, four), five));
564         check(5, make_app(make_app(div, five), one));
565         check(2, make_app(make_app(div, five), two));
566         check(1, make_app(make_app(div, five), three));
567         check(1, make_app(make_app(div, five), four));
568         check(1, make_app(make_app(div, five), five));
569
570         print("checking mod");
571         check(0, make_app(make_app(mod, zero), one));
572         check(0, make_app(make_app(mod, zero), two));
573         check(0, make_app(make_app(mod, zero), three));
574         check(0, make_app(make_app(mod, zero), four));
575         check(0, make_app(make_app(mod, zero), five));
576         check(0, make_app(make_app(mod, one), one));
577         check(1, make_app(make_app(mod, one), two));
578         check(1, make_app(make_app(mod, one), three));
579         check(1, make_app(make_app(mod, one), four));
580         check(1, make_app(make_app(mod, one), five));
581         check(0, make_app(make_app(mod, two), one));
582         check(0, make_app(make_app(mod, two), two));
583         check(2, make_app(make_app(mod, two), three));
584         check(2, make_app(make_app(mod, two), four));
585         check(2, make_app(make_app(mod, two), five));
586         check(0, make_app(make_app(mod, three), one));
587         check(1, make_app(make_app(mod, three), two));
588         check(0, make_app(make_app(mod, three), three));
589         check(3, make_app(make_app(mod, three), four));
590         check(3, make_app(make_app(mod, three), five));
591         check(0, make_app(make_app(mod, four), one));
592         check(0, make_app(make_app(mod, four), two));
593         check(1, make_app(make_app(mod, four), three));
594         check(0, make_app(make_app(mod, four), four));
595         check(4, make_app(make_app(mod, four), five));
596         check(0, make_app(make_app(mod, five), one));
597         check(1, make_app(make_app(mod, five), two));
598         check(2, make_app(make_app(mod, five), three));
599         check(1, make_app(make_app(mod, five), four));
600         check(0, make_app(make_app(mod, five), five));
601
602         if (!g_cbv) {
603                 print("checking fact1");
604                 check(1, make_app(fact1, zero));
605                 check(1, make_app(fact1, one));
606                 check(2, make_app(fact1, two));
607                 check(6, make_app(fact1, three));
608                 check(24, make_app(fact1, four));
609         }
610
611         if (!g_cbv) {
612                 print("checking fact2");
613                 check(1, make_app(fact2, zero));
614                 check(1, make_app(fact2, one));
615                 check(2, make_app(fact2, two));
616                 check(6, make_app(fact2, three));
617                 check(24, make_app(fact2, four));
618         }
619
620         if (g_cbv<2) {
621                 print("checking fact3");
622                 check(1, make_app(fact3, zero));
623                 check(1, make_app(fact3, one));
624                 check(2, make_app(fact3, two));
625                 check(6, make_app(fact3, three));
626                 check(24, make_app(fact3, four));
627         }
628
629         if (!g_cbv) {
630                 print("checking fact4");
631                 check(1, make_app(fact4, zero));
632                 check(1, make_app(fact4, one));
633                 check(2, make_app(fact4, two));
634                 check(6, make_app(fact4, three));
635                 check(24, make_app(fact4, four));
636         }
637
638         if (g_cbv<2) {
639                 print("checking fact5");
640                 check(1, make_app(fact5, zero));
641                 check(1, make_app(fact5, one));
642                 check(2, make_app(fact5, two));
643                 check(6, make_app(fact5, three));
644                 check(24, make_app(fact5, four));
645         }
646
647 }
648
649
650 test();
651