From d0659464ed7376ecce04def6ae3bdbe7b737a729 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Mon, 8 Apr 2024 02:38:29 +0200
Subject: More assistance

---
 index.html | 44 +++++++++++++++++++++++++++++++++++++++++++-
 main.js    | 18 ++++++++++++------
 style.css  | 21 +++++++++++++++++++++
 3 files changed, 76 insertions(+), 7 deletions(-)

diff --git a/index.html b/index.html
index aa4e228..0393d8c 100644
--- a/index.html
+++ b/index.html
@@ -80,7 +80,30 @@ y = \(\(1 (0 0)) \(1 (0 0)))
             >
               Cantor dust
             </option>
-            <option value="">Vicsek saltire</option>
+            <option
+              value="-- some common definitions for copy-pasting
+w = \\1
+b = \\0
+isw = \0
+isb = \((0 b) w)
+invert = \\\((2 0) 1)
+build = \\\\\((((0 4) 3) 2) 1)
+empty = ((((build b) b) b) b)
+tl = \\\\3
+tr = \\\\2
+bl = \\\\1
+br = \\\\0
+get = \\(0 1)
+settl = \\(1 \\\\\((((0 5) 3) 2) 1))
+settr = \\(1 \\\\\((((0 4) 5) 2) 1))
+setbl = \\(1 \\\\\((((0 4) 3) 5) 1))
+setbr = \\(1 \\\\\((((0 4) 3) 2) 5))
+map = \\(0 \\\\\((((0 (6 4)) (6 3)) (6 2)) (6 1)))
+qsplit = \(0 \\\\\((((0 ((4 \((((0 \\1) \\1) \\1) \\1)) \((((0 \\0) \\0) \\0) \\0))) ((3 \((((0 \\1) \\1) \\1) \\1)) \((((0 \\0) \\0) \\0) \\0))) ((2 \((((0 \\1) \\1) \\1) \\1)) \((((0 \\0) \\0) \\0) \\0))) ((1 \((((0 \\1) \\1) \\1) \\1)) \((((0 \\0) \\0) \\0) \\0))))
+\0"
+            >
+              Template
+            </option>
           </select>
         </div>
         <span id="error"></span>
@@ -93,6 +116,25 @@ y = \(\(1 (0 0)) \(1 (0 0)))
         ></textarea>
       </div>
       <button id="render">Render!</button>
+      <footer>
+        <ul>
+          <li>
+            <a
+              href="https://text.marvinborner.de/2024-03-25-02.html"
+              target="_blank"
+              >Blog post</a
+            >
+          </li>
+          <li><a href="javascript:helpSyntax()">Syntax</a></li>
+          <li>
+            <a
+              href="https://github.com/marvinborner/lambda-screen"
+              target="_blank"
+              >Source-code</a
+            >
+          </li>
+        </ul>
+      </footer>
     </main>
     <script src="main.js"></script>
     <script charset="utf-8">
diff --git a/main.js b/main.js
index e583a7a..b0eed38 100644
--- a/main.js
+++ b/main.js
@@ -151,18 +151,19 @@ const parseLam = (str) => {
     case "λ":
     case "\\":
     case "[": // bruijn
-      const [body, _tail] = parseLam(tail);
-      return [abs(body), head == "[" ? _tail.slice(1) : _tail];
+      const [body, _tail] = parseLam(tail.trim());
+      return [abs(body), head == "[" ? _tail.trim().slice(1) : _tail.trim()];
     case "(":
       const [left, tail1] = parseLam(tail);
-      const [right, tail2] = parseLam(tail1.slice(1));
-      return [app(left)(right), tail2.slice(1)];
+      const [right, tail2] = parseLam(tail1.trim());
+      return [app(left)(right), tail2.trim().slice(1)];
     case ")":
     case "]":
       error("in parseLam");
       return [];
     default:
-      if (str[0] >= "a" && str[0] <= "z") {
+      if (head == " ") return parseLam(tail);
+      if (head >= "a" && head <= "z") {
         // substitution
         let name = "";
         while (str && str[0] >= "a" && str[0] <= "z") {
@@ -436,7 +437,6 @@ const snf = (_t) => {
   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);
@@ -512,3 +512,9 @@ const reduceLoop = (worker, root, _t) => {
     }
   }
 };
+
+function helpSyntax() {
+  alert(
+    "The syntax uses standard notations for de Bruijn indexed lambda calculus. The de Bruijn indices start at 0. You can use `\\`, `λ`, or `[..]` for abstractions. Applications use parenthesis and currently do *not* assume left associativity by default. All terms can also be replaced by a string of binary lambda calculus (BLC) - useful if you're not comfortable with de Bruijn indices (e.g. by using John Tromp's `lam` compiler).\nYou can define substitutions (like in the presets) using `=`.\n\nHave fun!",
+  );
+}
diff --git a/style.css b/style.css
index 752487e..30003d2 100644
--- a/style.css
+++ b/style.css
@@ -55,6 +55,27 @@ span#error {
     color: red;
 }
 
+footer {
+    position: fixed;
+    bottom: 0;
+    text-align: center;
+}
+
+footer a {
+    text-decoration: none;
+    color: black;
+}
+
+footer > ul {
+    list-style-type: none;
+    padding: 0;
+}
+
+footer > ul > li {
+    display: inline;
+    margin: 0 8px;
+}
+
 .inputWrap {
     display: block;
     margin: 0 auto;
-- 
cgit v1.2.3