sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

perf: faster LCNF internalization

Browse Source
This commit is contained in:
Henrik Böving
2026-03-10 12:59:31 +00:00
parent ff6816a854
commit 7217ddc052
1 changed files with 6 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
src/Lean/Compiler/LCNF/Internalize.lean
View File

@@ -32,14 +32,10 @@ def InternalizeM.run' (x : InternalizeM pu α) (state : FVarSubst pu) (ctx : Con
private def refreshBinderName (binderName : Name) : InternalizeM pu Name := do
match binderName with
| .num p _ =>
let r := .num p (← getThe CompilerM.State).nextIdx
modifyThe CompilerM.State fun s => { s with nextIdx := s.nextIdx + 1 }
return r
return .num p (← modifyGetThe CompilerM.State fun s => (s.nextIdx, { s with nextIdx := s.nextIdx + 1 }))
| _ =>
if (← read).uniqueIdents then
let r := .num binderName (← getThe CompilerM.State).nextIdx
modifyThe CompilerM.State fun s => { s with nextIdx := s.nextIdx + 1 }
return r
return .num binderName (← modifyGetThe CompilerM.State fun s => (s.nextIdx, { s with nextIdx := s.nextIdx + 1 }))
else
return binderName
@@ -59,7 +55,10 @@ private def mkNewFVarId (fvarId : FVarId) : InternalizeM pu FVarId := do
addFVarSubst fvarId fvarId'
return fvarId'
private partial def internalizeExpr (e : Expr) : InternalizeM pu Expr :=
private partial def internalizeExpr (e : Expr) : InternalizeM pu Expr := do
if pu == .impure then
-- impure types don't contain fvars
return e
go e
where
goApp (e : Expr) : InternalizeM pu Expr := do