web: add /kripke

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>

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>

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} />

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;
+  }
+}

packages/kripke/syntax.ts

@@ -79,11 +79,11 @@ export const unicodeSymbols: Symbols = {
 };
 
 export const latexSymbols: Symbols = {
-  top: "\\top",
+  top: "\\top ",
-  bot: "\\bot",
+  bot: "\\bot ",
-  box: "\\Box",
+  box: "\\Box ",
-  diamond: "\\Diamond",
+  diamond: "\\Diamond ",
-  not: "\\neg",
+  not: "\\neg ",
   and: "\\land",
   or: "\\lor",
   to: "\\to",