From d8e03512adc57607c72caf2a6028077209868dbd Mon Sep 17 00:00:00 2001
From: cannorin <cannorin@users.noreply.github.com>
Date: Sat, 22 Feb 2025 10:53:58 +0900
Subject: [PATCH] kripke: support word syntax

---
 .../src/routes/kripke/components/rules.svelte | 41 +++++++++++----
 packages/kripke/parser.ts                     | 51 ++++++++++++-------
 packages/kripke/semantics.ts                  |  2 +-
 packages/kripke/syntax.ts                     | 20 ++++----
 4 files changed, 75 insertions(+), 39 deletions(-)

diff --git a/apps/web/src/routes/kripke/components/rules.svelte b/apps/web/src/routes/kripke/components/rules.svelte
index 75580f8..c3787e8 100644
--- a/apps/web/src/routes/kripke/components/rules.svelte
+++ b/apps/web/src/routes/kripke/components/rules.svelte
@@ -1,5 +1,18 @@
 <script lang="ts">
 import Katex from "$lib/components/katex.svelte";
+import {
+  andSymbols,
+  botSymbols,
+  boxSymbols,
+  diamondSymbols,
+  eqSymbols,
+  lParenSymbols,
+  notSymbols,
+  orSymbols,
+  rParenSymbols,
+  toSymbols,
+  topSymbols,
+} from "@cannorin/kripke";
 import LuHeart from "lucide-svelte/icons/heart";
 
 let { relationSize }: { relationSize: number } = $props();
@@ -41,18 +54,24 @@ const validCount =
   </li>
 </ul>
 
