perf: no-import matcher info

Author: Kha

src/Lean/Meta/Match/MatcherInfo.lean

@@ -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
@@ -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 :=
@@ -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