diff options
| -rw-r--r-- | canvasWorker.js | 2 | ||||
| -rw-r--r-- | common.js | 68 | ||||
| -rw-r--r-- | index.html | 32 | ||||
| -rw-r--r-- | main.js | 363 | ||||
| -rw-r--r-- | readme.md | 8 | ||||
| -rw-r--r-- | reductionWorker.js | 224 |
6 files changed, 334 insertions, 363 deletions
diff --git a/canvasWorker.js b/canvasWorker.js index 4b1e81b..a869810 100644 --- a/canvasWorker.js +++ b/canvasWorker.js @@ -85,7 +85,6 @@ self.onmessage = (msg) => { draw = initGL(); } else { [color, x, y, width, height] = msg.data; - if (width < 2 || height < 2) return; draw([x, y + height, x + width, y + height, x + width, y, x, y], color); } }; @@ -98,6 +97,7 @@ self.onmessage = (msg) => { // gl = canvas.getContext("2d"); // } else { // [color, x, y, width, height] = msg.data; +// if (width < 2 || height < 2) return; // gl.fillStyle = color; // gl.fillRect(x, y, width, height); // } diff --git a/common.js b/common.js deleted file mode 100644 index b8e8464..0000000 --- a/common.js +++ /dev/null @@ -1,68 +0,0 @@ -/* lambda calculus */ - -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) 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; -}; - -/* lambda screen */ - -const WHITE = 0; -const BLACK = 1; -const UNKNOWN = 2; - -// [[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; @@ -56,12 +56,12 @@ invert = \\\((2 0) 1) T-square v1 </option> <option - value="00010001010101000000000001010101101111101111011101100101000001101100000110100101000001101100000110010100000110110000010100101000001101100000110010100000110110000010010100000110110000010100101000001101100000110010100000110110000010010100000110110000010010100000110110000010100100010001010100010001110000101110110100001110000101110110100000000101100000000101000000010110111011001111110111001011111110111110110000010000110110100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101010001000111000010111011010000111000010111011010000000010110000000010111111100111111011101101101100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101110111010101001010000000101101110110000000000101010100000000000101010110111110111101110110111101110110000010010100000001011011101100000000001010101000000000001010101101111101111011101101111011100000101001010000000101101110110000000000101010100000000000101010110111110111101110110111100000101101001000101000000010110111011010000010000000000101010100000000000101010110111110111101110110000010111011010" + value="00010001010101000000000001010101101111101111011101100101000001101100000110100101000001101100000110010100000110110000010100101000001101100000110010100000110110000010010100000110110000010100101000001101100000110010100000110110000010010100000110110000010010100000110110000010100100010001010100010001110000101110110100001110000101110110100000000101100000000101000000010110111011001111110111001011111110111110110000010000110110100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101010001000111000010111011010000111000010111011010000000010110000000010111111100111111011101101101100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101110111010101001010000000101101110110000000000101010100000000000101010110111110111101110110111101110110010101010000000000010101011011111011110111011000001000001100000110000010010100000001011011101100000000001010101000000000001010101101111101111011101101111011100101010100000000000101010110111110111101110110000011000001000001000001101001010000000101101110110000000000101010100000000000101010110111110111101110110111100101010100000000000101010110111110111101110110000011000001000001000001101101001000101000000010110111011010000010000000000101010100000000000101010110111110111101110110010101010000000000010101011011111011110111011000001000001100000110000010111011010" > T-square v2 (1/2) TODO </option> <option - value="00010001010101000000000001010101101111101111011101100101000001101100000110100101000001101100000110010100000110110000010100101000001101100000110010100000110110000010010100000110110000010100101000001101100000110010100000110110000010010100000110110000010010100000110110000010100100010001010100010001110000101110110100001110000101110110100000000101100000000101000000010110111011001111110111001011111110111110110000010000110110100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101010001000111000010111011010000111000010111011010000000010110000000010111111100111111011101101101100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101110111010101001010000000101101110110000000000101010100000000000101010110111110111101110110111101110110010101010000000000010101011011111011110111011000001000001100000110000010010100000001011011101100000000001010101000000000001010101101111101111011101101111011100101010100000000000101010110111110111101110110000011000001000001000001101001010000000101101110110000000000101010100000000000101010110111110111101110110111100101010100000000000101010110111110111101110110000011000001000001000001101101001000101000000010110111011010000010000000000101010100000000000101010110111110111101110110010101010000000000010101011011111011110111011000001000001100000110000010111011010" + value="000100010101010000000000010101011011111011110111011001010000011011000001101001010000011011000001100101000001101100000101001010000011011000001100101000001101100000100101000001101100000101001010000011011000001100101000001101100000100101000001101100000100101000001101100000101001000100010101000100011100001011101101000011100001011101101000000001011000000001010000000101101110110011111101110010111111101111101100000100001101101001010100010001110000101110110100001110000101110110100000000101100000000101000000010110111011001111110111001011111110111110110000010000001010100010001110000101110110100001110000101110110100000000101100000000101111111001111110111011011011001010100010001110000101110110100001110000101110110100000000101100000000101000000010110111011001111110111001011111110111110110000010000001011101110101010010100000001011011101100000000001010101000000000001010101101111101111011101101111011101100101010100000000000101010110111110111101110110010101010000000000010101011011111011110111011000001000001100000110000011000001100000110000010010100000001011011101100000000001010101000000000001010101101111101111011101101111011100101010100000000000101010110111110111101110110000011001010101000000000001010101101111101111011101100000110000010000011000001100000100000110100101000000010110111011000000000010101010000000000010101011011111011110111011011110010101010000000000010101011011111011110111011000001100000100101010100000000000101010110111110111101110110000011000001100000100000110000011011010010001010000000101101110110100000100000000001010101000000000001010101101111101111011101100101010100000000000101010110111110111101110110000010000011000001100101010100000000000101010110111110111101110110000011000001100000110000010111011010" > Sierpinski carpet </option> @@ -87,7 +87,33 @@ y = \(\(1 (0 0)) \(1 (0 0))) </div> <button id="render">Render!</button> </main> - <script src="common.js"></script> <script src="main.js"></script> + <script charset="utf-8"> + const canvas = window.canvas; + 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]); + + window.examples.addEventListener("change", () => { + clearScreen(worker); + window.term.value = window.examples.value; + }); + + window.render.addEventListener("click", () => { + clearScreen(worker); + clearErrors(); + console.time("reduceLoop"); + reduceLoop( + worker, + root, + app(parse(window.term.value))( + parse("\\((((0 \\\\1) \\\\1) \\\\1) \\\\1)"), + ), + ); + console.timeEnd("reduceLoop"); + }); + </script> </body> </html> @@ -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)")), - ); -}); @@ -4,11 +4,13 @@ See the accompanying [blog post](https://text.marvinborner.de/2024-03-25-02.html) for more information. -## Implementation +## Details - WebGL for drawing the squares - 1 Webworker for handling paint requests -- 4 Webworkers for reducing top-left, top-right, bottom-left, and - bottom-right terms (using 4 priority queues) +- single-threaded reduction via randomized stack popping (see + [4fa7012](https://github.com/marvinborner/lambda-screen/tree/4fa7012e03e09fa62bd0080f2c7bfbf02b00a6ca) + for an implementation using 4 parallel reduction workers; they + crashed firefox consistently) - Currently no higher-order reduction - No libraries diff --git a/reductionWorker.js b/reductionWorker.js deleted file mode 100644 index acf75ce..0000000 --- a/reductionWorker.js +++ /dev/null @@ -1,224 +0,0 @@ -// TODO: reduction could be made faster using higher-order reduction (see my infinite-apply implementation) - -importScripts("common.js"); - -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 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]; - - 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; -}; - -let running = false; -const stack = []; -const reduce = () => { - running = true; - - for (let i = 0; stack.length > 0; 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 = 1000000; - depth = 0; - canceled = false; - try { - t = snf(t); - } catch (e) { - error(e); - return null; - } - if (t === null) { - error("in reduce"); - return null; - } - - // smaller resolutions apparently crash the browser tab lol - if (ctx.x[1] - ctx.x[0] < 3) continue; - - postMessage({ ctx, t }); - } - - running = false; -}; - -self.onmessage = (msg) => { - stack.push(msg.data); - if (!running) reduce(); -}; |