diff options
Diffstat (limited to 'main.js')
| -rw-r--r-- | main.js | 363 |
1 files changed, 299 insertions, 64 deletions
@@ -11,26 +11,17 @@ const clearErrors = () => { /* canvas */ -const canvas = window.canvas; +const WHITE = 0; +const BLACK = 1; +const UNKNOWN = 2; -const root = { x: [0, canvas.width], y: [0, canvas.height] }; - -const offscreen = canvas.transferControlToOffscreen(); -const worker = new Worker("canvasWorker.js"); -worker.postMessage({ canvas: offscreen }, [offscreen]); - -const drawAt = (x, y, color) => { +const drawAt = (worker, x, y, color) => { worker.postMessage([ color == WHITE ? [1, 1, 1, 1] : color == BLACK ? [0, 0, 0, 1] - : [0.1, 0.1, 0.1, 0.4], - // color == WHITE - // ? "white" - // : color == BLACK - // ? "black" - // : "grey", + : [0.1, 0.1, 0.1, 0.3], x[0], y[0], x[1] - x[0], @@ -38,31 +29,31 @@ const drawAt = (x, y, color) => { ]); }; -const drawTopLeft = (ctx, color) => { +const drawTopLeft = (worker, ctx, color) => { const newX = [ctx.x[0], ctx.x[0] + (ctx.x[1] - ctx.x[0]) / 2]; const newY = [ctx.y[0], ctx.y[0] + (ctx.y[1] - ctx.y[0]) / 2]; - drawAt(newX, newY, color); + drawAt(worker, newX, newY, color); return { x: newX, y: newY }; }; -const drawTopRight = (ctx, color) => { +const drawTopRight = (worker, ctx, color) => { const newX = [ctx.x[0] + (ctx.x[1] - ctx.x[0]) / 2, ctx.x[1]]; const newY = [ctx.y[0], ctx.y[0] + (ctx.y[1] - ctx.y[0]) / 2]; - drawAt(newX, newY, color); + drawAt(worker, newX, newY, color); return { x: newX, y: newY }; }; -const drawBottomLeft = (ctx, color) => { +const drawBottomLeft = (worker, ctx, color) => { const newX = [ctx.x[0], ctx.x[0] + (ctx.x[1] - ctx.x[0]) / 2]; const newY = [ctx.y[0] + (ctx.y[1] - ctx.y[0]) / 2, ctx.y[1]]; - drawAt(newX, newY, color); + drawAt(worker, newX, newY, color); return { x: newX, y: newY }; }; -const drawBottomRight = (ctx, color) => { +const drawBottomRight = (worker, ctx, color) => { const newX = [ctx.x[0] + (ctx.x[1] - ctx.x[0]) / 2, ctx.x[1]]; const newY = [ctx.y[0] + (ctx.y[1] - ctx.y[0]) / 2, ctx.y[1]]; - drawAt(newX, newY, color); + drawAt(worker, newX, newY, color); return { x: newX, y: newY }; }; @@ -72,6 +63,49 @@ const drawBottomRight = (ctx, color) => { // `return null` and `if (foo === null) return null` are the monads of JavaScript!! // --- +const allHashes = {}; +const hash = (s) => { + let h = 0; + for (let i = 0; i < s.length; i++) { + const chr = s.charCodeAt(i); + h = (h << 5) - h + chr; + h |= 0; + } + while (h in allHashes && allHashes[h] !== s) { + console.warn("hash collision"); + h += 1; + } + allHashes[h] = s; + return h; +}; + +const abs = (body) => { + if (body === null) return null; + const t = { type: "abs", body }; + t.hash = hash("abs" + body.hash); + return t; +}; + +const app = (left) => (right) => { + if (left === null || right === null) return null; + const t = { type: "app", left, right }; + t.hash = hash("app" + left.hash + right.hash); + return t; +}; + +const idx = (idx) => { + if (idx === null) return null; + const t = { type: "idx", idx }; + t.hash = hash("idx" + idx); + return t; +}; + +const def = (name) => { + const t = { type: "def", name }; + t.hash = hash("def" + name); + return t; +}; + const show = (t) => { if (t === null) return ""; switch (t.type) { @@ -169,8 +203,9 @@ const parseTerm = (str) => { if (isOpen(t)) { error("is open"); return null; + } else { + return t; } - return t; }; const substDef = (i, t, n) => { @@ -221,42 +256,255 @@ const parse = (str) => { /* lambda screen */ -const clearScreen = () => { +// [[1]]=w, [[0]]=b, other=g +const toColor = (t) => { + if (t.type === "abs" && t.body.type === "abs" && t.body.body.type === "idx") + return t.body.body.idx === 1 + ? WHITE + : t.body.body.idx === 0 + ? BLACK + : UNKNOWN; + return UNKNOWN; +}; + +// [((((0 tl) tr) bl) br)] +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 = (worker) => { worker.postMessage("clear"); }; /* beta reduction */ -const loadBalance = (msg) => { - const { ctx, t } = msg.data; - // console.log(t); - - if (seemsScreeny(t)) { - const tl = t.body.left.left.left.right; - tlWorker.postMessage({ ctx: drawTopLeft(ctx, toColor(tl)), t: tl }); - const tr = t.body.left.left.right; - trWorker.postMessage({ ctx: drawTopRight(ctx, toColor(tr)), t: tr }); - const bl = t.body.left.right; - blWorker.postMessage({ ctx: drawBottomLeft(ctx, toColor(bl)), t: bl }); - const br = t.body.right; - brWorker.postMessage({ ctx: drawBottomRight(ctx, toColor(br)), t: br }); - } else { - // TODO: could we risk gnfing here? - drawAt(ctx.x, ctx.y, toColor(t)); +let MAX = 0; +let depth = 0; +let canceled = false; +const cancelReduction = () => { + if (depth++ > MAX && !canceled) { + MAX **= 1.4; + if ( + !confirm( + `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; + return true; + } } + return canceled; }; -const tlWorker = new Worker("reductionWorker.js"); -tlWorker.addEventListener("message", loadBalance); -const trWorker = new Worker("reductionWorker.js"); -trWorker.addEventListener("message", loadBalance); -const blWorker = new Worker("reductionWorker.js"); -blWorker.addEventListener("message", loadBalance); -const brWorker = new Worker("reductionWorker.js"); -brWorker.addEventListener("message", loadBalance); - -const reduce = (_t) => { - tlWorker.postMessage({ ctx: root, t: _t }); +const incCache = {}; +const inc = (i, t) => { + if (cancelReduction() || t === null) { + error("in inc"); + return null; + } + + if (t.hash in incCache && i in incCache[t.hash]) return incCache[t.hash][i]; + + let newT; + switch (t.type) { + case "idx": + newT = idx(i <= t.idx ? t.idx + 1 : t.idx); + break; + case "app": + newT = app(inc(i, t.left))(inc(i, t.right)); + break; + case "abs": + newT = abs(inc(i + 1, t.body)); + break; + case "def": + error("unexpected def"); + return null; + } + + if (!(t.hash in incCache)) incCache[t.hash] = {}; + incCache[t.hash][i] = newT; + return newT; +}; + +const substCache = {}; +const subst = (i, t, s) => { + if (cancelReduction() || t === null) { + error("in subst"); + return null; + } + + const h = hash("" + t.hash + s.hash); + if (h in substCache && i in substCache[h]) return substCache[h][i]; + + let newT; + switch (t.type) { + case "idx": + newT = i == t.idx ? s : idx(t.idx > i ? t.idx - 1 : t.idx); + break; + case "app": + newT = app(subst(i, t.left, s))(subst(i, t.right, s)); + break; + case "abs": + newT = abs(subst(i + 1, t.body, inc(0, s))); + break; + case "def": + error("unexpected def"); + return null; + } + + if (!(h in substCache)) substCache[h] = {}; + substCache[h][i] = newT; + return newT; +}; + +// 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 whnfCache = {}; +const whnf = (t) => { + if (cancelReduction() || t === null) { + error("in whnf"); + return null; + } + + if (t.hash in whnfCache) return whnfCache[t.hash]; + + let newT; + switch (t.type) { + case "app": + const _left = whnf(t.left); + if (_left === null) return null; + newT = + _left.type === "abs" + ? whnf(subst(0, _left.body, t.right)) + : app(_left)(t.right); + break; + case "def": + error("unexpected def"); + return null; + default: + newT = t; + break; + } + + whnfCache[t.hash] = newT; + return newT; +}; + +// screen normal form +// one of [((((0 tl) tr) bl) br)], [[0]], [[1]] +const snfCache = {}; +const snf = (_t) => { + if (_t !== null && _t.hash in snfCache) return snfCache[_t.hash]; + + 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)) { + // TODO: a bit unsure about this + switch (t.type) { + case "app": + const _left = whnf(t.left); + t = + _left.type === "abs" + ? subst(0, _left.body, t.right) + : app(_left)(whnf(t.right)); + break; + case "abs": + t = abs(whnf(t.body)); + break; + case "def": + error("unexpected def"); + return null; + default: + error("type"); + return null; + } + } + + snfCache[_t.hash] = t; + return t; +}; + +const reduceLoop = (worker, root, _t) => { + const stack = [{ ctx: root, t: _t }]; + for (let i = 0; stack.length > 0 && i < 4 ** 10; i++) { + // console.log(i, stack.length); + let [{ ctx, t }] = stack.splice( + Math.floor(Math.random() * stack.length), + 1, + ); + // let { ctx, t } = stack.shift(); + // let { ctx, t } = stack.pop(); + + // TODO: priority queue on context size + if (toColor(t) !== UNKNOWN) continue; + + // could loop in gnf, therefore limit depth + MAX = 10000000; + depth = 0; + canceled = false; + try { + t = snf(t); + } catch (e) { + error(e); + return null; + } + if (t === null) { + error("in reduceLoop"); + return null; + } + + // smaller resolutions apparently crash the browser tab lol + if (ctx.x[1] - ctx.x[0] < 2) continue; + + if (seemsScreeny(t)) { + const tl = t.body.left.left.left.right; + stack.push({ ctx: drawTopLeft(worker, ctx, toColor(tl)), t: tl }); + const tr = t.body.left.left.right; + stack.push({ ctx: drawTopRight(worker, ctx, toColor(tr)), t: tr }); + const bl = t.body.left.right; + stack.push({ ctx: drawBottomLeft(worker, ctx, toColor(bl)), t: bl }); + const br = t.body.right; + stack.push({ ctx: drawBottomRight(worker, ctx, toColor(br)), t: br }); + } else { + // TODO: could we risk gnfing here? + drawAt(ctx.x, ctx.y, toColor(t)); + } + } }; /* interface */ @@ -274,16 +522,3 @@ const reduce = (_t) => { // window.slider.style.opacity = 0; // } // }); - -window.examples.addEventListener("change", () => { - clearScreen(); - window.term.value = window.examples.value; -}); - -window.render.addEventListener("click", () => { - clearScreen(); - clearErrors(); - reduce( - app(parse(window.term.value))(parse("\\((((0 \\\\1) \\\\1) \\\\1) \\\\1)")), - ); -}); |