{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "fe7a3037-5c49-4097-9a5d-575b958cc7f8",
   "metadata": {},
   "source": [
    "# Data Extraction"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "fc68ad1d-e64c-48b7-9461-50d872d30473",
   "metadata": {},
   "outputs": [],
   "source": [
    "import os\n",
    "from pathlib import Path\n",
    "from pantograph.server import Server"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fd13c644-d731-4f81-964e-584bbd43e51c",
   "metadata": {},
   "source": [
    "## Tactic Invocation\n",
    "\n",
    "Pantograph can extract tactic invocation data from a Lean file. A **tactic\n",
    "invocation** is a tuple containing the before and after goal states, and the\n",
    "tactic which converts the \"before\" state to the \"after\" state.\n",
    "\n",
    "To extract tactic invocation data, use `server.tactic_invocations(file_name)`\n",
    "and supply the file name of the input Lean file."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "a0a2a661-e357-4b80-92d1-4172670ab061",
   "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",
      "  by aesop\n",
      "\n",
      "\n",
      "==== #1 ====\n",
      "example : ∀ (p q: Prop), p ∨ q → q ∨ p := by\n",
      "  intro p q h\n",
      "  -- Here are some comments\n",
      "  cases h\n",
      "  . apply Or.inr\n",
      "    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",
    "for i in invocations:\n",
    "    print(f\"{i.before}\\n{i.tactic}\\n{i.after}\\n\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "51f5398b-5416-4dc1-81cd-6d2514758232",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.12.6"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}