More configuration

3 files changed, 60 insertions, 27 deletions

diff --git a/index.html b/index.html
index 8587e99..63e6c0a 100644
--- a/index.html
+++ b/index.html
@@ -266,17 +266,36 @@ map = \\(0 \\\\\(0 (6 4) (6 3) (6 2) (6 1)))
       <details>
         <summary>Configuration</summary>
         <fieldset>
-          <label for="resolutionConfig">Resolution: </label>
-          <input
-            type="range"
-            min="100"
-            max="10000"
-            step="10"
-            name="resolutionConfig"
-            id="resolutionConfig"
-            value="1000"
-          />
-          <em id="resolutionConfigLabel" style="font-style: normal">1000</em>
+          <div>
+            <label for="resolutionConfig">Resolution: </label>
+            <input
+              type="range"
+              min="100"
+              max="10000"
+              step="10"
+              name="resolutionConfig"
+              id="resolutionConfig"
+              value="1000"
+            />
+            <em id="resolutionConfigLabel" style="font-style: normal">1000</em>
+          </div>
+          <div>
+            <label for="schedulerConfig">Scheduler: </label>
+            <select type="range" name="schedulerConfig" id="schedulerConfig">
+              <option value="fifo">FIFO/BFS/queue</option>
+              <option value="lifo">LIFO/DFS/stack</option>
+              <option value="random">random</option>
+            </select>
+          </div>
+          <div>
+            <label for="cachingConfig">Caching: </label>
+            <input
+              type="checkbox"
+              name="cachingConfig"
+              id="cachingConfig"
+              checked="checked"
+            />
+          </div>
         </fieldset>
         <b>Warning:</b> Larger resolutions will often need exponentially more
         memory/computation!
@@ -338,13 +357,25 @@ map = \\(0 \\\\\(0 (6 4) (6 3) (6 2) (6 1)))
         window.render.disabled = true;
         window.render.textContent = "Rendering...";
 
+        // TODO: priority queue on context size
+        let scheduler =
+          window.schedulerConfig.value == "lifo"
+            ? (stack) => stack.pop()
+            : window.schedulerConfig.value == "fifo"
+              ? (stack) => stack.shift()
+              : (stack) =>
+                  stack.splice(Math.floor(Math.random() * stack.length), 1)[0];
+        const caching = window.cachingConfig.checked;
+        const logger = (str) => {
+          window.debugInfo.innerHTML += str;
+        };
+
         // button doesn't update text without timeout
         setTimeout(() => {
           let cnt;
           try {
             cnt = reduceLoop(
-              worker,
-              root,
+              { worker, root, logger, scheduler, caching },
               app(t)(parse("\\((((0 \\\\1) \\\\1) \\\\1) \\\\1)")),
             );
           } catch (e) {
diff --git a/main.js b/main.js
index dc717e7..a69cb57 100644
--- a/main.js
+++ b/main.js
@@ -1,4 +1,5 @@
 let MAXRES = 2;
+let doCache = true;
 
 let errors = [];
 const error = (s) => {
@@ -390,7 +391,7 @@ const inc = (i, t) => {
   }
 
   const h = hash("" + i + t.hash);
-  if (h in incCache) return incCache[h];
+  if (doCache && h in incCache) return incCache[h];
 
   let newT;
   switch (t.type) {
@@ -420,7 +421,7 @@ const subst = (i, t, s) => {
   }
 
   const h = hash("" + i + t.hash + s.hash);
-  if (h in substCache) return substCache[h];
+  if (doCache && h in substCache) return substCache[h];
 
   let newT;
   switch (t.type) {
@@ -475,7 +476,7 @@ const whnf = (t) => {
     return null;
   }
 
-  if (t.hash in whnfCache) return whnfCache[t.hash];
+  if (doCache && t.hash in whnfCache) return whnfCache[t.hash];
 
   let newT;
   switch (t.type) {
@@ -505,7 +506,7 @@ const whnf = (t) => {
 //       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];
+  if (doCache && _t !== null && _t.hash in snfCache) return snfCache[_t.hash];
 
   let t = whnf(_t);
   if (t === null || t.type !== "abs") {
@@ -541,19 +542,15 @@ const snf = (_t) => {
   return t;
 };
 
-const reduceLoop = (worker, root, _t) => {
+const reduceLoop = (conf, _t) => {
+  const { worker, root, logger, scheduler, caching } = conf;
   let cnt = 0;
-  window.debugInfo.innerHTML += `Term size: ${size(_t)} bit (BLC)<br>`;
+  logger(`Term size: ${size(_t)} bit (BLC)<br>`);
   const stack = [{ ctx: root, t: _t }];
+  doCache = caching;
   for (cnt = 0; stack.length > 0 && !canceled; cnt++) {
-    // 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
+    let { ctx, t } = scheduler(stack);
+
     if (toColor(t) !== UNKNOWN) continue;
 
     // could loop in gnf, therefore limit depth
diff --git a/style.css b/style.css
index bf0295e..1cba329 100644
--- a/style.css
+++ b/style.css
@@ -57,6 +57,11 @@ span#error {
 
 fieldset {
 	display: flex;
+	flex-flow: column;
+}
+
+fieldset div {
+	display: flex;
 	align-items: center;
 	flex-wrap: wrap;
 }