doc: Clarify data

lenianiva · Oct 25, 2024 · 93ecd0d · 93ecd0d
1 parent a61cea3
commit 93ecd0d
Showing 1 changed file with 82 additions and 20 deletions.
diff --git a/docs/data.ipynb b/docs/data.ipynb
@@ -38,14 +38,42 @@
   {
    "cell_type": "code",
    "execution_count": 2,
-   "id": "a0a2a661-e357-4b80-92d1-4172670ab061",
+   "id": "6282dc6f-4eac-4263-8277-9d54d19ad1a5",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example\n"
+     ]
+    }
+   ],
+   "source": [
+    "project_path = Path(os.getcwd()).parent.resolve() / 'examples/Example'\n",
+    "print(f\"$PWD: {project_path}\")\n",
+    "server = Server(imports=['Example'], project_path=project_path)\n",
+    "units, invocations = server.tactic_invocations(project_path / \"Example.lean\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "c3c1be91-27a5-4481-b09d-a32dbb94b058",
+   "metadata": {},
+   "source": [
+    "The function returns a tuple `([str], [TacticInvocation])`. The former element is a list of strings containing each compilation unit, comment data included."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "id": "e994aa2b-5d5e-4f86-af6c-40e0b3a032d2",
    "metadata": {},
    "outputs": [
     {
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example\n",
       "==== #0 ====\n",
       "/-- Ensure that Aesop is running -/\n",
       "example : α → α :=\n",
@@ -61,77 +89,111 @@
       "    assumption\n",
       "  . apply Or.inl\n",
       "    assumption\n",
-      "\n",
-      "==== Invocations ====\n",
+      "\n"
+     ]
+    }
+   ],
+   "source": [
+    "for i, u in enumerate(units):\n",
+    "    print(f\"==== #{i} ====\")\n",
+    "    print(u)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "52e650fc-4a87-445f-8aa8-707ed9e36c03",
+   "metadata": {},
+   "source": [
+    "The latter is a list of `TacticInvocation`, which contains the `.before` (corresponding to the state before the tactic), `.after` (corresponding to the state after the tactic), and `.tactic` (tactic executed) fields. "
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "id": "8e0f0def-dd3c-4550-8a7c-b4aec6c7fd7f",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "=== Before ===\n",
       "α : Sort ?u.7\n",
       "⊢ α → α\n",
+      "===Tactic===\n",
       "aesop\n",
+      "===After===\n",
       "\n",
-      "\n",
+      "=== Before ===\n",
       "⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
+      "===Tactic===\n",
       "intro p q h\n",
+      "===After===\n",
       "p q : Prop\n",
       "h : p ∨ q\n",
       "⊢ q ∨ p\n",
-      "\n",
+      "=== Before ===\n",
       "p q : Prop\n",
       "h : p ∨ q\n",
       "⊢ q ∨ p\n",
+      "===Tactic===\n",
       "cases h\n",
+      "===After===\n",
       "case inl\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ q ∨ p\n",
       "case inr p q : Prop h✝ : q ⊢ q ∨ p\n",
-      "\n",
+      "=== Before ===\n",
       "case inl\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ q ∨ p\n",
+      "===Tactic===\n",
       "apply Or.inr\n",
+      "===After===\n",
       "case inl.h\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ p\n",
-      "\n",
+      "=== Before ===\n",
       "case inl.h\n",
       "p q : Prop\n",
       "h✝ : p\n",
       "⊢ p\n",
+      "===Tactic===\n",
       "assumption\n",
+      "===After===\n",
       "\n",
-      "\n",
+      "=== Before ===\n",
       "case inr\n",
       "p q : Prop\n",
       "h✝ : q\n",
       "⊢ q ∨ p\n",
+      "===Tactic===\n",
       "apply Or.inl\n",
+      "===After===\n",
       "case inr.h\n",
       "p q : Prop\n",
       "h✝ : q\n",
       "⊢ q\n",
-      "\n",
+      "=== Before ===\n",
       "case inr.h\n",
       "p q : Prop\n",
       "h✝ : q\n",
       "⊢ q\n",
+      "===Tactic===\n",
       "assumption\n",
-      "\n",
+      "===After===\n",
       "\n"
      ]
     }
    ],
    "source": [
-    "project_path = Path(os.getcwd()).parent.resolve() / 'examples/Example'\n",
-    "print(f\"$PWD: {project_path}\")\n",
-    "server = Server(imports=['Example'], project_path=project_path)\n",
-    "units, invocations = server.tactic_invocations(project_path / \"Example.lean\")\n",
-    "for i, u in enumerate(units):\n",
-    "    print(f\"==== #{i} ====\")\n",
-    "    print(u)\n",
-    "print(\"==== Invocations ====\")\n",
     "for i in invocations:\n",
-    "    print(f\"{i.before}\\n{i.tactic}\\n{i.after}\\n\")"
+    "    print(f\"=== Before ===\\n{i.before}\")\n",
+    "    print(f\"===Tactic===\\n{i.tactic}\")\n",
+    "    print(f\"===After===\\n{i.after}\")"
    ]
   },
   {