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 unwind(this, stack);
+ // return unwind(this, stack);
+ // trampoline to, args
+ return [null, unwind(this, stack)];
};
this.eval_cbv = function (aggressive) {
return this;
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);
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;
}
};
- 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();
}
};
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);
- 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) {
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];
}
}
}
} 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)));
+}
+
+*/
+