feat: expression types and tests

.gitignore

@@ -9,3 +9,4 @@
 /dist
 
 pantograph/pantograph
+pantograph/lean-toolchain

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")

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

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()