refactor: simplify MonadCache and generalize instantiateExprMVars
This commit is contained in:
Leonardo de Moura
parent
c865abb340
commit
620647f2f1
5 changed files with 58 additions and 119 deletions
|
|
@ -124,8 +124,10 @@ instance {α} : Inhabited (MetaM α) :=
|
|||
instance : MonadLCtx MetaM :=
|
||||
{ getLCtx := do pure (← read).lctx }
|
||||
|
||||
instance : MonadMCtx MetaM :=
|
||||
{ getMCtx := do pure (← get).mctx }
|
||||
instance : MonadMCtx MetaM := {
|
||||
getMCtx := do pure (← get).mctx,
|
||||
modifyMCtx := fun f => modify fun s => { s with mctx := f s.mctx }
|
||||
}
|
||||
|
||||
instance : AddMessageContext MetaM :=
|
||||
{ addMessageContext := addMessageContextFull }
|
||||
|
|
@ -169,8 +171,6 @@ variables {n : Type → Type} [MonadControlT MetaM n] [Monad n]
|
|||
def getLocalInstances : m LocalInstances := liftMetaM do pure (← read).localInstances
|
||||
def getConfig : m Config := liftMetaM do pure (← read).config
|
||||
def setMCtx (mctx : MetavarContext) : m Unit := liftMetaM $ modify fun s => { s with mctx := mctx }
|
||||
@[inline] def modifyMCtx (f : MetavarContext → MetavarContext) : m Unit :=
|
||||
liftMetaM $ modify fun s => { s with mctx := f s.mctx }
|
||||
def resetZetaFVarIds : m Unit := liftMetaM $ modify fun s => { s with zetaFVarIds := {} }
|
||||
def getZetaFVarIds : m NameSet := liftMetaM do pure (← get).zetaFVarIds
|
||||
|
||||
|
|
@ -271,7 +271,7 @@ match mctx.findDecl? mvarId with
|
|||
| some d => pure d
|
||||
| none => throwError! "unknown metavariable '{mkMVar mvarId}'"
|
||||
|
||||
def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : m Unit :=
|
||||
def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : m Unit := liftMetaM do
|
||||
modifyMCtx fun mctx => mctx.setMVarKind mvarId kind
|
||||
|
||||
def isReadOnlyExprMVar (mvarId : MVarId) : m Bool := liftMetaM do
|
||||
|
|
@ -293,7 +293,7 @@ match mctx.findLevelDepth? mvarId with
|
|||
| some depth => pure $ depth != mctx.depth
|
||||
| _ => throwError! "unknown universe metavariable '{mkLevelMVar mvarId}'"
|
||||
|
||||
def renameMVar (mvarId : MVarId) (newUserName : Name) : m Unit :=
|
||||
def renameMVar (mvarId : MVarId) (newUserName : Name) : m Unit := liftMetaM do
|
||||
modifyMCtx fun mctx => mctx.renameMVar mvarId newUserName
|
||||
|
||||
def isExprMVarAssigned (mvarId : MVarId) : m Bool := liftMetaM do
|
||||
|
|
@ -335,13 +335,17 @@ match (← getLCtx).findFromUserName? userName with
|
|||
| some d => pure d
|
||||
| none => throwError! "unknown local declaration '{userName}'"
|
||||
|
||||
def instantiateLevelMVarsImp (u : Level) : MetaM Level :=
|
||||
MetavarContext.instantiateLevelMVars u
|
||||
|
||||
def instantiateLevelMVars (u : Level) : m Level := liftMetaM do
|
||||
instantiateLevelMVarsImp u
|
||||
|
||||
def instantiateMVarsImp (e : Expr) : MetaM Expr :=
|
||||
(MetavarContext.instantiateExprMVars e).run
|
||||
|
||||
def instantiateMVars (e : Expr) : m Expr := liftMetaM do
|
||||
if e.hasMVar then
|
||||
modifyGet fun s =>
|
||||
let (e, mctx) := s.mctx.instantiateMVars e;
|
||||
(e, { s with mctx := mctx })
|
||||
else
|
||||
pure e
|
||||
instantiateMVarsImp e
|
||||
|
||||
def instantiateLocalDeclMVars (localDecl : LocalDecl) : m LocalDecl := liftMetaM do
|
||||
match localDecl with
|
||||
|
|
@ -902,19 +906,10 @@ withConfig (fun config => { config with foApprox := true, ctxApprox := true, qua
|
|||
@[inline] def fullApproxDefEq {α} : n α → n α :=
|
||||
mapMetaM fullApproxDefEqImp
|
||||
|
||||
@[inline] private def liftStateMCtx {α} (x : StateM MetavarContext α) : MetaM α := do
|
||||
let mctx ← getMCtx
|
||||
let (a, mctx) := x.run mctx
|
||||
setMCtx mctx
|
||||
pure a
|
||||
|
||||
def instantiateLevelMVars (u : Level) : m Level :=
|
||||
liftMetaM $ liftStateMCtx $ MetavarContext.instantiateLevelMVars u
|
||||
|
||||
def normalizeLevel (u : Level) : m Level :=
|
||||
liftMetaM do let u ← instantiateLevelMVars u; pure u.normalize
|
||||
|
||||
def assignLevelMVar (mvarId : MVarId) (u : Level) : m Unit :=
|
||||
def assignLevelMVar (mvarId : MVarId) (u : Level) : m Unit := liftMetaM do
|
||||
modifyMCtx fun mctx => mctx.assignLevel mvarId u
|
||||
|
||||
def whnfD [MonadLiftT MetaM n] (e : Expr) : n Expr :=
|
||||
|
|
|
|||
|
|
@ -286,6 +286,17 @@ structure MetavarContext :=
|
|||
(eAssignment : PersistentHashMap MVarId Expr := {})
|
||||
(dAssignment : PersistentHashMap MVarId DelayedMetavarAssignment := {})
|
||||
|
||||
class MonadMCtx (m : Type → Type) :=
|
||||
(getMCtx : m MetavarContext)
|
||||
(modifyMCtx : (MetavarContext → MetavarContext) → m Unit)
|
||||
|
||||
export MonadMCtx (getMCtx modifyMCtx)
|
||||
|
||||
instance (m n) [MonadMCtx m] [MonadLift m n] : MonadMCtx n := {
|
||||
getMCtx := liftM (getMCtx : m _),
|
||||
modifyMCtx := fun f => liftM (modifyMCtx f : m _)
|
||||
}
|
||||
|
||||
namespace MetavarContext
|
||||
|
||||
instance : Inhabited MetavarContext := ⟨{}⟩
|
||||
|
|
@ -487,56 +498,43 @@ def hasAssignableMVar (mctx : MetavarContext) : Expr → Bool
|
|||
| Expr.mvar mvarId _ => mctx.isExprAssignable mvarId
|
||||
| Expr.localE _ _ _ _ => unreachable!
|
||||
|
||||
partial def instantiateLevelMVars : Level → StateM MetavarContext Level
|
||||
partial def instantiateLevelMVars {m} [Monad m] [MonadMCtx m] : Level → m Level
|
||||
| lvl@(Level.succ lvl₁ _) => do return Level.updateSucc! lvl (← instantiateLevelMVars lvl₁)
|
||||
| lvl@(Level.max lvl₁ lvl₂ _) => do return Level.updateMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂)
|
||||
| lvl@(Level.imax lvl₁ lvl₂ _) => do return Level.updateIMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂)
|
||||
| lvl@(Level.mvar mvarId _) => do
|
||||
let mctx ← get
|
||||
match getLevelAssignment? mctx mvarId with
|
||||
match getLevelAssignment? (← getMCtx) mvarId with
|
||||
| some newLvl =>
|
||||
if !newLvl.hasMVar then pure newLvl
|
||||
else do
|
||||
let newLvl' ← instantiateLevelMVars newLvl
|
||||
modify fun mctx => mctx.assignLevel mvarId newLvl'
|
||||
modifyMCtx fun mctx => mctx.assignLevel mvarId newLvl'
|
||||
pure newLvl'
|
||||
| none => pure lvl
|
||||
| lvl => pure lvl
|
||||
|
||||
namespace InstantiateExprMVars
|
||||
private abbrev M := StateM (WithHashMapCache Expr Expr MetavarContext)
|
||||
|
||||
@[inline] def instantiateLevelMVars (lvl : Level) : M Level :=
|
||||
WithHashMapCache.fromState $ MetavarContext.instantiateLevelMVars lvl
|
||||
|
||||
@[inline] private def getMCtx : M MetavarContext := do
|
||||
let s ← get; pure s.state
|
||||
|
||||
@[inline] private def modifyCtx (f : MetavarContext → MetavarContext) : M Unit :=
|
||||
modify fun s => { s with state := f s.state }
|
||||
|
||||
/-- instantiateExprMVars main function -/
|
||||
partial def main (e : Expr) : M Expr :=
|
||||
partial def instantiateExprMVars {m ω} [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLiftT (ST ω) m] (e : Expr) : MonadCacheT Expr Expr m Expr :=
|
||||
if !e.hasMVar then
|
||||
pure e
|
||||
else checkCache e fun e => do match e with
|
||||
| Expr.proj _ _ s _ => return e.updateProj! (← main s)
|
||||
| Expr.forallE _ d b _ => return e.updateForallE! (← main d) (← main b)
|
||||
| Expr.lam _ d b _ => return e.updateLambdaE! (← main d) (← main b)
|
||||
| Expr.letE _ t v b _ => return e.updateLet! (← main t) (← main v) (← main b)
|
||||
| Expr.proj _ _ s _ => return e.updateProj! (← instantiateExprMVars s)
|
||||
| Expr.forallE _ d b _ => return e.updateForallE! (← instantiateExprMVars d) (← instantiateExprMVars b)
|
||||
| Expr.lam _ d b _ => return e.updateLambdaE! (← instantiateExprMVars d) (← instantiateExprMVars b)
|
||||
| Expr.letE _ t v b _ => return e.updateLet! (← instantiateExprMVars t) (← instantiateExprMVars v) (← instantiateExprMVars b)
|
||||
| Expr.const _ lvls _ => return e.updateConst! (← lvls.mapM instantiateLevelMVars)
|
||||
| Expr.sort lvl _ => return e.updateSort! (← instantiateLevelMVars lvl)
|
||||
| Expr.mdata _ b _ => return e.updateMData! (← main b)
|
||||
| Expr.mdata _ b _ => return e.updateMData! (← instantiateExprMVars b)
|
||||
| Expr.app _ _ _ => e.withApp fun f args => do
|
||||
let instArgs (f : Expr) : M Expr := do
|
||||
let args ← args.mapM main
|
||||
let instArgs (f : Expr) : MonadCacheT Expr Expr m Expr := do
|
||||
let args ← args.mapM instantiateExprMVars
|
||||
pure (mkAppN f args)
|
||||
let instApp : M Expr := do
|
||||
let instApp : MonadCacheT Expr Expr m Expr := do
|
||||
let wasMVar := f.isMVar
|
||||
let f ← main f
|
||||
let f ← instantiateExprMVars f
|
||||
if wasMVar && f.isLambda then
|
||||
/- Some of the arguments in args are irrelevant after we beta reduce. -/
|
||||
main (f.betaRev args.reverse)
|
||||
instantiateExprMVars (f.betaRev args.reverse)
|
||||
else
|
||||
instArgs f
|
||||
match f with
|
||||
|
|
@ -558,11 +556,11 @@ partial def main (e : Expr) : M Expr :=
|
|||
when we are checking for unassigned metavariables in an elaborated term. -/
|
||||
instArgs f
|
||||
else
|
||||
let newVal ← main val
|
||||
let newVal ← instantiateExprMVars val
|
||||
if newVal.hasExprMVar then
|
||||
instArgs f
|
||||
else do
|
||||
let args ← args.mapM main
|
||||
let args ← args.mapM instantiateExprMVars
|
||||
/-
|
||||
Example: suppose we have
|
||||
`?m t1 t2 t3`
|
||||
|
|
@ -582,17 +580,24 @@ partial def main (e : Expr) : M Expr :=
|
|||
let mctx ← getMCtx
|
||||
match mctx.getExprAssignment? mvarId with
|
||||
| some newE => do
|
||||
let newE' ← main newE
|
||||
modifyCtx fun mctx => mctx.assignExpr mvarId newE'
|
||||
let newE' ← instantiateExprMVars newE
|
||||
modifyMCtx fun mctx => mctx.assignExpr mvarId newE'
|
||||
pure newE'
|
||||
| none => pure e
|
||||
| e => pure e
|
||||
|
||||
end InstantiateExprMVars
|
||||
instance {ω} : MonadMCtx (StateRefT MetavarContext (ST ω)) := {
|
||||
getMCtx := get,
|
||||
modifyMCtx := modify
|
||||
}
|
||||
|
||||
def instantiateMVars (mctx : MetavarContext) (e : Expr) : Expr × MetavarContext :=
|
||||
if !e.hasMVar then (e, mctx)
|
||||
else (WithHashMapCache.toState $ InstantiateExprMVars.main e).run mctx
|
||||
if !e.hasMVar then
|
||||
(e, mctx)
|
||||
else
|
||||
let instantiate {ω} (e : Expr) : (MonadCacheT Expr Expr $ StateRefT MetavarContext $ ST ω) Expr :=
|
||||
instantiateExprMVars e
|
||||
runST fun _ => instantiate e $.run $.run mctx
|
||||
|
||||
def instantiateLCtxMVars (mctx : MetavarContext) (lctx : LocalContext) : LocalContext × MetavarContext :=
|
||||
lctx.foldl
|
||||
|
|
@ -1105,12 +1110,4 @@ def getExprAssignmentDomain (mctx : MetavarContext) : Array MVarId :=
|
|||
|
||||
end MetavarContext
|
||||
|
||||
class MonadMCtx (m : Type → Type) :=
|
||||
(getMCtx : m MetavarContext)
|
||||
|
||||
export MonadMCtx (getMCtx)
|
||||
|
||||
instance (m n) [MonadMCtx m] [MonadLift m n] : MonadMCtx n :=
|
||||
{ getMCtx := liftM (getMCtx : m _) }
|
||||
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -74,57 +74,4 @@ instance : MonadControl m (MonadCacheT α β m) := inferInstanceAs (MonadControl
|
|||
instance [MonadFinally m] : MonadFinally (MonadCacheT α β m) := inferInstanceAs (MonadFinally (StateRefT _ _))
|
||||
|
||||
end MonadCacheT
|
||||
|
||||
/-- Auxiliary structure for "adding" a `HashMap` to a state object. -/
|
||||
structure WithHashMapCache (α β σ : Type) [HasBeq α] [Hashable α] :=
|
||||
(state : σ)
|
||||
(cache : HashMap α β := {})
|
||||
|
||||
namespace WithHashMapCache
|
||||
|
||||
@[inline] def getCache {α β σ : Type} [HasBeq α] [Hashable α] : StateM (WithHashMapCache α β σ) (HashMap α β) := do
|
||||
let s ← get; pure s.cache
|
||||
|
||||
@[inline] def modifyCache {α β σ : Type} [HasBeq α] [Hashable α] (f : HashMap α β → HashMap α β) : StateM (WithHashMapCache α β σ) Unit :=
|
||||
modify fun s => { s with cache := f s.cache }
|
||||
|
||||
instance (α β σ : Type) [HasBeq α] [Hashable α] : MonadHashMapCacheAdapter α β (StateM (WithHashMapCache α β σ)) :=
|
||||
{ getCache := WithHashMapCache.getCache,
|
||||
modifyCache := WithHashMapCache.modifyCache }
|
||||
|
||||
@[inline] def getCacheE {α β ε σ : Type} [HasBeq α] [Hashable α] : EStateM ε (WithHashMapCache α β σ) (HashMap α β) := do
|
||||
let s ← get; pure s.cache
|
||||
|
||||
@[inline] def modifyCacheE {α β ε σ : Type} [HasBeq α] [Hashable α] (f : HashMap α β → HashMap α β) : EStateM ε (WithHashMapCache α β σ) Unit :=
|
||||
modify fun s => { s with cache := f s.cache }
|
||||
|
||||
instance (α β ε σ : Type) [HasBeq α] [Hashable α] : MonadHashMapCacheAdapter α β (EStateM ε (WithHashMapCache α β σ)) :=
|
||||
{ getCache := WithHashMapCache.getCacheE,
|
||||
modifyCache := WithHashMapCache.modifyCacheE }
|
||||
|
||||
@[inline] def fromState {α β σ δ : Type} [HasBeq α] [Hashable α] (x : StateM σ δ) : StateM (WithHashMapCache α β σ) δ :=
|
||||
adaptState
|
||||
(fun (s : WithHashMapCache α β σ) => (s.state, s.cache))
|
||||
(fun (s : σ) (cache : HashMap α β) => { state := s, cache := cache })
|
||||
x
|
||||
|
||||
@[inline] def toState {α β σ δ : Type} [HasBeq α] [Hashable α] (x : StateM (WithHashMapCache α β σ) δ) : StateM σ δ :=
|
||||
adaptState'
|
||||
(fun (s : σ) => ({ state := s } : WithHashMapCache α β σ))
|
||||
(fun (s : WithHashMapCache α β σ) => s.state)
|
||||
x
|
||||
|
||||
@[inline] def fromEState {α β σ ε δ : Type} [HasBeq α] [Hashable α] (x : EStateM ε σ δ) : EStateM ε (WithHashMapCache α β σ) δ :=
|
||||
adaptState
|
||||
(fun (s : WithHashMapCache α β σ) => (s.state, s.cache))
|
||||
(fun (s : σ) (cache : HashMap α β) => { state := s, cache := cache })
|
||||
x
|
||||
|
||||
@[inline] def toEState {α β σ ε δ : Type} [HasBeq α] [Hashable α] (x : EStateM ε (WithHashMapCache α β σ) δ) : EStateM ε σ δ :=
|
||||
adaptState'
|
||||
(fun (s : σ) => ({ state := s } : WithHashMapCache α β σ))
|
||||
(fun (s : WithHashMapCache α β σ) => s.state)
|
||||
x
|
||||
|
||||
end WithHashMapCache
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -44,7 +44,7 @@ builtin_initialize ppExt : EnvExtension PPFns ←
|
|||
registerEnvExtension $ ppFnsRef.get
|
||||
|
||||
def ppExpr (ctx : PPContext) (e : Expr) : IO Format :=
|
||||
let e := (ctx.mctx.instantiateMVars e).1
|
||||
let e := ctx.mctx.instantiateMVars e $.1
|
||||
if getPPRaw ctx.opts then
|
||||
pure $ format (toString e)
|
||||
else
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format :=
|
|||
let lctx := lctx.sanitizeNames.run' { options := opts }
|
||||
let ppCtx := { ppCtx with lctx := lctx }
|
||||
let pp (e : Expr) : IO Format := ppExpr ppCtx e
|
||||
let instMVars (e : Expr) : Expr := (mctx.instantiateMVars e).1
|
||||
let instMVars (e : Expr) : Expr := mctx.instantiateMVars e $.1
|
||||
let addLine (fmt : Format) : Format := if fmt.isNil then fmt else fmt ++ Format.line
|
||||
let pushPending (ids : List Name) (type? : Option Expr) (fmt : Format) : IO Format :=
|
||||
if ids.isEmpty then
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue