From 39ec79e6bb11a49d6f0137385e6a70969d3c55c5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 8 Mar 2025 21:07:15 -0800 Subject: [PATCH] feat: Monad lifting in `GoalState.withContext` --- Pantograph/Goal.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index aaff02d..43f3e85 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -74,13 +74,14 @@ protected def GoalState.metaState (state: GoalState): Meta.State := protected def GoalState.coreState (state: GoalState): Core.SavedState := state.savedState.term.meta.core -protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do +protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState - +protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α := + Meta.mapMetaM <| state.withContext' mvarId protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α := - Meta.mapMetaM <| state.withContext state.parentMVar?.get! + Meta.mapMetaM <| state.withContext' state.parentMVar?.get! protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α := - Meta.mapMetaM <| state.withContext state.root + Meta.mapMetaM <| state.withContext' state.root private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k