lambda.js: tweak
[lambda.git] / code / lambda.js
index c0dbb0f..50880fc 100644 (file)
@@ -115,14 +115,19 @@ function Variable(name, tag) {
     this.tag = tag || 0;
     this.to_string = function () {
         // append count copies of str to accum
     this.tag = tag || 0;
     this.to_string = function () {
         // append count copies of str to accum
-        function markup(accum, count) {
-            if (count === 0) {
-                return accum;
-            } else {
-                return markup(accum + "'", count - 1);
-            }
-        }
-        return markup(this.name, this.tag);
+//         function markup(accum, count) {
+//             if (count === 0) {
+//                 return accum;
+//             } else {
+//                 return markup(accum + "'", count - 1);
+//             }
+//         }
+//         return markup(this.name, this.tag);
+               var s = this.name;
+               for (var count = 0; count < this.tag; count += 1) {
+                       s += "'";
+               }
+               return s;
     };
     this.equal = function (other) {
         return (this.tag === other.tag) && (this.name === other.name);
     };
     this.equal = function (other) {
         return (this.tag === other.tag) && (this.name === other.name);
@@ -192,15 +197,24 @@ function Lambda_var(variable) {
     };
     this.eval_loop = function (stack, eta) {
         function unwind(left, stack) {
     };
     this.eval_loop = function (stack, eta) {
         function unwind(left, stack) {
-            if (stack.length === 0) {
-                return left;
-            } else {
-                var x = stack[0];
-                var xs = stack.slice(1);
-                return unwind(new Lambda_app(left, x.eval_loop([], eta)), xs);
-            }
+//             if (stack.length === 0) {
+//                 return left;
+//             } else {
+//                 var x = stack[0];
+//                 var xs = stack.slice(1);
+//                 return unwind(new Lambda_app(left, x.eval_loop([], eta)), xs);
+//             }
+                       var res = left, x;
+                       while (stack.length) {
+                               x = stack.shift();
+                               // res = new Lambda_app(res, x.eval_loop([], eta));
+                               res = new Lambda_app(res, reduce(x, eta, false));
+                       }
+                       return res;
         }
         }
-        return unwind(this, stack);
+        // return unwind(this, stack);
+               // trampoline to, args
+               return [null, unwind(this, stack)];
     };
     this.eval_cbv = function (aggressive) {
         return this;
     };
     this.eval_cbv = function (aggressive) {
         return this;
@@ -250,7 +264,9 @@ function Lambda_app(left, right) {
     this.eval_loop = function (stack, eta) {
         var new_stack = stack.slice(0);
         new_stack.unshift(this.right);
     this.eval_loop = function (stack, eta) {
         var new_stack = stack.slice(0);
         new_stack.unshift(this.right);
-        return this.left.eval_loop(new_stack, eta);
+        // return this.left.eval_loop(new_stack, eta);
+               // trampoline to, args
+               return [this.left, new_stack, eta];
     };
     this.eval_cbv = function (aggressive) {
         var left = this.left.eval_cbv(aggressive);
     };
     this.eval_cbv = function (aggressive) {
         var left = this.left.eval_cbv(aggressive);
@@ -344,16 +360,19 @@ function Lambda_lam(variable, body) {
     };
     this.eval_loop = function (stack, eta) {
         if (stack.length === 0) {
     };
     this.eval_loop = function (stack, eta) {
         if (stack.length === 0) {
-            var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
-            if (eta) {
-                return term.check_eta();
-            } else {
-                return term;
-            }
+                       // var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
+                       var term = new Lambda_lam(this.bound, reduce(this.body, eta, false));
+                       if (eta) {
+                               return [null, term.check_eta()];
+                       } else {
+                               return [null, term];
+                       }
         } else {
             var x = stack[0];
             var xs = stack.slice(1);
         } else {
             var x = stack[0];
             var xs = stack.slice(1);
-            return subst(this.bound, x, this.body).eval_loop(xs, eta);
+            // return subst(this.bound, x, this.body).eval_loop(xs, eta);
+                       // trampoline to, args
+                       return [subst(this.bound, x, this.body), xs, eta];
         }
     };
     this.eval_cbv = function (aggressive) {
         }
     };
     this.eval_cbv = function (aggressive) {
@@ -364,16 +383,31 @@ function Lambda_lam(variable, body) {
         }
     };
     this.to_int = function (sofar) {
         }
     };
     this.to_int = function (sofar) {
-        if (this.body.body && this.body.body.variable && this.body.bound.equal(this.body.body.variable)) {
-            return 0 + sofar;
-        } else if (this.body.variable && this.bound.equal(this.body.variable)) {
-            return 1 + sofar;
-        } else if (this.body.body && this.body.body.left && this.body.body.left.variable && this.bound.equal(this.body.body.left.variable)) {
-            var new_int = new Lambda_lam(this.bound, new Lambda_lam(this.body.bound, this.body.body.right));
-            return new_int.to_int(1 + sofar);
-        } else {
-            return "not a church numeral";
-        }
+//         if (this.body.body && this.body.body.variable && this.body.bound.equal(this.body.body.variable)) {
+//             return 0 + sofar;
+//         } else if (this.body.variable && this.bound.equal(this.body.variable)) {
+//             return 1 + sofar;
+//         } else if (this.body.body && this.body.body.left && this.body.body.left.variable && this.bound.equal(this.body.body.left.variable)) {
+//             var new_int = new Lambda_lam(this.bound, new Lambda_lam(this.body.bound, this.body.body.right));
+//             return new_int.to_int(1 + sofar);
+//         } else {
+//             return "not a church numeral";
+//         }
+               var res = 0, s = this.bound, z, cursor;
+               if (this.body.variable && s.equal(this.body.variable)) {
+                       return 1;
+               } else if (this.body.bound) {
+                       z = this.body.bound;
+                       cursor = this.body.body;
+                       while (cursor.left && cursor.left.variable && s.equal(cursor.left.variable)) {
+                               res += 1;
+                               cursor = cursor.right;
+                       }
+                       if (cursor.variable && z.equal(cursor.variable)) {
+                               return res;
+                       }
+               }
+               return "not a church numeral";
     };
 }
 
     };
 }
 
@@ -388,7 +422,13 @@ function reduce(expr, eta, cbv) {
     if (cbv) {
         return expr.eval_cbv(cbv > 1);
     } else {
     if (cbv) {
         return expr.eval_cbv(cbv > 1);
     } else {
-        return expr.eval_loop([], eta);
+        // return expr.eval_loop([], eta);
+               var to_eval = expr, res = [[], eta];
+               while (to_eval !== null) {
+                       res = to_eval.eval_loop.apply(to_eval, res);
+                       to_eval = res.shift();
+               }
+               return res[0];
     }
 }
 
     }
 }