Merge pull request #29 from Paper-Proof/parser

Fix parser to correctly link calc example

Examples.lean

@@ -11,8 +11,14 @@ import Mathlib.Algebra.GCDMonoid.Multiset
 import Lean
 import Paperproof
 
+theorem simple_ex (n m : ℕ)
+  (h1 : ∀ {a b : Nat}, a + b = b + a)
+  (h2 : ∀ {a b : Nat}, a = b + b):
+    n + m = m + n := by
+  simp [h1, h2]
+
 example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by
-  have h3 : m + 3 ≤ 9 := by calc
+  have h3 := calc
       m + 3 ≤ 2 * n - 1 := by gcongr
       _ ≤ 2 * 5 - 1 := by gcongr
       _ = 9 := by norm_num

app/src/services/updateUI/services/buildProofTree/services/CreateElement/createArrows.ts

@@ -75,13 +75,29 @@ const createArrows = (shared: UIShared): UIElement => {
         });
 
         // 3. Draw arrows between this tactic and `have` windows
-        if (tactic.haveWindowId && tactic.hypArrows[0]) {
-          const window = getWindowByHypId(shared.proofTree, tactic.hypArrows[0].toIds[0]);
-          if (!window) return
-          const fromWindowId = findIdInApp(shared.editor, CreateId.window(tactic.haveWindowId));
-          const toTacticId = findIdInApp(shared.editor, CreateId.hypTactic(tactic.id, null, window.id));
-          if (!fromWindowId || !toTacticId) return
-          DrawShape.arrow(shared.editor, fromWindowId, toTacticId, "goalArrow");
+        for (const haveWindowId of tactic.haveWindowIds) {
+          if (tactic.hypArrows[0]) {
+            const window = getWindowByHypId(
+              shared.proofTree,
+              tactic.hypArrows[0].toIds[0]
+            );
+            if (!window) return;
+            const fromWindowId = findIdInApp(
+              shared.editor,
+              CreateId.window(haveWindowId)
+            );
+            const toTacticId = findIdInApp(
+              shared.editor,
+              CreateId.hypTactic(tactic.id, null, window.id)
+            );
+            if (!fromWindowId || !toTacticId) return;
+            DrawShape.arrow(
+              shared.editor,
+              fromWindowId,
+              toTacticId,
+              "goalArrow"
+            );
+          }
         }
       });
     }

app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts

@@ -128,9 +128,11 @@ const createWindowInsides = (shared: UIShared, parentId: TLParentId | undefined,
             CreateId.hypTactic(tactic.id, hypArrow.fromId, window.id)
           );
 
-          const haveWindows = shared.proofTree.windows
-            .filter(w => tactic.haveWindowId === w.id)
-            .map(w => createWindow(shared, parentId, w, depth + 1));
+          const haveWindows = tactic.haveWindowIds
+            .flatMap(
+              (id) => shared.proofTree.windows.find((w) => w.id === id) ?? []
+            )
+            .map((w) => createWindow(shared, parentId, w, depth + 1));
           const hTree: UIHypTree = {
             tactic: vStack(0, [hStack(shared.inBetweenMargin, haveWindows), tacticNode]),
             level,

app/src/services/updateUI/services/converter.ts

@@ -216,7 +216,11 @@ const addToEquivalentIds = (pretty : ConvertedProofTree, beforeId : string, afte
   }
 }
 
