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