{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "a1078f98-fcaf-4cda-8ad4-3cbab44f114b",
   "metadata": {},
   "source": [
    "# Pantograph Example\n",
    "\n",
    "The only interface for interacting with Pantograph is the `Server` class. It can be used either standalone (with no Lean project specified) or in a Lean project in order to access the project's symbols.\n",
    "\n",
    "The server's `imports` argument must be specified as a list of Lean modules to import. With no import statements, there are no symbols available and no useful work can be done. By default, `imports` is `[\"Init\"]`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "101f4591-ec31-4000-96a6-ac3fc3dd0fa2",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pantograph import Server\n",
    "\n",
    "server = Server()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1fbdb837-740e-44ef-a7e9-c40f79584639",
   "metadata": {},
   "source": [
    "We can initialize a proof by providing the target statement."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "4affc375-360b-40cf-8d22-4fdcc12dba0d",
   "metadata": {},
   "outputs": [],
   "source": [
    "state0 = server.goal_start(\"forall (p : Prop), p -> p\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "deb7994a-273f-4b52-be2d-e1086d4c1d55",
   "metadata": {},
   "source": [
    "This invocation creates a *goal state*, which consists of a finite number of goals. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "29f7ae15-7f69-4740-a6fa-71fbb1ccabd8",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "GoalState(state_id=0, goals=[Goal(variables=[], target='forall (p : Prop), p -> p', name=None, is_conversion=False)], _sentinel=[])"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "state0"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "274f50da-85c1-445e-bf9f-cb716f66e36f",
   "metadata": {},
   "source": [
    "Execute tactics on the goal state via `Server.goal_tactic`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "bfbd5512-fcb0-428d-8131-4da4005e743c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "GoalState(state_id=2, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p✝')], target='p✝ → p✝', name=None, is_conversion=False)], _sentinel=[1])"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro\")\n",
    "state1"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1c1c5ab4-5518-40b0-8a2f-50e095a3702a",
   "metadata": {},
   "source": [
    "Recover the usual string form of a goal by the `str` function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "2d18d6dc-7936-4bb6-b47d-f781dd8ddacd",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'p✝ : Prop\\n⊢ p✝ → p✝'"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "str(state1.goals[0])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fc560b88-0222-4e40-bff9-37ab70af075e",
   "metadata": {},
   "source": [
    "When a tactic fails, it throws an exception:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "a0fdd3b3-9b38-4602-84a3-89065822f6e8",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\"tactic 'assumption' failed\\np✝ : Prop\\n⊢ p✝ → p✝\"]\n"
     ]
    }
   ],
   "source": [
    "try:\n",
    "    state2 = server.goal_tactic(state1, goal_id=0, tactic=\"assumption\")\n",
    "    print(\"Should not reach this\")\n",
    "except Exception as e:\n",
    "    print(e)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c801bbb4-9248-4f75-945b-1dd665bb08d1",
   "metadata": {},
   "source": [
    "A state with no goals is considered solved"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "9d18045a-9734-415c-8f40-7aadb6cb18f4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "GoalState(state_id=7, goals=[], _sentinel=[1, 3, 4, 5])"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "state2 = server.goal_tactic(state1, goal_id=0, tactic=\"intro h\")\n",
    "state3 = server.goal_tactic(state2, goal_id=0, tactic=\"exact h\")\n",
    "state3"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "aa5a2800-cae3-48df-b746-d19a8d84eaf5",
   "metadata": {},
   "source": [
    "Execute `Server.gc()` to clean up unused goals once in a while"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "ee98de99-3cfc-4449-8d62-00e8eaee03db",
   "metadata": {},
   "outputs": [],
   "source": [
    "server.gc()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "78cfb9ac-c5ec-4901-97a5-4d19e6b8ecbb",
   "metadata": {},
   "source": [
    "## Loading Projects\n",
    "\n",
    "Pantograph would not be useful if it could not load symbols from other projects. In `examples/Example` is a standard Lean 4 project, with its toolchain version precisely equal to the toolchain version of Pantograph. Executing `lake new PROJECT_NAME` or `lake init` in an empty folder initializes a project according to this specification. To use a project in Pantograph, compile the project by running `lake build` in its root directory. This sets up output folders and builds the binary Lean files.\n",
    "\n",
    "Load the example project by providing `project_path` and `lean_path` to `Server`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "ecf5d9d3-e53e-4f67-969e-d38e3d97c65e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "$PWD: /Users/aniva/Projects/atp/PyPantograph/examples/Example\n",
      "$LEAN_PATH: b'././.lake/packages/std/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/build/lib:/Users/aniva/.elan/toolchains/leanprover--lean4---v4.8.0-rc1/lib/lean\\n'\n"
     ]
    }
   ],
   "source": [
    "import subprocess, os\n",
    "from pathlib import Path\n",
    "def get_project_and_lean_path():\n",
    "    cwd = Path(os.getcwd()).resolve() / 'Example'\n",
    "    p = subprocess.check_output(['lake', 'env', 'printenv', 'LEAN_PATH'], cwd=cwd)\n",
    "    return cwd, p\n",
    "project_path, lean_path = get_project_and_lean_path()\n",
    "print(f\"$PWD: {project_path}\")\n",
    "print(f\"$LEAN_PATH: {lean_path}\")\n",
    "server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "67123741-3d23-4077-98ab-91110b4e39f1",
   "metadata": {},
   "source": [
    "With the project loaded, all dependencies of the project, be it Mathlib or Aesop, are now available."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "bf485778-baa9-4c1c-80fa-960f9cf9bc8a",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "state0 = server.goal_start(\"forall (p q: Prop), Or p q -> Or q p\")\n",
    "state1 = server.goal_tactic(state0, goal_id=0, tactic=\"aesop\")\n",
    "state1.is_solved"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8c3f9d90-bacc-4cba-95a4-23cc31a58a4f",
   "metadata": {},
   "source": [
    "## Reading Symbols\n",
    "\n",
    "Pantograph can also query proof states from a project by directly calling into Lean's compiler internals. Run the Lean compiler on a project module via `Server.compile_unit`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "8ff6007b-50df-4449-9a86-6d3eb0bc0caa",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "==== #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",
      "==== #2 ====\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": [
    "units, invocations = server.compile_unit(\"Example\")\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": "cb5bbbcc-01dc-4a35-81ba-e155cedb9a91",
   "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.4"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}