leafs->leaves
[lambda.git] / code / lambda.js
index 609cce0..83ae7c4 100644 (file)
@@ -207,11 +207,14 @@ function Lambda_var(variable) {
                        var res = left, x;
                        while (stack.length) {
                                x = stack.shift();
                        var res = left, x;
                        while (stack.length) {
                                x = stack.shift();
-                               res = new Lambda_app(res, x.eval_loop([], eta));
+                               // res = new Lambda_app(res, x.eval_loop([], eta));
+                               res = new Lambda_app(res, reduce(x, eta, false));
                        }
                        return res;
         }
                        }
                        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;
@@ -261,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);
@@ -288,16 +293,16 @@ function Lambda_lam(variable, body) {
         return new Db_lam(this.body.debruijn(new_seq));
     };
     this.to_string = function (as_atom) {
         return new Db_lam(this.body.debruijn(new_seq));
     };
     this.to_string = function (as_atom) {
-        var base = "\\" + this.to_string_funct();
+        var base = "\\" + this.to_dotted();
         if (as_atom) {
             return "(" + base + ")";
         } else {
             return base;
         }
     };
         if (as_atom) {
             return "(" + base + ")";
         } else {
             return base;
         }
     };
-    this.to_string_funct = function () {
-        if (this.body.to_string_funct) {
-            return this.bound.to_string() + " " + this.body.to_string_funct();
+    this.to_dotted = function () {
+        if (this.body.to_dotted) {
+            return this.bound.to_string() + " " + this.body.to_dotted();
         } else {
             return this.bound.to_string() + ". " + this.body.to_string();
         }
         } else {
             return this.bound.to_string() + ". " + this.body.to_string();
         }
@@ -355,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) {
@@ -414,7 +422,14 @@ 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);
+               // using trampoline to reduce call stack overflows
+               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];
     }
 }
 
     }
 }
 
@@ -436,212 +451,184 @@ try {
     }
 } catch (e) {}
 
     }
 } catch (e) {}
 
