Experiment with tracking of parents

1 files changed, 54 insertions, 43 deletions

diff --git a/main.js b/main.js
index 445c05c..554c98e 100644
--- a/main.js
+++ b/main.js
@@ -90,27 +90,30 @@ const hash = (s) => {
 
 const abs = (body) => {
   if (body === null) return null;
-  const t = { type: "abs", body };
+  const t = { type: "abs", parents: [], body };
   t.hash = hash("abs" + body.hash);
+  body.parents.push(t);
   return t;
 };
 
 const app = (left) => (right) => {
   if (left === null || right === null) return null;
-  const t = { type: "app", left, right };
+  const t = { type: "app", parents: [], left, right };
   t.hash = hash("app" + left.hash + right.hash);
+  left.parents.push(t);
+  right.parents.push(t);
   return t;
 };
 
 const idx = (idx) => {
   if (idx === null) return null;
-  const t = { type: "idx", idx };
+  const t = { type: "idx", parents: [], idx };
   t.hash = hash("idx" + idx);
   return t;
 };
 
 const def = (name) => {
-  const t = { type: "def", name };
+  const t = { type: "def", parents: [], name };
   t.hash = hash("def" + name);
   return t;
 };
@@ -501,6 +504,8 @@ const whnf = (t) => {
 
 // screen normal form
 // one of [((((0 tl) tr) bl) br)], [[0]], [[1]]
+// TODO: Is this form of caching fundamentally wrong? (incongruences after subst or idx shifts!?)
+//       Does this only work accidentally because of WHNF, deliberate symmetry and closed terms or sth?
 const snfCache = {};
 const snf = (_t) => {
   if (_t !== null && _t.hash in snfCache) return snfCache[_t.hash];
@@ -535,7 +540,25 @@ const snf = (_t) => {
     }
   }
 
-  if (t !== null) snfCache[_t.hash] = t;
+  if (t === null) return null;
+
+  snfCache[_t.hash] = t;
+  const parents = [...t.parents];
+  while (parents.length !== 0) {
+    const parent = parents.pop();
+    switch (parent.type) {
+      case "app":
+        if (parent.left.hash == t) {
+        }
+      case "abs":
+        break;
+      default:
+        error("unexpected parent " + parent.type);
+        return null;
+    }
+    snfCache[parent.hash];
+  }
+
   return t;
 };
 
@@ -577,44 +600,32 @@ const reduceLoop = (worker, root, _t) => {
     // smaller resolutions apparently crash the browser tab lol
     if (ctx.x[1] - ctx.x[0] < MAXRES) continue;
 
-    const commitScreen = (__t, __ctx) => {
-      const commitStack = [{ t: __t, ctx: __ctx }];
-      while (commitStack.length !== 0) {
-        const p = commitStack.shift();
-        const _t = p.t;
-        const _ctx = p.ctx;
-        if (seemsScreeny(_t)) {
-          const tl = _t.body.left.left.left.right;
-          const tlCtx = ctxTopLeft(_ctx);
-          if (tl.hash in snfCache)
-            commitStack.push({ ctx: tlCtx, t: snfCache[tl.hash] });
-          else stack.push({ ctx: tlCtx, t: tl });
-
-          const tr = _t.body.left.left.right;
-          const trCtx = ctxTopRight(_ctx);
-          stack.push({ ctx: trCtx, t: tr });
-
-          const bl = _t.body.left.right;
-          const blCtx = ctxBottomLeft(_ctx);
-          stack.push({ ctx: blCtx, t: bl });
-
-          const br = _t.body.right;
-          const brCtx = ctxBottomRight(_ctx);
-          stack.push({ ctx: brCtx, t: br });
-
-          drawScreen(
-            worker,
-            [tlCtx, trCtx, blCtx, brCtx],
-            [toColor(tl), toColor(tr), toColor(bl), toColor(br)],
-          );
-        } else {
-          // TODO: could we risk gnfing here?
-          drawAt(worker, _ctx.x, _ctx.y, toColor(_t));
-        }
-      }
-    };
-
-    commitScreen(t, ctx);
+    if (seemsScreeny(t)) {
+      const tl = t.body.left.left.left.right;
+      const tlCtx = ctxTopLeft(ctx);
+      stack.push({ ctx: tlCtx, t: tl });
+
+      const tr = t.body.left.left.right;
+      const trCtx = ctxTopRight(ctx);
+      stack.push({ ctx: trCtx, t: tr });
+
+      const bl = t.body.left.right;
+      const blCtx = ctxBottomLeft(ctx);
+      stack.push({ ctx: blCtx, t: bl });
+
+      const br = t.body.right;
+      const brCtx = ctxBottomRight(ctx);
+      stack.push({ ctx: brCtx, t: br });
+
+      drawScreen(
+        worker,
+        [tlCtx, trCtx, blCtx, brCtx],
+        [toColor(tl), toColor(tr), toColor(bl), toColor(br)],
+      );
+    } else {
+      // TODO: could we risk gnfing here?
+      drawAt(worker, ctx.x, ctx.y, toColor(t));
+    }
   }
 
   console.log(foo);