Add footnotes to typst export (#12)

* feat: add conditions to typst export

* fix: fix typst export

* fix: use predicate identifier value

* fix: allow empty lhs on create, fix typst footnotes

Author: WhySoBad

backend/src/lib/derivation/statement.rs

@@ -16,6 +16,7 @@ use super::formula::{Formula, Identifier};
     Serialize, Deserialize, Debug, Clone, ToSchema, IntoParams, Ord, PartialEq, PartialOrd, Eq,
 )]
 pub struct Statement {
+    #[serde(default)]
     pub lhs: Vec<Formula>,
     pub formula: Formula,
     pub sidecondition: Vec<SideCondition>,

frontend/src/lib/components/createExercise.tsx

@@ -98,7 +98,7 @@ const CreateExerciseForm = () => {
           createExerciseRequest: {
             statement: {
               formula: rhs,
-              lhs: lhs,
+              lhs: lhs || [],
               sidecondition: sideCon,
             },
           },

frontend/src/lib/components/exercise/exerciseInterface.tsx

@@ -45,7 +45,7 @@ const ExerciseInterface = ({ exercise }: ExerciseInterfaceProps) => {
         </Box>
       )}
       <Flex pt={0}>
-        {exercise.sidecondition.map((sidecondition, index) => (
+        {exercise.sidecondition?.map((sidecondition, index) => (
           <SideCondition sideCondition={sidecondition} key={index} />
         ))}
       </Flex>

frontend/src/lib/components/exerciseListElement.tsx

@@ -108,7 +108,7 @@ const ExerciseListElment = ({ exercise }: exerciseListElementProps) => {
           </Indicator>
         </Link>
       </Flex>
-      {exercise.exercise.sidecondition.map((sideCondition, i) => (
+      {exercise.exercise.sidecondition?.map((sideCondition, i) => (
         <SideCondition sideCondition={sideCondition} key={i} />
       ))}
     </Card>

frontend/src/lib/utils/export.ts

@@ -5,24 +5,56 @@ import { getTypstRuleByName } from "./rule";
 export function exportToTypst(root: NodeType, nodes: Array<NodeType>): string {
   const imp = `#import "@preview/curryst:0.5.0": rule, prooftree`;
   const page = `#set page(fill: none, width: auto, height: auto, margin: (x: 1em, y: 1em))`;
-  const prooftree = `#prooftree(${exportSubformula(root, nodes)})`;
-  return `${imp}\n${page}\n${prooftree}`;
+  const [formula, footnotes] = exportSubformula(root, nodes, 1);
+  const prooftree = `#prooftree(${formula})`;
+
+  const conditions = (root.statement.sidecondition || []).map(({ NotFree: { element, placeholder } }) => {
+    return `${element.value} "not occuring freely in" ${placeholder.value}`
+  });
+  conditions.push(...footnotes.map(([id, note]) => `$"${id}:" ${note}$`));
+
+  let typstStr = `${imp}\n${page}\n${prooftree}`;
+
+  if (conditions.length > 0) {
+    typstStr += "\n#set text(size: 7pt)"
+    typstStr += "\n#let footnotes(body) = context {\n\tpad(top: 4pt, line(length: measure(body).width, stroke: 0.5pt + black))\n\tbody\n}";
+    typstStr += `\n#footnotes[#stack(dir: ttb, spacing: 4pt, ${conditions.join(", ")})]`
+  }
+
+  return typstStr;
 }
 
-function exportSubformula(node: NodeType, nodes: Array<NodeType>): string {
-  const name = getTypstRuleByName(node.rule as Rules);
+function exportSubformula(node: NodeType, nodes: Array<NodeType>, footnoteNumber: number): [string, Array<[number, string]>] {
+  let name = getTypstRuleByName(node.rule as Rules, footnoteNumber);
   const lhs = node.statement.lhs.map(formulaToTypst).join(", ") || "emptyset";
   const current = formulaToTypst(node.statement.formula);
+  let currentFootnoteNumber = footnoteNumber;
+  const footnotes: Array<[number, string]> = [];
+  if (Array.isArray(name)) {
+    currentFootnoteNumber++;
+    const formula = node.statement.formula as Formula & { type: "Exists" | "Forall"};
+    const footnote = name[1]
+      .replaceAll("%%identifier%%", formula.body.identifier.value)
+      .replaceAll("%%lhs%%", lhs)
+      .replaceAll("%%rhs%%", current);
+    footnotes.push([footnoteNumber, footnote]);
+    name = name[0];
+  };
 
   const premisses = node.premisses
     .map((premisse) => {
       return nodes.find((node) => node.name === premisse);
     })
     .filter(Boolean)
-    .map((node) => exportSubformula(node as NodeType, nodes))
+    .map((node) => {
+      const [subformula, extraFootnotes] = exportSubformula(node as NodeType, nodes, currentFootnoteNumber);
+      currentFootnoteNumber += extraFootnotes.length;
+      footnotes.push(...extraFootnotes);
+      return subformula;
+    })
     .join(",\n");
 
-  return `rule(name: $${name}$,$${lhs} tack ${current}$,${premisses})`;
+  return [`rule(name: $${name}$,$${lhs} tack ${current}$,${premisses})`, footnotes];
 }
 
 function formulaToTypst(formula: Formula): string {
@@ -47,7 +79,7 @@ function formulaToTypst(formula: Formula): string {
       return `exists ${formulaToTypst({ type: "Ident", body: formula.body.identifier })}. ${formulaToTypst(formula.body.formula)}`;
     case "Predicate": {
       const vars = formula.body.identifiers.map((id) => id.value).join(", ");
-      return `${formula.body.identifier}(${vars})`;
+      return `${formula.body.identifier.value}(${vars})`;
     }
     default:
       return "";

frontend/src/lib/utils/rule.ts

@@ -41,7 +41,7 @@ export function getRuleByName(name: Rules): string {
   }
 }
 
-export function getTypstRuleByName(name: Rules): string {
+export function getTypstRuleByName(name: Rules, footnote: number): string | [string, string] {
   switch (name) {
     case "AndElimL":
       return 'and "EL"';
@@ -52,15 +52,15 @@ export function getTypstRuleByName(name: Rules): string {
     case "Ax":
       return '"AXIOM"';
     case "ExistsElim":
-      return 'exists "E**"';
+      return [`exists "E"^(${footnote})`, '%%identifier%% "does not occur freely in any formula in" %%lhs%% "or" %%rhs%%'];
     case "ExistsIntro":
       return 'exists "I"';
     case "FalseElim":
       return 'bot "E"';
     case "ForallElim":
       return 'forall "E"';
     case "ForallIntro":
-      return 'forall "I*"';
+      return [`forall "I"^$(${footnote})`, '%%identifier%% "does not occur freely in any formula in" %%lhs%%'];
     case "ImplElim":
       return 'arrow.r "E"';
     case "ImplIntro":
@@ -76,8 +76,8 @@ export function getTypstRuleByName(name: Rules): string {
     case "OrIntroR":
       return 'or "I"';
     case "AlphaExists":
-      return 'alpha exists "***"';
+      return [`alpha exists^(${footnote})`, '"the binding structure is preserved"'];
     case "AlphaForall":
-      return 'alpha forall "***"';
+      return [`alpha forall^(${footnote})`, '"the binding structure is preserved"'];
   }
 }