max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: preserve usedAssignment flag when replacing MetavarContext

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-04 05:49:54 -07:00
parent 64d46272c2
commit 6b2d2ffac6
2 changed files with 6 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Lean/Meta/Basic.lean
View file

@ -307,8 +307,8 @@ protected def saveState : MetaM SavedState :=
/-- Restore backtrackable parts of the state. -/
def SavedState.restore (b : SavedState) : MetaM Unit := do
Core.restore b.core
let usedAssignment := (← getMCtx).usedAssignment
modify fun s => { s with mctx := { b.meta.mctx with usedAssignment }, zetaFVarIds := b.meta.zetaFVarIds, postponed := b.meta.postponed }
setMCtx b.meta.mctx -- Recall that `setMCtx` propagate `usedAssignment`
modify fun s => { s with zetaFVarIds := b.meta.zetaFVarIds, postponed := b.meta.postponed }
instance : MonadBacktrack SavedState MetaM where
saveState := Meta.saveState
@ -363,9 +363,6 @@ def getLocalInstances : MetaM LocalInstances :=
def getConfig : MetaM Config :=
return (← read).config
def setMCtx (mctx : MetavarContext) : MetaM Unit :=
modify fun s => { s with mctx := mctx }
def resetZetaFVarIds : MetaM Unit :=
modify fun s => { s with zetaFVarIds := {} }
@ -1144,13 +1141,8 @@ private def withNewMCtxDepthImp (x : MetaM α) : MetaM α := do
try
x
finally
-- TODO: document why we need to restore defEqCache
modify fun s => { s with
mctx := saved.mctx
cache.defEqDefault := saved.cache.defEqDefault
cache.defEqAll := saved.cache.defEqAll
postponed := saved.postponed
}
setMCtx saved.mctx -- Recall that `setMCtx` propagate `usedAssignment`
modify fun s => { s with postponed := saved.postponed }
/--
Save cache and `MetavarContext`, bump the `MetavarContext` depth, execute `x`,

4
src/Lean/MetavarContext.lean
View file

@ -294,8 +294,8 @@ instance (m n) [MonadLift m n] [MonadMCtx m] : MonadMCtx n where
def markUsedAssignment [MonadMCtx m] : m Unit :=
modifyMCtx fun mctx => { mctx with usedAssignment := true }
abbrev setMCtx [MonadMCtx m] (mctx : MetavarContext) : m Unit :=
modifyMCtx fun _ => mctx
abbrev setMCtx [MonadMCtx m] (mctx' : MetavarContext) : m Unit :=
modifyMCtx fun mctx => { mctx' with usedAssignment := mctx'.usedAssignment || mctx.usedAssignment }
abbrev getLevelMVarAssignment? [Monad m] [MonadMCtx m] (mvarId : MVarId) : m (Option Level) := do
let result? := (← getMCtx).lAssignment.find? mvarId