+
+function equal(expr1, expr2) {
+ return expr1.debruijn([]).equal(expr2.debruijn([]));
+}
+
+function contains(expr1, expr2) {
+ return expr1.debruijn([]).contains(expr2.debruijn([]));
+}
+
+
+function Lambda_var(variable) {
+ this.variable = variable;
+ this.debruijn = function (seq) {
+ return this.variable.position(seq);
+ };
+ this.to_string = function (as_atom) {
+ return this.variable.to_string();
+ };
+ this.has_free = function (v) {
+ if (v.name !== this.variable.name) {
+ return [false, v];
+ } else if (v.tag === this.variable.tag) {
+ return [true, v];
+ } else {
+ return [false, this.variable];
+ }
+ };
+ this.subst = function (v, new_term) {
+ if (this.variable.equal(v)) {
+ return new_term;
+ } else {
+ return this;
+ }
+ };
+ this.check_eta = function () {
+ return this;
+ };
+ 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);
+ }
+ }
+ return unwind(this, stack);
+ };
+ this.eval_cbv = function (aggressive) {
+ return this;
+ };
+}
+
+function Lambda_app(left, right) {
+ this.left = left;
+ this.right = right;
+ this.debruijn = function (seq) {
+ return new Db_app(this.left.debruijn(seq), this.right.debruijn(seq));
+ };
+ this.to_string = function (as_atom) {
+ var base;
+ if (this.left.left) {
+ base = this.left.to_string() + " " + this.right.to_string(true);
+ } else {
+ base = this.left.to_string(true) + " " + this.right.to_string(true);
+ }
+ if (as_atom) {
+ return "(" + base + ")";
+ } else {
+ return base;
+ }
+ };
+ this.has_free = function (v) {
+ var left_res = this.left.has_free(v);
+ var right_res = this.right.has_free(v);
+ var left_bool = left_res[0];
+ var right_bool = right_res[0];
+ var left_tag = left_res[1].tag;
+ var right_tag = right_res[1].tag;
+ var res;
+ if (left_tag > right_tag) {
+ res = left_res[1];
+ } else {
+ res = right_res[1];
+ }
+ return [left_bool || right_bool, res];
+ };
+ this.subst = function (v, new_term) {
+ return new Lambda_app(subst(v, new_term, this.left), subst(v, new_term, this.right));
+ };
+ this.check_eta = function () {
+ 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);
+ };
+ this.eval_cbv = function (aggressive) {
+ var left = this.left.eval_cbv(aggressive);
+ var right = this.right.eval_cbv(aggressive);
+ if (left.body) {
+ return subst(left.bound, right, left.body).eval_cbv(aggressive);
+ } else {
+ return new Lambda_app(left, right);
+ }
+ };
+}
+
+
+// (* if v occurs free_in term, returns Some v' where v' is the highest-tagged
+// * variable with the same name as v occurring (free or bound) in term *)
+
+
+function Lambda_lam(variable, body) {
+ this.bound = variable;
+ this.body = body;
+ this.debruijn = function (seq) {
+ var new_seq = seq.slice(0);
+ new_seq.unshift(this.bound);
+ return new Db_lam(this.body.debruijn(new_seq));
+ };
+ this.to_string = function (as_atom) {
+ var base = "\\" + this.to_string_funct();
+ 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();
+ } else {
+ return this.bound.to_string() + ". " + this.body.to_string();
+ }
+ };
+ this.has_free = function (v) {
+ if (this.bound.equal(v)) {
+ return [false, v];
+ } else {
+ return this.body.has_free(v);
+ }
+ };
+ this.subst = function (v, new_term) {
+ function bump_tag(v1, v2) {
+ var max;
+ if (v1.tag > v2.tag) {
+ max = v1.tag;
+ } else {
+ max = v2.tag;
+ }
+ return new Variable(v1.name, max + 1);
+ }
+ function bump_tag2(v1, v2) {
+ if (v1.name !== v2.name) {
+ return v1;
+ } else {
+ return bump_tag(v1, v2);
+ }
+ }
+ if (this.bound.equal(v)) {
+ return this;
+ } else {
+ var res = free_in(this.bound, new_term);
+ // if x is free in the inserted term new_term, a capture is possible
+ if (res) {
+ // this.bound is free in new_term, need to alpha-convert
+ var uniq_x = bump_tag2(bump_tag(this.bound, res), v);
+ var res2 = free_in(uniq_x, this.body);
+ if (res2) {
+ uniq_x = bump_tag(uniq_x, res2);
+ }
+ var body2 = subst(this.bound, new Lambda_var(uniq_x), this.body);
+ return new Lambda_lam(uniq_x, subst(v, new_term, body2));
+ } else {
+ // this.bound not free in new_term, can substitute new_term for v without any captures
+ return new Lambda_lam(this.bound, subst(v, new_term, this.body));
+ }
+ }
+ };
+ this.check_eta = function () {
+ if (this.body.right && this.body.right.variable && this.bound.equal(this.body.right.variable) && !free_in(this.bound, this.body.left)) {
+ return this.body.left;
+ } else {
+ return this;
+ }
+ };
+ 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;
+ }
+ } else {
+ var x = stack[0];
+ var xs = stack.slice(1);
+ return subst(this.bound, x, this.body).eval_loop(xs, eta);
+ }
+ };
+ this.eval_cbv = function (aggressive) {
+ if (aggressive) {
+ return new Lambda_lam(this.bound, this.body.eval_cbv(aggressive));
+ } else {
+ return this;
+ }
+ };
+ 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";
+ }
+ };
+}
+
+
+
+///////////////////////////////////////////////////////////////////////////////////
+
+// cbv is false: use call-by-name
+// cbv is 1: use call-by-value, don't descend inside lambda
+// cbv is 2: applicative order
+function reduce(expr, eta, cbv) {
+ if (cbv) {
+ return expr.eval_cbv(cbv > 1);
+ } else {
+ return expr.eval_loop([], eta);
+ }
+}
+
+function make_var(name) {
+ return new Variable(name);
+}
+function make_app(aa, bb) {
+ return new Lambda_app(aa, bb);
+}
+function make_lam(a, aa) {
+ return new Lambda_lam(a, aa);
+}
+
+try {
+ if (console && console.debug) {
+ function print() {
+ console.debug.apply(this, arguments);
+ }
+ }
+} 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)));
+// }