- 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";
- }
- };
+ 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";
+ }
+ };