diff --git a/README.md b/README.md index b533429..d44c1c2 100644 --- a/README.md +++ b/README.md @@ -8,8 +8,9 @@ Execute ```bash poetry build ``` -If the build is successful, the following command should succeed and output the current version of Pantograph. +To run server tests: ``` bash python -m pantograph.server ``` +The tests in `pantograph/server.py` also serve as simple interaction examples diff --git a/pantograph/expr.py b/pantograph/expr.py index 91b35c1..71ef971 100644 --- a/pantograph/expr.py +++ b/pantograph/expr.py @@ -2,7 +2,7 @@ Data structures for expressions and goals """ from dataclasses import dataclass -from typing import Optional, Union +from typing import Optional, Union, List Expr = str @@ -16,7 +16,7 @@ class Variable: name: Optional[str] = None @staticmethod - def _parse(payload: dict) -> "Variable": # Replace 'Self' with 'Variable' + def parse(payload: dict) -> "Variable": # Replace 'Self' with 'Variable' name = payload.get("userName") t = parse_expr(payload["type"]) v = payload.get("value") @@ -33,7 +33,7 @@ class Variable: @dataclass(frozen=True) class Goal: - variables: list[Variable] + variables: List[Variable] target: Expr name: Optional[str] = None is_conversion: bool = False @@ -43,11 +43,11 @@ class Goal: return Goal(variables=[], target=target) @staticmethod - def _parse(payload: dict) -> "Goal": # Replace 'Self' with 'Goal' + def parse(payload: dict) -> "Goal": # Replace 'Self' with 'Goal' 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"] + is_conversion = payload.get("isConversion", False) # Handle missing keys return Goal(variables, target, name, is_conversion) def __str__(self): @@ -57,18 +57,27 @@ class Goal: @dataclass(frozen=True) class GoalState: state_id: int - goals: list[Goal] + goals: List[Goal] @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) -> "GoalState": # Replace 'Self' with 'GoalState' + state_id = payload.get("nextStateId", 0) # Handle missing keys + goals = [Goal.parse(g) for g in payload.get("goals", [])] + return GoalState(state_id, goals) @dataclass(frozen=True) class TacticHave: branch: str -Tactic = Union[TacticNormal, TacticHave] +@dataclass(frozen=True) +class TacticCalc: + step: str + +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()