Merge pull request #16 from cannorin/kripke-refactor

kripke: refactor
This commit is contained in:
cannorin
2025-02-21 08:55:25 +09:00
committed by GitHub
14 changed files with 134 additions and 100 deletions

View File

@@ -21,5 +21,6 @@
}, },
"[jsonc]": { "[jsonc]": {
"editor.defaultFormatter": "biomejs.biome" "editor.defaultFormatter": "biomejs.biome"
} },
"biome.lspBin": "./node_modules/@biomejs/biome/bin/biome"
} }

View File

@@ -1,7 +1,11 @@
import type { SeoProps } from "$components/seo"; import type { SeoProps } from "$components/seo";
import { dailySeed } from "./lib/system";
export async function load() { export async function load() {
const seed = dailySeed();
return { return {
seed,
seo: { seo: {
title: "KRIPKE - cannorin.net", title: "KRIPKE - cannorin.net",
description: "KRIPKE - WORDLE, but for Kripke frames!", description: "KRIPKE - WORDLE, but for Kripke frames!",

View File

@@ -6,15 +6,17 @@ import LuRotateCw from "lucide-svelte/icons/rotate-cw";
import LuX from "lucide-svelte/icons/x"; import LuX from "lucide-svelte/icons/x";
import { onMount } from "svelte"; import { onMount } from "svelte";
import FrameInput from "./frame-input.svelte"; import FrameInput from "./components/frame-input.svelte";
import Game, { type GameStatus, type Move } from "./game.svelte"; import Game, { type GameStatus } from "./components/game.svelte";
import Rules from "./rules.svelte"; import Rules from "./components/rules.svelte";
import Share from "./share.svelte"; import Share from "./components/share.svelte";
import { getFrameBySeed, getTimeUntilNextGame } from "./lib/system";
import { daily } from "./store"; import { daily } from "./store";
import { getDailyFrame, getTimeUntilNextGame } from "./system";
const { id, frame } = getDailyFrame(); let { data } = $props();
const seed = data.seed;
const { id, frame } = getFrameBySeed(seed);
const guess = (frameId: number) => isomorphic[frameId] === id; const guess = (frameId: number) => isomorphic[frameId] === id;
const check = (formula: Formula) => validWorlds(frame, formula).length; const check = (formula: Formula) => validWorlds(frame, formula).length;
const getAnswer = () => id; const getAnswer = () => id;
@@ -46,7 +48,10 @@ onMount(() => {
<span class="font-bold">Daily Challenge: </span> <span class="font-bold">Daily Challenge: </span>
{timeUntilNextGame.hours}:{timeUntilNextGame.minutes}:{timeUntilNextGame.seconds} until the next game. {timeUntilNextGame.hours}:{timeUntilNextGame.minutes}:{timeUntilNextGame.seconds} until the next game.
</h2> </h2>
<Game bind:moves={$daily.moves} bind:status relationSize={relationSize} guess={guess} check={check} getAnswer={getAnswer} /> <Game
bind:moves={$daily.moves} bind:status relationSize={relationSize}
guess={guess} check={check} getAnswer={getAnswer}
onShare={() => { dialogOpen = true; }} />
</section> </section>
<section class="w-[300px] prose prose-sm"> <section class="w-[300px] prose prose-sm">
@@ -57,7 +62,7 @@ onMount(() => {
<li>You can also play <a href="/kripke/random">Random Challenge</a>.</li> <li>You can also play <a href="/kripke/random">Random Challenge</a>.</li>
</ul> </ul>
<Rules /> <Rules relationSize={relationSize} />
</section> </section>
</div> </div>
</main> </main>
@@ -80,7 +85,7 @@ onMount(() => {
</Dialog.Header> </Dialog.Header>
<div class="flex flex-col items-center w-fit rounded bg-background mx-auto"> <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> <span class="text-xs text-muted self-start px-2 py-1">id: {answerId}, seed: <a class="text-primary underline font-medium" href="/kripke/random/{seed}">{seed}</a></span>
<FrameInput class="pb-6" disabled width={250} height={250} frame={frame} /> <FrameInput class="pb-6" disabled width={250} height={250} frame={frame} />
</div> </div>
@@ -88,8 +93,7 @@ onMount(() => {
<div class="flex flex-col md:flex-row gap-2 w-full justify-end"> <div class="flex flex-col md:flex-row gap-2 w-full justify-end">
<Share date={$daily.date} moves={$daily.moves} status={status} /> <Share date={$daily.date} moves={$daily.moves} status={status} />
<Button <Button
href="/kripke/random" href="/kripke/random">
data-sveltekit-reload>
<LuRotateCw class="w-4 h-4 mt-[2px]" /> Play Random Challenge <LuRotateCw class="w-4 h-4 mt-[2px]" /> Play Random Challenge
</Button> </Button>
<Button <Button

View File

@@ -9,7 +9,7 @@ import {
worlds, worlds,
} from "@cannorin/kripke"; } from "@cannorin/kripke";
import type { SVGAttributes } from "svelte/elements"; import type { SVGAttributes } from "svelte/elements";
import { type Vector, add, degree, rotate, sub, theta } from "./vector"; import { type Vector, add, degree, rotate, sub, theta } from "../lib/vector";
export interface FrameInputProps extends SVGAttributes<SVGElement> { export interface FrameInputProps extends SVGAttributes<SVGElement> {
frame?: Frame | undefined; frame?: Frame | undefined;
@@ -116,7 +116,10 @@ function getPath(rel: Relation) {
} }
</script> </script>
<style> <!-- svelte-ignore a11y_click_events_have_key_events -->
<!-- svelte-ignore a11y_no_static_element_interactions -->
<svg width={width ?? 250} height={height ?? 250} {...rest} viewBox="0,0,250,250" onclick={handleSvgClick} xmlns="http://www.w3.org/2000/svg">
<style>
.node { .node {
fill: rgb(var(--background)); fill: rgb(var(--background));
stroke: rgb(var(--foreground)); stroke: rgb(var(--foreground));
@@ -132,11 +135,10 @@ function getPath(rel: Relation) {
fill: none; fill: none;
marker-end: url(#arrowhead); marker-end: url(#arrowhead);
} }
</style> .arrowhead {
fill: rgb(var(--foreground));
<!-- svelte-ignore a11y_click_events_have_key_events --> }
<!-- svelte-ignore a11y_no_static_element_interactions --> </style>
<svg width={width ?? 250} height={height ?? 250} {...rest} viewBox="0,0,250,250" onclick={handleSvgClick}>
<defs> <defs>
<marker <marker
id="arrowhead" id="arrowhead"
@@ -148,7 +150,7 @@ function getPath(rel: Relation) {
orient="auto" orient="auto"
markerUnits="strokeWidth" markerUnits="strokeWidth"
> >
<path d="M0,0 L0,10 L10,5 z" fill="rgb(var(--foreground))" /> <path class="arrowhead" d="M0,0 L0,10 L10,5 z" />
</marker> </marker>
</defs> </defs>

View File

@@ -31,6 +31,7 @@ export type Props = {
guess: (frameId: number) => boolean | Promise<boolean>; guess: (frameId: number) => boolean | Promise<boolean>;
check: (formula: Formula) => number | Promise<number>; check: (formula: Formula) => number | Promise<number>;
getAnswer: () => number | Promise<number>; getAnswer: () => number | Promise<number>;
onShare?: () => void;
}; };
let { let {
@@ -40,13 +41,16 @@ let {
guess: guessImpl, guess: guessImpl,
check: checkImpl, check: checkImpl,
getAnswer, getAnswer,
onShare,
}: Props = $props(); }: Props = $props();
let formula: Formula | undefined = $state(undefined); let formula: Formula | undefined = $state(undefined);
let formulaStr = $derived( let formulaStr = $derived(
formula ? prettyPrint(formula, { symbols: latexSymbols }) : "", formula ? prettyPrint(formula, { symbols: latexSymbols }) : "",
); );
let frame: Frame = $state(getFrame(0)); let frame: Frame = $state(
getFrame(moves.findLast((move) => move.type === "guess")?.frameId ?? 0),
);
let frameId = $derived(getId(frame)); let frameId = $derived(getId(frame));
let remainingRelations = $derived(relationSize - frame.relations.size); let remainingRelations = $derived(relationSize - frame.relations.size);
@@ -200,12 +204,20 @@ const colors: Record<number, string> = {
</li> </li>
{/if} {/if}
{#if status === "win"} {#if status === "win"}
<li class="flex flex-col items-center gap-2 rounded bg-green-700 text-background p-5 animate-fade-in"> <li>
<button
class="flex flex-col items-center gap-2 rounded bg-green-700 text-background p-5 animate-fade-in w-full"
onclick={() => onShare?.()}>
<p class="text-xl font-bold">YOU WIN!</p> <p class="text-xl font-bold">YOU WIN!</p>
<p class="sr-only">Open result screen</p>
</button>
</li> </li>
{:else if status === "lose"} {:else if status === "lose"}
{#await getAnswer() then answerId} {#await getAnswer() then answerId}
<li class="flex flex-col gap-2 rounded bg-foreground text-background p-5 animate-fade-in"> <li>
<button
class="flex flex-col gap-2 rounded bg-foreground text-background p-5 animate-fade-in w-full"
onclick={() => onShare?.()}>
<div> <div>
<p class="text-xl font-bold">YOU LOSE!</p> <p class="text-xl font-bold">YOU LOSE!</p>
<p class="text-sm">The answer was:</p> <p class="text-sm">The answer was:</p>
@@ -214,6 +226,8 @@ const colors: Record<number, string> = {
<span class="text-xs text-muted self-start px-2 py-1">id: {answerId}</span> <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)} /> <FrameInput class="pb-6" disabled width={250} height={250} frame={getFrame(answerId)} />
</div> </div>
<p class="sr-only">Open result screen</p>
</button>
</li> </li>
{/await} {/await}
{/if} {/if}

View File

@@ -2,8 +2,11 @@
import Katex from "$lib/components/katex.svelte"; import Katex from "$lib/components/katex.svelte";
import LuHeart from "lucide-svelte/icons/heart"; import LuHeart from "lucide-svelte/icons/heart";
let { relationSize }: { relationSize: number } = $props();
const frame = "\\footnotesize \\mathcal{F} = \\left<W, R\\right>"; const frame = "\\footnotesize \\mathcal{F} = \\left<W, R\\right>";
const numberConstraint = "\\footnotesize |W| = 4"; const worldConstraint = "\\footnotesize |W| = 4";
const relationConstraint = `\\footnotesize |R| = ${relationSize}`;
const f = "\\footnotesize \\mathcal{F}"; const f = "\\footnotesize \\mathcal{F}";
const validCount = const validCount =
"\\footnotesize \\mathrm{N}(\\varphi) = \\bigl| \\Set{ w \\in W | \\forall \\mathop{\\Vdash}\\, (w \\Vdash \\varphi) } \\bigr|"; "\\footnotesize \\mathrm{N}(\\varphi) = \\bigl| \\Set{ w \\in W | \\forall \\mathop{\\Vdash}\\, (w \\Vdash \\varphi) } \\bigr|";
@@ -12,11 +15,8 @@ const validCount =
<h2>Rules</h2> <h2>Rules</h2>
<ul> <ul>
<li> <li>
A Kripke frame with 4 worlds is generated: A <a href="https://en.wikipedia.org/wiki/Kripke_semantics" target="_blank" rel="noopener noreferrer">Kripke frame</a> with 4 worlds and {relationSize} relation(s) is generated:
<Katex math={frame} />, where <Katex math={numberConstraint} />. <Katex math={frame} />, where <Katex math={worldConstraint} /> and <Katex math={relationConstraint} />.
</li>
<li>
The game tells you how many accessibility relations are in the frame <Katex math={f} />, but not the exact shape of it.
</li> </li>
<li> <li>
You have a total of 10 moves <span class="inline-flex items-center max-w-fit">(<LuHeart aria-label="♡" size=12 class="mt-1"/>)</span>. You have a total of 10 moves <span class="inline-flex items-center max-w-fit">(<LuHeart aria-label="♡" size=12 class="mt-1"/>)</span>.
@@ -32,7 +32,7 @@ const validCount =
</li> </li>
<li> <li>
Guess the Kripke frame. Guess the Kripke frame.
If your frame is equal or isomorphic to the secret frame <Katex math={f} />, you win. If your frame is equal or isomorphic to <Katex math={f} />, you win.
</li> </li>
</ul> </ul>
</li> </li>

View File

@@ -35,7 +35,7 @@ let shareText = $derived.by(() => {
${history} ${status === "win" ? moves.length : "X"}/10 ${history} ${status === "win" ? moves.length : "X"}/10
https://www.cannorin.net/kripke${seed ? `/random?seed=${seed}` : ""}`; https://www.cannorin.net/kripke${seed ? `/random/${seed}` : ""}`;
return encodeURIComponent(text); return encodeURIComponent(text);
}); });

View File

@@ -20,26 +20,17 @@ function cyrb53(str: string, seed = 0): number {
export const date = () => new Date().toISOString().split("T")[0]; export const date = () => new Date().toISOString().split("T")[0];
export function getDailyFrame() { export const dailySeed = () => {
// Use UTC ISO string so it's consistent across time zones
const dateStr = date(); const dateStr = date();
const hash = cyrb53(dateStr); return cyrb53(dateStr) % 0x100000000;
const index = hash % nontrivials.length; };
return {
date: dateStr,
id: nontrivials[index],
frame: getFrame(nontrivials[index]),
};
}
export const randomSeed = () => Math.floor(Math.random() * 0x100000000); export const randomSeed = () => Math.floor(Math.random() * 0x100000000);
export function getRandomFrame(seed?: number) { export function getFrameBySeed(seed: number) {
const actualSeed = seed ?? randomSeed();
const hash = cyrb53("random", seed); const hash = cyrb53("random", seed);
const index = hash % nontrivials.length; const index = hash % nontrivials.length;
return { return {
seed: actualSeed,
id: nontrivials[index], id: nontrivials[index],
frame: getFrame(nontrivials[index]), frame: getFrame(nontrivials[index]),
}; };

View File

@@ -1,5 +1,5 @@
import type { SeoProps } from "$components/seo"; import { redirect } from "@sveltejs/kit";
import { randomSeed } from "../system.js"; import { randomSeed } from "../lib/system";
export async function load({ url }) { export async function load({ url }) {
const seedStr = url.searchParams.get("seed"); const seedStr = url.searchParams.get("seed");
@@ -13,20 +13,5 @@ export async function load({ url }) {
return randomSeed(); return randomSeed();
} }
})(); })();
redirect(302, `/kripke/random/${seed}`);
return {
seed,
seo: {
title: "KRIPKE (random challenge) - cannorin.net",
description: "KRIPKE - WORDLE, but for Kripke frames!",
openGraph: {
title: "KRIPKE (random challenge) - cannorin.net",
description: "KRIPKE - WORDLE, but for Kripke frames!",
},
twitter: {
title: "KRIPKE (random challenge) - cannorin.net",
description: "KRIPKE - WORDLE, but for Kripke frames!",
},
} as SeoProps,
};
} }

View File

@@ -0,0 +1,31 @@
import type { SeoProps } from "$components/seo";
import { error } from "@sveltejs/kit";
export async function load({ params }) {
const seedStr = params.seed;
const seed = (() => {
try {
const seed = Number.parseInt(seedStr);
if (!Number.isSafeInteger(seed)) throw error(400);
return seed;
} catch {
throw error(400);
}
})();
return {
seed,
seo: {
title: `KRIPKE (seed ${seed}) - cannorin.net`,
description: "KRIPKE - WORDLE, but for Kripke frames!",
openGraph: {
title: `KRIPKE (seed ${seed}) - cannorin.net`,
description: "KRIPKE - WORDLE, but for Kripke frames!",
},
twitter: {
title: `KRIPKE (seed ${seed}) - cannorin.net`,
description: "KRIPKE - WORDLE, but for Kripke frames!",
},
} as SeoProps,
};
}

View File

@@ -5,15 +5,15 @@ import { type Formula, isomorphic, validWorlds } from "@cannorin/kripke";
import LuRotateCw from "lucide-svelte/icons/rotate-cw"; import LuRotateCw from "lucide-svelte/icons/rotate-cw";
import LuX from "lucide-svelte/icons/x"; import LuX from "lucide-svelte/icons/x";
import FrameInput from "../frame-input.svelte"; import FrameInput from "../../components/frame-input.svelte";
import Game, { type GameStatus, type Move } from "../game.svelte"; import Game, { type GameStatus, type Move } from "../../components/game.svelte";
import Rules from "../rules.svelte"; import Rules from "../../components/rules.svelte";
import Share from "../share.svelte"; import Share from "../../components/share.svelte";
import { getRandomFrame } from "../system"; import { getFrameBySeed } from "../../lib/system";
let { data } = $props(); let { data } = $props();
const seed = data.seed; const seed = data.seed;
const { id, frame } = getRandomFrame(seed); const { id, frame } = getFrameBySeed(seed);
const guess = (frameId: number) => isomorphic[frameId] === id; const guess = (frameId: number) => isomorphic[frameId] === id;
const check = (formula: Formula) => validWorlds(frame, formula).length; const check = (formula: Formula) => validWorlds(frame, formula).length;
const getAnswer = () => id; const getAnswer = () => id;
@@ -29,7 +29,7 @@ $effect(() => {
</script> </script>
{#snippet seedNumber()} {#snippet seedNumber()}
<a class="text-primary font-medium underline" href={`/kripke/random?seed=${seed}`}>{seed}</a> <a class="text-primary font-medium underline" href={`/kripke/random/${seed}`}>{seed}</a>
{/snippet} {/snippet}
<main class="flex flex-col min-h-screen max-w-full items-center gap-12 lg:gap-16 py-8"> <main class="flex flex-col min-h-screen max-w-full items-center gap-12 lg:gap-16 py-8">
@@ -41,19 +41,22 @@ $effect(() => {
<span class="font-bold">Random Challenge</span> <span class="font-bold">Random Challenge</span>
<span>(seed: {@render seedNumber()})</span> <span>(seed: {@render seedNumber()})</span>
</h2> </h2>
<Game bind:moves bind:status relationSize={relationSize} guess={guess} check={check} getAnswer={getAnswer} /> <Game
bind:moves bind:status relationSize={relationSize}
guess={guess} check={check} getAnswer={getAnswer}
onShare={() => { dialogOpen = true; }}/>
</section> </section>
<section class="w-[300px] prose prose-sm"> <section class="w-[300px] prose prose-sm">
<h2>Random Challenge!</h2> <h2>Random Challenge!</h2>
<ul> <ul>
<li>The answer of the game is determined by a seed number {@render seedNumber()}, which changes on every reload.</li> <li>The answer of the game is determined by a seed number {@render seedNumber()}.</li>
<li>You can right-click on the seed number to obtain a permalink to this exact game.</li> <li>You can right-click on the seed number to obtain a permalink to this exact game.</li>
<li>Unlike Daily Challenge, the progress of the game does not persist.</li> <li>Unlike Daily Challenge, the progress of the game does not persist.</li>
<li>You can also play <a href="/kripke">Daily Challenge</a>, if you have not yet.</li> <li>You can also play <a href="/kripke">Daily Challenge</a>, if you have not yet.</li>
</ul> </ul>
<Rules /> <Rules relationSize={relationSize} />
</section> </section>
</div> </div>
</main> </main>
@@ -76,7 +79,7 @@ $effect(() => {
</Dialog.Header> </Dialog.Header>
<div class="flex flex-col items-center w-fit rounded bg-background mx-auto"> <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> <span class="text-xs text-muted self-start px-2 py-1">id: {answerId}, seed: <a class="text-primary underline font-medium" href="/kripke/random/{seed}">{seed}</a></span>
<FrameInput class="pb-6" disabled width={250} height={250} frame={frame} /> <FrameInput class="pb-6" disabled width={250} height={250} frame={frame} />
</div> </div>
@@ -84,8 +87,7 @@ $effect(() => {
<div class="flex flex-col md:flex-row gap-2 w-full justify-end"> <div class="flex flex-col md:flex-row gap-2 w-full justify-end">
<Share seed={seed} moves={moves} status={status} /> <Share seed={seed} moves={moves} status={status} />
<Button <Button
href="/kripke/random" href="/kripke/random">
data-sveltekit-reload>
<LuRotateCw class="w-4 h-4 mt-[2px]" /> Play New Game <LuRotateCw class="w-4 h-4 mt-[2px]" /> Play New Game
</Button> </Button>
<Button <Button

View File

@@ -1,6 +1,6 @@
import { persisted } from "svelte-persisted-store"; import { persisted } from "svelte-persisted-store";
import type { Move } from "./game.svelte"; import type { Move } from "./components/game.svelte";
import { date } from "./system"; import { date } from "./lib/system";
export type Daily = { export type Daily = {
date: string; date: string;