aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

feat: Used constants in tactic step

This commit is contained in:
Leni Aniva 2024-11-11 21:02:02 -08:00
parent b89f3a19bf
commit 66af206594
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 39 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
docs/data.ipynb
View File

@ -117,83 +117,83 @@
"name": "stdout",
"output_type": "stream",
"text": [
"=== Before ===\n",
"[Before]\n",
"α : Sort ?u.7\n",
"⊢ α → α\n",
"===Tactic===\n",
"aesop\n",
"===After===\n",
"[Tactic]\n",
"aesop (using [])\n",
"[Afte]\n",
"\n",
"=== Before ===\n",
"[Before]\n",
"⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
"===Tactic===\n",
"intro p q h\n",
"===After===\n",
"[Tactic]\n",
"intro p q h (using [])\n",
"[Afte]\n",
"p q : Prop\n",
"h : p ∨ q\n",
"⊢ q ∨ p\n",
"=== Before ===\n",
"[Before]\n",
"p q : Prop\n",
"h : p ∨ q\n",
"⊢ q ∨ p\n",
"===Tactic===\n",
"cases h\n",
"===After===\n",
"[Tactic]\n",
"cases h (using ['Eq.refl', 'Or'])\n",
"[Afte]\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",
"[Before]\n",
"case inl\n",
"p q : Prop\n",
"h✝ : p\n",
"⊢ q ∨ p\n",
"===Tactic===\n",
"apply Or.inr\n",
"===After===\n",
"[Tactic]\n",
"apply Or.inr (using ['Or.inr'])\n",
"[Afte]\n",
"case inl.h\n",
"p q : Prop\n",
"h✝ : p\n",
"⊢ p\n",
"=== Before ===\n",
"[Before]\n",
"case inl.h\n",
"p q : Prop\n",
"h✝ : p\n",
"⊢ p\n",
"===Tactic===\n",
"assumption\n",
"===After===\n",
"[Tactic]\n",
"assumption (using [])\n",
"[Afte]\n",
"\n",
"=== Before ===\n",
"[Before]\n",
"case inr\n",
"p q : Prop\n",
"h✝ : q\n",
"⊢ q ∨ p\n",
"===Tactic===\n",
"apply Or.inl\n",
"===After===\n",
"[Tactic]\n",
"apply Or.inl (using ['Or.inl'])\n",
"[Afte]\n",
"case inr.h\n",
"p q : Prop\n",
"h✝ : q\n",
"⊢ q\n",
"=== Before ===\n",
"[Before]\n",
"case inr.h\n",
"p q : Prop\n",
"h✝ : q\n",
"⊢ q\n",
"===Tactic===\n",
"assumption\n",
"===After===\n",
"[Tactic]\n",
"assumption (using [])\n",
"[Afte]\n",
"\n"
]
}
],
"source": [
"for i in invocations:\n",
" print(f\"=== Before ===\\n{i.before}\")\n",
" print(f\"===Tactic===\\n{i.tactic}\")\n",
" print(f\"===After===\\n{i.after}\")"
" print(f\"[Before]\\n{i.before}\")\n",
" print(f\"[Tactic]\\n{i.tactic} (using {i.used_constants})\")\n",
" print(f\"[Afte]\\n{i.after}\")"
]
},
{

10
pantograph/compiler.py
View File

@ -9,9 +9,13 @@ class TacticInvocation:
before: str
after: str
tactic: str
used_constants: list[str]
@staticmethod
def parse(payload: dict):
return TacticInvocation(before=payload["goalBefore"],
after=payload["goalAfter"],
tactic=payload["tactic"])
return TacticInvocation(
before=payload["goalBefore"],
after=payload["goalAfter"],
tactic=payload["tactic"],
used_constants=payload.get('usedConstants', []),
)

2
src

@ -1 +1 @@
Subproject commit 8fe4c78c2aea194869bb7b4b7e61087b6374ff66
Subproject commit 4f6ccd3e82dd41402b7244484a1b0312d9e27018