+/*jslint bitwise: true,
+ eqeqeq: true,
+ immed: true,
+ newcap: true,
+ nomen: true,
+ onevar: true,
+ plusplus: true,
+ regexp: true,
+ rhino: true,
+ browser: false,
+ undef: true,
+ white: true,
+
+ evil: false,
+ regexp: false,
+ sub: true,
+ laxbreak: true,
+ onevar: false,
+ debug: true */
+
+
+// DeBruijn terms
+// substitution and translation algorithms from Chris Hankin, An Introduction to Lambda Calculi for Comptuer Scientists
+//
+function Db_free(variable) {
+ this.variable = variable;
+ this.subst = function (m, new_term) {
+ return this;
+ };
+ this.renumber = function (m, i) {
+ return this;
+ };
+ // we assume that other will have variable iff it's a Db_free
+ this.equal = function (other) {
+ return other.variable && this.variable.equal(other.variable);
+ };
+ this.contains = this.equal;
+}
+
+function Db_index(i) {
+ this.index = i;
+ this.subst = function (m, new_term) {
+ if (this.index < m) {
+ return this;
+ } else if (this.index > m) {
+ return new Db_index(this.index - 1);
+ } else {
+ return new_term.renumber(this.index, 1);
+ }
+ };
+ this.renumber = function (m, i) {
+ if (this.index < i) {
+ return this;
+ } else {
+ return new Db_index(this.index + m - 1);
+ }
+ };
+ // we assume that other will have index iff it's a Db_index
+ this.equal = function (other) {
+ return this.index === other.index;
+ };
+ this.contains = this.equal;
+}
+
+function Db_app(left, right) {
+ this.left = left;
+ this.right = right;
+ this.subst = function (m, new_term) {
+ return new Db_app(this.left.subst(m, new_term), this.right.subst(m, new_term));
+ };
+ this.renumber = function (m, i) {
+ return new Db_app(this.left.renumber(m, i), this.right.renumber(m, i));
+ };
+ // we assume that other will have left iff it's a Db_app
+ this.equal = function (other) {
+ return other.left && this.left.equal(other.left) && this.right.equal(other.right);
+ };
+ this.contains = function (other) {
+ if (other.left && this.left.equal(other.left) && this.right.equal(other.right)) {
+ return true;
+ } else {
+ return this.left.contains(other) || this.right.contains(other);
+ }
+ };
+}
+
+function Db_lam(body) {
+ this.body = body;
+ this.subst = function (m, new_term) {
+ return new Db_lam(this.body.subst(m + 1, new_term));
+ };
+ this.renumber = function (m, i) {
+ return new Db_lam(this.body.renumber(m, i + 1));
+ };
+ // we assume that other will have body iff it's a Db_lam
+ this.equal = function (other) {
+ return other.body && this.body.equal(other.body);
+ };
+ this.contains = function (other) {
+ if (other.body && this.body.equal(other.body)) {
+ return true;
+ } else {
+ return this.body.contains(other);
+ }
+ };
+}
+
+
+// lambda terms
+// substitution and normal-order evaluator based on Haskell version by Oleg Kisleyov
+// http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell
+//
+function Variable(name, tag) {
+ this.name = name;
+ 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);
+ 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);
+ };
+ // position of this in seq
+ this.position = function (seq) {
+ for (var i = 0; i < seq.length; i += 1) {
+ if (this.equal(seq[i])) {
+ return new Db_index(i + 1);
+ }
+ }
+ return new Db_free(this);
+ };
+}
+
+// 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 free_in(v, term) {
+ var res = term.has_free(v);
+ return res[0] && res[1];
+}
+
+function subst(v, new_term, expr) {
+ if (new_term.variable && new_term.variable.equal(v)) {
+ return expr;
+ } else {
+ return expr.subst(v, new_term);
+ }
+}
+
+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);
+// }
+ 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);
+ // trampoline to, args
+ return [null, 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);
+ // trampoline to, args
+ return [this.left, 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_dotted();
+ if (as_atom) {
+ return "(" + base + ")";
+ } else {
+ return base;
+ }
+ };
+ 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.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));
+ 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);
+ // trampoline to, args
+ return [subst(this.bound, x, this.body), 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";
+// }
+ 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";
+ };
+}
+
+
+
+///////////////////////////////////////////////////////////////////////////////////
+
+// 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);
+ // 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];
+ }
+}
+
+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) {}
+
+
+
+
+/* Chris's original
+