kripke: make it playable

2025-02-19 16:59:47 +09:00
parent 2c901b44f6
commit 002531d48f
16 changed files with 559 additions and 47 deletions
--- a/apps/web/package.json
+++ b/apps/web/package.json
@@ -20,6 +20,7 @@
    "@sveltejs/vite-plugin-svelte": "4.0.4",
    "@types/prismjs": "1.26.5",
    "autoprefixer": "10.4.20",
+    "bits-ui": "1.3.0",
    "katex": "0.16.21",
    "mdsvex": "0.12.3",
    "misskey-js": "2024.11.1-alpha.0",
@@ -33,6 +34,7 @@
    "svelte": "5.16.1",
    "svelte-check": "4.1.4",
    "svgo": "3.3.2",
+    "tailwind-variants": "0.3.1",
    "tailwindcss": "3.4.17",
    "typescript": "5.7.3",
    "vite": "5.4.12"
--- a/apps/web/src/lib/components/ui/button/button.svelte
+++ b/apps/web/src/lib/components/ui/button/button.svelte
@@ -0,0 +1,79 @@
+<script lang="ts" module>
+import type { WithElementRef } from "bits-ui";
+import type {
+  HTMLAnchorAttributes,
+  HTMLButtonAttributes,
+} from "svelte/elements";
+import { type VariantProps, tv } from "tailwind-variants";
+
+export const buttonVariants = tv({
+  base: "focus-visible:ring-ring inline-flex items-center justify-center gap-2 whitespace-nowrap rounded-md text-sm font-medium transition-colors focus-visible:outline-none focus-visible:ring-1 disabled:pointer-events-none disabled:opacity-50 [&_svg]:pointer-events-none [&_svg]:size-4 [&_svg]:shrink-0",
+  variants: {
+    variant: {
+      default: "bg-primary text-background hover:bg-primary/90 shadow",
+      destructive:
+        "bg-destructive text-destructive-foreground hover:bg-destructive/90 shadow-sm",
+      outline:
+        "border-input bg-background hover:bg-accent hover:text-accent-foreground border shadow-sm",
+      secondary:
+        "bg-secondary text-secondary-foreground hover:bg-secondary/80 shadow-sm",
+      ghost: "hover:bg-accent hover:text-accent-foreground",
+      link: "text-primary underline-offset-4 hover:underline",
+    },
+    size: {
+      default: "h-9 px-4 py-2",
+      sm: "h-8 rounded-md px-3 text-xs",
+      lg: "h-10 rounded-md px-8",
+      icon: "h-9 w-9",
+    },
+  },
+  defaultVariants: {
+    variant: "default",
+    size: "default",
+  },
+});
+
+export type ButtonVariant = VariantProps<typeof buttonVariants>["variant"];
+export type ButtonSize = VariantProps<typeof buttonVariants>["size"];
+
+export type ButtonProps = WithElementRef<HTMLButtonAttributes> &
+  WithElementRef<HTMLAnchorAttributes> & {
+    variant?: ButtonVariant;
+    size?: ButtonSize;
+  };
+</script>
+
+<script lang="ts">
+	import { cn } from "$lib/utils.js";
+
+	let {
+		class: className,
+		variant = "default",
+		size = "default",
+		ref = $bindable(null),
+		href = undefined,
+		type = "button",
+		children,
+		...restProps
+	}: ButtonProps = $props();
+</script>
+
+{#if href}
+	<a
+		bind:this={ref}
+		class={cn(buttonVariants({ variant, size }), className)}
+		{href}
+		{...restProps}
+	>
+		{@render children?.()}
+	</a>
+{:else}
+	<button
+		bind:this={ref}
+		class={cn(buttonVariants({ variant, size }), className)}
+		{type}
+		{...restProps}
+	>
+		{@render children?.()}
+	</button>
+{/if}
--- a/apps/web/src/lib/components/ui/button/index.ts
+++ b/apps/web/src/lib/components/ui/button/index.ts
@@ -0,0 +1,17 @@
+import Root, {
+  type ButtonProps,
+  type ButtonSize,
+  type ButtonVariant,
+  buttonVariants,
+} from "./button.svelte";
+
+export {
+  Root,
+  type ButtonProps as Props,
+  //
+  Root as Button,
+  buttonVariants,
+  type ButtonProps,
+  type ButtonSize,
+  type ButtonVariant,
+};
--- a/apps/web/src/lib/components/ui/dialog/dialog-content.svelte
+++ b/apps/web/src/lib/components/ui/dialog/dialog-content.svelte
@@ -0,0 +1,41 @@
+<script lang="ts">
+import { cn } from "$lib/utils.js";
+import {
+  Dialog as DialogPrimitive,
+  type WithoutChildrenOrChild,
+} from "bits-ui";
+import X from "lucide-svelte/icons/x";
+import type { Snippet } from "svelte";
+import * as Dialog from "./index.js";
+
+let {
+  ref = $bindable(null),
+  class: className,
+  portalProps,
+  children,
+  ...restProps
+}: WithoutChildrenOrChild<DialogPrimitive.ContentProps> & {
+  portalProps?: DialogPrimitive.PortalProps;
+  children: Snippet;
+} = $props();
+</script>
+
+<Dialog.Portal {...portalProps}>
+	<Dialog.Overlay />
+	<DialogPrimitive.Content
+		bind:ref
+		class={cn(
+			"bg-background data-[state=open]:animate-in data-[state=closed]:animate-out data-[state=closed]:fade-out-0 data-[state=open]:fade-in-0 data-[state=closed]:zoom-out-95 data-[state=open]:zoom-in-95 data-[state=closed]:slide-out-to-left-1/2 data-[state=closed]:slide-out-to-top-[48%] data-[state=open]:slide-in-from-left-1/2 data-[state=open]:slide-in-from-top-[48%] fixed left-[50%] top-[50%] z-50 grid w-full max-w-lg translate-x-[-50%] translate-y-[-50%] gap-4 border p-6 shadow-lg duration-200 sm:rounded-lg",
+			className
+		)}
+		{...restProps}
+	>
+		{@render children?.()}
+		<DialogPrimitive.Close
+			class="ring-offset-background focus:ring-ring data-[state=open]:bg-muted data-[state=open]:text-muted-foreground absolute right-4 top-4 rounded-sm opacity-70 transition-opacity hover:opacity-100 focus:outline-none focus:ring-2 focus:ring-offset-2 disabled:pointer-events-none"
+		>
+			<X class="size-4" />
+			<span class="sr-only">Close</span>
+		</DialogPrimitive.Close>
+	</DialogPrimitive.Content>
+</Dialog.Portal>
--- a/apps/web/src/lib/components/ui/dialog/dialog-description.svelte
+++ b/apps/web/src/lib/components/ui/dialog/dialog-description.svelte
@@ -0,0 +1,16 @@
+<script lang="ts">
+import { cn } from "$lib/utils.js";
+import { Dialog as DialogPrimitive } from "bits-ui";
+
+let {
+  ref = $bindable(null),
+  class: className,
+  ...restProps
+}: DialogPrimitive.DescriptionProps = $props();
+</script>
+
+<DialogPrimitive.Description
+	bind:ref
+	class={cn("text-muted-foreground text-sm", className)}
+	{...restProps}
+/>
--- a/apps/web/src/lib/components/ui/dialog/dialog-footer.svelte
+++ b/apps/web/src/lib/components/ui/dialog/dialog-footer.svelte
@@ -0,0 +1,20 @@
+<script lang="ts">
+import { cn } from "$lib/utils.js";
+import type { WithElementRef } from "bits-ui";
+import type { HTMLAttributes } from "svelte/elements";
+
+let {
+  ref = $bindable(null),
+  class: className,
+  children,
+  ...restProps
+}: WithElementRef<HTMLAttributes<HTMLDivElement>> = $props();
+</script>
+
+<div
+	bind:this={ref}
+	class={cn("flex flex-col-reverse sm:flex-row sm:justify-end sm:space-x-2", className)}
+	{...restProps}
+>
+	{@render children?.()}
+</div>
--- a/apps/web/src/lib/components/ui/dialog/dialog-header.svelte
+++ b/apps/web/src/lib/components/ui/dialog/dialog-header.svelte
@@ -0,0 +1,20 @@
+<script lang="ts">
+import { cn } from "$lib/utils.js";
+import type { WithElementRef } from "bits-ui";
+import type { HTMLAttributes } from "svelte/elements";
+
+let {
+  ref = $bindable(null),
+  class: className,
+  children,
+  ...restProps
+}: WithElementRef<HTMLAttributes<HTMLDivElement>> = $props();
+</script>
+
+<div
+	bind:this={ref}
+	class={cn("flex flex-col space-y-1.5 text-center sm:text-left", className)}
+	{...restProps}
+>
+	{@render children?.()}
+</div>
--- a/apps/web/src/lib/components/ui/dialog/dialog-overlay.svelte
+++ b/apps/web/src/lib/components/ui/dialog/dialog-overlay.svelte
@@ -0,0 +1,19 @@
+<script lang="ts">
+import { cn } from "$lib/utils.js";
+import { Dialog as DialogPrimitive } from "bits-ui";
+
+let {
+  ref = $bindable(null),
+  class: className,
+  ...restProps
+}: DialogPrimitive.OverlayProps = $props();
+</script>
+
+<DialogPrimitive.Overlay
+	bind:ref
+	class={cn(
+		"data-[state=open]:animate-in data-[state=closed]:animate-out data-[state=closed]:fade-out-0 data-[state=open]:fade-in-0  fixed inset-0 z-50 bg-black/80",
+		className
+	)}
+	{...restProps}
+/>
--- a/apps/web/src/lib/components/ui/dialog/dialog-title.svelte
+++ b/apps/web/src/lib/components/ui/dialog/dialog-title.svelte
@@ -0,0 +1,16 @@
+<script lang="ts">
+import { cn } from "$lib/utils.js";
+import { Dialog as DialogPrimitive } from "bits-ui";
+
+let {
+  ref = $bindable(null),
+  class: className,
+  ...restProps
+}: DialogPrimitive.TitleProps = $props();
+</script>
+
+<DialogPrimitive.Title
+	bind:ref
+	class={cn("text-lg font-semibold leading-none tracking-tight", className)}
+	{...restProps}
+/>
--- a/apps/web/src/lib/components/ui/dialog/index.ts
+++ b/apps/web/src/lib/components/ui/dialog/index.ts
@@ -0,0 +1,37 @@
+import { Dialog as DialogPrimitive } from "bits-ui";
+
+import Content from "./dialog-content.svelte";
+import Description from "./dialog-description.svelte";
+import Footer from "./dialog-footer.svelte";
+import Header from "./dialog-header.svelte";
+import Overlay from "./dialog-overlay.svelte";
+import Title from "./dialog-title.svelte";
+
+const Root: typeof DialogPrimitive.Root = DialogPrimitive.Root;
+const Trigger: typeof DialogPrimitive.Trigger = DialogPrimitive.Trigger;
+const Close: typeof DialogPrimitive.Close = DialogPrimitive.Close;
+const Portal: typeof DialogPrimitive.Portal = DialogPrimitive.Portal;
+
+export {
+  Root,
+  Title,
+  Portal,
+  Footer,
+  Header,
+  Trigger,
+  Overlay,
+  Content,
+  Description,
+  Close,
+  //
+  Root as Dialog,
+  Title as DialogTitle,
+  Portal as DialogPortal,
+  Footer as DialogFooter,
+  Header as DialogHeader,
+  Trigger as DialogTrigger,
+  Overlay as DialogOverlay,
+  Content as DialogContent,
+  Description as DialogDescription,
+  Close as DialogClose,
+};
--- a/apps/web/src/routes/kripke/+page.server.ts
+++ b/apps/web/src/routes/kripke/+page.server.ts
@@ -0,0 +1,18 @@
+import type { SeoProps } from "$components/seo";
+
+export async function load() {
+  return {
+    seo: {
+      title: "KRIPKE - cannorin.net",
+      description: "KRIPKE - WORDLE, but for Kripke frames!",
+      openGraph: {
+        title: "KRIPKE - cannorin.net",
+        description: "KRIPKE - WORDLE, but for Kripke frames!",
+      },
+      twitter: {
+        title: "KRIPKE - cannorin.net",
+        description: "KRIPKE - WORDLE, but for Kripke frames!",
+      },
+    } as SeoProps,
+  };
+}
--- a/apps/web/src/routes/kripke/+page.svelte
+++ b/apps/web/src/routes/kripke/+page.svelte
@@ -9,13 +9,14 @@ const dailyFrameId = isomorphic[getId(dailyFrame)];
 const relationSize = dailyFrame.relations.size;
 const guess = (frameId: number) => isomorphic[frameId] === dailyFrameId;
 const check = (formula: Formula) => validWorlds(dailyFrame, formula).length;
+const getAnswer = () => dailyFrameId;
 </script>

 <main class="flex flex-col min-h-screen max-w-full items-center gap-12 lg:gap-16 py-8">
  <h1 class="font-display text-6xl">KRiPkE</h1>

  <div class="flex flex-col md:flex-row-reverse gap-x-20 gap-y-8">
-    <Game relationSize={relationSize} guess={guess} check={check} />
+    <Game relationSize={relationSize} guess={guess} check={check} getAnswer={getAnswer} />

    <div class="w-[300px] prose prose-sm">
      <h2>Rules</h2>
@@ -49,15 +50,15 @@ const check = (formula: Formula) => validWorlds(dailyFrame, formula).length;
      <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>T</code>, <code>⊤</code>, <code>1</code>, <code>\top</code></li>
-        <li>falsum: <code>F</code>, <code>⊥</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>L</code>, <code>\Box</code></li>
-        <li>diamond modality: <code>&lt;&gt;</code>, <code>⋄</code>, <code>M</code>, <code>\Diamond</code></li>
-        <li>conjunction: <code>&amp;</code>, <code>^</code>, <code>∧</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>-&gt;</code>, <code>→</code>, <code>\rightarrow</code>, <code>\to</code>, <code>\implies</code></li>
-        <li>equivalence: <code>&lt;-&gt;</code>, <code>↔</code>, <code>\leftrightarrow</code>, <code>\iff</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>
      </ul>
    </div>
--- a/apps/web/src/routes/kripke/frame-input.svelte
+++ b/apps/web/src/routes/kripke/frame-input.svelte
@@ -8,15 +8,21 @@ import {
  right,
  worlds,
 } from "@cannorin/kripke";
+import type { SVGAttributes } from "svelte/elements";
 import { type Vector, add, degree, rotate, sub, theta } from "./vector";

+export interface FrameInputProps extends SVGAttributes<SVGElement> {
+  frame?: Frame | undefined;
+  disabled?: boolean | undefined;
+}
+
 let {
  frame = $bindable<Frame>({ relations: new Set() }),
  disabled = false,
-}: {
-  frame?: Frame | undefined;
-  disabled?: boolean | undefined;
-} = $props();
+  width,
+  height,
+  ...rest
+}: FrameInputProps = $props();

 let selected: World | null = $state(null);

