Skip to content

Commit 83a316f

Browse files
The-Ray-ManThe-Ray-Man
authored
fix and format (#15)
1 parent 277c83b commit 83a316f

File tree

3 files changed

+99
-57
lines changed

3 files changed

+99
-57
lines changed

‎frontend/src/lib/components/exercise/matcher.tsx‎

Lines changed: 52 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -26,9 +26,15 @@ import {
2626
Text,
2727
Textarea,
2828
TextInput,
29+
Tooltip,
2930
} from "@mantine/core";
3031
import { useListState } from "@mantine/hooks";
31-
import { IconCheck, IconPlus, IconX } from "@tabler/icons-react";
32+
import {
33+
IconCheck,
34+
IconInfoCircle,
35+
IconPlus,
36+
IconX,
37+
} from "@tabler/icons-react";
3238
import { UUID } from "crypto";
3339
import { useEffect, useState } from "react";
3440
import { v4 as uuidv4 } from "uuid";
@@ -39,6 +45,7 @@ import { getSideCondition } from "@/lib/utils/rule";
3945
import { RuleIdent } from "../rule/ruleParts";
4046
import Formula from "../formula/formula";
4147
import { cornersOfRectangle } from "@dnd-kit/core/dist/utilities/algorithms/helpers";
48+
import GrammarTooltip from "../grammarTooltip";
4249

4350
const Matcher = () => {
4451
const {
@@ -56,22 +63,17 @@ const Matcher = () => {
5663

5764
const current_node = nodes?.find((n) => n.name == target);
5865

59-
60-
6166
const sideConditionText = getSideCondition(current_rule!.name);
6267

6368
const allIdentifiers = getAllIdentifiers(current_rule!);
6469

65-
const [formulaIdentifier, formulaIdentifierHandler] = useListState<number>(
66-
allIdentifiers
67-
.filter((ident) => ident.type === "Formula")
68-
.map((ident) => ident.value),
69-
);
70-
const [elementIdentifier, elementIdentifierHandler] = useListState<string>(
71-
allIdentifiers
72-
.filter((ident) => ident.type === "Element")
73-
.map((ident) => ident.value),
74-
);
70+
const formulaIdentifier = allIdentifiers
71+
.filter((ident) => ident.type === "Formula")
72+
.map((ident) => ident.value);
73+
74+
const elementIdentifier = allIdentifiers
75+
.filter((ident) => ident.type === "Element")
76+
.map((ident) => ident.value);
7577

7678
const [formulaMatcher, formulaMatcherHandler] =
7779
useListState<FormulaMappingType>([]);
@@ -90,19 +92,11 @@ const Matcher = () => {
9092
const [applyError, setApplyError] = useState<string | undefined>(undefined);
9193

9294
useEffect(() => {
93-
if (counter == undefined) {
95+
if (counter == undefined || allIdentifiers == undefined) {
9496
setHighlighted(undefined);
9597
} else {
96-
if (counter < formulaIdentifier.length) {
97-
setHighlighted(formulaIdentifier[counter]);
98-
} else if (
99-
counter <
100-
formulaIdentifier.length + elementIdentifier.length
101-
) {
102-
setHighlighted(elementIdentifier[counter - formulaIdentifier.length]);
103-
} else {
104-
setHighlighted(undefined);
105-
}
98+
let identifier = allIdentifiers[counter];
99+
setHighlighted(identifier.value);
106100
}
107101
}, [counter]);
108102

@@ -135,6 +129,7 @@ const Matcher = () => {
135129
return !elementMatcher.find((m) => m.from === ident.value);
136130
}
137131
});
132+
console.log(identifier_index);
138133
if (identifier_index.length == 0) {
139134
setCounter(undefined);
140135
return;
@@ -161,20 +156,23 @@ const Matcher = () => {
161156

162157
const handleClick = (f: FormulaType) => {
163158
if (counter == undefined) return;
164-
if (counter < formulaIdentifier.length) {
165-
formulaMatcherHandler.append({ from: formulaIdentifier[counter], to: f });
166-
next();
167-
} else if (
168-
counter >= formulaIdentifier.length &&
169-
counter < formulaIdentifier.length + elementIdentifier.length
159+
let lhs_matching = allIdentifiers[counter];
160+
if (
161+
lhs_matching.type == "Element" &&
162+
f.type === "Ident" &&
163+
f.body.type === "Element"
170164
) {
171-
if (f.type === "Ident" && f.body.type === "Element") {
172-
elementMatcherHandler.append({
173-
from: elementIdentifier[counter - formulaIdentifier.length],
174-
to: f.body.value,
175-
});
176-
next();
177-
}
165+
elementMatcherHandler.append({
166+
from: lhs_matching.value,
167+
to: f.body.value,
168+
});
169+
next();
170+
return;
171+
}
172+
173+
if (lhs_matching.type === "Formula") {
174+
formulaMatcherHandler.append({ from: lhs_matching.value, to: f });
175+
next();
178176
}
179177
};
180178

@@ -333,12 +331,19 @@ const Matcher = () => {
333331
</Stack>
334332

335333
<Stack>
336-
<Box pt={"xs"}>
334+
<Text maw={300}>
335+
Match the highlighted part by clicking on the formula.
336+
</Text>
337+
<Text maw={300}>
338+
If you need a formula not present in your statement, use the input
339+
field.
340+
</Text>
341+
<Center pt={"xs"}>
337342
<Statement
338343
statement={current_node?.statement!}
339344
click={handleClick}
340345
/>
341-
</Box>
346+
</Center>
342347
<Group>
343348
<TextInput
344349
value={customFormula}
@@ -365,7 +370,7 @@ const Matcher = () => {
365370
/>
366371
)}
367372

368-
<Center pt={"md"}>
373+
<Center pt={"xl"}>
369374
<ButtonGroup>
370375
<Button
371376
variant="light"
@@ -379,7 +384,13 @@ const Matcher = () => {
379384
>
380385
Clear
381386
</Button>
382-
<Button disabled={counter != undefined} onClick={applyRule}>
387+
<Button
388+
disabled={
389+
counter != undefined ||
390+
(sideConditionText != undefined && !sideCondition)
391+
}
392+
onClick={applyRule}
393+
>
383394
Apply
384395
</Button>
385396
</ButtonGroup>

‎frontend/src/lib/utils/export.ts‎

Lines changed: 27 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -8,53 +8,69 @@ export function exportToTypst(root: NodeType, nodes: Array<NodeType>): string {
88
const [formula, footnotes] = exportSubformula(root, nodes, 1);
99
const prooftree = `#prooftree(${formula})`;
1010

11-
const conditions = (root.statement.sidecondition || []).map(({ NotFree: { element, placeholder } }) => {
12-
return `${element.value} "not occuring freely in" ${placeholder.value}`
13-
});
11+
const conditions = (root.statement.sidecondition || []).map(
12+
({ NotFree: { element, placeholder } }) => {
13+
return `${element.value} "not occuring freely in" ${placeholder.value}`;
14+
},
15+
);
1416
conditions.push(...footnotes.map(([id, note]) => `$"${id}:" ${note}$`));
1517

1618
let typstStr = `${imp}\n${page}\n${prooftree}`;
1719

1820
if (conditions.length > 0) {
19-
typstStr += "\n#set text(size: 7pt)"
20-
typstStr += "\n#let footnotes(body) = context {\n\tpad(top: 4pt, line(length: measure(body).width, stroke: 0.5pt + black))\n\tbody\n}";
21-
typstStr += `\n#footnotes[#stack(dir: ttb, spacing: 4pt, ${conditions.join(", ")})]`
21+
typstStr += "\n#set text(size: 7pt)";
22+
typstStr +=
23+
"\n#let footnotes(body) = context {\n\tpad(top: 4pt, line(length: measure(body).width, stroke: 0.5pt + black))\n\tbody\n}";
24+
typstStr += `\n#footnotes[#stack(dir: ttb, spacing: 4pt, ${conditions.join(", ")})]`;
2225
}
2326

2427
return typstStr;
2528
}
2629

27-
function exportSubformula(node: NodeType, nodes: Array<NodeType>, footnoteNumber: number): [string, Array<[number, string]>] {
30+
function exportSubformula(
31+
node: NodeType,
32+
nodes: Array<NodeType>,
33+
footnoteNumber: number,
34+
): [string, Array<[number, string]>] {
2835
let name = getTypstRuleByName(node.rule as Rules, footnoteNumber);
2936
const lhs = node.statement.lhs.map(formulaToTypst).join(", ") || "emptyset";
3037
const current = formulaToTypst(node.statement.formula);
3138
let currentFootnoteNumber = footnoteNumber;
3239
const footnotes: Array<[number, string]> = [];
3340
if (Array.isArray(name)) {
3441
currentFootnoteNumber++;
35-
const formula = node.statement.formula as Formula & { type: "Exists" | "Forall"};
42+
const formula = node.statement.formula as Formula & {
43+
type: "Exists" | "Forall";
44+
};
3645
const footnote = name[1]
3746
.replaceAll("%%identifier%%", formula.body.identifier.value)
3847
.replaceAll("%%lhs%%", lhs)
3948
.replaceAll("%%rhs%%", current);
4049
footnotes.push([footnoteNumber, footnote]);
4150
name = name[0];
42-
};
51+
}
4352

4453
const premisses = node.premisses
4554
.map((premisse) => {
4655
return nodes.find((node) => node.name === premisse);
4756
})
4857
.filter(Boolean)
4958
.map((node) => {
50-
const [subformula, extraFootnotes] = exportSubformula(node as NodeType, nodes, currentFootnoteNumber);
59+
const [subformula, extraFootnotes] = exportSubformula(
60+
node as NodeType,
61+
nodes,
62+
currentFootnoteNumber,
63+
);
5164
currentFootnoteNumber += extraFootnotes.length;
5265
footnotes.push(...extraFootnotes);
5366
return subformula;
5467
})
5568
.join(",\n");
5669

57-
return [`rule(name: $${name}$,$${lhs} tack ${current}$,${premisses})`, footnotes];
70+
return [
71+
`rule(name: $${name}$,$${lhs} tack ${current}$,${premisses})`,
72+
footnotes,
73+
];
5874
}
5975

6076
function formulaToTypst(formula: Formula): string {

‎frontend/src/lib/utils/rule.ts‎

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,10 @@ export function getRuleByName(name: Rules): string {
4141
}
4242
}
4343

44-
export function getTypstRuleByName(name: Rules, footnote: number): string | [string, string] {
44+
export function getTypstRuleByName(
45+
name: Rules,
46+
footnote: number,
47+
): string | [string, string] {
4548
switch (name) {
4649
case "AndElimL":
4750
return 'and "EL"';
@@ -52,15 +55,21 @@ export function getTypstRuleByName(name: Rules, footnote: number): string | [str
5255
case "Ax":
5356
return '"AXIOM"';
5457
case "ExistsElim":
55-
return [`exists "E"^(${footnote})`, '%%identifier%% "does not occur freely in any formula in" %%lhs%% "or" %%rhs%%'];
58+
return [
59+
`exists "E"^(${footnote})`,
60+
'%%identifier%% "does not occur freely in any formula in" %%lhs%% "or" %%rhs%%',
61+
];
5662
case "ExistsIntro":
5763
return 'exists "I"';
5864
case "FalseElim":
5965
return 'bot "E"';
6066
case "ForallElim":
6167
return 'forall "E"';
6268
case "ForallIntro":
63-
return [`forall "I"^$(${footnote})`, '%%identifier%% "does not occur freely in any formula in" %%lhs%%'];
69+
return [
70+
`forall "I"^$(${footnote})`,
71+
'%%identifier%% "does not occur freely in any formula in" %%lhs%%',
72+
];
6473
case "ImplElim":
6574
return 'arrow.r "E"';
6675
case "ImplIntro":
@@ -76,9 +85,15 @@ export function getTypstRuleByName(name: Rules, footnote: number): string | [str
7685
case "OrIntroR":
7786
return 'or "I"';
7887
case "AlphaExists":
79-
return [`alpha exists^(${footnote})`, '"the binding structure is preserved"'];
88+
return [
89+
`alpha exists^(${footnote})`,
90+
'"the binding structure is preserved"',
91+
];
8092
case "AlphaForall":
81-
return [`alpha forall^(${footnote})`, '"the binding structure is preserved"'];
93+
return [
94+
`alpha forall^(${footnote})`,
95+
'"the binding structure is preserved"',
96+
];
8297
}
8398
}
8499

0 commit comments

Comments
 (0)