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

Merge pull request #47 from lenianiva/feat/tactic-extraction 

feat: Used constants in tactic step
This commit is contained in:
Leni Aniva 2024-12-05 17:30:33 -08:00 committed by GitHub
parent 70544d4298 66af206594
commit 605fbd0bd7
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
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", "name": "stdout",
"output_type": "stream", "output_type": "stream",
"text": [ "text": [
"=== Before ===\n", "[Before]\n",
"α : Sort ?u.7\n", "α : Sort ?u.7\n",
"⊢ α → α\n", "⊢ α → α\n",
"===Tactic===\n", "[Tactic]\n",
"aesop\n", "aesop (using [])\n",
"===After===\n", "[Afte]\n",
"\n", "\n",
"=== Before ===\n", "[Before]\n",
"⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n", "⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
"===Tactic===\n", "[Tactic]\n",
"intro p q h\n", "intro p q h (using [])\n",
"===After===\n", "[Afte]\n",
"p q : Prop\n", "p q : Prop\n",
"h : p ∨ q\n", "h : p ∨ q\n",
"⊢ q ∨ p\n", "⊢ q ∨ p\n",
"=== Before ===\n", "[Before]\n",
"p q : Prop\n", "p q : Prop\n",
"h : p ∨ q\n", "h : p ∨ q\n",
"⊢ q ∨ p\n", "⊢ q ∨ p\n",
"===Tactic===\n", "[Tactic]\n",
"cases h\n", "cases h (using ['Eq.refl', 'Or'])\n",
"===After===\n", "[Afte]\n",
"case inl\n", "case inl\n",
"p q : Prop\n", "p q : Prop\n",
"h✝ : p\n", "h✝ : p\n",
"⊢ q ∨ p\n", "⊢ q ∨ p\n",
"case inr p q : Prop h✝ : q ⊢ q ∨ p\n", "case inr p q : Prop h✝ : q ⊢ q ∨ p\n",
"=== Before ===\n", "[Before]\n",
"case inl\n", "case inl\n",
"p q : Prop\n", "p q : Prop\n",
"h✝ : p\n", "h✝ : p\n",
"⊢ q ∨ p\n", "⊢ q ∨ p\n",
"===Tactic===\n", "[Tactic]\n",
"apply Or.inr\n", "apply Or.inr (using ['Or.inr'])\n",
"===After===\n", "[Afte]\n",
"case inl.h\n", "case inl.h\n",
"p q : Prop\n", "p q : Prop\n",
"h✝ : p\n", "h✝ : p\n",
"⊢ p\n", "⊢ p\n",
"=== Before ===\n", "[Before]\n",
"case inl.h\n", "case inl.h\n",
"p q : Prop\n", "p q : Prop\n",
"h✝ : p\n", "h✝ : p\n",
"⊢ p\n", "⊢ p\n",
"===Tactic===\n", "[Tactic]\n",
"assumption\n", "assumption (using [])\n",
"===After===\n", "[Afte]\n",
"\n", "\n",
"=== Before ===\n", "[Before]\n",
"case inr\n", "case inr\n",
"p q : Prop\n", "p q : Prop\n",
"h✝ : q\n", "h✝ : q\n",
"⊢ q ∨ p\n", "⊢ q ∨ p\n",
"===Tactic===\n", "[Tactic]\n",
"apply Or.inl\n", "apply Or.inl (using ['Or.inl'])\n",
"===After===\n", "[Afte]\n",
"case inr.h\n", "case inr.h\n",
"p q : Prop\n", "p q : Prop\n",
"h✝ : q\n", "h✝ : q\n",
"⊢ q\n", "⊢ q\n",
"=== Before ===\n", "[Before]\n",
"case inr.h\n", "case inr.h\n",
"p q : Prop\n", "p q : Prop\n",
"h✝ : q\n", "h✝ : q\n",
"⊢ q\n", "⊢ q\n",
"===Tactic===\n", "[Tactic]\n",
"assumption\n", "assumption (using [])\n",
"===After===\n", "[Afte]\n",
"\n" "\n"
] ]
} }
], ],
"source": [ "source": [
"for i in invocations:\n", "for i in invocations:\n",
" print(f\"=== Before ===\\n{i.before}\")\n", " print(f\"[Before]\\n{i.before}\")\n",
" print(f\"===Tactic===\\n{i.tactic}\")\n", " print(f\"[Tactic]\\n{i.tactic} (using {i.used_constants})\")\n",
" print(f\"===After===\\n{i.after}\")" " print(f\"[Afte]\\n{i.after}\")"
] ]
}, },
{ {

10
pantograph/compiler.py
View File

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

2
src

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