-const handleTacticApp = (tactic: LeanTactic, pretty : ConvertedProofTree, haveWindowId : string | null = null) => {
+const handleTacticApp = (
+  tactic: LeanTactic,
+  pretty: ConvertedProofTree,
+  haveWindowIds: string[] = []
+) => {
   // We assume `tactic.goalsBefore[0]` is always the goal the tactic worked on!
   // Is it fair to assume? So far seems good.
   const mainGoalBefore = tactic.goalsBefore[0];
@@ -245,19 +249,20 @@ const handleTacticApp = (tactic: LeanTactic, pretty : ConvertedProofTree, haveWi
     const nextGoal = tactic.goalsAfter[0];
 
     pretty.tactics.push({
-      id           : newTacticId(),
-      text         : tactic.tacticString,
-      dependsOnIds : tactic.tacticDependsOn,
-      goalArrows   : [],
-      hypArrows    : [],
+      id: newTacticId(),
+      text: tactic.tacticString,
+      dependsOnIds: tactic.tacticDependsOn,
+      goalArrows: [],
+      hypArrows: [],
       // success arrows are better not drawn (noisy!), we should just mark the tactic as 🎉.
       // .dependsOnIds will convey all the information we want to see.
-      isSuccess    : nextGoal ? '🎉' : 'For all goals, 🎉!',
+      isSuccess: nextGoal ? "🎉" : "For all goals, 🎉!",
       successGoalId: mainGoalBefore.id,
+      haveWindowIds,
     });
   }
   // - we updated the goal!
-  else if (relevantGoalsAfter.length === 1) { 
+  else if (relevantGoalsAfter.length === 1) {
     const updatedGoal = relevantGoalsAfter[0];
 
     // 1. Draw goal nodes and arrows
@@ -273,47 +278,57 @@ const handleTacticApp = (tactic: LeanTactic, pretty : ConvertedProofTree, haveWi
       currentWindow.goalNodes.push({
         text: updatedGoal.type,
         name: updatedGoal.username,
-        id  : updatedGoal.id
+        id: updatedGoal.id,
       });
-      prettyGoalArrows = [{
-        fromId: mainGoalBefore.id,
-        toId: updatedGoal.id
-      }];
+      prettyGoalArrows = [
+        {
+          fromId: mainGoalBefore.id,
+          toId: updatedGoal.id,
+        },
+      ];
     }
 
     // 2. Draw hypothesis nodes and arrows
     const hypsBefore = mainGoalBefore.hyps;
-    const hypsAfter  = updatedGoal.hyps;
-    let [prettyHypNodes, prettyHypArrows] = drawNewHypothesisLayer(pretty, hypsBefore, hypsAfter);
+    const hypsAfter = updatedGoal.hyps;
+    let [prettyHypNodes, prettyHypArrows] = drawNewHypothesisLayer(
+      pretty,
+      hypsBefore,
+      hypsAfter
+    );
 
     if (prettyHypNodes.length > 0) {
       currentWindow.hypNodes.push(prettyHypNodes);
     }
 
     pretty.tactics.push({
-      id           : newTacticId(),
-      text         : tactic.tacticString,
-      dependsOnIds : tactic.tacticDependsOn,
-      goalArrows   : prettyGoalArrows,
-      hypArrows    : prettyHypArrows,
-      isSuccess    : false,
-      ...(haveWindowId && { haveWindowId })
+      id: newTacticId(),
+      text: tactic.tacticString,
+      dependsOnIds: tactic.tacticDependsOn,
+      goalArrows: prettyGoalArrows,
+      hypArrows: prettyHypArrows,
+      isSuccess: false,
+      haveWindowIds,
     });
   }
   // - we forked the goal!
   else if (relevantGoalsAfter.length > 1) {
     // 1. Draw goal nodes and arrows
     const prettyGoalArrows = relevantGoalsAfter.map((goal) => ({
       fromId: mainGoalBefore.id,
-      toId: goal.id
+      toId: goal.id,
     }));
 
     const prettyHypArrows: Tactic["hypArrows"] = [];
     // We are creating new child windows
     const childWindows = relevantGoalsAfter.map((goal) => {
       const hypsBefore = mainGoalBefore.hyps;
-      const hypsAfter  = goal.hyps;
-      const [prettyHypNodes, prettyHypArrowsForAChild] = drawNewHypothesisLayer(pretty, hypsBefore, hypsAfter);
+      const hypsAfter = goal.hyps;
+      const [prettyHypNodes, prettyHypArrowsForAChild] = drawNewHypothesisLayer(
+        pretty,
+        hypsBefore,
+        hypsAfter
+      );
       prettyHypArrows.push(...prettyHypArrowsForAChild);
 
       return {
@@ -323,30 +338,34 @@ const handleTacticApp = (tactic: LeanTactic, pretty : ConvertedProofTree, haveWi
           {
             text: goal.type,
             name: goal.username,
-            id: goal.id
-          }
+            id: goal.id,
+          },
         ],
-        hypNodes: prettyHypNodes.length > 0 ? [prettyHypNodes] : []
-      }
+        hypNodes: prettyHypNodes.length > 0 ? [prettyHypNodes] : [],
+      };
     });
     pretty.windows.push(...childWindows);
 
     pretty.tactics.push({
-      id           : newTacticId(),
-      text         : tactic.tacticString,
-      dependsOnIds : tactic.tacticDependsOn,
-      goalArrows   : prettyGoalArrows,
-      hypArrows    : prettyHypArrows,
-      isSuccess    : false
+      id: newTacticId(),
+      text: tactic.tacticString,
+      dependsOnIds: tactic.tacticDependsOn,
+      goalArrows: prettyGoalArrows,
+      hypArrows: prettyHypArrows,
+      isSuccess: false,
+      haveWindowIds,
     });
   }
-}
+};
 
