From 4fa7012e03e09fa62bd0080f2c7bfbf02b00a6ca Mon Sep 17 00:00:00 2001 From: Marvin Borner Date: Sun, 7 Apr 2024 14:40:15 +0200 Subject: Experiments with parallel reduction workers --- bruijn/Experiments.bruijn | 83 ++----- canvasWorker.js | 104 +++++++++ common.js | 68 ++++++ index.html | 48 +++-- main.js | 289 +++++++++++++++++++++++++ readme.md | 14 ++ reductionWorker.js | 224 +++++++++++++++++++ script.js | 537 ---------------------------------------------- worker.js | 90 -------- 9 files changed, 756 insertions(+), 701 deletions(-) create mode 100644 canvasWorker.js create mode 100644 common.js create mode 100644 main.js create mode 100644 readme.md create mode 100644 reductionWorker.js delete mode 100644 script.js delete mode 100644 worker.js diff --git a/bruijn/Experiments.bruijn b/bruijn/Experiments.bruijn index 2e2173d..d1bc116 100644 --- a/bruijn/Experiments.bruijn +++ b/bruijn/Experiments.bruijn @@ -1,63 +1,26 @@ :import std/Combinator . -:import Screen . - -# stable -s w - -a-sierpinski0 [build w w w w] - -a-sierpinski1 [build tl tr bl br] - tl build w w w (build w s s b) - tr build w w (build s w b s) w - bl build w (build s b w s) w w - br build (build b s s w) w w w - -a-sierpinski2 [build tl tr bl br] - tl build tl tr bl br - tl build w w w (build w s s b) - tr build w w (build s w b s) w - bl build w (build s b w s) w w - br build (build b s s w) s s b - tr build tl tr bl br - tl build w w w (build w s s b) - tr build w w (build s w b s) w - bl build s (build s b w s) b s - br build (build b s s w) w w w - bl build tl tr bl br - tl build w w w (build w s s b) - tr build s b (build s w b s) s - bl build w (build s b w s) w w - br build (build b s s w) w w w - br build tl tr bl br - tl build b s s (build w s s b) - tr build w w (build s w b s) w - bl build w (build s b w s) w w - br build (build b s s w) w w w - -b-sierpinski0 y [gen] - gen qsplit → color - color &[[[[[0 (5 (tl 4)) (5 (tr 3)) (5 (bl 2)) (5 (br 1))]]]]] - tl &[[[[[0 4 3 2 b]]]]] - tr &[[[[[0 4 3 b 1]]]]] - bl &[[[[[0 4 b 2 1]]]]] - br &[[[[[0 b 3 2 1]]]]] - :import std/List . +:import Screen . -b-sierpinski1 color - color [[build tl tr bl br] mut] - mut y* ([[[[build 3 2 1 b]]]] : ([[[[build 3 2 b 0]]]] : ([[[[build 3 b 1 0]]]] : {}[[[[build b 2 1 0]]]]))) - tl ^0 - tr ^(~0) - bl ^(~(~0)) - br ^(~(~(~0))) - -:import std/Number . - -b-sierpinskin y [[[=?1 0 (gen 0)]]] (+7) - gen qsplit → color - color &[[[[[0 (7 --6 (tl 4)) (7 --6 (tr 3)) (7 --6 (bl 2)) (7 --6 (br 1))]]]]] - tl &[[[[[0 4 3 2 b]]]]] - tr &[[[[[0 4 3 b 1]]]]] - bl &[[[[[0 4 b 2 1]]]]] - br &[[[[[0 b 3 2 1]]]]] +t-square-1 [[build tl tr bl br] mut] + mut y* ([[[[build 3 2 1 b]]]] : ([[[[build 3 2 b 0]]]] : ([[[[build 3 b 1 0]]]] : {}[[[[build b 2 1 0]]]]))) + tl ^0 + tr ^(~0) + bl ^(~(~0)) + br ^(~(~(~0))) + +t-square-2 [[build tl tr bl br] mut] + mut y* ([[[[build 3 2 1 (build b w w b)]]]] : ([[[[build 3 2 (build w b b w) 0]]]] : ([[[[build 3 (build w b b w) 1 0]]]] : {}[[[[build (build b w w b) 2 1 0]]]]))) + tl ^0 + tr ^(~0) + bl ^(~(~0)) + br ^(~(~(~0))) + +sierpinski-carpet [[build tl tr bl br] mut] + mut y* ([[[[build 3 2 1 (build (build b w w w) w w b)]]]] : ([[[[build 3 2 (build w (build w b w w) b w) 0]]]] : ([[[[build 3 (build w b (build w w b w) w) 1 0]]]] : {}[[[[build (build b w w (build w w w b)) 2 1 0]]]]))) + tl ^0 + tr ^(~0) + bl ^(~(~0)) + br ^(~(~(~0))) + +sierpinski-triangle [y [build 0 b 0 0]] diff --git a/canvasWorker.js b/canvasWorker.js new file mode 100644 index 0000000..4b1e81b --- /dev/null +++ b/canvasWorker.js @@ -0,0 +1,104 @@ +let canvas, gl; + +const createShader = (gl, type, source) => { + const shader = gl.createShader(type); + gl.shaderSource(shader, source); + gl.compileShader(shader); + const success = gl.getShaderParameter(shader, gl.COMPILE_STATUS); + if (success) return shader; + + console.error(gl.getShaderInfoLog(shader)); + gl.deleteShader(shader); +}; + +const createProgram = (gl, vertexShader, fragmentShader) => { + const program = gl.createProgram(); + gl.attachShader(program, vertexShader); + gl.attachShader(program, fragmentShader); + gl.linkProgram(program); + const success = gl.getProgramParameter(program, gl.LINK_STATUS); + if (success) return program; + + console.error(gl.getProgramInfoLog(program)); + gl.deleteProgram(program); +}; + +const initGL = () => { + const vertexShaderSource = ` + attribute vec2 a_position; + uniform vec2 u_resolution; + void main() { + vec2 inverted = vec2(a_position.x, u_resolution.y - a_position.y - 1.0); // !! :) + vec2 zeroToOne = inverted / u_resolution; + vec2 zeroToTwo = zeroToOne * 2.0; + vec2 clipSpace = zeroToTwo - 1.0; + gl_Position = vec4(clipSpace, 0, 1); + }`; + const fragmentShaderSource = ` + precision mediump float; + uniform vec4 u_color; + void main() { + gl_FragColor = u_color; + }`; + + const vertexShader = createShader(gl, gl.VERTEX_SHADER, vertexShaderSource); + const fragmentShader = createShader( + gl, + gl.FRAGMENT_SHADER, + fragmentShaderSource, + ); + + const program = createProgram(gl, vertexShader, fragmentShader); + const positionAttributeLocation = gl.getAttribLocation(program, "a_position"); + const colorUniformLocation = gl.getUniformLocation(program, "u_color"); + const resolutionUniformLocation = gl.getUniformLocation( + program, + "u_resolution", + ); + + const positionBuffer = gl.createBuffer(); + gl.bindBuffer(gl.ARRAY_BUFFER, positionBuffer); + gl.viewport(0, 0, gl.canvas.width, gl.canvas.height); + gl.useProgram(program); + gl.uniform2f(resolutionUniformLocation, gl.canvas.width, gl.canvas.height); + gl.enableVertexAttribArray(positionAttributeLocation); + gl.vertexAttribPointer(positionAttributeLocation, 2, gl.FLOAT, false, 0, 0); + + return (positions, color) => { + gl.bufferData(gl.ARRAY_BUFFER, new Float32Array(positions), gl.STATIC_DRAW); + gl.bindBuffer(gl.ARRAY_BUFFER, positionBuffer); + gl.uniform4f(colorUniformLocation, ...color); + gl.drawArrays(gl.TRIANGLE_FAN, 0, 4); + }; +}; + +let draw; +self.onmessage = (msg) => { + if (msg.data == "clear") { + gl.clearColor(0, 0, 0, 0); + gl.clear(gl.COLOR_BUFFER_BIT); + } else if ("canvas" in msg.data) { + canvas = msg.data.canvas; + gl = canvas.getContext("webgl", { preserveDrawingBuffer: true }); + if (!gl) alert("no webgl"); + gl.viewport(0, 0, canvas.width, canvas.height); + 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); + } +}; + +// self.onmessage = (msg) => { +// if (msg.data == "clear") { +// gl.clearRect(0, 0, canvas.width, canvas.height); +// } else if ("canvas" in msg.data) { +// canvas = msg.data.canvas; +// gl = canvas.getContext("2d"); +// } else { +// [color, x, y, width, height] = msg.data; +// gl.fillStyle = color; +// gl.fillRect(x, y, width, height); +// } +// }; diff --git a/common.js b/common.js new file mode 100644 index 0000000..b8e8464 --- /dev/null +++ b/common.js @@ -0,0 +1,68 @@ +/* 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; diff --git a/index.html b/index.html index d1997cb..e3b28f9 100644 --- a/index.html +++ b/index.html @@ -9,17 +9,17 @@
-
-
- Reduction mode: - -
- -
+ + + + + + + + + + +
Load preset: @@ -51,10 +51,29 @@ invert = \\\((2 0) 1) Invert + + + + +
@@ -68,6 +87,7 @@ invert = \\\((2 0) 1)
- + + diff --git a/main.js b/main.js new file mode 100644 index 0000000..56d0202 --- /dev/null +++ b/main.js @@ -0,0 +1,289 @@ +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 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]); + +const drawAt = (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", + x[0], + y[0], + x[1] - x[0], + y[1] - y[0], + ]); +}; + +const drawTopLeft = (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); + return { x: newX, y: newY }; +}; + +const drawTopRight = (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); + return { x: newX, y: newY }; +}; + +const drawBottomLeft = (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); + return { x: newX, y: newY }; +}; + +const drawBottomRight = (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); + return { x: newX, y: newY }; +}; + +/* lambda calculus */ + +// --- +// `return null` and `if (foo === null) return null` are the monads of JavaScript!! +// --- + +const show = (t) => { + if (t === null) return ""; + switch (t.type) { + case "abs": + // return `\\${show(t.body)}`; + return `[${show(t.body)}]`; + case "app": + return `(${show(t.left)} ${show(t.right)})`; + case "idx": + return `${t.idx}`; + case "def": + return t.name; + } +}; + +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 "\\": + case "[": // bruijn + const [body, _tail] = parseLam(tail); + return [abs(body), head == "[" ? _tail.slice(1) : _tail]; + case "(": + const [left, tail1] = parseLam(tail); + const [right, tail2] = parseLam(tail1.slice(1)); + return [app(left)(right), tail2.slice(1)]; + case ")": + case "]": + error("in parseLam"); + return []; + default: + 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]; + } + } +}; + +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; + } + 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.startsWith("--") || line.length == 0) return true; + 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 */ + +const clearScreen = () => { + 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)); + } +}; + +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 }); +}; + +/* interface */ + +// window.reductionMode.addEventListener("change", () => { +// const state = window.reductionMode.value; +// if (state === "auto") { +// window.slider.disabled = true; +// window.slider.style.opacity = 0; +// } else if (state === "slider") { +// window.slider.disabled = false; +// window.slider.style.opacity = 100; +// } else if (state === "click") { +// window.slider.disabled = true; +// 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)")), + ); +}); diff --git a/readme.md b/readme.md new file mode 100644 index 0000000..c4eaee6 --- /dev/null +++ b/readme.md @@ -0,0 +1,14 @@ +# Lambda Screen + +See the accompanying [blog +post](https://text.marvinborner.de/2024-03-25-02.html) for more +information. + +## Implementation + +- 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) +- Currently no higher-order reduction +- No libraries diff --git a/reductionWorker.js b/reductionWorker.js new file mode 100644 index 0000000..acf75ce --- /dev/null +++ b/reductionWorker.js @@ -0,0 +1,224 @@ +// 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(); +}; diff --git a/script.js b/script.js deleted file mode 100644 index fcfd1ff..0000000 --- a/script.js +++ /dev/null @@ -1,537 +0,0 @@ -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; -const BLACK = 1; -const UNKNOWN = 2; - -const canvas = window.canvas; - -const root = { x: [0, canvas.width], y: [0, canvas.height] }; - -const offscreen = canvas.transferControlToOffscreen(); -const worker = new Worker("worker.js"); -worker.postMessage({ canvas: offscreen }, [offscreen]); - -const drawAt = (x, y, color) => { - worker.postMessage([ - color == WHITE - ? [1, 1, 1, 1] - : color == BLACK - ? [0, 0, 0, 1] - : [0.1, 0.1, 0.1, 0.3], - x[0], - y[0], - x[1] - x[0], - y[1] - y[0], - ]); -}; - -const drawTopLeft = (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); - return { x: newX, y: newY }; -}; - -const drawTopRight = (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); - return { x: newX, y: newY }; -}; - -const drawBottomLeft = (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); - return { x: newX, y: newY }; -}; - -const drawBottomRight = (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); - return { x: newX, y: newY }; -}; - -/* lambda calculus */ - -// --- -// `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) 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) { - case "abs": - // return `\\${show(t.body)}`; - return `[${show(t.body)}]`; - case "app": - return `(${show(t.left)} ${show(t.right)})`; - case "idx": - return `${t.idx}`; - case "def": - return t.name; - } -}; - -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 "\\": - case "[": // bruijn - const [body, _tail] = parseLam(tail); - return [abs(body), head == "[" ? _tail.slice(1) : _tail]; - case "(": - const [left, tail1] = parseLam(tail); - const [right, tail2] = parseLam(tail1.slice(1)); - return [app(left)(right), tail2.slice(1)]; - case ")": - case "]": - error("in parseLam"); - return []; - default: - 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]; - } - } -}; - -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.startsWith("--") || line.length == 0) return true; - 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 = (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.postMessage("clear"); -}; - -/* beta reduction */ - -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]; - - 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 reduce = (_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(); - 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 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 { - // TODO: could we risk gnfing here? - drawAt(ctx.x, ctx.y, toColor(t)); - } - } -}; - -/* interface */ - -window.reductionMode.addEventListener("change", () => { - const state = window.reductionMode.value; - if (state === "auto") { - window.slider.disabled = true; - window.slider.style.opacity = 0; - } else if (state === "slider") { - window.slider.disabled = false; - window.slider.style.opacity = 100; - } else if (state === "click") { - window.slider.disabled = true; - 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)")), - ); -}); diff --git a/worker.js b/worker.js deleted file mode 100644 index 3b35129..0000000 --- a/worker.js +++ /dev/null @@ -1,90 +0,0 @@ -let canvas, gl; - -const createShader = (gl, type, source) => { - const shader = gl.createShader(type); - gl.shaderSource(shader, source); - gl.compileShader(shader); - const success = gl.getShaderParameter(shader, gl.COMPILE_STATUS); - if (success) return shader; - - console.error(gl.getShaderInfoLog(shader)); - gl.deleteShader(shader); -}; - -const createProgram = (gl, vertexShader, fragmentShader) => { - const program = gl.createProgram(); - gl.attachShader(program, vertexShader); - gl.attachShader(program, fragmentShader); - gl.linkProgram(program); - const success = gl.getProgramParameter(program, gl.LINK_STATUS); - if (success) return program; - - console.error(gl.getProgramInfoLog(program)); - gl.deleteProgram(program); -}; - -const initGL = () => { - const vertexShaderSource = ` - attribute vec2 a_position; - uniform vec2 u_resolution; - void main() { - vec2 inverted = vec2(a_position.x, u_resolution.y - a_position.y - 1.0); // !! :) - vec2 zeroToOne = inverted / u_resolution; - vec2 zeroToTwo = zeroToOne * 2.0; - vec2 clipSpace = zeroToTwo - 1.0; - gl_Position = vec4(clipSpace, 0, 1); - }`; - const fragmentShaderSource = ` - precision mediump float; - uniform vec4 u_color; - void main() { - gl_FragColor = u_color; - }`; - - const vertexShader = createShader(gl, gl.VERTEX_SHADER, vertexShaderSource); - const fragmentShader = createShader( - gl, - gl.FRAGMENT_SHADER, - fragmentShaderSource, - ); - - const program = createProgram(gl, vertexShader, fragmentShader); - const positionAttributeLocation = gl.getAttribLocation(program, "a_position"); - const colorUniformLocation = gl.getUniformLocation(program, "u_color"); - const resolutionUniformLocation = gl.getUniformLocation( - program, - "u_resolution", - ); - - const positionBuffer = gl.createBuffer(); - gl.bindBuffer(gl.ARRAY_BUFFER, positionBuffer); - gl.viewport(0, 0, gl.canvas.width, gl.canvas.height); - gl.useProgram(program); - gl.uniform2f(resolutionUniformLocation, gl.canvas.width, gl.canvas.height); - gl.enableVertexAttribArray(positionAttributeLocation); - gl.vertexAttribPointer(positionAttributeLocation, 2, gl.FLOAT, false, 0, 0); - - return (positions, color) => { - gl.bufferData(gl.ARRAY_BUFFER, new Float32Array(positions), gl.STATIC_DRAW); - gl.bindBuffer(gl.ARRAY_BUFFER, positionBuffer); - gl.uniform4f(colorUniformLocation, ...color); - gl.drawArrays(gl.TRIANGLE_FAN, 0, 4); - }; -}; - -let draw; -self.onmessage = (msg) => { - if (msg.data == "clear") { - gl.clearColor(0, 0, 0, 0); - gl.clear(gl.COLOR_BUFFER_BIT); - } else if ("canvas" in msg.data) { - canvas = msg.data.canvas; - gl = canvas.getContext("webgl", { preserveDrawingBuffer: true }); - if (!gl) alert("no webgl"); - gl.viewport(0, 0, canvas.width, canvas.height); - draw = initGL(); - } else { - [color, x, y, width, height] = msg.data; - draw([x, y + height, x + width, y + height, x + width, y, x, y], color); - } -}; -- cgit v1.2.3