refactor: rename TheoremPattern to EMatchTheorem

src/Lean/Elab/Tactic/Grind.lean

@@ -26,7 +26,7 @@ def elabGrindPattern : CommandElab := fun stx => do
           let pattern ← instantiateMVars (← elabTerm term none)
           let pattern ← Grind.unfoldReducible pattern
           return pattern.abstract xs
-        Grind.addTheoremPattern declName xs.size patterns.toList
+        Grind.addEMatchTheorem declName xs.size patterns.toList
   | _ => throwUnsupportedSyntax
 
 def grind (mvarId : MVarId) (mainDeclName : Name) : MetaM Unit := do

src/Lean/Meta/Tactic/Grind.lean

@@ -21,7 +21,7 @@ import Lean.Meta.Tactic.Grind.PP
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Ctor
 import Lean.Meta.Tactic.Grind.Parser
-import Lean.Meta.Tactic.Grind.TheoremPatterns
+import Lean.Meta.Tactic.Grind.EMatchTheorem
 
 namespace Lean
 

src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean → src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -32,8 +32,8 @@ def Origin.key : Origin → Name
   | .stx id _      => id
   | .other         => `other
 
--- TODO: find better name
-structure TheoremPattern where
+/-- A theorem for heuristic instantiation based on E-matching. -/
+structure EMatchTheorem where
   proof       : Expr
   numParams   : Nat
   patterns    : List Expr
@@ -42,21 +42,21 @@ structure TheoremPattern where
   origin      : Origin
   deriving Inhabited
 
--- TODO: find better name
-abbrev TheoremPatterns := PHashMap Name (List TheoremPattern)
+/-- The key is a symbol from `EMatchTheorem.symbols`. -/
+abbrev EMatchTheorems := PHashMap Name (List EMatchTheorem)
 
-def TheoremPatterns.insertTheorem (s : TheoremPatterns) (thm : TheoremPattern) : TheoremPatterns := Id.run do
+def EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchTheorems := Id.run do
   let .const declName :: syms := thm.symbols
     | unreachable!
   let thm := { thm with symbols := syms }
   if let some thms := s.find? declName then
-    return s.insert declName (thm::thms)
+    return PersistentHashMap.insert s declName (thm::thms)
   else
-    return s.insert declName [thm]
+    return PersistentHashMap.insert s declName [thm]
 
-builtin_initialize theoremPatternsExt : SimpleScopedEnvExtension TheoremPattern TheoremPatterns ←
+private builtin_initialize ematchTheoremsExt : SimpleScopedEnvExtension EMatchTheorem EMatchTheorems ←
   registerSimpleScopedEnvExtension {
-    addEntry := TheoremPatterns.insertTheorem
+    addEntry := EMatchTheorems.insert
     initial  := .empty
   }
 
@@ -295,7 +295,7 @@ private def ppParamsAt (proof : Expr) (numParms : Nat) (paramPos : List Nat) : M
         msg := msg ++ m!"{x} : {← inferType x}"
     addMessageContextFull msg
 
-def addTheoremPattern (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM Unit := do
+def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM Unit := do
   let .thmInfo info ← getConstInfo declName
     | throwError "`{declName}` is not a theorem, you cannot assign patterns to non-theorems for the `grind` tactic"
   let us := info.levelParams.map mkLevelParam
@@ -306,12 +306,12 @@ def addTheoremPattern (declName : Name) (numParams : Nat) (patterns : List Expr)
   if let .missing pos ← checkCoverage proof numParams bvarFound then
      let pats : MessageData := m!"{patterns.map ppPattern}"
      throwError "invalid pattern(s) for `{declName}`{indentD pats}\nthe following theorem parameters cannot be instantiated:{indentD (← ppParamsAt proof numParams pos)}"
-  theoremPatternsExt.add {
+  ematchTheoremsExt.add {
      proof, patterns, numParams, symbols
      origin := .decl declName
   }
 
-def getTheoremPatterns : CoreM TheoremPatterns :=
-  return theoremPatternsExt.getState (← getEnv)
+def getEMatchTheorems : CoreM EMatchTheorems :=
+  return ematchTheoremsExt.getState (← getEnv)
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -50,7 +50,7 @@ private def activateTheoremPatterns (fName : Name) : GoalM Unit := do
         modify fun s => { s with newThms := s.newThms.push thm }
       | _ =>
         trace[grind.pattern] "reinsert `{thm.origin.key}`"
-        modify fun s => { s with thmMap := s.thmMap.insertTheorem thm }
+        modify fun s => { s with thmMap := s.thmMap.insert thm }
 
 partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
   if (← alreadyInternalized e) then return ()

src/Lean/Meta/Tactic/Grind/Run.lean

@@ -46,7 +46,7 @@ def GrindM.run (x : GrindM α) (mainDeclName : Name) : MetaM α := do
 def mkGoal (mvarId : MVarId) : GrindM Goal := do
   let trueExpr ← getTrueExpr
   let falseExpr ← getFalseExpr
-  let thmMap ← getTheoremPatterns
+  let thmMap ← getEMatchTheorems
   GoalM.run' { mvarId, thmMap } do
     mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0)
     mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0)

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -13,7 +13,7 @@ import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.Attr
-import Lean.Meta.Tactic.Grind.TheoremPatterns
+import Lean.Meta.Tactic.Grind.EMatchTheorem
 
 namespace Lean.Meta.Grind
 
@@ -275,14 +275,14 @@ structure Goal where
   /-- Next unique index for creating ENodes -/
   nextIdx      : Nat := 0
   /-- Active theorems that we have performed ematching at least once. -/
-  thms         : PArray TheoremPattern := {}
+  thms         : PArray EMatchTheorem := {}
   /-- Active theorems that we have not performed any round of ematching yet. -/
-  newThms      : PArray TheoremPattern := {}
+  newThms      : PArray EMatchTheorem := {}
   /--
   Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols.
   Local theorem provided by users are added directly into `newThms`.
   -/
-  thmMap       : TheoremPatterns
+  thmMap       : EMatchTheorems
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=