Merge pull request #47 from lenianiva/feat/tactic-extraction

feat: Used constants in tactic step
lenianiva · Dec 6, 2024 · 605fbd0 · 605fbd0
2 parents 70544d4 + 66af206
commit 605fbd0
Show file tree

Hide file tree

Showing 3 changed files with 39 additions and 35 deletions.
diff --git a/docs/data.ipynb b/docs/data.ipynb
@@ -117,83 +117,83 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "=== Before ===\n",
+      "[Before]\n",
       "α : Sort ?u.7\n",
       "⊢ α → α\n",
-      "===Tactic===\n",
-      "aesop\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "aesop (using [])\n",
+      "[Afte]\n",
       "\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
-      "===Tactic===\n",
-      "intro p q h\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "intro p q h (using [])\n",
+      "[Afte]\n",
       "p q : Prop\n",
       "h : p ∨ q\n",
       "⊢ q ∨ p\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "p q : Prop\n",
       "h : p ∨ q\n",
       "⊢ q ∨ p\n",
-      "===Tactic===\n",
-      "cases h\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "cases h (using ['Eq.refl', 'Or'])\n",
+      "[Afte]\n",
       "case inl\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ q ∨ p\n",
       "case inr p q : Prop h✝ : q ⊢ q ∨ p\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "case inl\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ q ∨ p\n",
-      "===Tactic===\n",
-      "apply Or.inr\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "apply Or.inr (using ['Or.inr'])\n",
+      "[Afte]\n",
       "case inl.h\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ p\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "case inl.h\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ p\n",
-      "===Tactic===\n",
-      "assumption\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "assumption (using [])\n",
+      "[Afte]\n",
       "\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "case inr\n",
       "p q : Prop\n",
       "h✝ : q\n",
       "⊢ q ∨ p\n",
-      "===Tactic===\n",
-      "apply Or.inl\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "apply Or.inl (using ['Or.inl'])\n",
+      "[Afte]\n",
       "case inr.h\n",
       "p q : Prop\n",
       "h✝ : q\n",
       "⊢ q\n",
-      "=== Before ===\n",
+      "[Before]\n",
       "case inr.h\n",
       "p q : Prop\n",
       "h✝ : q\n",
       "⊢ q\n",
-      "===Tactic===\n",
-      "assumption\n",
-      "===After===\n",
+      "[Tactic]\n",
+      "assumption (using [])\n",
+      "[Afte]\n",
       "\n"
      ]
     }
    ],
    "source": [
     "for i in invocations:\n",
-    "    print(f\"=== Before ===\\n{i.before}\")\n",
-    "    print(f\"===Tactic===\\n{i.tactic}\")\n",
-    "    print(f\"===After===\\n{i.after}\")"
+    "    print(f\"[Before]\\n{i.before}\")\n",
+    "    print(f\"[Tactic]\\n{i.tactic} (using {i.used_constants})\")\n",
+    "    print(f\"[Afte]\\n{i.after}\")"
    ]
   },
   {

diff --git a/pantograph/compiler.py b/pantograph/compiler.py
@@ -9,9 +9,13 @@ class TacticInvocation:
     before: str
     after: str
     tactic: str
+    used_constants: list[str]
 
     @staticmethod
     def parse(payload: dict):
-        return TacticInvocation(before=payload["goalBefore"],
-                                after=payload["goalAfter"],
-                                tactic=payload["tactic"])
+        return TacticInvocation(
+            before=payload["goalBefore"],
+            after=payload["goalAfter"],
+            tactic=payload["tactic"],
+            used_constants=payload.get('usedConstants', []),
+        )
diff --git a/src b/src
+14 −1		Pantograph/Frontend/Elab.lean
+3 −0		Pantograph/Protocol.lean
+7 −5		Test/Integration.lean