feat: Have, calc, conv

pantograph/expr.py

@@ -16,7 +16,7 @@ class Variable:
     name: Optional[str] = None
 
     @staticmethod
-    def _parse(payload: dict) -> Self:
+    def parse(payload: dict) -> Self:
         name = payload.get("userName")
         t = parse_expr(payload["type"])
         v = payload.get("value")
@@ -43,9 +43,9 @@ class Goal:
         return Goal(variables=[], target=target)
 
     @staticmethod
-    def _parse(payload: dict) -> Self:
+    def parse(payload: dict) -> Self:
         name = payload.get("userName")
-        variables = [Variable._parse(v) for v in payload["vars"]]
+        variables = [Variable.parse(v) for v in payload["vars"]]
         target = parse_expr(payload["target"])
         is_conversion = payload["isConversion"]
         return Goal(variables, target, name, is_conversion)
@@ -62,13 +62,22 @@ class GoalState:
 
     @property
     def is_solved(self) -> bool:
+        """
+        WARNING: Does not handle dormant goals.
+        """
         return not self.goals
 
-@dataclass(frozen=True)
+    @staticmethod
-class TacticNormal:
+    def parse(payload: dict) -> Self:
-    payload: str
+        state_id = payload["nextStateId"]
+        goals = [Goal.parse(g) for g in payload["goals"]]
+        return GoalState(state_id, goals)
+
 @dataclass(frozen=True)
 class TacticHave:
     branch: str
+@dataclass(frozen=True)
+class TacticCalc:
+    step: str
 
-Tactic = Union[TacticNormal, TacticHave]
+Tactic = Union[str, TacticHave, TacticCalc]

pantograph/server.py

@@ -3,7 +3,8 @@ 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, Tactic, TacticNormal
+from pantograph.expr import Variable, Goal, GoalState, \
+    Tactic, TacticHave, TacticCalc
 
 def _get_proc_cwd():
     return pathlib.Path(__file__).parent
@@ -67,10 +68,14 @@ class Server:
 
     def goal_tactic(self, state: GoalState, goal_id: int, tactic: Tactic) -> GoalState:
         args = {"stateId": state.state_id, "goalId": goal_id}
-        if isinstance(tactic, TacticNormal):
+        if isinstance(tactic, str):
-            args["tactic"] = tactic.payload
+            args["tactic"] = tactic
+        elif isinstance(tactic, TacticHave):
+            args["have"] = tactic.branch
+        elif isinstance(tactic, TacticCalc):
+            args["calc"] = tactic.step
         else:
-            raise Exception(f"Invalid tactic type: {tactic}")
+            raise RuntimeError(f"Invalid tactic type: {tactic}")
         result = self.run('goal.tactic', args)
         if "error" in result:
             raise ServerError(result["desc"])
@@ -78,9 +83,28 @@ class Server:
             raise ServerError(result["tacticErrors"])
         if "parseError" in result:
             raise ServerError(result["parseError"])
-        state_id = result["nextStateId"]
+        return GoalState.parse(result)
-        goals = [Goal._parse(payload) for payload in result["goals"]]
+
-        return GoalState(state_id, goals)
+    def goal_conv_begin(self, state: GoalState, goal_id: int) -> GoalState:
+        result = self.run('goal.tactic', {"stateId": state.state_id, "goalId": goal_id, "conv": True})
+        if "error" in result:
+            raise ServerError(result["desc"])
+        if "tacticErrors" in result:
+            raise ServerError(result["tacticErrors"])
+        if "parseError" in result:
+            raise ServerError(result["parseError"])
+        return GoalState.parse(result)
+
+    def goal_conv_end(self, state: GoalState) -> GoalState:
+        result = self.run('goal.tactic', {"stateId": state.state_id, "goalId": 0, "conv": False})
+        if "error" in result:
+            raise ServerError(result["desc"])
+        if "tacticErrors" in result:
+            raise ServerError(result["tacticErrors"])
+        if "parseError" in result:
+            raise ServerError(result["parseError"])
+        return GoalState.parse(result)
+
 
 def get_version():
     import subprocess
@@ -99,7 +123,7 @@ class TestServer(unittest.TestCase):
         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, goal_id=0, tactic=TacticNormal("intro a"))
+        state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a")
         self.assertEqual(state1.state_id, 1)
         self.assertEqual(state1.goals, [Goal(
             variables=[Variable(name="a", t="Prop")],
@@ -108,5 +132,39 @@ class TestServer(unittest.TestCase):
         )])
         self.assertEqual(str(state1.goals[0]),"a : Prop\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a")
 
+    def test_conv_calc(self):
+        server = Server()
+        state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
+
+        variables = [
+            Variable(name="a", t="Nat"),
+            Variable(name="b", t="Nat"),
+            Variable(name="h", t="b = 2"),
+        ]
+        state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a b h")
+        state2 = server.goal_tactic(state1, goal_id=0, tactic=TacticCalc("1 + a + 1 = a + 1 + 1"))
+        self.assertEqual(state2.goals, [
+            Goal(
+                variables,
+                target="1 + a + 1 = a + 1 + 1",
+                name='calc',
+            ),
+            Goal(
+                variables,
+                target="a + 1 + 1 = a + b",
+            ),
+        ])
+        state_c1 = server.goal_conv_begin(state2, goal_id=0)
+        state_c2 = server.goal_tactic(state_c1, goal_id=0, tactic="rhs")
+        state_c3 = server.goal_tactic(state_c2, goal_id=0, tactic="rw [Nat.add_comm]")
+        state_c4 = server.goal_conv_end(state_c3)
+        state_c5 = server.goal_tactic(state_c4, goal_id=0, tactic="rfl")
+        self.assertTrue(state_c5.is_solved)
+
+        state3 = server.goal_tactic(state2, goal_id=1, tactic=TacticCalc("_ = a + 2"))
+        state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
+        self.assertTrue(state4.is_solved)
+
+
 if __name__ == '__main__':
     unittest.main()