From 9fbc65829d24eaded6ed2111555c28daddb94096 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 8 Apr 2024 12:50:41 -0700 Subject: [PATCH] feat: FFI interface to conv functions --- Pantograph/Library.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 5ac38c8..04d1a57 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -162,15 +162,23 @@ def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := @[export pantograph_goal_tactic_m] def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := - runTermElabM <| GoalState.tryTactic state goalId tactic + runTermElabM <| state.tryTactic goalId tactic @[export pantograph_goal_assign_m] def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := - runTermElabM <| GoalState.tryAssign state goalId expr + runTermElabM <| state.tryAssign goalId expr @[export pantograph_goal_have_m] def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := - runTermElabM <| GoalState.tryHave state goalId binderName type + runTermElabM <| state.tryHave goalId binderName type + +@[export pantograph_goal_conv_m] +def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := + runTermElabM <| state.conv goalId + +@[export pantograph_goal_conv_exit_m] +def goalConvExit (state: GoalState): Lean.CoreM TacticResult := + runTermElabM <| state.convExit @[export pantograph_goal_continue] def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=