kripke: add frame input

apps/web/src/routes/kripke/+page.svelte

@@ -1,17 +1,32 @@
 <script lang="ts">
 import Katex from "$lib/components/katex.svelte";
-import { type Formula, latexSymbols, prettyPrint } from "@cannorin/kripke";
+import {
+  type Formula,
+  type Frame,
+  latexSymbols,
+  prettyPrint,
+} from "@cannorin/kripke";
 import FormulaInput from "./formula-input.svelte";
+import FrameInput from "./frame-input.svelte";
 
 let formula: Formula | undefined = $state(undefined);
+let frame: Frame = $state({ relations: new Set() });
 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">
+<div class="flex flex-col min-h-screen max-w-full items-center gap-12 lg:gap-16 py-8">
-  <Katex math={math} />
 
-  <FormulaInput bind:formula />
+  <h1 class="font-display text-6xl">KRiPkE</h1>
+
+  <div class="w-[300px] flex flex-col gap-10">
+    <div class="flex flex-col items-center gap-2">
+      <Katex math={math} />
+      <FormulaInput bind:formula />
+    </div>
+
+    <FrameInput bind:frame />
+  </div>
 </div>

apps/web/src/routes/kripke/formula-input.svelte

@@ -20,6 +20,7 @@ $effect(() => {
 </script>
 
 <input
-  class={["rounded border border-foreground ring-0 focus:outline-none focus:ring-0 p-2", error && "border-primary"]}
+  class={["rounded border border-foreground ring-0 focus:outline-none focus:ring-0 p-2 w-full", error && "border-primary"]}
   type="text"
+  placeholder="Enter modal formula"
   bind:value={input} />

apps/web/src/routes/kripke/frame-input.svelte

@@ -0,0 +1,176 @@
+<script lang="ts">
+import {
+  type Frame,
+  type Relation,
+  type World,
+  left,
+  reverse,
+  right,
+  worlds,
+} from "@cannorin/kripke";
+import { type Vector, add, degree, rotate, sub, theta } from "./vector";
+
+let {
+  frame = $bindable<Frame>({ relations: new Set() }),
+}: {
+  frame?: Frame | undefined;
+} = $props();
+
+let relations = $state(new Set<Relation>());
+
+$effect(() => {
+  frame = { relations };
+});
+
+let selected: World | null = $state(null);
+
+function toggle(rel: Relation) {
+  if (relations.has(rel)) {
+    relations.delete(rel);
+  } else {
+    relations.add(rel);
+  }
+  // Reassign to trigger reactivity
+  relations = new Set(relations);
+}
+
+function handleNodeClick(node: World, event: MouseEvent) {
+  event.stopPropagation();
+  if (selected === null) {
+    // Start a new edge
+    selected = node;
+  } else {
+    // Toggle the edge from selectedNode -> nodeId
+    const rel: Relation = `${selected}${node}` as Relation;
+    toggle(rel);
+    selected = null;
+  }
+}
+
+function handleEdgeClick(rel: Relation, event: MouseEvent) {
+  event.stopPropagation();
+  toggle(rel);
+}
+
+// Clear selection if the user clicks on the background
+function handleSvgClick() {
+  selected = null;
+}
+
+const positions: Record<World, Vector> = {
+  a: {
+    x: 75,
+    y: 75,
+  },
+  b: {
+    x: 225,
+    y: 75,
+  },
+  c: {
+    x: 225,
+    y: 225,
+  },
+  d: {
+    x: 75,
+    y: 225,
+  },
+};
+
+const center: Vector = { x: 150, y: 150 };
+
+const radius: Vector = { x: 20, y: 0 };
+
+function getSelfPath(w: World) {
+  const angle = theta(sub(center, positions[w])) + Math.PI;
+  const offset = degree(45);
+  const loopRadius = 20;
+  const start = add(positions[w], rotate(radius, angle - offset));
+  const end = add(positions[w], rotate(radius, angle + offset));
+
+  return `
+    M ${start.x} ${start.y}
+    A ${loopRadius} ${loopRadius} 0 1 1 ${end.x} ${end.y}
+  `;
+}
+
+function getPath(rel: Relation) {
+  const l = left(rel);
+  const r = right(rel);
+  if (l === r) return getSelfPath(l);
+
+  const angle = theta(sub(positions[r], positions[l]));
+
+  const offset = relations.has(reverse(rel)) ? degree(10) : 0;
+
+  const dl = rotate(radius, angle + offset);
+  const dr = rotate(radius, angle + Math.PI - offset);
+  const from = add(positions[l], dl);
+  const to = add(positions[r], dr);
+
+  if (!relations.has(reverse(rel)))
+    return `M ${from.x} ${from.y} L ${to.x} ${to.y}`;
+
+  return `M ${from.x} ${from.y} C ${from.x + dl.x * 2} ${from.y + dl.y * 2}, ${to.x + dr.x * 2} ${to.y + dr.y * 2}, ${to.x} ${to.y}`;
+}
+</script>
+
+<style>
+  .node {
+    fill: rgb(var(--background));
+    stroke: rgb(var(--foreground));
+    stroke-width: 1;
+    cursor: pointer;
+  }
+  .node.selected {
+    fill: rgb(var(--primary));
+    stroke: rgb(var(--foreground));
+  }
+  .edge {
+    stroke: rgb(var(--foreground));
+    stroke-width: 1;
+    fill: none;
+    cursor: pointer;
+    marker-end: url(#arrowhead);
+  }
+</style>
+
+<!-- svelte-ignore a11y_click_events_have_key_events -->
+<!-- svelte-ignore a11y_no_static_element_interactions -->
+<svg class="border border-foreground rounded" width="300" height="300" onclick={handleSvgClick}>
+  <defs>
+    <marker
+      id="arrowhead"
+      viewBox="0 0 10 10"
+      refX="8"
+      refY="5"
+      markerWidth="6"
+      markerHeight="6"
+      orient="auto"
+      markerUnits="strokeWidth"
+    >
+      <path d="M0,0 L0,10 L10,5 z" fill="#333" />
+    </marker>
+  </defs>
+
+  {#each Array.from(relations) as rel}
+    {#key rel}
+      <path
+        d={getPath(rel)}
+        class="edge"
+        onclick={(e) => handleEdgeClick(rel, e)}
+      />
+    {/key}
+  {/each}
+
+  {#each worlds as w}
+    {@const x = positions[w].x}
+    {@const y = positions[w].y}
+    <circle
+      cx={x}
+      cy={y}
+      r={radius.x}
+      class="node {selected === w ? 'selected' : ''}"
+      onclick={(e) => handleNodeClick(w, e)}
+    />
+  {/each}
+</svg>

apps/web/src/routes/kripke/vector.ts

@@ -0,0 +1,28 @@
+export type Vector = {
+  x: number;
+  y: number;
+};
+
+export type Radian = number;
+
+export const degree = (value: number) => ((value / 180) * Math.PI) as Radian;
+
+export const sub = (v1: Vector, v2: Vector) =>
+  ({
+    x: v1.x - v2.x,
+    y: v1.y - v2.y,
+  }) as Vector;
+
+export const add = (v1: Vector, v2: Vector) =>
+  ({
+    x: v1.x + v2.x,
+    y: v1.y + v2.y,
+  }) as Vector;
+
+export const theta = ({ x, y }: Vector) => Math.atan2(y, x) as Radian;
+
+export const rotate = ({ x, y }: Vector, rad: Radian) =>
+  ({
+    x: x * Math.cos(rad) - y * Math.sin(rad),
+    y: x * Math.sin(rad) + y * Math.cos(rad),
+  }) as Vector;

packages/kripke/semantics.ts

@@ -8,6 +8,8 @@ export type World = (typeof worlds)[number];
 export type Relation = `${World}${World}`;
 export const left = (rel: Relation) => rel[0] as World;
 export const right = (rel: Relation) => rel[1] as World;
+export const reverse = (rel: Relation) =>
+  `${right(rel)}${left(rel)}` as Relation;
 
 export const relation: Relation[] = worlds.flatMap((w) =>
   worlds.map((x) => `${w}${x}` as const),
@@ -148,15 +150,15 @@ export function generateAllFrames() {
     }
   }
 
-  const mapping: Uint16Array = new Uint16Array(total);
+  const isomorphic: Uint16Array = new Uint16Array(total);
   for (let id = 0; id < total; id++) {
     const value = map.get(id);
     if (value === undefined) throw Error(`impossible (${id})`);
-    mapping[id] = value;
+    isomorphic[id] = value;
   }
 
-  return { canonicals, mapping };
+  return { canonicals, isomorphic };
 }
 
-const { canonicals, mapping } = generateAllFrames();
+const { canonicals, isomorphic } = generateAllFrames();
-export { canonicals, mapping };
+export { canonicals, isomorphic };