diff --git a/pantograph/expr.py b/pantograph/expr.py index 8bbb338..4ae0367 100644 --- a/pantograph/expr.py +++ b/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) -class TacticNormal: - payload: str + @staticmethod + def parse(payload: dict) -> Self: + 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] diff --git a/pantograph/server.py b/pantograph/server.py index 28fc63b..52a7661 100644 --- a/pantograph/server.py +++ b/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 @@ -66,11 +67,15 @@ class Server: return GoalState(state_id = result["stateId"], goals = [Goal.sentence(expr)]) def goal_tactic(self, state: GoalState, goal_id: int, tactic: Tactic) -> GoalState: - args = { "stateId": state.state_id, "goalId": goal_id} - if isinstance(tactic, TacticNormal): - args["tactic"] = tactic.payload + args = {"stateId": state.state_id, "goalId": goal_id} + if isinstance(tactic, str): + 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"] - goals = [Goal._parse(payload) for payload in result["goals"]] - return GoalState(state_id, goals) + return GoalState.parse(result) + + 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()