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

perf: use lean_instantiate_level_mvars (#4912)

Browse source 
implemented in C/C++.
Next step: same for `instantiateExprMVars`
This commit is contained in:
Leonardo de Moura 2024-08-05 01:21:57 +02:00 • committed by GitHub
parent 2d09c96caf
commit f62359acc7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Lean/MetavarContext.lean
View file

@ -541,20 +541,10 @@ This operation is performed at `instantiateExprMVars`, `elimMVarDeps`, and `leve
@[extern "lean_instantiate_level_mvars"]
opaque instantiateLevelMVarsImp (mctx : MetavarContext) (l : Level) : MetavarContext × Level
partial def instantiateLevelMVars [Monad m] [MonadMCtx m] : Level → m Level
| lvl@(Level.succ lvl₁) => return Level.updateSucc! lvl (← instantiateLevelMVars lvl₁)
| lvl@(Level.max lvl₁ lvl₂) => return Level.updateMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂)
| lvl@(Level.imax lvl₁ lvl₂) => return Level.updateIMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂)
| lvl@(Level.mvar mvarId) => do
match (← getLevelMVarAssignment? mvarId) with
| some newLvl =>
if !newLvl.hasMVar then pure newLvl
else do
let newLvl' ← instantiateLevelMVars newLvl
assignLevelMVar mvarId newLvl'
pure newLvl'
| none => pure lvl
| lvl => pure lvl
partial def instantiateLevelMVars [Monad m] [MonadMCtx m] (l : Level) : m Level := do
let (mctx, lNew) := instantiateLevelMVarsImp (← getMCtx) l
setMCtx mctx
return lNew
@[extern "lean_instantiate_expr_mvars"]
opaque instantiateExprMVarsImp (mctx : MetavarContext) (e : Expr) : MetavarContext × Expr