Performance

5 files changed, 144 insertions, 42 deletions

diff --git a/bruijn/Screen.bruijn b/bruijn/Screen.bruijn
index f132c66..465df25 100644
--- a/bruijn/Screen.bruijn
+++ b/bruijn/Screen.bruijn
@@ -74,3 +74,7 @@ br! [[1 [[[[[0 4 3 2 5]]]]]]]
 map [&[[[[[0 (5 4) (5 3) (5 2) (5 1)]]]]]]
 
 :test (map invert empty) (build w w w w)
+
+qsplit map [w? 0 (build w w w w) (build b b b b)]
+
+:test (qsplit (build b w b w)) (build (build b b b b) (build w w w w) (build b b b b) (build w w w w))
diff --git a/index.html b/index.html
index 51c033e..d1997cb 100644
--- a/index.html
+++ b/index.html
@@ -25,12 +25,20 @@
           Load preset:
           <select id="examples">
             <option value="" selected>Empty</option>
-            <option value="\0">Identity</option>
             <option
-              value="tl = \\0
+              value="-- the final term gets applied with the empty screen
+\0"
+            >
+              Identity
+            </option>
+            <option
+              value="-- define substitutions of top-left, top-right, bottom-left, bottom-right black pixels
+tl = \\0
 tr = \\0
 bl = \\0
 br = \\0
+
+-- two abstractions to ignore the screen state and replace the entire screen
 \\((((0 tl) tr) bl) br)"
             >
               Just black
@@ -42,6 +50,11 @@ invert = \\\((2 0) 1)
             >
               Invert
             </option>
+            <option
+              value="010100010001110011010000111001101000000001010100010101011000001100000001000000010001011010010101000000011100111101001000100000110110000000000001010101100111111101111100111111101111001111111011100111111101100001010100101001010101000000000001010101101111101111011101100000110000011000001100000110010101010000000000010101011011111011110111011000001000001000001000001001000001101100000000000010101011001011111111100100010100000110110000010010101011001010000000101101110110000000001111000000000011110111100100000110110000001010000000101101110110010000000000011110010101011111101111011101101011001000000000001110010101011111101111011101101010010000011011000000101000000010110111011001000000000001110010101011111101111011101101011001000000000001100101010111111011110111011010110010000011011000000101000000010110111011001000000000001100101010111111011110111011010110010000000000011110010101011111101111011101101011011111110010100000110110000000000001010101101111101111011100000101111100101111111110010001010000011011000001001010101100101000000010110111011000000000111100000000001111011110010000011011000000101000000010110111011001000000000001111001010101111110111101110110101100100000000000111001010101111110111101110110101001000001101100000010100000001011011101100100000000000111001010101111110111101110110101100100000000000110010101011111101111011101101011001000001101100000010100000001011011101100100000000000110010101011111101111011101101011001000000000001111001010101111110111101110110101101111111001010000011011000000000000101010110111110111100000101101111001011111111100100010100000110110000010010101011001010000000101101110110000000001111000000000011110111100100000110110000001010000000101101110110010000000000011110010101011111101111011101101011001000000000001110010101011111101111011101101010010000011011000000101000000010110111011001000000000001110010101011111101111011101101011001000000000001100101010111111011110111011010110010000011011000000101000000010110111011001000000000001100101010111111011110111011010110010000000000011110010101011111101111011101101011011111110010100000110110000000000001010101101111100000101110110111001011111111100100010100000110110000010010101011001010000000101101110110000000001111000000000011110111100100000110110000001010000000101101110110010000000000011110010101011111101111011101101011001000000000001110010101011111101111011101101010010000011011000000101000000010110111011001000000000001110010101011111101111011101101011001000000000001100101010111111011110111011010110010000011011000000101000000010110111011001000000000001100101010111111011110111011010110010000000000011110010101011111101111011101101011011111110010100000110110000000000001010101100000101111011101101101000000000011100111100111011110"
+            >
+              sierpinski-like
+            </option>
           </select>
         </div>
         <span id="error"></span>
diff --git a/script.js b/script.js
index 9bab3c4..36fef75 100644
--- a/script.js
+++ b/script.js
@@ -16,40 +16,47 @@ const BLACK = 1;
 const UNKNOWN = 2;
 
 const canvas = window.canvas;
-const screen = canvas.getContext("2d");
 
 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) => {
-  screen.fillStyle =
-    color == WHITE ? "white" : color == BLACK ? "black" : "grey";
-  screen.fillRect(x[0], y[0], x[1], y[1]);
+  worker.postMessage([
+    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[1] / 2];
-  const newY = [ctx.y[0], ctx.y[1] / 2];
+  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[1] / 2, ctx.x[1]];
-  const newY = [ctx.y[0], ctx.y[1] / 2];
+  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[1] / 2];
-  const newY = [ctx.y[1] / 2, ctx.y[1]];
+  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[1] / 2, ctx.x[1]];
-  const newY = [ctx.y[1] / 2, ctx.y[1]];
+  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 };
 };
