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

perf: zero startup time function summaries

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-26 21:55:37 -07:00
parent ad98df80fe
commit 39249f0c1d
1 changed files with 19 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/Lean/Compiler/IR/ElimDeadBranches.lean
View file

@ -122,21 +122,34 @@ def widening (env : Environment) (v₁ v₂ : Value) : Value :=
end Value
abbrev FunctionSummaries := SMap FunId Value
abbrev FunctionSummaries := PHashMap FunId Value
private abbrev declLt (a b : FunId × Value) :=
Name.quickLt a.1 b.1
private abbrev sortEntries (entries : Array (FunId × Value)) : Array (FunId × Value) :=
entries.qsort declLt
private abbrev findAtSorted? (entries : Array (FunId × Value)) (fid : FunId) : Option Value :=
if let some (_, value) := entries.binSearch (fid, default) declLt then
some value
else
none
builtin_initialize functionSummariesExt : SimplePersistentEnvExtension (FunId × Value) FunctionSummaries ←
registerSimplePersistentEnvExtension {
addImportedFn := fun as =>
let cache : FunctionSummaries := mkStateFromImportedEntries (fun s (p : FunId × Value) => s.insert p.1 p.2) {} as
cache.switch,
addImportedFn := fun _ => {}
addEntryFn := fun s ⟨e, n⟩ => s.insert e n
toArrayFn := fun s => sortEntries s.toArray
}
def addFunctionSummary (env : Environment) (fid : FunId) (v : Value) : Environment :=
functionSummariesExt.addEntry env (fid, v)
functionSummariesExt.addEntry (env.addExtraName fid) (fid, v)
def getFunctionSummary? (env : Environment) (fid : FunId) : Option Value :=
(functionSummariesExt.getState env).find? fid
match env.getModuleIdxFor? fid with
| some modIdx => findAtSorted? (functionSummariesExt.getModuleEntries env modIdx) fid
| none => functionSummariesExt.getState env |>.find? fid
abbrev Assignment := HashMap VarId Value