From b3bd3cdde87ca40c89a125d77d3af79153ff2bf2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 2 Oct 2024 11:09:58 -0700 Subject: [PATCH] feat: Add binder name option in `TacticHave` --- pantograph/expr.py | 1 + pantograph/server.py | 16 ++++++++++++++++ 2 files changed, 17 insertions(+) diff --git a/pantograph/expr.py b/pantograph/expr.py index 895e56a..4312545 100644 --- a/pantograph/expr.py +++ b/pantograph/expr.py @@ -92,6 +92,7 @@ class GoalState: @dataclass(frozen=True) class TacticHave: branch: str + binder_name: Optional[str] = None @dataclass(frozen=True) class TacticCalc: step: str diff --git a/pantograph/server.py b/pantograph/server.py index 17927eb..e0f6870 100644 --- a/pantograph/server.py +++ b/pantograph/server.py @@ -123,6 +123,8 @@ class Server: args["tactic"] = tactic elif isinstance(tactic, TacticHave): args["have"] = tactic.branch + if tactic.binder_name: + args["binderName"] = tactic.binder_name elif isinstance(tactic, TacticCalc): args["calc"] = tactic.step else: @@ -285,6 +287,20 @@ class TestServer(unittest.TestCase): ) ]) + def test_have(self): + server = Server() + state0 = server.goal_start("1 + 1 = 2") + state1 = server.goal_tactic(state0, goal_id=0, tactic=TacticHave(branch="2 = 1 + 1", binder_name="h")) + self.assertEqual(state1.goals, [ + Goal( + variables=[], + target="2 = 1 + 1", + ), + Goal( + variables=[Variable(name="h", t="2 = 1 + 1")], + target="1 + 1 = 2", + ), + ]) def test_conv_calc(self): server = Server(options={"automaticMode": False})