-/*
-let true = K in
-let false = \x y. y in
-let and = \l r. l r false in
-let or = \l r. l true r in
-let pair = \u v f. f u v in
-let triple = \u v w f. f u v w in
-let succ = \n s z. s (n s z) in
-let pred = \n s z. n (\u v. v (u s)) (K z) I in
-let ifzero = \n. n (\u v. v (u succ)) (K 0) (\n withp whenz. withp n) in
-let add = \m n. n succ m in
-let mul = \m n. n (\z. add m z) 0 in
-let mul = \m n s. m (n s) in
-let sub = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
-let min = \m n. sub m (sub m n) in
-let max = \m n. add n (sub m n) in
-let lt = (\mzero msucc mtail. \n m. n mtail (m msucc mzero) true (\x. true) false) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
-let leq = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true (\x. false) true) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
-let eq = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true (\x. false) true) (pair 0 (K (pair 1 I))) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
-let divmod = (\mzero msucc mtail. \n divisor.
-               (\dhead. n (mtail dhead) (\sel. dhead (sel 0 0)))
-              (divisor msucc mzero (\a b c. c x))
-              (\d m a b c. pair d m) )
-          (triple succ (K 0) I)
-          (\d. triple I succ (K d))
-          (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz)))) in
-let div = \n d. divmod n d true in
-let mod = \n d. divmod n d false in
-let Y = \f. (\y. f(y y)) (\y. f(y y)) in
-let Z = (\u f. f(u u f)) (\u f. f(u u f)) in
-let fact = \y. y (\f n. ifzero n (\p. mul n (f p)) 1) in
-fact Z 3
-*/
 
 
 
 
 
 
-// // Basic data structure, essentially a LISP/Scheme-like cons
-// // pre-terminal nodes are expected to be of the form new cons(null, "string")
-// function cons(car, cdr) {
-//   this.car = car;
-//   this.cdr = cdr;
-// }
-
-// // takes a stack of symbols, returns a pair: a tree and the remaining symbols
-// function parse(split) {
-//   if (split == null) return (new cons (null, null));
-//   if (split.length == 0) return (new cons (null, null));
-//   var token = split.shift();
-//   if (token == ")") return (new cons (null, split));
-//   var next = parse(split);
-//   if (token == "(") {
-//     var nextnext = parse(next.cdr);
-//     return (new cons ((new cons (next.car, nextnext.car)),
-//                       nextnext.cdr));
-//   }
-//   return (new cons ((new cons ((new cons (null, token)),
-//                                next.car)),
-//                     next.cdr))
-// }
-
-// // substitute arg in for v in tree
-// function sub(tree, v, arg) {
-//   if (tree == null) return (null);
-//   if (tree.car == null) if (tree.cdr == v) return (arg);
-//   if (tree.car == null) return (tree);
-
-//   // perform alpha reduction to prevent variable collision
-//   if (isBindingForm(tree)) 
-//     return (new cons (tree.car, 
-//                       sub(sub(tree.cdr,         // inner sub = alpha reduc.
-//                               tree.cdr.car.cdr, 
-//                               fresh(tree.cdr.car.cdr)),
-//                           v,
-//                           arg)));
-
-//   return (new cons ((sub (tree.car, v, arg)),
-//                     (sub (tree.cdr, v, arg))))
-// }
-
-// // Guaranteed unique for each call as long as string is not empty.
-// var i = 0;
-// function fresh(string) {
-//   i = i+1;
-//   if (typeof(string) != "string") return (string);
-//   return (new cons (null,  
-//                     string.substring(0,1) + (i).toString()));
-// }
-
-// // Keep reducing until there is no more change
-// function fixedPoint (tree) {
-//   var t2 = reduce(tree);
-//   if (treeToString(tree) == treeToString(t2)) return (tree);
-//   return (fixedPoint (t2));
-// }
-
-// // Reduce all the arguments, then try to do beta conversion on the whole
-// function reduce(tree) {
-//   if (tree == null) return (tree);
-//   if (typeof(tree) == "string") return (tree);
-//   return (convert (new cons (reduce (tree.car), mapReduce (tree.cdr))));
-// }
-
-// // Reduce all the arguments in a list
-// function mapReduce(tree) {
-//   if (tree == null) return (tree);
-//   if (tree.car == null) return (tree);
-//   return (new cons (reduce (tree.car), mapReduce(tree.cdr )));
-// }
-
-// // If the list is of the form ((lambda var body) arg), do beta reduc.
-// function convert(tree) {
-//     if (isLet(tree)) {
-//       return (sub(tree.cdr.car, tree.car.cdr.car.cdr, tree.car.cdr.cdr.car));}
-//     else 
-//       if (isConvertable(tree)) {
-//         return (sub(tree.car.cdr.cdr.car, tree.car.cdr.car.cdr, tree.cdr.car));}
-//       else return(tree);
-// } 
-
-// // Is of form ((let var arg) body)?
-// function isLet(tree) {
-//   if (tree == null) return (false);
-//   if (!(isBindingForm(tree.car))) return (false);
-//   if (tree.car.car.cdr != "let") return (false);
-//   if (tree.cdr == null) return (false);
-//   if (tree.cdr.car == null) return (false);
-//   return(true);
-// }  
-
-// // Is of form ((lambda var body) arg)?
-// function isConvertable(tree) {
-//   if (tree == null) return (false);
-//   if (!(isBindingForm(tree.car))) return (false);
-//   if (tree.car.car.cdr != "lambda") return (false);
-//   if (tree.cdr == null) return (false);
-//   if (tree.cdr.car == null) return (false);
-//   return(true);
-// }  
-
-// // Is of form (lambda var body)?
-// function isBindingForm(tree) {
-//   if (tree == null) return (false);
-//   if (tree.car == null) return (false);
-//   if (tree.car.car != null) return (false);
-//   if ((tree.car.cdr != "lambda") 
-//       && (tree.car.cdr != "let")
-//       && (tree.car.cdr != "exists")
-//       && (tree.car.cdr != "forall")
-//       && (tree.car.cdr != "\u03BB")
-//       && (tree.car.cdr != "\u2200")
-//       && (tree.car.cdr != "\u2203")
-//      )
-//     return (false);
-//   if (tree.car.cdr == null) return (false);
-//   if (tree.cdr.car == null) return (false);
-//   if (tree.cdr.car.car != null) return (false);
-//   if (tree.cdr.cdr == null) return (false);
-//   return (true);
-// }
-
-// function treeToString(tree) {
-//   if (tree == null) return ("")
-//   if (tree.car == null) return (tree.cdr)
-//   if ((tree.car).car == null) 
-//     return (treeToString(tree.car) + " " + treeToString(tree.cdr))
-//   return ("(" + treeToString(tree.car) + ")" + treeToString(tree.cdr))
-// }
-
-// // use this instead of treeToString if you want to see the full structure
-// function treeToStringRaw(tree) {
-//   if (tree == null) return ("@")
-//   if (typeof(tree) == "string") return (tree);
-//   return ("(" + treeToStringRaw(tree.car) + "." + 
-//                 treeToStringRaw(tree.cdr) + ")")
-// }
-
-// // Make sure each paren will count as a separate token
-// function stringToTree(input) {
-//   input = input.replace(/let/g, " ( ( let ");
-//   input = input.replace(/=/g, " ");
-//   input = input.replace(/in/g, " ) ");
-//   input = input.replace(/\(/g, " ( ");
-//   input = input.replace(/\)/g, " ) ");
-//   input = input.replace(/;.*\n/g," ");
-//   input = input.replace(/\^/g, " ^ ");
-//   input = input.replace(/[\\]/g, " lambda ");
-//   input = input.replace(/\u03BB/g, " lambda ");
-//   return ((parse(input.split(/[ \f\n\r\t\v]+/))).car)
-// }
-
-// // Adjust spaces to print pretty
-// function formatTree(tree) {
-//   output = treeToStringRaw (tree);
-//   output = output.replace(/^[ \f\n\r\t\v]+/, "");
-//   output = output.replace(/[ \f\n\r\t\v]+$/, "");
-//   output = output.replace(/[ \f\n\r\t\v]+\)/g, ")");
-//   output = output.replace(/\)([^)(])/g, ") $1");
-//   output = output.replace(/lambda/g, "\\");
-// //  output = output.replace(/lambda/g, "\u03BB");
-// //  output = output.replace(/exists/g, "\u2203");
-// //  output = output.replace(/forall/g, "\u2200");
-//   return (output)
-// }
-
-// function mytry(form) { 
-//   i = 0;
-//   form.result.value = formatTree((stringToTree(form.input.value)));
-//   // form.result.value = formatTree(fixedPoint(stringToTree(form.input.value)));
-// }
+/* Chris's original
+
+// Basic data structure, essentially a LISP/Scheme-like cons
+// pre-terminal nodes are expected to be of the form new cons(null, "string")
+function cons(car, cdr) {
+  this.car = car;
+  this.cdr = cdr;
+}
+
+// takes a stack of symbols, returns a pair: a tree and the remaining symbols
+function parse(split) {
+  if (split == null) return (new cons (null, null));
+  if (split.length == 0) return (new cons (null, null));
+  var token = split.shift();
+  if (token == ")") return (new cons (null, split));
+  var next = parse(split);
+  if (token == "(") {
+       var nextnext = parse(next.cdr);
+       return (new cons ((new cons (next.car, nextnext.car)),
+                                         nextnext.cdr));
+  }
+  return (new cons ((new cons ((new cons (null, token)),
+                                                          next.car)),
+                                       next.cdr))
+}
+
+// substitute arg in for v in tree
+function sub(tree, v, arg) {
+  if (tree == null) return (null);
+  if (tree.car == null) if (tree.cdr == v) return (arg);
+  if (tree.car == null) return (tree);
+
+  // perform alpha reduction to prevent variable collision
+  if (isBindingForm(tree)) 
+       return (new cons (tree.car, 
+                                         sub(sub(tree.cdr,         // inner sub = alpha reduc.
+                                                         tree.cdr.car.cdr, 
+                                                         fresh(tree.cdr.car.cdr)),
+                                                 v,
+                                                 arg)));
+
+  return (new cons ((sub (tree.car, v, arg)),
+                                       (sub (tree.cdr, v, arg))))
+}
+
+// Guaranteed unique for each call as long as string is not empty.
+var i = 0;
+function fresh(string) {
+  i = i+1;
+  if (typeof(string) != "string") return (string);
+  return (new cons (null,  
+                                       string.substring(0,1) + (i).toString()));
+}
+
+// Keep reducing until there is no more change
+function fixedPoint (tree) {
+  var t2 = reduce(tree);
+  if (treeToString(tree) == treeToString(t2)) return (tree);
+  return (fixedPoint (t2));
+}
+
+// Reduce all the arguments, then try to do beta conversion on the whole
+function reduce(tree) {
+  if (tree == null) return (tree);
+  if (typeof(tree) == "string") return (tree);
+  return (convert (new cons (reduce (tree.car), mapReduce (tree.cdr))));
+}
+
+// Reduce all the arguments in a list
+function mapReduce(tree) {
+  if (tree == null) return (tree);
+  if (tree.car == null) return (tree);
+  return (new cons (reduce (tree.car), mapReduce(tree.cdr )));
+}
+
+// If the list is of the form ((lambda var body) arg), do beta reduc.
+function convert(tree) {
+       if (isLet(tree)) {
+         return (sub(tree.cdr.car, tree.car.cdr.car.cdr, tree.car.cdr.cdr.car));}
+       else 
+         if (isConvertable(tree)) {
+               return (sub(tree.car.cdr.cdr.car, tree.car.cdr.car.cdr, tree.cdr.car));}
+         else return(tree);
+} 
+
+// Is of form ((let var arg) body)?
+function isLet(tree) {
+  if (tree == null) return (false);
+  if (!(isBindingForm(tree.car))) return (false);
+  if (tree.car.car.cdr != "let") return (false);
+  if (tree.cdr == null) return (false);
+  if (tree.cdr.car == null) return (false);
+  return(true);
+}  
+
+// Is of form ((lambda var body) arg)?
+function isConvertable(tree) {
+  if (tree == null) return (false);
+  if (!(isBindingForm(tree.car))) return (false);
+  if (tree.car.car.cdr != "lambda") return (false);
+  if (tree.cdr == null) return (false);
+  if (tree.cdr.car == null) return (false);
+  return(true);
+}  
+
+// Is of form (lambda var body)?
+function isBindingForm(tree) {
+  if (tree == null) return (false);
+  if (tree.car == null) return (false);
+  if (tree.car.car != null) return (false);
+  if ((tree.car.cdr != "lambda") 
+         && (tree.car.cdr != "let")
+         && (tree.car.cdr != "exists")
+         && (tree.car.cdr != "forall")
+         && (tree.car.cdr != "\u03BB")
+         && (tree.car.cdr != "\u2200")
+         && (tree.car.cdr != "\u2203")
+        )
+       return (false);
+  if (tree.car.cdr == null) return (false);
+  if (tree.cdr.car == null) return (false);
+  if (tree.cdr.car.car != null) return (false);
+  if (tree.cdr.cdr == null) return (false);
+  return (true);
+}
+
+function treeToString(tree) {
+  if (tree == null) return ("")
+  if (tree.car == null) return (tree.cdr)
+  if ((tree.car).car == null) 
+       return (treeToString(tree.car) + " " + treeToString(tree.cdr))
+  return ("(" + treeToString(tree.car) + ")" + treeToString(tree.cdr))
+}
+
+// use this instead of treeToString if you want to see the full structure
+function treeToStringRaw(tree) {
+  if (tree == null) return ("@")
+  if (typeof(tree) == "string") return (tree);
+  return ("(" + treeToStringRaw(tree.car) + "." + 
+                               treeToStringRaw(tree.cdr) + ")")
+}
+
+// Make sure each paren will count as a separate token
+function stringToTree(input) {
+  input = input.replace(/let/g, " ( ( let ");
+  input = input.replace(/=/g, " ");
+  input = input.replace(/in/g, " ) ");
+  input = input.replace(/\(/g, " ( ");
+  input = input.replace(/\)/g, " ) ");
+  input = input.replace(/;.*\n/g," ");
+  input = input.replace(/\^/g, " ^ ");
+  input = input.replace(/[\\]/g, " lambda ");
+  input = input.replace(/\u03BB/g, " lambda ");
+  return ((parse(input.split(/[ \f\n\r\t\v]+/))).car)
+}
+
+// Adjust spaces to print pretty
+function formatTree(tree) {
+  output = treeToStringRaw (tree);
+  output = output.replace(/^[ \f\n\r\t\v]+/, "");
+  output = output.replace(/[ \f\n\r\t\v]+$/, "");
+  output = output.replace(/[ \f\n\r\t\v]+\)/g, ")");
+  output = output.replace(/\)([^)(])/g, ") $1");
+  output = output.replace(/lambda/g, "\\");
+//  output = output.replace(/lambda/g, "\u03BB");
+//  output = output.replace(/exists/g, "\u2203");
+//  output = output.replace(/forall/g, "\u2200");
+  return (output)
+}
+
+function mytry(form) { 
+  i = 0;
+  form.result.value = formatTree((stringToTree(form.input.value)));
+  // form.result.value = formatTree(fixedPoint(stringToTree(form.input.value)));
+}
+
+*/
+