From 93ecd0d5ad95fca453b10194bdb5546e4cc32273 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 25 Oct 2024 00:21:52 -0700
Subject: [PATCH] doc: Clarify data

---
 docs/data.ipynb | 192 ++++++++++++++++++++++++++++++++----------------
 1 file changed, 127 insertions(+), 65 deletions(-)

diff --git a/docs/data.ipynb b/docs/data.ipynb
index cb616f6..4c09b4d 100644
--- 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",
-      "α : Sort ?u.7\n",
-      "⊢ α → α\n",
-      "aesop\n",
-      "\n",
-      "\n",
-      "⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
-      "intro p q h\n",
-      "p q : Prop\n",
-      "h : p ∨ q\n",
-      "⊢ q ∨ p\n",
-      "\n",
-      "p q : Prop\n",
-      "h : p ∨ q\n",
-      "⊢ q ∨ p\n",
-      "cases h\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",
-      "case inl\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ q ∨ p\n",
-      "apply Or.inr\n",
-      "case inl.h\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ p\n",
-      "\n",
-      "case inl.h\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ p\n",
-      "assumption\n",
-      "\n",
-      "\n",
-      "case inr\n",
-      "p q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q ∨ p\n",
-      "apply Or.inl\n",
-      "case inr.h\n",
-      "p q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q\n",
-      "\n",
-      "case inr.h\n",
-      "p q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q\n",
-      "assumption\n",
-      "\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",
+    "    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",
+      "=== 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",
+      "=== 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",
+      "=== 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",
+      "=== Before ===\n",
+      "case inl.h\n",
+      "p q : Prop\n",
+      "h✝ : p\n",
+      "⊢ p\n",
+      "===Tactic===\n",
+      "assumption\n",
+      "===After===\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",
+      "=== Before ===\n",
+      "case inr.h\n",
+      "p q : Prop\n",
+      "h✝ : q\n",
+      "⊢ q\n",
+      "===Tactic===\n",
+      "assumption\n",
+      "===After===\n",
+      "\n"
+     ]
+    }
+   ],
+   "source": [
     "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}\")"
    ]
   },
   {