+{#snippet symbols(words: string[])}
+  {#each words as word, i}
+    {i > 0 ? ", " : ""}<code>{word}</code>
+  {/each}
+{/snippet}
+
 <h2>Syntax</h2>
 <p>You may use the following symbols:</p>
 <ul>
-  <li>propositional variables: <code>p</code>, <code>q</code>, <code>r</code>, <code>s</code></li>
-  <li>verum: <code>⊤</code>, <code>T</code>, <code>1</code>, <code>\top</code></li>
-  <li>falsum: <code>⊥</code>, <code>F</code>, <code>0</code>, <code>\bot</code></li>
-  <li>negation: <code>¬</code>, <code>~</code>, <code>\neg</code>, <code>\lnot</code></li>
-  <li>box modality: <code>□</code>, <code>[]</code>, <code>!</code>, <code>L</code>, <code>\Box</code></li>
-  <li>diamond modality: <code>⋄</code>, <code>&lt;&gt;</code>, <code>?</code>, <code>M</code>, <code>\Diamond</code></li>
-  <li>conjunction: <code>∧</code>, <code>^</code>, <code>&amp;</code>,  <code>\wedge</code>, <code>\land</code></li>
-  <li>disjunction: <code>∨</code>, <code>v</code>, <code>|</code>, <code>\vee</code>, <code>\lor</code></li>
-  <li>implication: <code>→</code>, <code>-&gt;</code>, <code>&gt;</code>, <code>\rightarrow</code>, <code>\to</code></li>
-  <li>equivalence: <code>↔</code>,  <code>&lt;-&gt;</code>, <code>=</code>, <code>\leftrightarrow</code>, <code>\equiv</code></li>
-  <li>parentheses: <code>(</code>, <code>)</code></li>
+  <li>propositional variables: {@render symbols(["p", "q", "r", "s"])}</li>
+  <li>verum: {@render symbols(topSymbols)}</li>
+  <li>falsum: {@render symbols(botSymbols)}</li>
+  <li>negation: {@render symbols(notSymbols)}</li>
+  <li>box: {@render symbols(boxSymbols)}</li>
+  <li>diamond: {@render symbols(diamondSymbols)}</li>
+  <li>conjunction: {@render symbols(andSymbols)}</li>
+  <li>disjunction: {@render symbols(orSymbols)}</li>
+  <li>implication: {@render symbols(toSymbols)}</li>
+  <li>equivalence: {@render symbols(eqSymbols)}</li>
+  <li>parentheses: {@render symbols([...lParenSymbols, ...rParenSymbols])}</li>
 </ul>
diff --git a/packages/kripke/parser.ts b/packages/kripke/parser.ts
index 7ff737e..5ce8121 100644
--- a/packages/kripke/parser.ts
+++ b/packages/kripke/parser.ts
@@ -17,7 +17,7 @@ import {
   bot,
   box,
   diamond,
-  iff,
+  eq,
   not,
   or,
   propVars,
@@ -36,25 +36,42 @@ enum TokenKind {
   And = 6,
   Or = 7,
   To = 8,
-  Iff = 9,
+  Eq = 9,
   LParen = 10,
   RParen = 11,
   Space = 12,
 }
 
+const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, "\\$&");
+
+const generateAlt = (words: string[]) =>
+  new RegExp(`^(${words.map((s) => escapeRegExp(s)).join("|")})`, "g");
+
+export const topSymbols = ["⊤", "T", "1", "\\top", "top"];
+export const botSymbols = ["⊥", "F", "0", "\\bot", "bot"];
+export const notSymbols = ["¬", "~", "\\neg", "\\lnot", "not"];
+export const boxSymbols = ["□", "[]", "!", "L", "\\Box", "box"];
+export const diamondSymbols = ["⋄", "<>", "?", "M", "\\Diamond", "dia"];
+export const andSymbols = ["∧", "^", "&", "\\wedge", "\\land", "and"];
+export const orSymbols = ["∨", "v", "|", "\\vee", "\\lor", "or"];
+export const toSymbols = ["→", "->", ">", "\\rightarrow", "\\to", "to"];
+export const eqSymbols = ["↔", "<->", "=", "\\leftrightarrow", "\\equiv", "eq"];
+export const lParenSymbols = ["(", "\\left"];
+export const rParenSymbols = [")", "\\right"];
+
 const lexer = buildLexer([
   [true, /^[pqrs]/g, TokenKind.PropVar],
-  [true, /^(T|⊤|1|\\top)/g, TokenKind.Top],
-  [true, /^(F|⊥|0|\\bot)/g, TokenKind.Bot],
-  [true, /^(~|¬|\\neg|\\lnot)/g, TokenKind.Not],
-  [true, /^(\[\]|□|!|L|\\Box)/g, TokenKind.Box],
-  [true, /^(<>|⋄|\?|M|\\Diamond)/g, TokenKind.Diamond],
-  [true, /^(&|\^|∧|\\wedge|\\land)/g, TokenKind.And],
-  [true, /^(\||v|∨|\\vee|\\lor)/g, TokenKind.Or],
-  [true, /^(>|->|→|\\rightarrow|\\to)/g, TokenKind.To],
-  [true, /^(=|<->|↔|\\leftrightarrow|\\equiv)/g, TokenKind.Iff],
-  [true, /^(\(|\\left\()/g, TokenKind.LParen],
-  [true, /^(\)|\\right\))/g, TokenKind.RParen],
+  [true, generateAlt(topSymbols), TokenKind.Top],
+  [true, generateAlt(botSymbols), TokenKind.Bot],
+  [true, generateAlt(notSymbols), TokenKind.Not],
+  [true, generateAlt(boxSymbols), TokenKind.Box],
+  [true, generateAlt(diamondSymbols), TokenKind.Diamond],
+  [true, generateAlt(andSymbols), TokenKind.And],
+  [true, generateAlt(orSymbols), TokenKind.Or],
+  [true, generateAlt(toSymbols), TokenKind.To],
+  [true, generateAlt(eqSymbols), TokenKind.Eq],
+  [true, generateAlt(lParenSymbols), TokenKind.LParen],
+  [true, generateAlt(rParenSymbols), TokenKind.RParen],
   [false, /^\s+/g, TokenKind.Space],
 ]);
 
@@ -96,7 +113,7 @@ function unary([op, value]: [
 function binary(
   left: Formula,
   [op, right]: [
-    Token<TokenKind.And | TokenKind.Or | TokenKind.To | TokenKind.Iff>,
+    Token<TokenKind.And | TokenKind.Or | TokenKind.To | TokenKind.Eq>,
     Formula,
   ],
 ): Formula {
@@ -107,8 +124,8 @@ function binary(
       return or(left, right);
     case TokenKind.To:
       return to(left, right);
-    case TokenKind.Iff:
-      return iff(left, right);
+    case TokenKind.Eq:
+      return eq(left, right);
     default:
       throw new Error(`Unknown binary operator: ${op.text}`);
   }
@@ -140,7 +157,7 @@ ANDOR.setPattern(
 );
 
 EXP.setPattern(
-  lrec_sc(ANDOR, seq(alt(tok(TokenKind.To), tok(TokenKind.Iff)), EXP), binary),
+  lrec_sc(ANDOR, seq(alt(tok(TokenKind.To), tok(TokenKind.Eq)), EXP), binary),
 );
 
 export function parse(expr: string): Formula {
diff --git a/packages/kripke/semantics.ts b/packages/kripke/semantics.ts
index db24b72..f49699d 100644
--- a/packages/kripke/semantics.ts
+++ b/packages/kripke/semantics.ts
@@ -64,7 +64,7 @@ export function satisfy(m: Model, w: World, fml: Formula): boolean {
       if (!satisfy(m, w, fml.left)) return false;
       return satisfy(m, w, fml.right);
     }
-    case "iff": {
+    case "eq": {
       return satisfy(m, w, fml.left) === satisfy(m, w, fml.right);
     }
   }
diff --git a/packages/kripke/syntax.ts b/packages/kripke/syntax.ts
index 787d2ec..eb77cd9 100644
--- a/packages/kripke/syntax.ts
+++ b/packages/kripke/syntax.ts
@@ -7,7 +7,7 @@ export type Formula =
   | { type: "propvar"; name: PropVar }
   | { type: "not" | "box" | "diamond"; fml: Formula }
   | {
-      type: "to" | "or" | "and" | "iff";
+      type: "to" | "or" | "and" | "eq";
       left: Formula;
       right: Formula;
     };
@@ -24,7 +24,7 @@ export function vars(fml: Formula): Set<PropVar> {
     case "to":
     case "or":
     case "and":
-    case "iff":
+    case "eq":
       return new Set([...vars(fml.left), ...vars(fml.right)]);
     case "propvar":
       return new Set([fml.name]);
@@ -49,8 +49,8 @@ export const and = (left: Formula, right: Formula) =>
   ({ type: "and", left, right }) as const satisfies Formula;
 export const or = (left: Formula, right: Formula) =>
   ({ type: "or", left, right }) as const satisfies Formula;
-export const iff = (left: Formula, right: Formula) =>
-  ({ type: "iff", left, right }) as const satisfies Formula;
+export const eq = (left: Formula, right: Formula) =>
+  ({ type: "eq", left, right }) as const satisfies Formula;
 
 export type Symbols = Record<Exclude<Formula["type"], "propvar">, string>;
 
@@ -63,7 +63,7 @@ export const asciiSymbols: Symbols = {
   and: "^",
   or: "v",
   to: "->",
-  iff: "<->",
+  eq: "<->",
 };
 
 export const unicodeSymbols: Symbols = {
@@ -75,7 +75,7 @@ export const unicodeSymbols: Symbols = {
   and: "∧",
   or: "∨",
   to: "→",
-  iff: "↔",
+  eq: "↔",
 };
 
 export const latexSymbols: Symbols = {
@@ -87,7 +87,7 @@ export const latexSymbols: Symbols = {
   and: "\\land",
   or: "\\lor",
   to: "\\to",
-  iff: "\\leftrightarrow",
+  eq: "\\leftrightarrow",
 };
 
 export function prettyPrint(
@@ -138,13 +138,13 @@ export function prettyPrint(
         `${prettyPrint(fml.left, { symbols, paren: true })} ${symbols.to} ${prettyPrint(fml.right, newConfig)}`,
       );
     }
-    case "iff": {
+    case "eq": {
       const newConfig: typeof config = {
         symbols,
-        paren: (f) => f.type !== "iff",
+        paren: (f) => f.type !== "eq",
       };
       return withParen(
-        `${prettyPrint(fml.left, newConfig)} ${symbols.iff} ${prettyPrint(fml.right, newConfig)}`,
+        `${prettyPrint(fml.left, newConfig)} ${symbols.eq} ${prettyPrint(fml.right, newConfig)}`,
       );
     }
   }