From 7a81594a863102dd6c6eecb7dde8b9b321f7d5b8 Mon Sep 17 00:00:00 2001
From: cannorin <cannorin@users.noreply.github.com>
Date: Tue, 18 Feb 2025 05:24:54 +0900
Subject: [PATCH] web: add /kripke

---
 apps/web/src/lib/components/katex.svelte      | 20 +++++++++++++++
 apps/web/src/routes/kripke/+page.svelte       | 17 +++++++++++++
 .../src/routes/kripke/formula-input.svelte    | 25 +++++++++++++++++++
 packages/kripke/parser.ts                     |  8 ++++++
 packages/kripke/syntax.ts                     | 10 ++++----
 5 files changed, 75 insertions(+), 5 deletions(-)
 create mode 100644 apps/web/src/lib/components/katex.svelte
 create mode 100644 apps/web/src/routes/kripke/+page.svelte
 create mode 100644 apps/web/src/routes/kripke/formula-input.svelte

diff --git a/apps/web/src/lib/components/katex.svelte b/apps/web/src/lib/components/katex.svelte
new file mode 100644
index 0000000..c2c3e48
--- /dev/null
+++ b/apps/web/src/lib/components/katex.svelte
@@ -0,0 +1,20 @@
+<script lang="ts">
+import katex from "katex";
+import "katex/dist/katex.min.css";
+import type { HTMLAttributes } from "svelte/elements";
+
+export interface KatexProps extends HTMLAttributes<HTMLDivElement> {
+  displayMode?: boolean;
+  math: string;
+}
+
+let { displayMode, math, ...rest }: KatexProps = $props();
+
+let katexString = $derived.by(() =>
+  katex.renderToString(math, { displayMode, throwOnError: false }),
+);
+</script>
+
+<div {...rest}>
+  {@html katexString}
+</div>
diff --git a/apps/web/src/routes/kripke/+page.svelte b/apps/web/src/routes/kripke/+page.svelte
new file mode 100644
index 0000000..69ee43f
--- /dev/null
+++ b/apps/web/src/routes/kripke/+page.svelte
@@ -0,0 +1,17 @@
+<script lang="ts">
+import Katex from "$lib/components/katex.svelte";
+import { type Formula, latexSymbols, prettyPrint } from "@cannorin/kripke";
+import FormulaInput from "./formula-input.svelte";
+
+let formula: Formula | undefined = $state(undefined);
+let math = $derived.by(() => {
+  if (formula) return prettyPrint(formula, { symbols: latexSymbols });
+  return "\\phantom{p}";
+});
+</script>
+
+<div class="flex flex-col min-h-screen items-center gap-12 lg:gap-16 py-8">
+  <Katex math={math} />
+
+  <FormulaInput bind:formula />
+</div>
diff --git a/apps/web/src/routes/kripke/formula-input.svelte b/apps/web/src/routes/kripke/formula-input.svelte
new file mode 100644
index 0000000..03257ce
--- /dev/null
+++ b/apps/web/src/routes/kripke/formula-input.svelte
@@ -0,0 +1,25 @@
+<script lang="ts">
+import { type Formula, tryParse } from "@cannorin/kripke";
+
+let {
+  formula = $bindable<Formula | undefined>(undefined),
+}: {
+  formula?: Formula | undefined;
+} = $props();
+
+let input = $state("");
+let error = $state(false);
+
+$effect(() => {
+  const fml = tryParse(input);
+  if (fml) {
+    formula = fml;
+    error = false;
+  } else if (input !== null && input.length > 0) error = true;
+});
+</script>
+
+<input
+  class={["rounded border border-foreground ring-0 focus:outline-none focus:ring-0 p-2", error && "border-primary"]}
+  type="text"
+  bind:value={input} />
diff --git a/packages/kripke/parser.ts b/packages/kripke/parser.ts
index 44dcfa4..42bc6a4 100644
--- a/packages/kripke/parser.ts
+++ b/packages/kripke/parser.ts
@@ -146,3 +146,11 @@ EXP.setPattern(
 export function parse(expr: string): Formula {
   return expectSingleResult(expectEOF(EXP.parse(lexer.parse(expr))));
 }
+
+export function tryParse(expr: string): Formula | undefined {
+  try {
+    return parse(expr);
+  } catch {
+    return undefined;
+  }
+}
diff --git a/packages/kripke/syntax.ts b/packages/kripke/syntax.ts
index ac06634..787d2ec 100644
--- a/packages/kripke/syntax.ts
+++ b/packages/kripke/syntax.ts
@@ -79,11 +79,11 @@ export const unicodeSymbols: Symbols = {
 };
 
 export const latexSymbols: Symbols = {
-  top: "\\top",
-  bot: "\\bot",
-  box: "\\Box",
-  diamond: "\\Diamond",
-  not: "\\neg",
+  top: "\\top ",
+  bot: "\\bot ",
+  box: "\\Box ",
+  diamond: "\\Diamond ",
+  not: "\\neg ",
   and: "\\land",
   or: "\\lor",
   to: "\\to",