From 8f6492078952bb8774f15d0ae712ae127f45575a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 Apr 2024 13:00:06 -0700 Subject: [PATCH] feat: expression types and tests --- .gitignore | 1 + build.py | 1 + pantograph/expr.py | 62 ++++++++++++++++++++++++++++++++++++++++ pantograph/server.py | 68 ++++++++++++++++++++++++++++++++++++-------- 4 files changed, 120 insertions(+), 12 deletions(-) create mode 100644 pantograph/expr.py diff --git a/.gitignore b/.gitignore index e5d0541..4bd6cec 100644 --- a/.gitignore +++ b/.gitignore @@ -9,3 +9,4 @@ /dist pantograph/pantograph +pantograph/lean-toolchain diff --git a/build.py b/build.py index f5ffad4..959c1ad 100644 --- a/build.py +++ b/build.py @@ -12,3 +12,4 @@ with subprocess.Popen(["make"], cwd=PATH_PANTOGRAPH) as p: path_executable = PATH_PY / "pantograph" shutil.copyfile(PATH_PANTOGRAPH / ".lake/build/bin/pantograph", path_executable) os.chmod(path_executable, os.stat(path_executable).st_mode | stat.S_IEXEC) +shutil.copyfile(PATH_PANTOGRAPH / "lean-toolchain", PATH_PY / "lean-toolchain") diff --git a/pantograph/expr.py b/pantograph/expr.py new file mode 100644 index 0000000..bf80d8c --- /dev/null +++ b/pantograph/expr.py @@ -0,0 +1,62 @@ +""" +Data structuers for expressions and goals +""" +from dataclasses import dataclass +from typing import Optional, Self + +Expr = str + +def parse_expr(payload: dict) -> Expr: + return payload["pp"] + +@dataclass(frozen=True) +class Variable: + t: Expr + v: Optional[Expr] = None + name: Optional[str] = None + + @staticmethod + def _parse(payload: dict) -> Self: + name = payload.get("userName") + t = parse_expr(payload["type"]) + v = payload.get("value") + if v: + v = parse_expr(v) + return Variable(t, v, name) + + def __str__(self): + result = self.name if self.name else "_" + result += f" : {self.t}" + if self.v: + result += f" = {self.v}" + return result + +@dataclass(frozen=True) +class Goal: + variables: list[Variable] + target: Expr + name: Optional[str] = None + + @staticmethod + def sentence(target: Expr) -> Self: + return Goal(variables=[], target=target) + + @staticmethod + def _parse(payload: dict) -> Self: + name = payload.get("userName") + variables = [Variable._parse(v) for v in payload["vars"]] + target = parse_expr(payload["target"]) + return Goal(variables, target, name) + + def __str__(self): + return "\n".join(str(v) for v in self.variables) + \ + f"\n⊢ {self.target}" + +@dataclass(frozen=True) +class GoalState: + state_id: int + goals: list[Goal] + + @property + def is_solved(self) -> bool: + return not self.goals diff --git a/pantograph/server.py b/pantograph/server.py index f06b4e4..eb54f6d 100644 --- a/pantograph/server.py +++ b/pantograph/server.py @@ -1,7 +1,17 @@ -import json, pexpect, pathlib +""" +Class which manages a Pantograph instance. All calls to the kernel uses this +interface. +""" +import json, pexpect, pathlib, unittest +from pantograph.expr import Variable, Goal, GoalState +def _get_proc_cwd(): + return pathlib.Path(__file__).parent def _get_proc_path(): - return pathlib.Path(__file__).parent / "pantograph" + return _get_proc_cwd() / "pantograph" + +class ServerError(Exception): + pass class Server: @@ -17,6 +27,7 @@ class Server: self.timeout = timeout self.imports = imports self.maxread = maxread + self.proc_cwd = _get_proc_cwd() self.proc_path = _get_proc_path() self.options = options @@ -30,7 +41,8 @@ class Server: self.proc = pexpect.spawn( f"{self.proc_path} {self.args}", encoding="utf-8", - maxread=self.maxread + maxread=self.maxread, + cwd=self.proc_cwd, ) self.proc.setecho(False) @@ -47,18 +59,50 @@ class Server: def reset(self): return self.run("reset", {}) - def goal_start(self, expr: str): - return self.run('goal.start', {"expr": str(expr)}) - def goal_tactic(self, stateId: int, goalId: int, tactic): - return self.run('goal.tactic', {"stateId": stateId, "goalId": goalId, "tactic": tactic}) + def goal_start(self, expr: str) -> GoalState: + result = self.run('goal.start', {"expr": str(expr)}) + if "error" in result: + raise ServerError(result["desc"]) + return GoalState(state_id = result["stateId"], goals = [Goal.sentence(expr)]) + def goal_tactic(self, state: GoalState, goalId: int, tactic: str) -> GoalState: + result = self.run('goal.tactic', { + "stateId": state.state_id, "goalId": goalId, "tactic": tactic}) + if "error" in result: + raise ServerError(result["desc"]) + if "tacticErrors" in result: + raise ServerError(result["tacticErrors"]) + if "parseError" in result: + raise ServerError(result["parseError"]) + state_id = result["nextStateId"] + goals = [Goal._parse(payload) for payload in result["goals"]] + return GoalState(state_id, goals) -def check_version(): +def get_version(): import subprocess - with subprocess.Popen([_get_proc_path(), "--version"], stdout=subprocess.PIPE) as p: - v = p.communicate()[0].decode('utf-8').strip() - print(v) + with subprocess.Popen([_get_proc_path(), "--version"], + stdout=subprocess.PIPE, + cwd=_get_proc_cwd()) as p: + return p.communicate()[0].decode('utf-8').strip() +class TestServer(unittest.TestCase): + + def test_version(self): + self.assertEqual(get_version(), "0.2.14") + + def test_goal_start(self): + server = Server() + state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p") + self.assertEqual(state0.state_id, 0) + state1 = server.goal_tactic(state0, goalId=0, tactic="intro a") + self.assertEqual(state1.state_id, 1) + self.assertEqual(state1.goals, [Goal( + variables=[Variable(name="a", t="Prop")], + target="∀ (q : Prop), a ∨ q → q ∨ a", + name=None, + )]) + self.assertEqual(str(state1.goals[0]),"a : Prop\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a") + if __name__ == '__main__': - check_version() + unittest.main()