Refactor Rules of Inference Playground
Update the Rules of Inference Playground to feature a single active drop zone in the center arena. The layout is changed to have premises and rules in separate columns above the arena. When a premise and rule are dropped, the system will now generate the resulting statements, removing the need for users to drag intermediate statements. The functionality to select a subset of premises for applying an inference rule has also been added. Intermediate statements below the arena have been removed.
This commit is contained in:
parent
3d2d2fdbff
commit
e0d0d73dc3
1 changed files with 194 additions and 134 deletions
|
|
@ -122,93 +122,122 @@ export default function RulesOfInferencePlayground() {
|
||||||
const [exampleId, setExampleId] = useState(EXAMPLES[0].id);
|
const [exampleId, setExampleId] = useState(EXAMPLES[0].id);
|
||||||
const example = useMemo(() => EXAMPLES.find((e) => e.id === exampleId)!, [exampleId]);
|
const example = useMemo(() => EXAMPLES.find((e) => e.id === exampleId)!, [exampleId]);
|
||||||
|
|
||||||
const [lines, setLines] = useState<Line[]>(Array.from({ length: 6 }, () => ({ status: "pending" })));
|
type Step = { used: string[]; rule: string; result: string };
|
||||||
|
|
||||||
|
const [steps, setSteps] = useState<Step[]>([]);
|
||||||
|
const [activePremises, setActivePremises] = useState<string[]>([]);
|
||||||
|
const [activeRule, setActiveRule] = useState<string | undefined>(undefined);
|
||||||
|
|
||||||
useEffect(() => {
|
useEffect(() => {
|
||||||
// Reset when example changes
|
// Reset when example changes
|
||||||
setLines(Array.from({ length: 6 }, () => ({ status: "pending" })));
|
setSteps([]);
|
||||||
|
setActivePremises([]);
|
||||||
|
setActiveRule(undefined);
|
||||||
}, [exampleId]);
|
}, [exampleId]);
|
||||||
|
|
||||||
const previousStatements = (upto: number) =>
|
const availableStatements = useMemo(
|
||||||
lines.slice(0, upto).map((l) => l.statement).filter(Boolean) as string[];
|
() => Array.from(new Set([...(example?.premises ?? []), ...steps.map((s) => s.result)])),
|
||||||
|
[example, steps]
|
||||||
|
);
|
||||||
|
|
||||||
const setLineStatement = (i: number, statement: string) => {
|
const reachedTarget = steps.some((s) => s.result === example.conclusion);
|
||||||
setLines((prev) => {
|
|
||||||
const next = [...prev];
|
|
||||||
next[i] = { ...next[i], statement, status: validateLine(i, { ...next[i], statement }) };
|
|
||||||
return next;
|
|
||||||
});
|
|
||||||
};
|
|
||||||
|
|
||||||
const setLineRule = (i: number, rule: string) => {
|
// Derivation logic for candidates based on the currently selected subset and rule
|
||||||
setLines((prev) => {
|
function deriveCandidates(rule?: string, selected: string[] = []): string[] {
|
||||||
const next = [...prev];
|
if (!rule || selected.length === 0) return [];
|
||||||
next[i] = { ...next[i], rule, status: validateLine(i, { ...next[i], rule }) };
|
|
||||||
return next;
|
|
||||||
});
|
|
||||||
};
|
|
||||||
|
|
||||||
const validateLine = (i: number, candidate?: Line): Line["status"] => {
|
|
||||||
const l = candidate ?? lines[i];
|
|
||||||
const stmt = l.statement?.trim();
|
|
||||||
const rule = l.rule;
|
|
||||||
|
|
||||||
// Premises allowed with no rule.
|
|
||||||
if (stmt && example.premises.includes(stmt) && !rule) return "correct";
|
|
||||||
|
|
||||||
if (!stmt || !rule) return "pending";
|
|
||||||
|
|
||||||
// Gather earlier statements
|
|
||||||
const prev = previousStatements(i);
|
|
||||||
|
|
||||||
// Validation rules specific to this example
|
|
||||||
if (example.id === "ex-resolution-1") {
|
if (example.id === "ex-resolution-1") {
|
||||||
switch (rule) {
|
switch (rule) {
|
||||||
case "distribution":
|
case "distribution": {
|
||||||
if (stmt === "p ∨ r" || stmt === "q ∨ r") {
|
// From (p ∧ q) ∨ r derive p ∨ r and q ∨ r
|
||||||
if (prev.includes("(p ∧ q) ∨ r")) return "correct";
|
if (selected.includes("(p ∧ q) ∨ r") && selected.length === 1) {
|
||||||
|
return ["p ∨ r", "q ∨ r"];
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
case "implication-elim":
|
}
|
||||||
if (stmt === "¬r ∨ s" && prev.includes("r → s")) return "correct";
|
case "implication-elim": {
|
||||||
|
// From r → s derive ¬r ∨ s
|
||||||
|
if (selected.includes("r → s") && selected.length === 1) {
|
||||||
|
return ["¬r ∨ s"];
|
||||||
|
}
|
||||||
break;
|
break;
|
||||||
case "resolution":
|
}
|
||||||
if (
|
case "resolution": {
|
||||||
stmt === "p ∨ s" &&
|
// From (p ∨ r) and (¬r ∨ s) derive (p ∨ s)
|
||||||
prev.includes("p ∨ r") &&
|
const hasPorR = selected.includes("p ∨ r");
|
||||||
prev.includes("¬r ∨ s")
|
const hasNotRorS = selected.includes("¬r ∨ s");
|
||||||
)
|
if (hasPorR && hasNotRorS && selected.length === 2) {
|
||||||
return "correct";
|
return ["p ∨ s"]; // Focused on intended path for this example
|
||||||
|
}
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
|
||||||
// Not validated
|
return [];
|
||||||
return "incorrect";
|
}
|
||||||
};
|
|
||||||
|
|
||||||
const handleStatementDrop = (lineIdx: number, e: React.DragEvent) => {
|
const candidates = useMemo(
|
||||||
|
() => deriveCandidates(activeRule, activePremises),
|
||||||
|
[activeRule, activePremises]
|
||||||
|
);
|
||||||
|
|
||||||
|
// Auto-apply when there is exactly one valid candidate
|
||||||
|
useEffect(() => {
|
||||||
|
if (candidates.length === 1 && activeRule && activePremises.length > 0) {
|
||||||
|
applyCandidate(candidates[0]);
|
||||||
|
}
|
||||||
|
// eslint-disable-next-line react-hooks/exhaustive-deps
|
||||||
|
}, [candidates.length]);
|
||||||
|
|
||||||
|
function applyCandidate(result: string) {
|
||||||
|
if (!activeRule || activePremises.length === 0) return;
|
||||||
|
|
||||||
|
// Validate again defensively
|
||||||
|
const valid = deriveCandidates(activeRule, activePremises).includes(result);
|
||||||
|
if (!valid) {
|
||||||
|
toast({
|
||||||
|
title: "Not quite",
|
||||||
|
description: "That rule doesn’t apply to the selected premises.",
|
||||||
|
variant: "destructive",
|
||||||
|
});
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
|
||||||
|
setSteps((prev) => [...prev, { used: [...activePremises], rule: activeRule, result }]);
|
||||||
|
setActivePremises([]);
|
||||||
|
setActiveRule(undefined);
|
||||||
|
|
||||||
|
if (result === example.conclusion) {
|
||||||
|
toast({ title: "Nice!", description: "You derived the target conclusion." });
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
function handlePremiseDrop(e: React.DragEvent) {
|
||||||
const data = parseDragData(e);
|
const data = parseDragData(e);
|
||||||
if (!data) return;
|
if (!data) return;
|
||||||
if (data.type === "premise" || data.type === "statement") {
|
if (data.type === "premise" || data.type === "statement") {
|
||||||
setLineStatement(lineIdx, data.value);
|
const value = data.value;
|
||||||
const status = validateLine(lineIdx, { ...lines[lineIdx], statement: data.value });
|
// Only allow from available set
|
||||||
if (status === "incorrect")
|
if (!availableStatements.includes(value)) return;
|
||||||
toast({ title: "Not quite", description: "That statement doesn’t follow from your chosen rule and prior lines.", variant: "destructive" });
|
setActivePremises((prev) => (prev.includes(value) ? prev : [...prev, value]));
|
||||||
|
}
|
||||||
}
|
}
|
||||||
};
|
|
||||||
|
|
||||||
const handleRuleDrop = (lineIdx: number, e: React.DragEvent) => {
|
function handleRuleDrop(e: React.DragEvent) {
|
||||||
const data = parseDragData(e);
|
const data = parseDragData(e);
|
||||||
if (!data) return;
|
if (!data) return;
|
||||||
if (data.type === "rule") {
|
if (data.type === "rule") setActiveRule(data.value);
|
||||||
setLineRule(lineIdx, data.value);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
const reset = () => {
|
||||||
|
setSteps([]);
|
||||||
|
setActivePremises([]);
|
||||||
|
setActiveRule(undefined);
|
||||||
};
|
};
|
||||||
|
|
||||||
const reset = () => setLines(Array.from({ length: 6 }, () => ({ status: "pending" })));
|
const removeActivePremise = (p: string) =>
|
||||||
|
setActivePremises((prev) => prev.filter((x) => x !== p));
|
||||||
const reachedTarget = lines.some((l) => l.statement === example.conclusion && l.status === "correct");
|
|
||||||
|
|
||||||
return (
|
return (
|
||||||
<div className="min-h-[70vh] space-y-4">
|
<div className="min-h-[70vh] space-y-4">
|
||||||
|
|
@ -236,95 +265,126 @@ export default function RulesOfInferencePlayground() {
|
||||||
</div>
|
</div>
|
||||||
</div>
|
</div>
|
||||||
|
|
||||||
{/* Arena */}
|
{/* Above the arena: two columns (Available statements | Rules) */}
|
||||||
<div className="grid grid-cols-1 gap-4 md:grid-cols-3">
|
<div className="grid grid-cols-1 gap-4 md:grid-cols-2">
|
||||||
{/* Left: Premises */}
|
<section aria-label="Available statements" className="space-y-2">
|
||||||
<section aria-label="Premises" className="space-y-2">
|
<h2 className="text-sm font-medium text-muted-foreground">Available statements</h2>
|
||||||
<h2 className="text-sm font-medium text-muted-foreground">Premises</h2>
|
|
||||||
<div className="space-y-2">
|
<div className="space-y-2">
|
||||||
|
<div className="space-y-2">
|
||||||
|
<p className="text-xs text-muted-foreground">Initial premises</p>
|
||||||
|
<div className="flex flex-wrap gap-2">
|
||||||
{example.premises.map((p) => (
|
{example.premises.map((p) => (
|
||||||
|
<DraggableChip key={p} label={p} onDragStart={(e) => onDragStart(e, "premise", p)} />
|
||||||
|
))}
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
{steps.length > 0 && (
|
||||||
|
<div className="space-y-2">
|
||||||
|
<p className="text-xs text-muted-foreground">Derived so far</p>
|
||||||
|
<div className="flex flex-wrap gap-2">
|
||||||
|
{steps.map((s, idx) => (
|
||||||
<DraggableChip
|
<DraggableChip
|
||||||
key={p}
|
key={`${s.result}-${idx}`}
|
||||||
label={p}
|
label={s.result}
|
||||||
onDragStart={(e) => onDragStart(e, "premise", p)}
|
onDragStart={(e) => onDragStart(e, "statement", s.result)}
|
||||||
/>
|
/>
|
||||||
))}
|
))}
|
||||||
</div>
|
</div>
|
||||||
</section>
|
</div>
|
||||||
|
|
||||||
{/* Center: Notepad lines with rule margin */}
|
|
||||||
<section aria-label="Workspace" className="relative">
|
|
||||||
<div className="rounded-lg border border-border bg-card p-2">
|
|
||||||
<div className="grid grid-rows-6 gap-2">
|
|
||||||
{Array.from({ length: 6 }).map((_, i) => {
|
|
||||||
const line = lines[i];
|
|
||||||
const ringCls =
|
|
||||||
line.status === "correct"
|
|
||||||
? "ring-1 ring-primary"
|
|
||||||
: line.status === "incorrect"
|
|
||||||
? "ring-1 ring-destructive"
|
|
||||||
: "";
|
|
||||||
return (
|
|
||||||
<div key={i} className="grid grid-cols-[1fr_112px] items-stretch gap-2">
|
|
||||||
{/* statement area (left) */}
|
|
||||||
<DropZone
|
|
||||||
onDrop={(e) => handleStatementDrop(i, e)}
|
|
||||||
className={"bg-background min-h-12 flex items-center " + ringCls}
|
|
||||||
>
|
|
||||||
<div className="px-2 text-sm text-foreground">
|
|
||||||
{line.statement ? (
|
|
||||||
<span>{line.statement}</span>
|
|
||||||
) : (
|
|
||||||
<span className="text-muted-foreground">Drop a statement or premise here</span>
|
|
||||||
)}
|
)}
|
||||||
</div>
|
</div>
|
||||||
</DropZone>
|
|
||||||
|
|
||||||
{/* rule margin (right) */}
|
|
||||||
<DropZone onDrop={(e) => handleRuleDrop(i, e)}>
|
|
||||||
<div className="flex h-full items-center justify-center rounded-md bg-muted/30 text-xs text-muted-foreground">
|
|
||||||
{line.rule ? <span>{line.rule}</span> : <span>Drop rule</span>}
|
|
||||||
</div>
|
|
||||||
</DropZone>
|
|
||||||
</div>
|
|
||||||
);
|
|
||||||
})}
|
|
||||||
</div>
|
|
||||||
|
|
||||||
{/* Target below last line */}
|
|
||||||
<div className="mt-3 rounded-md border border-border bg-background p-2 text-sm">
|
|
||||||
Target conclusion: <span className="font-medium text-foreground">{example.conclusion}</span>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
</section>
|
</section>
|
||||||
|
|
||||||
{/* Right: Rules */}
|
|
||||||
<section aria-label="Rules" className="space-y-2">
|
<section aria-label="Rules" className="space-y-2">
|
||||||
<h2 className="text-sm font-medium text-muted-foreground">Rules</h2>
|
<h2 className="text-sm font-medium text-muted-foreground">Inference rules</h2>
|
||||||
<div className="space-y-2">
|
<div className="space-y-2">
|
||||||
{example.rules.map((r) => (
|
{example.rules.map((r) => (
|
||||||
<div key={r.id} className="space-y-1">
|
<div key={r.id} className="space-y-1">
|
||||||
<DraggableChip
|
<DraggableChip label={r.id} onDragStart={(e) => onDragStart(e, "rule", r.id)} />
|
||||||
label={r.id}
|
{r.help && <p className="text-xs text-muted-foreground pl-1">{r.help}</p>}
|
||||||
onDragStart={(e) => onDragStart(e, "rule", r.id)}
|
|
||||||
/>
|
|
||||||
{r.help && (
|
|
||||||
<p className="text-xs text-muted-foreground pl-1">{r.help}</p>
|
|
||||||
)}
|
|
||||||
</div>
|
</div>
|
||||||
))}
|
))}
|
||||||
</div>
|
</div>
|
||||||
</section>
|
</section>
|
||||||
</div>
|
</div>
|
||||||
|
|
||||||
{/* Pool */}
|
{/* Arena (full width) */}
|
||||||
<section aria-label="Statements Pool" className="space-y-2">
|
<section aria-label="Workspace" className="space-y-3">
|
||||||
<h2 className="text-sm font-medium text-muted-foreground">Intermediate statements</h2>
|
<div className="rounded-lg border border-border bg-card p-3">
|
||||||
<div className="grid grid-cols-2 gap-2 md:grid-cols-4">
|
{/* History */}
|
||||||
{example.pool.map((s) => (
|
{steps.length > 0 && (
|
||||||
<DraggableChip key={s} label={s} onDragStart={(e) => onDragStart(e, "statement", s)} />
|
<div className="space-y-2 mb-3">
|
||||||
|
{steps.map((s, i) => (
|
||||||
|
<div key={i} className="grid grid-cols-1 md:grid-cols-[1fr_160px] items-center gap-2">
|
||||||
|
<div className="rounded-md border border-border bg-background p-2 text-sm text-foreground">
|
||||||
|
{s.result}
|
||||||
|
</div>
|
||||||
|
<div className="text-xs text-muted-foreground">
|
||||||
|
by <span className="font-medium">{s.rule}</span>
|
||||||
|
<span className="ml-1">from {s.used.join(", ")}</span>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
))}
|
))}
|
||||||
</div>
|
</div>
|
||||||
|
)}
|
||||||
|
|
||||||
|
{/* Active line */}
|
||||||
|
<div className="space-y-2">
|
||||||
|
<div className="grid grid-cols-1 md:grid-cols-[1fr_160px] items-stretch gap-2">
|
||||||
|
{/* premises selection zone */}
|
||||||
|
<DropZone onDrop={handlePremiseDrop} className="bg-background min-h-12">
|
||||||
|
<div className="flex flex-wrap items-center gap-2 p-2">
|
||||||
|
{activePremises.length === 0 ? (
|
||||||
|
<span className="text-sm text-muted-foreground">Drop premises here (you can drop multiple)</span>
|
||||||
|
) : (
|
||||||
|
activePremises.map((p) => (
|
||||||
|
<div
|
||||||
|
key={p}
|
||||||
|
className="flex items-center gap-2 rounded-md border border-border bg-card px-2 py-1 text-sm"
|
||||||
|
title={p}
|
||||||
|
>
|
||||||
|
<span className="text-foreground">{p}</span>
|
||||||
|
<button
|
||||||
|
className="rounded-md border border-transparent px-1 text-xs text-muted-foreground hover:text-foreground"
|
||||||
|
onClick={() => removeActivePremise(p)}
|
||||||
|
aria-label={`Remove ${p}`}
|
||||||
|
>
|
||||||
|
×
|
||||||
|
</button>
|
||||||
|
</div>
|
||||||
|
))
|
||||||
|
)}
|
||||||
|
</div>
|
||||||
|
</DropZone>
|
||||||
|
|
||||||
|
{/* rule zone */}
|
||||||
|
<DropZone onDrop={handleRuleDrop}>
|
||||||
|
<div className="flex h-full items-center justify-center rounded-md bg-muted/30 text-xs text-muted-foreground">
|
||||||
|
{activeRule ? <span>{activeRule}</span> : <span>Drop rule</span>}
|
||||||
|
</div>
|
||||||
|
</DropZone>
|
||||||
|
</div>
|
||||||
|
|
||||||
|
{/* Candidate results (if multiple) */}
|
||||||
|
{activeRule && activePremises.length > 0 && candidates.length > 1 && (
|
||||||
|
<div className="rounded-md border border-border bg-background p-2">
|
||||||
|
<p className="text-xs text-muted-foreground mb-2">Possible conclusions:</p>
|
||||||
|
<div className="flex flex-wrap gap-2">
|
||||||
|
{candidates.map((c) => (
|
||||||
|
<Button key={c} size="sm" variant="outline" onClick={() => applyCandidate(c)}>
|
||||||
|
{c}
|
||||||
|
</Button>
|
||||||
|
))}
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
)}
|
||||||
|
|
||||||
|
{/* Target below */}
|
||||||
|
<div className="rounded-md border border-border bg-background p-2 text-sm">
|
||||||
|
Target conclusion: <span className="font-medium text-foreground">{example.conclusion}</span>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
</section>
|
</section>
|
||||||
</div>
|
</div>
|
||||||
);
|
);
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue