From 1d0367d63505efa32d804bd686bbf3ee6a4b017b Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Tue, 5 Mar 2024 00:22:06 +0100
Subject: Surprisingly fun!
---
feather-sprite.svg | 1 +
index.html | 43 ++++++++
readme.md | 3 +
script.js | 304 +++++++++++++++++++++++++++++++++++++++++++++++++++++
style.css | 167 +++++++++++++++++++++++++++++
5 files changed, 518 insertions(+)
create mode 100644 feather-sprite.svg
create mode 100644 index.html
create mode 100644 readme.md
create mode 100644 script.js
create mode 100644 style.css
diff --git a/feather-sprite.svg b/feather-sprite.svg
new file mode 100644
index 0000000..e39bbc9
--- /dev/null
+++ b/feather-sprite.svg
@@ -0,0 +1 @@
+Infinite Apply
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/readme.md b/readme.md
new file mode 100644
index 0000000..7e5ced8
--- /dev/null
+++ b/readme.md
@@ -0,0 +1,3 @@
+# Infinite Apply
+
+> Infinite Craft but for lambda calculus
diff --git a/script.js b/script.js
new file mode 100644
index 0000000..6e412b6
--- /dev/null
+++ b/script.js
@@ -0,0 +1,304 @@
+let fresh = 0; // every term has an id
+
+const sidebar = document.querySelector(".sidebar");
+
+/* lambda calculus */
+
+const abs = (body) => {
+ if (body === null) return null;
+ return { type: "abs", body };
+};
+const app = (left, right) => {
+ if (left === null || right === null) return null; // something something monad
+ return { type: "app", left, right };
+};
+const idx = (idx) => {
+ if (idx === null) return null;
+ return { type: "idx", idx };
+};
+
+let MAX = 0;
+let depth = 0;
+let canceled = false;
+const cancelReduction = () => {
+ if (depth > MAX && !canceled) {
+ MAX *= 4;
+ if (
+ !confirm(
+ `This takes awfully long (${depth} steps!). The reduction potentially won't converge. Do you want to continue?\nWarning: This might crash your browser!`,
+ )
+ ) {
+ canceled = true;
+ return true;
+ }
+ }
+ return canceled;
+};
+
+const inc = (i, t) => {
+ if (cancelReduction()) return null;
+ if (t === null) return null;
+ depth++;
+ switch (t.type) {
+ case "idx":
+ return idx(i <= t.idx ? t.idx + 1 : t.idx);
+ case "app":
+ return app(inc(i, t.left), inc(i, t.right));
+ case "abs":
+ return abs(inc(i + 1, t.body));
+ }
+};
+
+const subst = (i, t, s) => {
+ if (cancelReduction()) return null;
+ if (t === null || s === null) return null;
+ depth++;
+ switch (t.type) {
+ case "idx":
+ return i == t.idx ? s : idx(t.idx > i ? t.idx - 1 : t.idx);
+ case "app":
+ return app(subst(i, t.left, s), subst(i, t.right, s));
+ case "abs":
+ return abs(subst(i + 1, t.body, inc(0, s)));
+ }
+};
+
+const gnf = (t) => {
+ if (cancelReduction()) return null;
+ if (t === null) return null;
+ depth++;
+ 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));
+ default:
+ return t;
+ }
+};
+
+const reduce = (t) => {
+ MAX = 16384;
+ depth = 0;
+ canceled = false;
+ try {
+ return gnf(t);
+ } catch (e) {
+ alert(e);
+ return null;
+ }
+};
+
+const show = (term) => {
+ switch (term.type) {
+ case "abs":
+ return `λ${show(term.body)}`;
+ case "app":
+ return `(${show(term.left)} ${show(term.right)})`;
+ case "idx":
+ return `${term.idx}`;
+ }
+};
+
+const parse = (str) => {
+ if (!str) return [{}, ""];
+ const head = str[0];
+ const tail = str.slice(1);
+ switch (head) {
+ case "λ":
+ const [body, _tail] = parse(tail);
+ return [abs(body), _tail];
+ case "(":
+ const [left, tail1] = parse(tail);
+ const [right, tail2] = parse(tail1.slice(1));
+ return [app(left, right), tail2.slice(1)];
+ case ")":
+ alert("fatal");
+ return [];
+ default:
+ let num = "";
+ while (str && str[0] >= "0" && str[0] <= "9") {
+ num += str[0];
+ str = str.slice(1);
+ }
+ return [idx(parseInt(num)), str];
+ }
+};
+
+/* box dragging */
+
+const toBox = (name, term) => {
+ return `${name}
`;
+};
+
+let offset = { x: 0, y: 0 };
+const main = document.querySelector(".main");
+
+const addDrag = (box) => {
+ box.addEventListener("dragstart", (e) => {
+ const from = box.parentElement.classList[0];
+ e.dataTransfer.setData("text/plain", box.getAttribute("data-id"));
+ offset.x = e.clientX - box.getBoundingClientRect().left;
+ offset.y = e.clientY - box.getBoundingClientRect().top;
+ });
+ box.addEventListener("click", () => {
+ box.toggleAttribute("clicked");
+ });
+ box.addEventListener("contextmenu", (e) => {
+ e.preventDefault();
+ const name = prompt("Name this term:", box.getAttribute("data-term"));
+ if (!name) return;
+ const term = box.getAttribute("data-term");
+ document.querySelectorAll(".box").forEach((box) => {
+ if (box.getAttribute("data-term") == term) box.innerText = name;
+ });
+ delete inventory[term];
+ discover(name, parse(term)[0]);
+ });
+};
+
+const merge = (box) => {
+ main.querySelectorAll(".box").forEach((other) => {
+ if (box === other) return;
+ const boxRect = box.getBoundingClientRect();
+ const otherRect = other.getBoundingClientRect();
+ if (
+ boxRect.left < otherRect.right &&
+ boxRect.right > otherRect.left &&
+ boxRect.top < otherRect.bottom &&
+ boxRect.bottom > otherRect.top
+ ) {
+ const term1 = box.getAttribute("data-term");
+ const term2 = other.getAttribute("data-term");
+ box.remove();
+ const nf = reduce(parse(`(${term2} ${term1})`)[0], 0);
+ if (nf) {
+ const str = show(nf);
+ const name = str in inventory ? inventory[str] : str;
+ other.setAttribute("data-term", str);
+ other.innerText = name;
+ if (discover(name, nf)) other.classList.add("discovered");
+ }
+ }
+ });
+};
+
+main.addEventListener("dragover", (e) => {
+ e.preventDefault();
+ e.dataTransfer.dropEffect = "move";
+});
+
+main.addEventListener("drop", (e) => {
+ e.preventDefault();
+ const id = e.dataTransfer.getData("text/plain");
+ const from = document.querySelector(`[data-id="${id}"]`);
+ const box = document.createElement("div");
+ box.classList.add("box");
+ box.setAttribute("data-id", fresh++);
+ box.setAttribute("draggable", "true");
+ box.setAttribute("data-term", from.getAttribute("data-term"));
+ box.innerText = from.innerText;
+ addDrag(box);
+
+ if (from.parentElement.classList[0] === "main") from.remove();
+
+ const x = e.clientX - offset.x;
+ const y = e.clientY - offset.y;
+ box.style.left = `${x}px`;
+ box.style.top = `${y}px`;
+ box.style.position = "absolute";
+ main.appendChild(box);
+ merge(box);
+});
+
+/* inventory */
+
+const inventory = {};
+const discover = (name, term) => {
+ const str = show(term);
+ if (str in inventory) return false;
+ inventory[str] = name;
+ sidebar.querySelector(".inventory").innerHTML = Object.keys(inventory)
+ .map((term) => toBox(inventory[term], term))
+ .join("");
+ sidebar.querySelectorAll(".inventory .box").forEach(addDrag);
+ localStorage.setItem("inventory", JSON.stringify(inventory));
+ return true;
+};
+
+const load = () => {
+ const inv = JSON.parse(localStorage.getItem("inventory"));
+ if (inv) {
+ Object.keys(inv).forEach((name) => {
+ discover(inv[name], parse(name)[0]);
+ });
+ }
+};
+
+load();
+
+const s = abs(abs(abs(app(app(idx(2), idx(0)), app(idx(1), idx(0))))));
+const k = abs(abs(idx(1)));
+discover("s", s);
+discover("k", k);
+
+/* search */
+
+sidebar.querySelector("input").addEventListener("keyup", (e) => {
+ const query = e.target.value;
+ const queryLambda = query.replaceAll("\\", "λ");
+ sidebar.querySelectorAll(".inventory .box").forEach((box) => {
+ if (
+ query == "" ||
+ box.getAttribute("data-term").includes(query) ||
+ box.innerText.includes(queryLambda)
+ ) {
+ box.style.display = "block";
+ } else {
+ box.style.display = "none";
+ }
+ });
+});
+
+/* popups */
+
+const popup = document.querySelector(".popup");
+
+const message = (str) => {
+ window.popupText.innerHTML = str;
+ window.popupClose.style.display = "block";
+ popup.classList.add("active");
+};
+
+/* buttons */
+
+window.clean.addEventListener("click", () => {
+ document
+ .querySelector(".main")
+ .querySelectorAll(".box")
+ .forEach((box) => {
+ box.remove();
+ });
+});
+
+window.popupClose.addEventListener("click", () => {
+ popup.classList.remove("active");
+});
+
+window.help.addEventListener("click", () => {
+ message(
+ "Every box on the side panel is a term of pure lambda calculus with de Bruijn indices . By dragging boxes into the left canvas you can apply them on each other. Two colliding boxes beta-reduce and form a new term. The dropped term is always on the right side of the application.bruijn .