Skip to content

perf: no-import matcher info #11046

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

perf: no-import matcher info #11046

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 11 additions & 6 deletions src/Lean/Meta/Match/MatcherInfo.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ structure MatcherInfo where
`discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`.
-/
discrInfos : Array DiscrInfo
deriving Inhabited

@[expose] def MatcherInfo.numAlts (info : MatcherInfo) : Nat :=
info.altNumParams.size
Expand Down Expand Up @@ -75,21 +76,20 @@ structure Entry where
info : MatcherInfo

structure State where
map : SMap Name MatcherInfo := {}
map : PHashMap Name MatcherInfo := {}

instance : Inhabited State := ⟨{}⟩

def State.addEntry (s : State) (e : Entry) : State := { s with map := s.map.insert e.name e.info }
def State.switch (s : State) : State := { s with map := s.map.switch }

builtin_initialize extension : SimplePersistentEnvExtension Entry State ←
private builtin_initialize extension : SimplePersistentEnvExtension Entry State ←
registerSimplePersistentEnvExtension {
addEntryFn := State.addEntry
addImportedFn := fun es => (mkStateFromImportedEntries State.addEntry {} es).switch
addImportedFn := fun _ => {}
asyncMode := .async .mainEnv
exportEntriesFnEx? := some fun env _ entries _ =>
-- Do not export info for private defs
entries.filter (env.contains (skipRealize := false) ·.name) |>.toArray
entries.filter (env.contains (skipRealize := false) ·.name) |>.toArray.qsort (Name.quickLt ·.name ·.name)
}

def addMatcherInfo (env : Environment) (matcherName : Name) (info : MatcherInfo) : Environment :=
Expand All @@ -100,7 +100,12 @@ def getMatcherInfo? (env : Environment) (declName : Name) : Option MatcherInfo :
-- avoid blocking on async decls whose names look nothing like matchers
let .str _ s := declName.eraseMacroScopes | none
guard <| s.startsWith "match_"
(extension.getState (asyncDecl := declName) env).map.find? declName
match env.getModuleIdxFor? declName with
| some modIdx =>
extension.getModuleEntries env modIdx
|>.binSearch { name := declName, info := default } (Name.quickLt ·.name ·.name)
|>.map (·.info)
| none => (extension.getState (asyncDecl := declName) env).map.find? declName

end Extension

Expand Down
Loading