feat: Compilation unit extraction
This commit is contained in:
parent
1d9fc38277
commit
174d1a3fd6
|
@ -1,11 +1,12 @@
|
||||||
import Aesop
|
import Aesop
|
||||||
|
|
||||||
-- Ensure that Aesop is running
|
/-- Ensure that Aesop is running -/
|
||||||
example : α → α :=
|
example : α → α :=
|
||||||
by aesop
|
by aesop
|
||||||
|
|
||||||
example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
|
example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
|
||||||
intro p q h
|
intro p q h
|
||||||
|
-- Here are some comments
|
||||||
cases h
|
cases h
|
||||||
. apply Or.inr
|
. apply Or.inr
|
||||||
assumption
|
assumption
|
||||||
|
|
|
@ -7,9 +7,12 @@ pushd Example
|
||||||
lake build
|
lake build
|
||||||
popd
|
popd
|
||||||
```
|
```
|
||||||
This would generate compiled `.olean` files. Then run the example from the
|
This would generate compiled `.olean` files. Then run one of the examples from the
|
||||||
project root:
|
project root:
|
||||||
``` sh
|
``` sh
|
||||||
poetry run examples/aesop.py
|
poetry run examples/aesop.py
|
||||||
|
poetry run examples/data.py
|
||||||
```
|
```
|
||||||
|
|
||||||
|
Warning: If you make modifications to any Lean files, you must re-run `lake build`!
|
||||||
|
|
||||||
|
|
|
@ -14,6 +14,10 @@ if __name__ == '__main__':
|
||||||
print(f"$PWD: {project_path}")
|
print(f"$PWD: {project_path}")
|
||||||
print(f"$LEAN_PATH: {lean_path}")
|
print(f"$LEAN_PATH: {lean_path}")
|
||||||
server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)
|
server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)
|
||||||
data = server.compile_tactics("Example")
|
units, invocations = server.compile_unit("Example")
|
||||||
for (before, tactic, after) in data:
|
for i, u in enumerate(units):
|
||||||
print(f"{before}\n{tactic}\n{after}\n\n")
|
print(f"==== #{i} ====")
|
||||||
|
print(u)
|
||||||
|
print("==== Invocations ====")
|
||||||
|
for i in invocations:
|
||||||
|
print(f"{i.before}\n{i.tactic}\n{i.after}\n")
|
|
@ -0,0 +1,13 @@
|
||||||
|
from dataclasses import dataclass
|
||||||
|
|
||||||
|
@dataclass(frozen=True)
|
||||||
|
class TacticInvocation:
|
||||||
|
before: str
|
||||||
|
after: str
|
||||||
|
tactic: str
|
||||||
|
|
||||||
|
@staticmethod
|
||||||
|
def parse(payload: dict):
|
||||||
|
return TacticInvocation(before=payload["goalBefore"],
|
||||||
|
after=payload["goalAfter"],
|
||||||
|
tactic=payload["tactic"])
|
|
@ -5,6 +5,7 @@ interface.
|
||||||
import json, pexpect, pathlib, unittest, os
|
import json, pexpect, pathlib, unittest, os
|
||||||
from pantograph.expr import parse_expr, Expr, Variable, Goal, GoalState, \
|
from pantograph.expr import parse_expr, Expr, Variable, Goal, GoalState, \
|
||||||
Tactic, TacticHave, TacticCalc
|
Tactic, TacticHave, TacticCalc
|
||||||
|
from pantograph.compiler import TacticInvocation
|
||||||
|
|
||||||
def _get_proc_cwd():
|
def _get_proc_cwd():
|
||||||
return pathlib.Path(__file__).parent
|
return pathlib.Path(__file__).parent
|
||||||
|
@ -136,12 +137,22 @@ class Server:
|
||||||
raise ServerError(result["parseError"])
|
raise ServerError(result["parseError"])
|
||||||
return GoalState.parse(result, self.to_remove_goal_states)
|
return GoalState.parse(result, self.to_remove_goal_states)
|
||||||
|
|
||||||
|
def compile_unit(self, module: str) -> tuple[list[str], list[TacticInvocation]]:
|
||||||
def compile_tactics(self, module: str) -> list[tuple[str, str, str]]:
|
file_path = self.project_path / (module.replace('.', '/') + '.lean')
|
||||||
result = self.run('compile.tactics', {'module': module})
|
result = self.run('compile.unit', {
|
||||||
|
'module': module,
|
||||||
|
'compilationUnits': True,
|
||||||
|
'invocations': True
|
||||||
|
})
|
||||||
if "error" in result:
|
if "error" in result:
|
||||||
raise ServerError(result["desc"])
|
raise ServerError(result["desc"])
|
||||||
return [(i['goalBefore'], i['tactic'], i['goalAfter']) for i in result['invocations']]
|
|
||||||
|
with open(file_path, 'rb') as f:
|
||||||
|
content = f.read()
|
||||||
|
units = [content[begin:end].decode('utf-8') for begin,end in result['units']]
|
||||||
|
|
||||||
|
invocations = [TacticInvocation.parse(i) for i in result['invocations']]
|
||||||
|
return units, invocations
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
2
src
2
src
|
@ -1 +1 @@
|
||||||
Subproject commit b9b16ba0e9d99279837527bcb40176277d11e725
|
Subproject commit 855e7716098667aff52e7374f6b911ba06a08578
|
Loading…
Reference in New Issue