From 2d2ff24017151bca6f1e466e7a4cf565fc055291 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 25 Jun 2024 17:01:49 -0400 Subject: [PATCH] feat: FFI interface for `evaluate` tactic --- Pantograph/Library.lean | 10 +++++++++- Pantograph/Tactic/Prograde.lean | 2 +- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index aa8bcbc..71dcdfe 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -186,7 +186,15 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St | .error error => return .parseError error runTermElabM do state.restoreElabM - state.execute goalId (Tactic.have_t binderName.toName type) + state.execute goalId (Tactic.«have» binderName.toName type) +@[export pantograph_goal_evaluate_m] +protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do + let type ← match (← Compile.parseTermM type) with + | .ok syn => pure syn + | .error error => return .parseError error + runTermElabM do + state.restoreElabM + state.execute goalId (Tactic.evaluate binderName.toName type) @[export pantograph_goal_let_m] def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goalId binderName type diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index 4c525c2..59acaf1 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -19,7 +19,7 @@ def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do pure [mvarUpstream.mvarId!] Elab.Tactic.setGoals nextGoals -def have_t (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do +def «have» (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal let nextGoals: List MVarId ← goal.withContext do let type ← Elab.Term.elabType (stx := type)