-const drawInitialGoal = (initialMainGoal: LeanGoal, pretty : ConvertedProofTree) => {
+const drawInitialGoal = (
+  initialMainGoal: LeanGoal,
+  pretty: ConvertedProofTree
+) => {
   const hypNodes = initialMainGoal.hyps.map((hyp: LeanHypothesis) => ({
     text: hyp.type,
     name: hyp.username,
-    id  : hyp.id
+    id: hyp.id,
   }));
   const initialWindow = {
     id: newWindowId(),
@@ -355,55 +374,63 @@ const drawInitialGoal = (initialMainGoal: LeanGoal, pretty : ConvertedProofTree)
       {
         text: initialMainGoal.type,
         name: initialMainGoal.username,
-        id  : initialMainGoal.id
-      }
+        id: initialMainGoal.id,
+      },
     ],
-    hypNodes: hypNodes.length > 0 ? [hypNodes.reverse()] : []
+    hypNodes: hypNodes.length > 0 ? [hypNodes.reverse()] : [],
   };
   pretty.windows.push(initialWindow);
-}
+};
 
+// TODO: Refactor it since this function relies on obsolete assumptions:
+// - There is only one initial goal (can be multiple `have <p, q> := <by rfl, by rfl>`)
+// - Order of tactics in steps reflects the order of the proof.
 const getInitialGoal = (subSteps: LeanProofTree): LeanGoal | undefined => {
   const firstStep = subSteps[0];
-  if ('tacticApp' in firstStep) {
+  if ("tacticApp" in firstStep) {
     return firstStep.tacticApp.t.goalsBefore[0];
-  } else if ('haveDecl' in firstStep) {
+  } else if ("haveDecl" in firstStep) {
     return firstStep.haveDecl.t.goalsBefore[0];
   }
-}
+};
 
-const recursive = (subSteps : LeanProofTree, pretty : ConvertedProofTree) => {
+const recursive = (subSteps: LeanProofTree, pretty: ConvertedProofTree) => {
   subSteps.forEach((subStep) => {
-    if ('tacticApp' in subStep) {
+    if ("tacticApp" in subStep) {
       handleTacticApp(subStep.tacticApp.t, pretty);
-    } else if ('haveDecl' in subStep) {
-      const haveWindowId = newWindowId();
-
-      handleTacticApp(subStep.haveDecl.t, pretty, haveWindowId);
-
-      const initialGoal = getInitialGoal(subStep.haveDecl.subSteps)!;
-
-      const initialWindow : Window = {
-        id: haveWindowId,
+    } else if ("haveDecl" in subStep) {
+      // TODO: Remove when new lean version reporting is set up.
+      const initialGoals =
+        "initialGoals" in subStep.haveDecl
+          ? subStep.haveDecl.initialGoals
+          : [getInitialGoal(subStep.haveDecl.subSteps)!];
+      const windows = initialGoals.map((goal) => ({
+        id: newWindowId(),
         // Parent window is such that has our goalId as a hypothesis.
         // `have`'s fvarid won't equal `have's` mvarid however - so the only way to match them would be by the username. many `have`s may have the same username though, so let's just store out parentId.
         parentId: "haveWindow",
         goalNodes: [
           {
-            text: initialGoal.type,
-            name: initialGoal.username,
-            id  : initialGoal.id
-          }
+            text: goal.type,
+            name: goal.username,
+            id: goal.id,
+          },
         ],
         // `have`s don't introduce any new hypotheses
-        hypNodes: []
-      };
-      pretty.windows.push(initialWindow);
+        hypNodes: [],
+      }));
+
+      handleTacticApp(
+        subStep.haveDecl.t,
+        pretty,
+        windows.map((w) => w.id)
+      );
+      pretty.windows.push(...windows);
 
       recursive(subStep.haveDecl.subSteps, pretty);
     }
-  })
-}
+  });
+};
 
 const postprocess = (pretty: ConvertedProofTree): ConvertedProofTree => {
   pretty.tactics.forEach((tactic) => {

app/types/ConvertedProofTree.ts

@@ -31,7 +31,11 @@ export interface Tactic {
   // hmm
   isSuccess: boolean | string;
   successGoalId?: string;
-  haveWindowId?: string
+  // TODO: Those are actually `byWindow`s which were used to create
+  // parameters for this tactic. For example in
+  // `have <p, q> := <by rfl, by trivial>`
+  // there are 2 `byWindow`s.
+  haveWindowIds: string[];
 }
 
 export interface ConvertedProofTree {

app/types/LeanProofTree.ts

@@ -29,8 +29,13 @@ export type LeanHaveDecl = {
   haveDecl: {
     t: LeanTactic;
     subSteps: LeanProofTree;
-    initialGoal: string;
-  }
+  } & (
+    | { version: undefined; initialGoal: string }
+    | {
+        version: 2;
+        initialGoals: LeanGoal[];
+      }
+  );
 };
 
 export type LeanProofTree = (LeanTacticApp | LeanHaveDecl)[];