kripke: refactor
This commit is contained in:
@@ -1,157 +1,21 @@
|
||||
<script lang="ts">
|
||||
import Katex from "$lib/components/katex.svelte";
|
||||
import {
|
||||
type Formula,
|
||||
type Frame,
|
||||
getFrame,
|
||||
getId,
|
||||
isomorphic,
|
||||
latexSymbols,
|
||||
prettyPrint,
|
||||
validWorlds,
|
||||
} from "@cannorin/kripke";
|
||||
import { type Formula, getId, isomorphic, validWorlds } from "@cannorin/kripke";
|
||||
import LuHeart from "lucide-svelte/icons/heart";
|
||||
import LuHeartCrack from "lucide-svelte/icons/heart-crack";
|
||||
import FormulaInput from "./formula-input.svelte";
|
||||
import FrameInput from "./frame-input.svelte";
|
||||
import Game from "./game.svelte";
|
||||
import { getDailyFrame } from "./system";
|
||||
|
||||
let formula: Formula | undefined = $state(undefined);
|
||||
let frame: Frame = $state(getFrame(0));
|
||||
let math = $derived.by(() => {
|
||||
if (formula) return prettyPrint(formula, { symbols: latexSymbols });
|
||||
return "\\phantom{p}";
|
||||
});
|
||||
|
||||
const dailyFrame = getDailyFrame();
|
||||
const dailyFrameId = isomorphic[getId(dailyFrame)];
|
||||
let remainingRelations = $derived(
|
||||
dailyFrame.relations.size - frame.relations.size,
|
||||
);
|
||||
|
||||
type Move =
|
||||
| { type: "guess"; frameId: number; correct: boolean }
|
||||
| { type: "check"; formulaStr: string; valid: number };
|
||||
|
||||
let moves: Move[] = $state([]);
|
||||
let life = $derived(10 - moves.length);
|
||||
|
||||
let canGuess = $derived.by(() => {
|
||||
if (remainingRelations !== 0) return false;
|
||||
const frameId = isomorphic[getId(frame)];
|
||||
return !moves.some(
|
||||
(move) => move.type === "guess" && move.frameId === frameId,
|
||||
);
|
||||
});
|
||||
function guess() {
|
||||
if (!canGuess) return;
|
||||
const frameId = isomorphic[getId(frame)];
|
||||
moves.push({ type: "guess", frameId, correct: frameId === dailyFrameId });
|
||||
moves = [...moves];
|
||||
}
|
||||
|
||||
let canCheck = $derived.by(() => {
|
||||
if (!formula) return false;
|
||||
const formulaStr = prettyPrint(formula);
|
||||
return !moves.some(
|
||||
(move) => move.type === "check" && move.formulaStr === formulaStr,
|
||||
);
|
||||
});
|
||||
function check() {
|
||||
if (!canCheck || !formula) return;
|
||||
const formulaStr = prettyPrint(formula);
|
||||
const valid = validWorlds(dailyFrame, formula).length;
|
||||
moves.push({ type: "check", formulaStr, valid });
|
||||
moves = [...moves];
|
||||
formula = undefined;
|
||||
}
|
||||
const relationSize = dailyFrame.relations.size;
|
||||
const guess = (frameId: number) => isomorphic[frameId] === dailyFrameId;
|
||||
const check = (formula: Formula) => validWorlds(dailyFrame, formula).length;
|
||||
</script>
|
||||
|
||||
{#snippet sampleArrow()}
|
||||
<svg width="50" height="10" class="mt-[1px]">
|
||||
<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="rgb(var(--foreground))" />
|
||||
</marker>
|
||||
</defs>
|
||||
<path d="M 5 5 L 45 5" stroke="rgb(var(--foreground))" stroke-width="1" marker-end="url(#arrowhead)" />
|
||||
</svg>
|
||||
{/snippet}
|
||||
|
||||
<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">
|
||||
<div class="w-[300px] flex flex-col gap-4">
|
||||
<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" />
|
||||
{:else}
|
||||
<LuHeartCrack class="text-muted" />
|
||||
{/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>
|
||||
<FrameInput bind:frame />
|
||||
<span class="text-sm px-2 py-1 self-end flex items-center">
|
||||
{@render sampleArrow()} × {remainingRelations}
|
||||
</span>
|
||||
</div>
|
||||
|
||||
<button
|
||||
onclick={guess}
|
||||
disabled={!canGuess}
|
||||
class={[
|
||||
"rounded w-full p-1 text-background bg-primary font-bold flex items-center justify-center gap-2",
|
||||
!canGuess && "bg-muted cursor-not-allowed"
|
||||
]}>
|
||||
Guess! <span class="flex items-center font-normal">(<LuHeart size=14 class="mt-1 mr-[1px]"/> 1)</span>
|
||||
</button>
|
||||
</div>
|
||||
|
||||
<div class="flex flex-col items-center gap-2">
|
||||
<Katex math={math} />
|
||||
<FormulaInput bind:formula />
|
||||
<button
|
||||
onclick={check}
|
||||
disabled={!canCheck}
|
||||
class={[
|
||||
"rounded w-full p-1 text-background bg-primary font-bold flex items-center justify-center gap-2",
|
||||
!canCheck && "bg-muted cursor-not-allowed"
|
||||
]}>
|
||||
Check! <span class="flex items-center font-normal">(<LuHeart size=14 class="mt-1 mr-[1px]"/> 1)</span>
|
||||
</button>
|
||||
</div>
|
||||
|
||||
<div>
|
||||
<ul class="flex flex-col gap-2">
|
||||
{#each moves as move}
|
||||
<li>
|
||||
{#if move.type === "guess"}
|
||||
Guess({move.frameId}) = {move.correct}
|
||||
{/if}
|
||||
{#if move.type === "check"}
|
||||
Valid({move.formulaStr}) = {move.valid}
|
||||
{/if}
|
||||
</li>
|
||||
{/each}
|
||||
</ul>
|
||||
</div>
|
||||
</div>
|
||||
<Game relationSize={relationSize} guess={guess} check={check} />
|
||||
|
||||
<div class="w-[300px] prose prose-sm">
|
||||
<h2>Rules</h2>
|
||||
|
||||
@@ -3,8 +3,10 @@ import { type Formula, prettyPrint, tryParse } from "@cannorin/kripke";
|
||||
|
||||
let {
|
||||
formula = $bindable<Formula | undefined>(undefined),
|
||||
disabled = false,
|
||||
}: {
|
||||
formula?: Formula | undefined;
|
||||
disabled?: boolean | undefined;
|
||||
} = $props();
|
||||
|
||||
let input = $state(formula ? prettyPrint(formula) : "");
|
||||
@@ -26,4 +28,5 @@ $effect(() => {
|
||||
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"
|
||||
disabled={disabled}
|
||||
bind:value={input} />
|
||||
|
||||
@@ -3,7 +3,6 @@ import {
|
||||
type Frame,
|
||||
type Relation,
|
||||
type World,
|
||||
getFrame,
|
||||
left,
|
||||
reverse,
|
||||
right,
|
||||
@@ -12,9 +11,11 @@ import {
|
||||
import { type Vector, add, degree, rotate, sub, theta } from "./vector";
|
||||
|
||||
let {
|
||||
frame = $bindable<Frame>(getFrame(0)),
|
||||
frame = $bindable<Frame>({ relations: new Set() }),
|
||||
disabled = false,
|
||||
}: {
|
||||
frame?: Frame | undefined;
|
||||
disabled?: boolean | undefined;
|
||||
} = $props();
|
||||
|
||||
let selected: World | null = $state(null);
|
||||
@@ -114,7 +115,6 @@ function getPath(rel: Relation) {
|
||||
fill: rgb(var(--background));
|
||||
stroke: rgb(var(--foreground));
|
||||
stroke-width: 1;
|
||||
cursor: pointer;
|
||||
}
|
||||
.node.selected {
|
||||
stroke: rgb(var(--primary));
|
||||
@@ -124,7 +124,6 @@ function getPath(rel: Relation) {
|
||||
stroke: rgb(var(--foreground));
|
||||
stroke-width: 1;
|
||||
fill: none;
|
||||
cursor: pointer;
|
||||
marker-end: url(#arrowhead);
|
||||
}
|
||||
</style>
|
||||
@@ -151,8 +150,8 @@ function getPath(rel: Relation) {
|
||||
{#key rel}
|
||||
<path
|
||||
d={getPath(rel)}
|
||||
class="edge"
|
||||
onclick={(e) => handleEdgeClick(rel, e)}
|
||||
class={["edge", !disabled && "cursor-pointer"]}
|
||||
onclick={(e) => !disabled && handleEdgeClick(rel, e)}
|
||||
/>
|
||||
{/key}
|
||||
{/each}
|
||||
@@ -164,8 +163,8 @@ function getPath(rel: Relation) {
|
||||
cx={x}
|
||||
cy={y}
|
||||
r={radius.x}
|
||||
class="node {selected === w ? 'selected' : ''}"
|
||||
onclick={(e) => handleNodeClick(w, e)}
|
||||
class={["node", selected === w && "selected", !disabled && "cursor-pointer"]}
|
||||
onclick={(e) => !disabled && handleNodeClick(w, e)}
|
||||
/>
|
||||
{/each}
|
||||
</svg>
|
||||
|
||||
178
apps/web/src/routes/kripke/game.svelte
Normal file
178
apps/web/src/routes/kripke/game.svelte
Normal file
@@ -0,0 +1,178 @@
|
||||
<script lang="ts">
|
||||
import Katex from "$lib/components/katex.svelte";
|
||||
import {
|
||||
type Formula,
|
||||
type Frame,
|
||||
getFrame,
|
||||
getId,
|
||||
isomorphic,
|
||||
latexSymbols,
|
||||
prettyPrint,
|
||||
} from "@cannorin/kripke";
|
||||
import LuHeart from "lucide-svelte/icons/heart";
|
||||
import LuHeartCrack from "lucide-svelte/icons/heart-crack";
|
||||
import FormulaInput from "./formula-input.svelte";
|
||||
import FrameInput from "./frame-input.svelte";
|
||||
|
||||
export type GameStatus = "win" | "lose" | "playing";
|
||||
|
||||
export type Move =
|
||||
| { type: "guess"; frameId: number; correct: boolean }
|
||||
| { type: "check"; formulaStr: string; valid: number };
|
||||
|
||||
export type Props = {
|
||||
status?: GameStatus;
|
||||
moves?: Move[];
|
||||
relationSize: number;
|
||||
guess: (frameId: number) => boolean | Promise<boolean>;
|
||||
check: (formula: Formula) => number | Promise<number>;
|
||||
};
|
||||
|
||||
let {
|
||||
status = $bindable<GameStatus>("playing"),
|
||||
moves = $bindable<Move[]>([]),
|
||||
relationSize,
|
||||
guess: guessImpl,
|
||||
check: checkImpl,
|
||||
}: Props = $props();
|
||||
|
||||
let formula: Formula | undefined = $state(undefined);
|
||||
let frame: Frame = $state(getFrame(0));
|
||||
let math = $derived.by(() => {
|
||||
if (formula) return prettyPrint(formula, { symbols: latexSymbols });
|
||||
return "\\phantom{p}";
|
||||
});
|
||||
|
||||
let remainingRelations = $derived(relationSize - frame.relations.size);
|
||||
|
||||
let life = $derived(10 - moves.length);
|
||||
|
||||
$effect(() => {
|
||||
if (life <= 0) {
|
||||
status = "lose";
|
||||
return;
|
||||
}
|
||||
if (moves.some((move) => move.type === "guess" && move.correct)) {
|
||||
status = "win";
|
||||
return;
|
||||
}
|
||||
});
|
||||
|
||||
let canGuess = $derived.by(() => {
|
||||
if (status !== "playing" || remainingRelations !== 0) return false;
|
||||
const frameId = isomorphic[getId(frame)];
|
||||
return !moves.some(
|
||||
(move) => move.type === "guess" && move.frameId === frameId,
|
||||
);
|
||||
});
|
||||
|
||||
async function guess() {
|
||||
if (!canGuess) return;
|
||||
const frameId = getId(frame);
|
||||
const correct = await guessImpl(frameId);
|
||||
moves.push({ type: "guess", frameId, correct });
|
||||
moves = [...moves];
|
||||
}
|
||||
|
||||
let canCheck = $derived.by(() => {
|
||||
if (status !== "playing" || life === 1 || !formula) return false;
|
||||
const formulaStr = prettyPrint(formula);
|
||||
return !moves.some(
|
||||
(move) => move.type === "check" && move.formulaStr === formulaStr,
|
||||
);
|
||||
});
|
||||
|
||||
async function check() {
|
||||
if (!canCheck || !formula) return;
|
||||
const valid = await checkImpl(formula);
|
||||
const formulaStr = prettyPrint(formula, { symbols: latexSymbols });
|
||||
moves.push({ type: "check", formulaStr, valid });
|
||||
moves = [...moves];
|
||||
formula = undefined;
|
||||
}
|
||||
</script>
|
||||
|
||||
{#snippet sampleArrow()}
|
||||
<svg width="50" height="10" class="mt-[2px]">
|
||||
<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="rgb(var(--foreground))" />
|
||||
</marker>
|
||||
</defs>
|
||||
<path d="M 5 5 L 45 5" stroke="rgb(var(--foreground))" stroke-width="1" marker-end="url(#arrowhead)" />
|
||||
</svg>
|
||||
{/snippet}
|
||||
|
||||
<div class="w-[300px] flex flex-col gap-4">
|
||||
<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" />
|
||||
{:else}
|
||||
<LuHeartCrack class="text-muted" />
|
||||
{/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>
|
||||
<FrameInput bind:frame disabled={status !== "playing"} />
|
||||
<span class="text-sm px-2 py-1 self-end flex items-center">
|
||||
{@render sampleArrow()} × {remainingRelations}
|
||||
</span>
|
||||
</div>
|
||||
|
||||
<button
|
||||
onclick={guess}
|
||||
disabled={!canGuess}
|
||||
class={[
|
||||
"rounded w-full p-1 text-background font-bold flex items-center justify-center gap-2",
|
||||
canGuess ? "bg-primary" : "bg-muted cursor-not-allowed"
|
||||
]}>
|
||||
Guess! <span class="flex items-center font-normal">(<LuHeart size=14 class="mt-1 mr-[1px]"/> 1)</span>
|
||||
</button>
|
||||
</div>
|
||||
|
||||
<div class="flex flex-col items-center gap-2">
|
||||
<Katex math={math} />
|
||||
<FormulaInput bind:formula disabled={status !== "playing"} />
|
||||
<button
|
||||
onclick={check}
|
||||
disabled={!canCheck}
|
||||
class={[
|
||||
"rounded w-full p-1 text-background font-bold flex items-center justify-center gap-2",
|
||||
canCheck ? "bg-primary" : "bg-muted cursor-not-allowed"
|
||||
]}>
|
||||
{#if life <= 1}
|
||||
Can't Check <span class="font-normal">(Last Move!)</span>
|
||||
{:else}
|
||||
Check! <span class="flex items-center font-normal">(<LuHeart size=14 class="mt-1 mr-[1px]"/> 1)</span>
|
||||
{/if}
|
||||
</button>
|
||||
</div>
|
||||
|
||||
<div>
|
||||
<ul class="flex flex-col gap-2">
|
||||
{#each moves as move}
|
||||
<li>
|
||||
{#if move.type === "guess"}
|
||||
Guess({move.frameId}) = {move.correct}
|
||||
{/if}
|
||||
{#if move.type === "check"}
|
||||
Valid({move.formulaStr}) = {move.valid}
|
||||
{/if}
|
||||
</li>
|
||||
{/each}
|
||||
</ul>
|
||||
</div>
|
||||
</div>
|
||||
Reference in New Issue
Block a user