doc: Clarify data
This commit is contained in:
Leni Aniva
parent
a61cea3a2f
commit
93ecd0d5ad
192
docs/data.ipynb
192
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}\")"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
|
|||
Loading…
Reference in New Issue