aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 2 Packages Projects Releases Wiki Activity

feat: Monad lifting in `GoalState.withContext`

This commit is contained in:
Leni Aniva 2025-03-08 21:07:15 -08:00
parent 999bb146fa
commit 39ec79e6bb
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Pantograph/Goal.lean
View File

@ -74,13 +74,14 @@ protected def GoalState.metaState (state: GoalState): Meta.State :=
protected def GoalState.coreState (state: GoalState): Core.SavedState := protected def GoalState.coreState (state: GoalState): Core.SavedState :=
state.savedState.term.meta.core 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 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 α := 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 α := 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 := private def GoalState.mvars (state: GoalState): SSet MVarId :=
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k