@@ -130,7 +136,7 @@ function getPath(rel: Relation) {

 <!-- svelte-ignore a11y_click_events_have_key_events -->
 <!-- svelte-ignore a11y_no_static_element_interactions -->
-<svg width="250" height="250" onclick={handleSvgClick}>
+<svg width={width ?? 250} height={height ?? 250} {...rest} viewBox="0,0,250,250" onclick={handleSvgClick}>
  <defs>
    <marker
      id="arrowhead"
--- a/apps/web/src/routes/kripke/game.svelte
+++ b/apps/web/src/routes/kripke/game.svelte
@@ -1,5 +1,8 @@
 <script lang="ts">
 import Katex from "$lib/components/katex.svelte";
+import { Button } from "$lib/components/ui/button";
+import * as Dialog from "$lib/components/ui/dialog";
+import { cn } from "$lib/utils";
 import {
  type Formula,
  type Frame,
@@ -9,8 +12,10 @@ import {
  latexSymbols,
  prettyPrint,
 } from "@cannorin/kripke";
+import LuCheck from "lucide-svelte/icons/check";
 import LuHeart from "lucide-svelte/icons/heart";
 import LuHeartCrack from "lucide-svelte/icons/heart-crack";
+import LuX from "lucide-svelte/icons/x";
 import FormulaInput from "./formula-input.svelte";
 import FrameInput from "./frame-input.svelte";

@@ -26,6 +31,7 @@ export type Props = {
  relationSize: number;
  guess: (frameId: number) => boolean | Promise<boolean>;
  check: (formula: Formula) => number | Promise<number>;
+  getAnswer: () => number | Promise<number>;
 };

 let {
@@ -34,10 +40,12 @@ let {
  relationSize,
  guess: guessImpl,
  check: checkImpl,
+  getAnswer,
 }: Props = $props();

 let formula: Formula | undefined = $state(undefined);
 let frame: Frame = $state(getFrame(0));
+let frameId = $derived(getId(frame));
 let math = $derived.by(() => {
  if (formula) return prettyPrint(formula, { symbols: latexSymbols });
  return "\\phantom{p}";
@@ -46,21 +54,24 @@ let math = $derived.by(() => {
 let remainingRelations = $derived(relationSize - frame.relations.size);

 let life = $derived(10 - moves.length);
+let dialogOpen = $state(false);

 $effect(() => {
  if (life <= 0) {
    status = "lose";
+    dialogOpen = true;
    return;
  }
  if (moves.some((move) => move.type === "guess" && move.correct)) {
    status = "win";
+    dialogOpen = true;
    return;
  }
 });

 let canGuess = $derived.by(() => {
  if (status !== "playing" || remainingRelations !== 0) return false;
-  const frameId = isomorphic[getId(frame)];
+  const frameId = getId(frame);
  return !moves.some(
    (move) => move.type === "guess" && move.frameId === frameId,
  );
@@ -90,6 +101,14 @@ async function check() {
  moves = [...moves];
  formula = undefined;
 }
+
+const colors: Record<number, string> = {
+  0: "bg-muted",
+  1: "bg-red-700",
+  2: "bg-amber-700",
+  3: "bg-yellow-600",
+  4: "bg-green-700",
+};
 </script>

 {#snippet sampleArrow()}
@@ -116,16 +135,16 @@ async function check() {
  <div class="flex items-center justify-between">
    {#each [1,2,3,4,5,6,7,8,9,10] as i}
      {#if i <= life}
-        <LuHeart class="text-primary" />
+        <LuHeart class={cn("text-primary", life <= 3 && "animate-pulse")} />
      {:else}
-        <LuHeartCrack class="text-muted" />
+        <LuHeartCrack class="text-muted animate-blink" />
      {/if}
    {/each}
  </div>

  <div class="flex flex-col items-center gap-2">
-    <div class="w-[300px] h-[300px] flex flex-col items-center justify-betwenn border rounded border-border">
-      <span class="text-xs text-muted self-start px-2 py-1">id: {isomorphic[getId(frame)]}</span>
+    <div class="w-[300px] h-[300px] flex flex-col items-center justify-between border rounded border-border">
+      <span class="text-xs text-muted self-start px-2 py-1">id: {frameId} (≈ {isomorphic[frameId]})</span>
      <FrameInput bind:frame disabled={status !== "playing"} />
      <span class="text-sm px-2 py-1 self-end flex items-center">
        {@render sampleArrow()} × {remainingRelations}
@@ -145,9 +164,12 @@ async function check() {

  <div class="flex flex-col items-center gap-2">
    <Katex math={math} />
+    <form
+      class="flex flex-col items-center gap-2"
+      onsubmit={(e) => { e.preventDefault(); check(); }}>
      <FormulaInput bind:formula disabled={status !== "playing"} />
      <button
-      onclick={check}
+        type="submit"
        disabled={!canCheck}
        class={[
          "rounded w-full p-1 text-background font-bold flex items-center justify-center gap-2",
@@ -159,20 +181,83 @@ async function check() {
          Check! <span class="flex items-center font-normal">(<LuHeart size=14 class="mt-1 mr-[1px]"/> 1)</span>
        {/if}
      </button>
+    </form>
  </div>

  <div>
    <ul class="flex flex-col gap-2">
      {#each moves as move}
-        <li>
        {#if move.type === "guess"}
-            Guess({move.frameId}) = {move.correct}
+          <li class="flex justify-between items-center animate-fade-in">
+            <FrameInput disabled width={125} height={125} frame={getFrame(move.frameId)} />
+            <span class={["rounded w-6 h-6 min-w-6 min-h-6 max-w-6 max-h-6 text-background flex items-center justify-center", move.correct ? "bg-green-700" : "bg-muted"]}>
+              {#if move.correct}
+                <LuCheck size=24 />
+              {:else}
+                <LuX size=24 />
+              {/if}
+            </span>
+          </li>
        {/if}
        {#if move.type === "check"}
-            Valid({move.formulaStr}) = {move.valid}
-          {/if}
+          <li class="flex justify-between items-center animate-fade-in">
+            <Katex math={move.formulaStr} />
+            <span class={["rounded w-6 h-6 min-w-6 min-h-6 max-w-6 max-h-6 text-background font-bold flex items-center justify-center pb-[2px]", colors[move.valid]]}>{move.valid}</span>
          </li>
+        {/if}
      {/each}
+      {#if status === "win"}
+        <li class="flex flex-col items-center gap-5 rounded bg-primary text-background p-5 animate-fade-in">
+          <p class="text-xl font-bold">YOU WIN!</p>
+        </li>
+      {:else if status === "lose"}
+        {#await getAnswer() then answerId}
+          <li class="flex flex-col gap-5 rounded bg-primary text-background p-5 animate-fade-in">
+            <div>
+              <p class="text-xl font-bold">YOU LOSE!</p>
+              <p class="text-sm">The answer was:</p>
+            </div>
+            <div class="flex flex-col items-center rounded bg-background w-full">
+              <span class="text-xs text-muted self-start px-2 py-1">id: {answerId}</span>
+              <FrameInput class="pb-6" disabled width={250} height={250} frame={getFrame(answerId)} />
+            </div>
+          </li>
+        {/await}
+      {/if}
    </ul>
  </div>
 </div>
+
+{#if status !== "playing"}
+  {#await getAnswer() then answerId}
+    <Dialog.Root bind:open={dialogOpen}>
+      <Dialog.Content class="animate-fade-in">
+        <Dialog.Header>
+          <Dialog.Title>
+            {#if status === "win"}
+              YOU WIN!
+            {:else if status === "lose"}
+              YOU LOSE!
+            {/if}
+          </Dialog.Title>
+          <Dialog.Description>
+            The answer was:
+          </Dialog.Description>
+        </Dialog.Header>
+
+        <div class="flex flex-col items-center w-fit rounded bg-background mx-auto">
+          <span class="text-xs text-muted self-start px-2 py-1">id: {answerId}</span>
+          <FrameInput class="pb-6" disabled width={250} height={250} frame={getFrame(answerId)} />
+        </div>
+
+        <Dialog.Footer class="gap-x-1 gap-y-2">
+          <Button
+            variant="outline"
+            onclick={() => (dialogOpen = false)}>
+            <LuX class="w-4 h-4 mt-[2px]" /> Close
+          </Button>
+        </Dialog.Footer>
+      </Dialog.Content>
+    </Dialog.Root>
+  {/await}
+{/if}
--- a/packages/kripke/parser.ts
+++ b/packages/kripke/parser.ts
@@ -47,12 +47,12 @@ const lexer = buildLexer([
  [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, /^(\[\]|□|!|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|\\implies)/g, TokenKind.To],
-  [true, /^(<->|↔|\\leftrightarrow|\\iff)/g, TokenKind.Iff],
+  [true, /^(>|->|→|\\rightarrow|\\to)/g, TokenKind.To],
+  [true, /^(=|<->|↔|\\leftrightarrow|\\equiv)/g, TokenKind.Iff],
  [true, /^(\(|\\left\()/g, TokenKind.LParen],
  [true, /^(\)|\\right\))/g, TokenKind.RParen],
  [false, /^\s+/g, TokenKind.Space],
--- a/yarn.lock
+++ b/yarn.lock
@@ -292,6 +292,32 @@ __metadata:
  languageName: node
  linkType: hard

+"@floating-ui/core@npm:^1.6.0, @floating-ui/core@npm:^1.6.4":
+  version: 1.6.9
+  resolution: "@floating-ui/core@npm:1.6.9"
+  dependencies:
+    "@floating-ui/utils": "npm:^0.2.9"
+  checksum: 10c0/77debdfc26bc36c6f5ae1f26ab3c15468215738b3f5682af4e1915602fa21ba33ad210273f31c9d2da1c531409929e1afb1138b1608c6b54a0f5853ee84c340d
+  languageName: node
+  linkType: hard
+
+"@floating-ui/dom@npm:^1.6.7":
+  version: 1.6.13
+  resolution: "@floating-ui/dom@npm:1.6.13"
+  dependencies:
+    "@floating-ui/core": "npm:^1.6.0"
+    "@floating-ui/utils": "npm:^0.2.9"
+  checksum: 10c0/272242d2eb6238ffcee0cb1f3c66e0eafae804d5d7b449db5ecf904bc37d31ad96cf575a9e650b93c1190f64f49a684b1559d10e05ed3ec210628b19116991a9
+  languageName: node
+  linkType: hard
+
+"@floating-ui/utils@npm:^0.2.9":
+  version: 0.2.9
+  resolution: "@floating-ui/utils@npm:0.2.9"
+  checksum: 10c0/48bbed10f91cb7863a796cc0d0e917c78d11aeb89f98d03fc38d79e7eb792224a79f538ed8a2d5d5584511d4ca6354ef35f1712659fd569868e342df4398ad6f
+  languageName: node
+  linkType: hard
+
 "@fontsource/poiret-one@npm:5.1.1":
  version: 5.1.1
  resolution: "@fontsource/poiret-one@npm:5.1.1"
@@ -491,6 +517,15 @@ __metadata:
  languageName: node
  linkType: hard

+"@internationalized/date@npm:^3.5.6":
+  version: 3.7.0
+  resolution: "@internationalized/date@npm:3.7.0"
+  dependencies:
+    "@swc/helpers": "npm:^0.5.0"
+  checksum: 10c0/4d0979dd49f0f979169073afa2b44ce8ae941407e22d4caba069e26e9d9a0c6d29fc11fb50d5e6fcad351f0f9b180e21cbd440fd4238e899719f5d3c84829985
+  languageName: node
+  linkType: hard
+
 "@isaacs/cliui@npm:^8.0.2":
  version: 8.0.2
  resolution: "@isaacs/cliui@npm:8.0.2"
@@ -878,6 +913,15 @@ __metadata:
  languageName: node
  linkType: hard

+"@swc/helpers@npm:^0.5.0":
+  version: 0.5.15
+  resolution: "@swc/helpers@npm:0.5.15"
+  dependencies:
+    tslib: "npm:^2.8.0"
+  checksum: 10c0/33002f74f6f885f04c132960835fdfc474186983ea567606db62e86acd0680ca82f34647e8e610f4e1e422d1c16fce729dde22cd3b797ab1fd9061a825dabca4
+  languageName: node
+  linkType: hard
+
 "@tailwindcss/typography@npm:0.5.15":
  version: 0.5.15
  resolution: "@tailwindcss/typography@npm:0.5.15"
@@ -1112,6 +1156,23 @@ __metadata:
  languageName: node
  linkType: hard

+"bits-ui@npm:1.3.0":
+  version: 1.3.0
+  resolution: "bits-ui@npm:1.3.0"
+  dependencies:
+    "@floating-ui/core": "npm:^1.6.4"
+    "@floating-ui/dom": "npm:^1.6.7"
+    "@internationalized/date": "npm:^3.5.6"
+    esm-env: "npm:^1.1.2"
+    runed: "npm:^0.23.2"
+    svelte-toolbelt: "npm:^0.7.1"
+    tabbable: "npm:^6.2.0"
+  peerDependencies:
+    svelte: ^5.11.0
+  checksum: 10c0/04a47e2a8059a8bfc9c430b614743886898573659cbd2a731f8df4ef8b6c1b42f3eedd6c561faf868ecb9ff48ca9af45840d9b7288d82fc901ad2dabbdd89076
+  languageName: node
+  linkType: hard
+
 "boolbase@npm:^1.0.0":
  version: 1.0.0
  resolution: "boolbase@npm:1.0.0"
@@ -1629,6 +1690,13 @@ __metadata:
  languageName: node
  linkType: hard

+"esm-env@npm:^1.0.0, esm-env@npm:^1.1.2":
+  version: 1.2.2
+  resolution: "esm-env@npm:1.2.2"
+  checksum: 10c0/3d25c973f2fd69c25ffff29c964399cea573fe10795ecc1d26f6f957ce0483d3254e1cceddb34bf3296a0d7b0f1d53a28992f064ba509dfe6366751e752c4166
+  languageName: node
+  linkType: hard
+
 "esm-env@npm:^1.2.1":
  version: 1.2.1
  resolution: "esm-env@npm:1.2.1"
@@ -2033,6 +2101,13 @@ __metadata:
  languageName: node
  linkType: hard

+"inline-style-parser@npm:0.2.4":
+  version: 0.2.4
+  resolution: "inline-style-parser@npm:0.2.4"
+  checksum: 10c0/ddc0b210eaa03e0f98d677b9836242c583c7c6051e84ce0e704ae4626e7871c5b78f8e30853480218b446355745775df318d4f82d33087ff7e393245efa9a881
+  languageName: node
+  linkType: hard
+
 "ip-address@npm:^9.0.5":
  version: 9.0.5
  resolution: "ip-address@npm:9.0.5"
@@ -2989,6 +3064,17 @@ __metadata:
  languageName: node
  linkType: hard

+"runed@npm:^0.23.2":
+  version: 0.23.4
+  resolution: "runed@npm:0.23.4"
+  dependencies:
+    esm-env: "npm:^1.0.0"
+  peerDependencies:
+    svelte: ^5.7.0
+  checksum: 10c0/e27400af9e69b966dca449b851e82e09b3d2ddde4095ba72237599aa80fc248a23d0737c0286f751ca6c12721a5e09eb21b9d8cc872cbd70e7b161442818eece
+  languageName: node
+  linkType: hard
+
 "sade@npm:^1.7.4, sade@npm:^1.8.1":
  version: 1.8.1
  resolution: "sade@npm:1.8.1"
@@ -3240,6 +3326,15 @@ __metadata:
  languageName: node
  linkType: hard

+"style-to-object@npm:^1.0.8":
+  version: 1.0.8
+  resolution: "style-to-object@npm:1.0.8"
+  dependencies:
+    inline-style-parser: "npm:0.2.4"
+  checksum: 10c0/daa6646b1ff18258c0ca33ed281fbe73485c8391192db1b56ce89d40c93ea64507a41e8701d0dadfe771bc2f540c46c9b295135f71584c8e5cb23d6a19be9430
+  languageName: node
+  linkType: hard
+
 "sucrase@npm:^3.35.0":
  version: 3.35.0
  resolution: "sucrase@npm:3.35.0"
@@ -3301,6 +3396,19 @@ __metadata:
  languageName: node
  linkType: hard

+"svelte-toolbelt@npm:^0.7.1":
+  version: 0.7.1
+  resolution: "svelte-toolbelt@npm:0.7.1"
+  dependencies:
+    clsx: "npm:^2.1.1"
+    runed: "npm:^0.23.2"
+    style-to-object: "npm:^1.0.8"
+  peerDependencies:
+    svelte: ^5.0.0
+  checksum: 10c0/a50db97c851fa65af7fbf77007bd76730a179ac0239c0121301bd26682c1078a4ffea77835492550b133849a42d3dffee0714ae076154d86be8d0b3a84c9a9bf
+  languageName: node
+  linkType: hard
+
 "svelte@npm:5.16.1":
  version: 5.16.1
  resolution: "svelte@npm:5.16.1"
@@ -3351,6 +3459,20 @@ __metadata:
  languageName: node
  linkType: hard

+"tabbable@npm:^6.2.0":
+  version: 6.2.0
+  resolution: "tabbable@npm:6.2.0"
+  checksum: 10c0/ced8b38f05f2de62cd46836d77c2646c42b8c9713f5bd265daf0e78ff5ac73d3ba48a7ca45f348bafeef29b23da7187c72250742d37627883ef89cbd7fa76898
+  languageName: node
+  linkType: hard
+
+"tailwind-merge@npm:2.5.4":
+  version: 2.5.4
+  resolution: "tailwind-merge@npm:2.5.4"
+  checksum: 10c0/6c3d2a1d44344f373859f005e6366f0dbd7f66131d330a51dbe823dab08f71c388b2efcbb2b6a2170ca469581d27079c25cd40c234ca1356c4893ae99c2febb3
+  languageName: node
+  linkType: hard
+
 "tailwind-merge@npm:2.6.0":
  version: 2.6.0
  resolution: "tailwind-merge@npm:2.6.0"
@@ -3358,6 +3480,17 @@ __metadata:
  languageName: node
  linkType: hard

+"tailwind-variants@npm:0.3.1":
+  version: 0.3.1
+  resolution: "tailwind-variants@npm:0.3.1"
+  dependencies:
+    tailwind-merge: "npm:2.5.4"
+  peerDependencies:
+    tailwindcss: "*"
+  checksum: 10c0/2ad4a9282ea3d9b66443329ede844bd86b6737b98ede3f31d6b495e3d1f210677c57ba360af2dbffede00cce0026dd1105eeb1af936e825ebd14e715eb6cbc11
+  languageName: node
+  linkType: hard
+
 "tailwindcss@npm:3.4.17":
  version: 3.4.17
  resolution: "tailwindcss@npm:3.4.17"
@@ -3456,7 +3589,7 @@ __metadata:
  languageName: node
  linkType: hard

-"tslib@npm:^2.4.0":
+"tslib@npm:^2.4.0, tslib@npm:^2.8.0":
  version: 2.8.1
  resolution: "tslib@npm:2.8.1"
  checksum: 10c0/9c4759110a19c53f992d9aae23aac5ced636e99887b51b9e61def52611732872ff7668757d4e4c61f19691e36f4da981cd9485e869b4a7408d689f6bf1f14e62
@@ -3827,6 +3960,7 @@ __metadata:
    "@tailwindcss/typography": "npm:0.5.15"
    "@types/prismjs": "npm:1.26.5"
    autoprefixer: "npm:10.4.20"
+    bits-ui: "npm:1.3.0"
    deepmerge: "npm:4.3.1"
    katex: "npm:0.16.21"
    lucide-svelte: "npm:0.475.0"
@@ -3845,6 +3979,7 @@ __metadata:
    sveltekit-rate-limiter: "npm:0.6.1"
    svgo: "npm:3.3.2"
    tailwind-merge: "npm:2.6.0"
+    tailwind-variants: "npm:0.3.1"
    tailwindcss: "npm:3.4.17"
    typescript: "npm:5.7.3"
    vite: "npm:5.4.12"