Introduce parser memoization to avoid exponentional behavior

src/Init/Data/Array/Subarray.lean

@@ -104,6 +104,28 @@ def any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
 def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
   Id.run <| as.allM p
 
+@[inline]
+def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) : m (Option β) :=
+  let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
+    | 0,   _ => pure none
+    | i+1, h => do
+      have : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self _) h
+      let r ← f as[i]
+      match r with
+      | some _ => pure r
+      | none   =>
+        have : i ≤ as.size := Nat.le_of_lt this
+        find i this
+  find as.size (Nat.le_refl _)
+
+@[inline]
+def findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Subarray α) (p : α → m Bool) : m (Option α) :=
+  as.findSomeRevM? fun a => return if (← p a) then some a else none
+
+@[inline]
+def findRev? {α : Type} (as : Subarray α) (p : α → Bool) : Option α :=
+  Id.run <| as.findRevM? p
+
 end Subarray
 
 namespace Array

src/Lean/Data/OpenDecl.lean

@@ -11,6 +11,7 @@ namespace Lean
 inductive OpenDecl where
   | simple   (ns : Name) (except : List Name)
   | explicit (id : Name) (declName : Name)
+  deriving BEq
 
 namespace OpenDecl
 instance : Inhabited OpenDecl := ⟨simple Name.anonymous []⟩

src/Lean/Data/Options.lean

@@ -16,6 +16,7 @@ instance : Inhabited Options where
   default := {}
 instance : ToString Options := inferInstanceAs (ToString KVMap)
 instance : ForIn m Options (Name × DataValue) := inferInstanceAs (ForIn _ KVMap _)
+instance : BEq Options := inferInstanceAs (BEq KVMap)
 
 structure OptionDecl where
   declName : Name := by exact decl_name%

src/Lean/Elab/BuiltinNotation.lean

@@ -89,15 +89,20 @@ private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) :
   match extractMacroScopes declName with
   | { name := .str _ s, .. } =>
     let kind := quote declName
-    let s    := quote s
-    ``(withAntiquot (mkAntiquot $s $kind $(quote withAnonymousAntiquot)) (leadingNode $kind $prec $e))
+    let mut p ← ``(withAntiquot
+      (mkAntiquot $(quote s) $kind $(quote withAnonymousAntiquot))
+      (leadingNode $kind $prec $e))
+    -- cache only unparameterized parsers
+    if (← getLCtx).all (·.isAuxDecl) then
+      p ← ``(withCache $kind $p)
+    return p
   | _  => throwError "invalid `leading_parser` macro, unexpected declaration name"
 
 @[builtin_term_elab «leading_parser»] def elabLeadingParserMacro : TermElab :=
-  adaptExpander fun stx => match stx with
-  | `(leading_parser $[: $prec?]? $[(withAnonymousAntiquot := $anon?)]? $e) =>
-    elabParserMacroAux (prec?.getD (quote Parser.maxPrec)) e (anon?.all (·.raw.isOfKind ``Parser.Term.trueVal))
-  | _ => throwUnsupportedSyntax
+  adaptExpander fun
+    | `(leading_parser $[: $prec?]? $[(withAnonymousAntiquot := $anon?)]? $e) =>
+        elabParserMacroAux (prec?.getD (quote Parser.maxPrec)) e (anon?.all (·.raw.isOfKind ``Parser.Term.trueVal))
+    | _ => throwUnsupportedSyntax
 
 private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
   let declName? ← getDeclName?