Experiments with parallel reduction workers

8 files changed, 666 insertions, 611 deletions

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/worker.js b/canvasWorker.js
index 3b35129..4b1e81b 100644
--- a/worker.js
+++ b/canvasWorker.js
@@ -85,6 +85,20 @@ 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);
   }
 };
+
+// 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 @@
   <body>
     <main>
       <canvas height="800" width="800" id="canvas"></canvas>
-      <div>
-        <div class="inputWrap">
-          Reduction mode:
-          <select id="reductionMode">
-            <option value="auto" selected>Reduce to normal form</option>
-            <option value="slider">Reduce by sliding</option>
-            <option value="click">Reduce by clicking</option>
-          </select>
-        </div>
-        <input type="range" min="0" max="20" value="0" id="slider" />
-      </div>
+      <!-- <div> -->
+      <!--   <div class="inputWrap"> -->
+      <!--     Reduction mode: -->
+      <!--     <select id="reductionMode"> -->
+      <!--       <option value="auto" selected>Reduce to normal form</option> -->
+      <!--       <option value="slider">Reduce by sliding</option> -->
+      <!--       <option value="click">Reduce by clicking</option> -->
+      <!--     </select> -->
+      <!--   </div> -->
+      <!--   <input type="range" min="0" max="20" value="0" id="slider" /> -->
+      <!-- </div> -->
       <div>
         <div class="inputWrap">
           Load preset:
@@ -51,10 +51,29 @@ invert = \\\((2 0) 1)
               Invert
             </option>
             <option
-              value="010100010001110011010000111001101000000001010100010101011000001100000001000000010001011010010101000000011100111101001000100000110110000000000001010101100111111101111100111111101111001111111011100111111101100001010100101001010101000000000001010101101111101111011101100000110000011000001100000110010101010000000000010101011011111011110111011000001000001000001000001001000001101100000000000010101011001011111111100100010100000110110000010010101011001010000000101101110110000000001111000000000011110111100100000110110000001010000000101101110110010000000000011110010101011111101111011101101011001000000000001110010101011111101111011101101010010000011011000000101000000010110111011001000000000001110010101011111101111011101101011001000000000001100101010111111011110111011010110010000011011000000101000000010110111011001000000000001100101010111111011110111011010110010000000000011110010101011111101111011101101011011111110010100000110110000000000001010101101111101111011100000101111100101111111110010001010000011011000001001010101100101000000010110111011000000000111100000000001111011110010000011011000000101000000010110111011001000000000001111001010101111110111101110110101100100000000000111001010101111110111101110110101001000001101100000010100000001011011101100100000000000111001010101111110111101110110101100100000000000110010101011111101111011101101011001000001101100000010100000001011011101100100000000000110010101011111101111011101101011001000000000001111001010101111110111101110110101101111111001010000011011000000000000101010110111110111100000101101111001011111111100100010100000110110000010010101011001010000000101101110110000000001111000000000011110111100100000110110000001010000000101101110110010000000000011110010101011111101111011101101011001000000000001110010101011111101111011101101010010000011011000000101000000010110111011001000000000001110010101011111101111011101101011001000000000001100101010111111011110111011010110010000011011000000101000000010110111011001000000000001100101010111111011110111011010110010000000000011110010101011111101111011101101011011111110010100000110110000000000001010101101111100000101110110111001011111111100100010100000110110000010010101011001010000000101101110110000000001111000000000011110111100100000110110000001010000000101101110110010000000000011110010101011111101111011101101011001000000000001110010101011111101111011101101010010000011011000000101000000010110111011001000000000001110010101011111101111011101101011001000000000001100101010111111011110111011010110010000011011000000101000000010110111011001000000000001100101010111111011110111011010110010000000000011110010101011111101111011101101011011111110010100000110110000000000001010101100000101111011101101101000000000011100111100111011110"
+              value="00010001010101000000000001010101101111101111011101100101000001101100000110100101000001101100000110010100000110110000010100101000001101100000110010100000110110000010010100000110110000010100101000001101100000110010100000110110000010010100000110110000010010100000110110000010100100010001010100010001110000101110110100001110000101110110100000000101100000000101000000010110111011001111110111001011111110111110110000010000110110100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101010001000111000010111011010000111000010111011010000000010110000000010111111100111111011101101101100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101110111010101001010000000101101110110000000000101010100000000000101010110111110111101110110111101110110000010010100000001011011101100000000001010101000000000001010101101111101111011101101111011100000101001010000000101101110110000000000101010100000000000101010110111110111101110110111100000101101001000101000000010110111011010000010000000000101010100000000000101010110111110111101110110000010111011010"
+            >
+              T-square v1
+            </option>
+            <option
+              value="00010001010101000000000001010101101111101111011101100101000001101100000110100101000001101100000110010100000110110000010100101000001101100000110010100000110110000010010100000110110000010100101000001101100000110010100000110110000010010100000110110000010010100000110110000010100100010001010100010001110000101110110100001110000101110110100000000101100000000101000000010110111011001111110111001011111110111110110000010000110110100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101010001000111000010111011010000111000010111011010000000010110000000010111111100111111011101101101100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101110111010101001010000000101101110110000000000101010100000000000101010110111110111101110110111101110110000010010100000001011011101100000000001010101000000000001010101101111101111011101101111011100000101001010000000101101110110000000000101010100000000000101010110111110111101110110111100000101101001000101000000010110111011010000010000000000101010100000000000101010110111110111101110110000010111011010"
+            >
+              T-square v2 (1/2) TODO
+            </option>
+            <option
+              value="00010001010101000000000001010101101111101111011101100101000001101100000110100101000001101100000110010100000110110000010100101000001101100000110010100000110110000010010100000110110000010100101000001101100000110010100000110110000010010100000110110000010010100000110110000010100100010001010100010001110000101110110100001110000101110110100000000101100000000101000000010110111011001111110111001011111110111110110000010000110110100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101010001000111000010111011010000111000010111011010000000010110000000010111111100111111011101101101100101010001000111000010111011010000111000010111011010000000010110000000010100000001011011101100111111011100101111111011111011000001000000101110111010101001010000000101101110110000000000101010100000000000101010110111110111101110110111101110110010101010000000000010101011011111011110111011000001000001100000110000010010100000001011011101100000000001010101000000000001010101101111101111011101101111011100101010100000000000101010110111110111101110110000011000001000001000001101001010000000101101110110000000000101010100000000000101010110111110111101110110111100101010100000000000101010110111110111101110110000011000001000001000001101101001000101000000010110111011010000010000000000101010100000000000101010110111110111101110110010101010000000000010101011011111011110111011000001000001100000110000010111011010"
+            >
+              Sierpinski carpet
+            </option>
+            <option
+              value="-- note how no white gets drawn since the highlighted parts would be infinitely detailed
+y = \(\(1 (0 0)) \(1 (0 0)))
+\(y \\((((0 1) \\0) 1) 1))"
             >
-              sierpinski-like
+              Sierpinski "triangle"
             </option>
+            <option value="">Cantor dust</option>
+            <option value="">Vicsek saltire</option>
           </select>
         </div>
         <span id="error"></span>
@@ -68,6 +87,7 @@ invert = \\\((2 0) 1)
       </div>
       <button id="render">Render!</button>
     </main>
-    <script src="script.js"></script>
+    <script src="common.js"></script>
+    <script src="main.js"></script>
   </body>
 </html>
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)")),
-  );
-});