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