@@ -60,23 +67,44 @@ 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) h += 1;
+  allHashes[h] = s;
+  return h;
+};
+
 const abs = (body) => {
   if (body === null) return null;
-  return { type: "abs", body };
+  const t = { type: "abs", body };
+  t.hash = hash("abs" + body.hash);
+  return t;
 };
 
 const app = (left) => (right) => {
   if (left === null || right === null) return null;
-  return { type: "app", left, right };
+  const t = { type: "app", left, right };
+  t.hash = hash("app" + left.hash + right.hash);
+  return t;
 };
 
 const idx = (idx) => {
   if (idx === null) return null;
-  return { type: "idx", idx };
+  const t = { type: "idx", idx };
+  t.hash = hash("idx" + idx);
+  return t;
 };
 
 const def = (name) => {
-  return { type: "def", name };
+  const t = { type: "def", name };
+  t.hash = hash("def" + name);
+  return t;
 };
 
 const show = (t) => {
@@ -121,11 +149,9 @@ const parseLam = (str) => {
   switch (head) {
     case "λ":
     case "\\":
-      const [body, _tail] = parseLam(tail);
-      return [abs(body), _tail];
     case "[": // bruijn
-      const [bbody, _btail] = parseLam(tail);
-      return [abs(bbody), _btail.slice(1)];
+      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));
@@ -217,6 +243,7 @@ const parse = (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;
@@ -252,7 +279,7 @@ const seemsScreeny = (t) =>
   t.body.left.left.left.left.idx === 0;
 
 const clearScreen = () => {
-  screen.clearRect(0, 0, canvas.width, canvas.height);
+  worker.postMessage("clear");
 };
 
 /* beta reduction */
@@ -275,40 +302,65 @@ const cancelReduction = () => {
   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":
-      return idx(i <= t.idx ? t.idx + 1 : t.idx);
+      newT = idx(i <= t.idx ? t.idx + 1 : t.idx);
+      break;
     case "app":
-      return app(inc(i, t.left))(inc(i, t.right));
+      newT = app(inc(i, t.left))(inc(i, t.right));
+      break;
     case "abs":
-      return abs(inc(i + 1, t.body));
+      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":
-      return i == t.idx ? s : idx(t.idx > i ? t.idx - 1 : t.idx);
+      newT = i == t.idx ? s : idx(t.idx > i ? t.idx - 1 : t.idx);
+      break;
     case "app":
-      return app(subst(i, t.left, s))(subst(i, t.right, s));
+      newT = app(subst(i, t.left, s))(subst(i, t.right, s));
+      break;
     case "abs":
-      return abs(subst(i + 1, t.body, inc(0, s)));
+      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
@@ -336,42 +388,53 @@ const gnf = (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;
-      return _left.type === "abs"
-        ? whnf(subst(0, _left.body, t.right))
-        : app(_left)(t.right);
+      newT =
+        _left.type === "abs"
+          ? whnf(subst(0, _left.body, t.right))
+          : app(_left)(t.right);
+      break;
     case "def":
       error("unexpected def");
       return null;
     default:
-      return t;
+      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)) {
-    if (cancelReduction()) {
-      error("in snf");
-      return null;
-    }
     // TODO: a bit unsure about this
     switch (t.type) {
       case "app":
@@ -392,18 +455,25 @@ const snf = (_t) => {
         return null;
     }
   }
+
+  snfCache[_t.hash] = t;
   return t;
 };
 
 const reduce = (_t) => {
-  console.log(show(_t));
   const stack = [{ ctx: root, t: _t }];
-  for (let i = 0; stack.length > 0 && i < 1024; i++) {
-    let { ctx, t } = stack.pop();
+  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 = 16384;
+    MAX = 10000000;
     depth = 0;
     canceled = false;
     try {
@@ -427,6 +497,7 @@ const reduce = (_t) => {
       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));
     }
   }
diff --git a/style.css b/style.css
index ee80e76..5c6db87 100644
--- a/style.css
+++ b/style.css
@@ -34,7 +34,7 @@ input#slider {
 
 textarea#term {
     width: 100%;
-    font-size: 2em;
+    font-size: 1.3em;
 }
 
 button#render {
diff --git a/worker.js b/worker.js
new file mode 100644
index 0000000..f89a699
--- /dev/null
+++ b/worker.js
@@ -0,0 +1,14 @@
+let canvas, screen;
+
+self.onmessage = (msg) => {
+  if (msg.data == "clear") {
+    screen.clearRect(0, 0, canvas.width, canvas.height);
+  } else if ("canvas" in msg.data) {
+    canvas = msg.data.canvas;
+    screen = canvas.getContext("2d");
+  } else {
+    [color, x, y, width, height] = msg.data;
+    screen.fillStyle = color;
+    screen.fillRect(x, y, width, height);
+  }
+};