aboutsummaryrefslogtreecommitdiffhomepage
path: root/script.js
diff options
context:
space:
mode:
Diffstat (limited to 'script.js')
-rw-r--r--script.js430
1 files changed, 305 insertions, 125 deletions
diff --git a/script.js b/script.js
index f5d1b8a..9bab3c4 100644
--- a/script.js
+++ b/script.js
@@ -1,3 +1,14 @@
+let errors = [];
+const error = (s) => {
+ errors.push(s);
+ console.error(s);
+ window.error.innerText = "invalid term: " + errors.toReversed().join(", ");
+};
+const clearErrors = () => {
+ errors = [];
+ window.error.innerText = "";
+};
+
/* canvas */
const WHITE = 0;
@@ -45,6 +56,10 @@ const drawBottomRight = (ctx, color) => {
/* lambda calculus */
+// ---
+// `return null` and `if (foo === null) return null` are the monads of JavaScript!!
+// ---
+
const abs = (body) => {
if (body === null) return null;
return { type: "abs", body };
@@ -60,98 +75,181 @@ const idx = (idx) => {
return { type: "idx", idx };
};
-const namedAbs = (name, body) => {
- if (body === null) return null;
- return { type: "named-abs", name, body };
-};
-
-const higherOrderAbs = (f) => {
- if (f === null) return null;
- return { type: "higher-order-abs", f };
+const def = (name) => {
+ return { type: "def", name };
};
-const higherOrderApp = (a) => {
- if (a === null) return () => null;
- else if (a.type == "higher-order-abs") return a.f;
- else return app(a);
-};
-
-const show = (term) => {
- if (term === null) return "";
- switch (term.type) {
+const show = (t) => {
+ if (t === null) return "";
+ switch (t.type) {
case "abs":
- return `\\${show(term.body)}`;
+ // return `\\${show(t.body)}`;
+ return `[${show(t.body)}]`;
case "app":
- return `(${show(term.left)} ${show(term.right)})`;
+ return `(${show(t.left)} ${show(t.right)})`;
case "idx":
- return `${term.idx}`;
+ return `${t.idx}`;
+ case "def":
+ return t.name;
}
};
-const parse = (str) => {
- if (!str) return [{}, ""];
+const isOpen = (t) => {
+ const go = (t, d) => {
+ if (t === null) return true;
+ switch (t.type) {
+ case "abs":
+ return go(t.body, d + 1);
+ case "app":
+ return go(t.left, d) || go(t.right, d);
+ case "idx":
+ return t.idx >= d;
+ case "def":
+ return false;
+ }
+ };
+ return go(t, 0);
+};
+
+const parseLam = (str) => {
+ if (!str) {
+ error("in parseLam");
+ return [{}, ""];
+ }
const head = str[0];
const tail = str.slice(1);
switch (head) {
+ case "λ":
case "\\":
- const [body, _tail] = parse(tail);
+ const [body, _tail] = parseLam(tail);
return [abs(body), _tail];
+ case "[": // bruijn
+ const [bbody, _btail] = parseLam(tail);
+ return [abs(bbody), _btail.slice(1)];
case "(":
- const [left, tail1] = parse(tail);
- const [right, tail2] = parse(tail1.slice(1));
+ const [left, tail1] = parseLam(tail);
+ const [right, tail2] = parseLam(tail1.slice(1));
return [app(left)(right), tail2.slice(1)];
case ")":
- alert("fatal");
+ case "]":
+ error("in parseLam");
return [];
default:
- let num = "";
- while (str && str[0] >= "0" && str[0] <= "9") {
- num += str[0];
- str = str.slice(1);
+ if (str[0] >= "a" && str[0] <= "z") {
+ // substitution
+ let name = "";
+ while (str && str[0] >= "a" && str[0] <= "z") {
+ name += str[0];
+ str = str.slice(1);
+ }
+ return [def(name), str];
+ } else {
+ // de Bruijn index
+ let num = "";
+ while (str && str[0] >= "0" && str[0] <= "9") {
+ num += str[0];
+ str = str.slice(1);
+ }
+ return [idx(parseInt(num)), str];
}
- return [idx(parseInt(num)), str];
}
};
+const parseBLC = (str) => {
+ if (!str) {
+ error("in parseBLC");
+ return [{}, ""];
+ }
+ if (str.slice(0, 2) === "00") {
+ const [body, tail] = parseBLC(str.slice(2));
+ return [abs(body), tail];
+ }
+ if (str.slice(0, 2) === "01") {
+ const [left, tail1] = parseBLC(str.slice(2));
+ const [right, tail2] = parseBLC(tail1);
+ return [app(left)(right), tail2];
+ }
+ const cnt = str.slice(1).indexOf("0");
+ return [idx(cnt), str.slice(cnt + 2)];
+};
+
+const parseTerm = (str) => {
+ const t = /^[01]+$/.test(str) ? parseBLC(str)[0] : parseLam(str)[0];
+ if (isOpen(t)) {
+ error("is open");
+ return null;
+ } else {
+ return t;
+ }
+};
+
+const substDef = (i, t, n) => {
+ switch (t.type) {
+ case "idx":
+ return t;
+ case "app":
+ return app(substDef(i, t.left, n))(substDef(i, t.right, n));
+ case "abs":
+ return abs(substDef(i + 1, t.body, n));
+ case "def":
+ return t.name === n ? idx(i) : t;
+ }
+};
+
+const resolveTerm = (_t, defs) => {
+ if (_t === null) return null;
+ let final = _t;
+ let len = Object.keys(defs).length;
+ for (let i = len; i > 0; i--) {
+ final = abs(final);
+ }
+ let d = len;
+ Object.entries(defs).forEach(([n, t]) => {
+ final = app(substDef(--d - len, final, n))(t);
+ });
+ return final;
+};
+
+const parse = (str) => {
+ const defs = {};
+ let t;
+ str
+ .trim()
+ .split(/\r?\n/)
+ .every((line) => {
+ if (!line.includes("=")) {
+ t = resolveTerm(parseTerm(line), defs);
+ return false;
+ }
+ [n, _t] = line.split("=");
+ defs[n.trim()] = resolveTerm(parseTerm(_t.trim()), defs);
+ return true;
+ });
+ return t;
+};
+
/* lambda screen */
// [[1]]=w, [[0]]=b, other=g
-const toColor = (term) => {
- if (
- term.type === "abs" &&
- term.body.type === "abs" &&
- term.body.body.type === "idx"
- )
- return term.body.body.idx === 1
+const toColor = (t) => {
+ if (t.type === "abs" && t.body.type === "abs" && t.body.body.type === "idx")
+ return t.body.body.idx === 1
? WHITE
- : term.body.body.idx === 0
+ : t.body.body.idx === 0
? BLACK
: UNKNOWN;
return UNKNOWN;
};
// [((((0 tl) tr) bl) br)]
-const seemsScreeny = (term) => {
- if (
- term.type === "abs" &&
- term.body.type === "app" &&
- term.body.left.type === "app" &&
- term.body.left.left.type === "app" &&
- term.body.left.left.left.type === "app" &&
- term.body.left.left.left.left.type === "idx" &&
- term.body.left.left.left.left.idx === 0
- )
- return true;
- return false;
-};
-
-const draw = (ctx, term) => {
- if (!("type" in term)) return;
- drawTopLeft(ctx, toColor(term.body.left.left.left.right));
- drawTopRight(ctx, toColor(term.body.left.left.right));
- drawBottomLeft(ctx, toColor(term.body.left.right));
- drawBottomRight(ctx, toColor(term.body.right));
-};
+const seemsScreeny = (t) =>
+ t.type === "abs" &&
+ t.body.type === "app" &&
+ t.body.left.type === "app" &&
+ t.body.left.left.type === "app" &&
+ t.body.left.left.left.type === "app" &&
+ t.body.left.left.left.left.type === "idx" &&
+ t.body.left.left.left.left.idx === 0;
const clearScreen = () => {
screen.clearRect(0, 0, canvas.width, canvas.height);
@@ -164,10 +262,10 @@ let depth = 0;
let canceled = false;
const cancelReduction = () => {
if (depth++ > MAX && !canceled) {
- MAX **= 1.5;
+ MAX **= 1.4;
if (
!confirm(
- `This takes awfully long (${depth} steps!). The reduction potentially won't converge. Do you want to continue?\nWarning: This might crash your browser!`,
+ `This takes awfully long (${depth} steps!). The reduction potentially won't converge to a valid screen (or at all!). Do you want to continue?\nWarning: This might crash your browser!`,
)
) {
canceled = true;
@@ -177,76 +275,160 @@ const cancelReduction = () => {
return canceled;
};
-const toTerm = () => {
- depth = 0;
- const go = (env) => (t) => {
- if (cancelReduction()) return null;
- if (t === null) return null;
- switch (t.type) {
- case "app":
- return app(go(env)(t.left))(go(env)(t.right));
- case "named-abs":
- return abs(go([t.name, ...env])(t.body));
- case "idx":
- return idx(t.idx in env ? env[t.idx] : t.idx);
- default:
- alert("fatal error");
- return null;
- }
- };
- return go([]);
+const inc = (i, t) => {
+ if (cancelReduction() || t === null) {
+ error("in inc");
+ return null;
+ }
+ switch (t.type) {
+ case "idx":
+ return idx(i <= t.idx ? t.idx + 1 : t.idx);
+ case "app":
+ return app(inc(i, t.left))(inc(i, t.right));
+ case "abs":
+ return abs(inc(i + 1, t.body));
+ case "def":
+ error("unexpected def");
+ return null;
+ }
};
-const toNamedTerm = () => {
- depth = 0;
- const go = (d) => (t) => {
- if (cancelReduction()) return null;
- if (t === null) return null;
- switch (t.type) {
- case "app":
- return app(go(d)(t.left))(go(d)(t.right));
- case "higher-order-abs":
- return namedAbs(d, go(d + 1)(t.f(idx(d))));
- case "idx":
- return idx(t.idx);
- default:
- alert("fatal error");
- return null;
- }
- };
- return go(0);
+const subst = (i, t, s) => {
+ if (cancelReduction() || t === null) {
+ error("in subst");
+ return null;
+ }
+ switch (t.type) {
+ case "idx":
+ return i == t.idx ? s : idx(t.idx > i ? t.idx - 1 : t.idx);
+ case "app":
+ return app(subst(i, t.left, s))(subst(i, t.right, s));
+ case "abs":
+ return abs(subst(i + 1, t.body, inc(0, s)));
+ case "def":
+ error("unexpected def");
+ return null;
+ }
};
-const toHigherOrder = () => {
- depth = 0;
- const go = (env) => (t) => {
- if (cancelReduction()) return null;
- if (t === null) return null;
+// guaranteed normal form
+// only use if sure that t is not a (potentially diverging) screen
+const gnf = (t) => {
+ if (cancelReduction() || t === null) {
+ error("in gnf");
+ return null;
+ }
+ switch (t.type) {
+ case "app":
+ const _left = gnf(t.left);
+ if (_left === null) return null;
+ return _left.type === "abs"
+ ? gnf(subst(0, _left.body, t.right))
+ : app(_left)(gnf(t.right));
+ case "abs":
+ return abs(gnf(t.body));
+ case "def":
+ error("unexpected def");
+ return null;
+ default:
+ return t;
+ }
+};
+
+// weak head normal form
+const whnf = (t) => {
+ if (cancelReduction() || t === null) {
+ error("in whnf");
+ return null;
+ }
+ switch (t.type) {
+ case "app":
+ const _left = whnf(t.left);
+ if (_left === null) return null;
+ return _left.type === "abs"
+ ? whnf(subst(0, _left.body, t.right))
+ : app(_left)(t.right);
+ case "def":
+ error("unexpected def");
+ return null;
+ default:
+ return t;
+ }
+};
+
+// screen normal form
+// one of [((((0 tl) tr) bl) br)], [[0]], [[1]]
+const snf = (_t) => {
+ let t = whnf(_t);
+ if (t === null || t.type !== "abs") {
+ error("not a screen/pixel");
+ return null;
+ }
+ t = abs(whnf(t.body));
+ if (t.body.type === "abs") return gnf(t); // not a screen, probably a pixel
+
+ while (t !== null && !seemsScreeny(t)) {
+ if (cancelReduction()) {
+ error("in snf");
+ return null;
+ }
+ // TODO: a bit unsure about this
switch (t.type) {
case "app":
- return higherOrderApp(go(env)(t.left))(go(env)(t.right));
+ const _left = whnf(t.left);
+ t =
+ _left.type === "abs"
+ ? subst(0, _left.body, t.right)
+ : app(_left)(whnf(t.right));
+ break;
case "abs":
- return higherOrderAbs((x) => go([x, ...env])(t.body));
- case "idx":
- if (t.idx in env) return env[t.idx];
- else return idx(t.idx);
+ t = abs(whnf(t.body));
+ break;
+ case "def":
+ error("unexpected def");
+ return null;
default:
- alert("fatal error");
+ error("type");
return null;
}
- };
- return go([]);
+ }
+ return t;
};
-const reduce = (t) => {
- MAX = 16384;
- canceled = false;
- try {
- return toTerm()(toNamedTerm()(toHigherOrder()(t)));
- } catch (e) {
- console.error(e);
- alert(e);
- return null;
+const reduce = (_t) => {
+ console.log(show(_t));
+ const stack = [{ ctx: root, t: _t }];
+ for (let i = 0; stack.length > 0 && i < 1024; i++) {
+ let { ctx, t } = stack.pop();
+ if (toColor(t) !== UNKNOWN) continue;
+
+ // could loop in gnf, therefore limit depth
+ MAX = 16384;
+ depth = 0;
+ canceled = false;
+ try {
+ t = snf(t);
+ } catch (e) {
+ error(e);
+ return null;
+ }
+ if (t === null) {
+ error("in reduce");
+ return null;
+ }
+
+ if (seemsScreeny(t)) {
+ const tl = t.body.left.left.left.right;
+ stack.push({ ctx: drawTopLeft(ctx, toColor(tl)), t: tl });
+ const tr = t.body.left.left.right;
+ stack.push({ ctx: drawTopRight(ctx, toColor(tr)), t: tr });
+ const bl = t.body.left.right;
+ stack.push({ ctx: drawBottomLeft(ctx, toColor(bl)), t: bl });
+ const br = t.body.right;
+ stack.push({ ctx: drawBottomRight(ctx, toColor(br)), t: br });
+ } else {
+ drawAt(ctx.x, ctx.y, toColor(t));
+ }
}
};
@@ -272,10 +454,8 @@ window.examples.addEventListener("change", () => {
});
window.render.addEventListener("click", () => {
- draw(
- root,
- reduce(
- parse(`(${window.term.value} \\((((0 \\\\1) \\\\1) \\\\1) \\\\1)`)[0],
- ),
+ clearErrors();
+ reduce(
+ app(parse(window.term.value))(parse("\\((((0 \\\\1) \\\\1) \\\\1) \\\\1)")),
);
});