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);
+// 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);
};
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);
- }
+// 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);
+ // 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);
};
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) {
}
};
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 (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";
};
}
if (cbv) {
return expr.eval_cbv(cbv > 1);
} else {
- return expr.eval_loop([], eta);
+ // return expr.eval_loop([], eta);
+ 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
+*/