feat: simproc declaration vs simproc attribute

Allow `simproc`s to be declared without setting the `[simproc]`
attribute. A `simproc` declaration is function + pattern.

Motivation: allow them to be provided as arguments to `simp` **and** `simp only`.

TODO: track their use in `simp`.
TODO: builtin simprocs

src/Init.lean

@@ -23,4 +23,5 @@ import Init.NotationExtra
 import Init.SimpLemmas
 import Init.Hints
 import Init.Conv
+import Init.Simproc
 import Init.SizeOfLemmas

src/Init/Simproc.lean

@@ -0,0 +1,89 @@
+prelude
+import Init.NotationExtra
+
+namespace Lean.Parser
+/--
+A user-defined simplification procedure used by the `simp` tactic, and its variants.
+Here is an example.
+```lean
+simproc reduce_add (_ + _) := fun e => do
+  unless (e.isAppOfArity ``HAdd.hAdd 6) do return none
+  let some n ← getNatValue? (e.getArg! 4) | return none
+  let some m ← getNatValue? (e.getArg! 5) | return none
+  return some (.done { expr := mkNatLit (n+m) })
+```
+The `simp` tactic invokes `reduce_add` whenever it finds a term of the form `_ + _`.
+The simplification procedures are stored in an (imperfect) discrimination tree.
+The procedure should **not** assume the term `e` perfectly matches the given pattern.
+The body of a simplification procedure must have type `Simproc`, which is an alias for
+`Expr → SimpM (Option Step)`.
+You can instruct the simplifier to apply the procedure before its sub-expressions
+have been simplified by using the modifier `↓` before the procedure name. Example.
+```lean
+simproc ↓ reduce_add (_ + _) := fun e => ...
+```
+Simplification procedures can be also scoped or local.
+-/
+syntax (docComment)? attrKind "simproc " (Tactic.simpPre <|> Tactic.simpPost)? ident " (" term ")" " := " term : command
+
+/--
+A user-defined simplification procedure declaration. To activate this procedure in `simp` tactic,
+we must provide it as an argument, or use the command `attribute` to set its `[simproc]` attribute.
+-/
+syntax (docComment)? "simproc_decl " ident " (" term ")" " := " term : command
+
+/--
+A builtin simplification procedure.
+-/
+syntax (docComment)? attrKind "builtin_simproc " (Tactic.simpPre <|> Tactic.simpPost)? ident " (" term ")" " := " term : command
+
+/--
+A builtin simplification procedure declaration.
+-/
+syntax (docComment)? "builtin_simproc_decl " ident " (" term ")" " := " term : command
+
+/--
+Auxiliary command for associating a pattern with a simplification procedure.
+-/
+syntax (name := simprocPattern) "simproc_pattern% " term " => " ident : command
+
+/--
+Auxiliary command for associating a pattern with a builtin simplification procedure.
+-/
+syntax (name := simprocPatternBuiltin) "builtin_simproc_pattern% " term " => " ident : command
+
+namespace Attr
+/--
+Auxiliary attribute for simplification procedures.
+-/
+syntax (name := simprocAttr) "simproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
+/--
+Auxiliary attribute for builtin simplification procedures.
+-/
+syntax (name := simprocBuiltinAttr) "builtin_simproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+end Attr
+
+macro_rules
+  | `($[$doc?:docComment]? simproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Simp.Simproc
+    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+      simproc_pattern% $pattern => $n)
+
+macro_rules
+  | `($[$doc?:docComment]? builtin_simproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Simp.Simproc
+    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+      builtin_simproc_pattern% $pattern => $n)
+
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind simproc $[$pre?]? $n:ident ($pattern:term) := $body) => do
+    `(simproc_decl $n ($pattern) := $body
+      attribute [$kind simproc $[$pre?]?] $n)
+
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind builtin_simproc $[$pre?]? $n:ident ($pattern:term) := $body) => do
+    `(builtin_simproc_decl $n ($pattern) := $body
+      attribute [$kind builtin_simproc $[$pre?]?] $n)
+
+end Lean.Parser

src/Init/Tactics.lean

@@ -796,29 +796,6 @@ If there are several with the same priority, it is uses the "most recent one". E
 ```
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
-
-/--
-Functions tagged with the `simproc` attribute are user-defined simplification procedures used
-by the `simp` tactic, and its variants. The function must have type `Simproc`, which is an alias for
-`Expr → SimpM (Option Step)`.
-Here is an example of a simplification procedure.
-```lean
-@[simproc _ + _] def simp_add : Simproc :=
-   ...
-```
-The `simp` tactic invokes `simp_add` whenever it finds a term of the form `_ + _`. Note that the term
-is only used to create a key for the discrimination tree storing all simplification procedures.
-You can instruct the simplifier to apply the procedure before its sub-expressions
-have been simplified by using the modifier `↓`.
-The simplifier applies the procedures using the given priority. If none is provided the default one is used.
-If there are several with the same priority, it is uses the "most recent one".
--/
-syntax (name := simproc) "simproc" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? term : attr
-
-/--
-A builtin simplification procedure.
--/
-syntax (name := simprocBuiltin) "builtin_simproc" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? term : attr
 end Attr
 
 end Parser

src/Lean/Elab/Tactic.lean

@@ -13,7 +13,7 @@ import Lean.Elab.Tactic.Match
 import Lean.Elab.Tactic.Rewrite
 import Lean.Elab.Tactic.Location
 import Lean.Elab.Tactic.Simp
-import Lean.Elab.Tactic.SimprocAttr
+import Lean.Elab.Tactic.Simproc
 import Lean.Elab.Tactic.BuiltinTactic
 import Lean.Elab.Tactic.Split
 import Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Simproc.lean

@@ -7,6 +7,7 @@ import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.Term
+import Lean.Elab.Command
 
 namespace Lean.Elab
 
@@ -14,32 +15,40 @@ open Lean Meta Simp
 
 def elabPattern (stx : Syntax) : MetaM Expr := do
   let go : TermElabM Expr := do
-    Term.withAutoBoundImplicit <| Term.elabBinders #[] fun xs => do
-      let pattern ← Term.elabTerm stx none
-      Term.synthesizeSyntheticMVars
-      let (_, _, pattern) ← lambdaMetaTelescope (← mkLambdaFVars xs pattern)
-      return pattern
+    let pattern ← Term.elabTerm stx none
+    Term.synthesizeSyntheticMVars
+    return pattern
   go.run'
 
-def checkSimprocType (declName : Name) : MetaM Unit := do
+def checkSimprocType (declName : Name) : CoreM Unit := do
   let decl ← getConstInfo declName
   match decl.type with
   | .const ``Simproc _ => pure ()
   | _ => throwError "unexpected type at '{declName}', 'Simproc' expected"
 
+namespace Command
+
+@[builtin_command_elab Lean.Parser.simprocPattern] def elabSimprocPattern : CommandElab := fun stx => do
+  let `(simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
+  let declName := declName.getId
+  liftTermElabM do
+    checkSimprocType declName
+    let pattern ← elabPattern pattern
+    let keys ← DiscrTree.mkPath pattern simpDtConfig
+    registerSimproc declName keys
+
+end Command
+
 builtin_initialize
   registerBuiltinAttribute {
     ref             := by exact decl_name%
-    name            := `simproc
+    name            := `simprocAttr
     descr           := "Simplification procedure"
     erase           := eraseSimprocAttr
     add             := fun declName stx attrKind => do
       let go : MetaM Unit := do
         let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-        let prio ← getAttrParamOptPrio stx[2]
-        let pattern ← elabPattern stx[3]
-        checkSimprocType declName
-        addSimprocAttr declName attrKind post prio pattern
+        addSimprocAttr declName attrKind post
       go.run' {}
     applicationTime := AttributeApplicationTime.afterCompilation
   }

src/Lean/Meta/Tactic/Simp/Simproc.lean

@@ -9,13 +9,68 @@ import Lean.Meta.Tactic.Simp.Types
 
 namespace Lean.Meta.Simp
 
+builtin_initialize builtinSimprocDeclsRef : IO.Ref (HashMap Name (Array SimpTheoremKey)) ← IO.mkRef {}
+
+structure SimprocDecl where
+  declName : Name
+  keys     : Array SimpTheoremKey
+  deriving Inhabited
+
+structure SimprocDeclExtState where
+  builtin    : HashMap Name (Array SimpTheoremKey)
+  newEntries : PHashMap Name (Array SimpTheoremKey) := {}
+  deriving Inhabited
+
+def SimprocDecl.lt (decl₁ decl₂ : SimprocDecl) : Bool :=
+  Name.quickLt decl₁.declName decl₂.declName
+
+builtin_initialize simprocDeclExt : PersistentEnvExtension SimprocDecl SimprocDecl SimprocDeclExtState ←
+  registerPersistentEnvExtension {
+    mkInitial       := return { builtin := (← builtinSimprocDeclsRef.get) }
+    addImportedFn   := fun _ => return { builtin := (← builtinSimprocDeclsRef.get) }
+    addEntryFn      := fun s d => { s with newEntries := s.newEntries.insert d.declName d.keys }
+    exportEntriesFn := fun s =>
+      let result := s.newEntries.foldl (init := #[]) fun result declName keys => result.push { declName, keys }
+      result.qsort SimprocDecl.lt
+  }
+
+def getSimprocDeclKeys? (declName : Name) : CoreM (Option (Array SimpTheoremKey)) := do
+  let env ← getEnv
+  let keys? ← match env.getModuleIdxFor? declName with
+    | some modIdx => do
+      let some decl := (simprocDeclExt.getModuleEntries env modIdx).binSearch { declName, keys := #[] } SimprocDecl.lt
+        | pure none
+      pure (some decl.keys)
+    | none        => pure ((simprocDeclExt.getState env).newEntries.find? declName)
+  if let some keys := keys? then
+    return some keys
+  else
+    return (simprocDeclExt.getState env).builtin.find? declName
+
+def isSimproc (declName : Name) : CoreM Bool :=
+  return (← getSimprocDeclKeys? declName).isSome
+
+def registerBuiltinSimproc (declName : Name) (keys : Array SimpTheoremKey) : IO Unit := do
+  unless (← initializing) do
+    throw (IO.userError s!"invalid builtin simproc declaration, it can only be registered during initialization")
+  if (← builtinSimprocDeclsRef.get).contains declName then
+    throw (IO.userError s!"invalid builtin simproc declaration '{declName}', it has already been declared")
+  builtinSimprocDeclsRef.modify fun s => s.insert declName keys
+
+def registerSimproc (declName : Name) (keys : Array SimpTheoremKey) : CoreM Unit := do
+  let env ← getEnv
+  unless (env.getModuleIdxFor? declName).isNone do
+    throwError "invalid simproc declaration '{declName}', function declaration is in an imported module"
+  if (← isSimproc declName) then
+    throwError "invalid simproc declaration '{declName}', it has already been declared"
+  modifyEnv fun env => simprocDeclExt.modifyState env fun s => { s with newEntries := s.newEntries.insert declName keys }
+
 abbrev Simproc := Expr → SimpM (Option Step)
 
 structure SimprocOLeanEntry where
   /-- Name of a declaration stored in the environment which has type `Simproc`. -/
   declName : Name
   post     : Bool := true
-  priority : Nat  := eval_prio default
   keys     : Array SimpTheoremKey := #[]
   deriving Inhabited
 
@@ -79,10 +134,11 @@ def eraseSimprocAttr (declName : Name) : AttrM Unit := do
     throwError "'{declName}' does not have [simproc] attribute"
   modifyEnv fun env => simprocExtension.modifyState env fun s => s.erase declName
 
-def addSimprocAttr (declName : Name) (kind : AttributeKind) (post : Bool) (priority : Nat) (pattern : Expr) : MetaM Unit := do
+def addSimprocAttr (declName : Name) (kind : AttributeKind) (post : Bool) : MetaM Unit := do
   let proc ← getSimprocFromDecl declName
-  let keys ← DiscrTree.mkPath pattern simpDtConfig
-  simprocExtension.add { declName, post, priority, keys, proc } kind
+  let some keys ← getSimprocDeclKeys? declName |
+    throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
+  simprocExtension.add { declName, post, keys, proc } kind
 
 def getSimprocState : CoreM SimprocState :=
   return simprocExtension.getState (← getEnv)
@@ -104,7 +160,6 @@ def simproc? (tag : String) (s : SimprocTree) (erased : PHashSet Name) (e : Expr
     trace[Debug.Meta.Tactic.simp] "no {tag}-simprocs found for {e}"
     return none
   else
-    let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
     for (simprocEntry, numExtraArgs) in candidates do
       unless erased.contains simprocEntry.declName do
         if let some step ← simprocEntry.try? numExtraArgs e then

tests/lean/run/simproc1.lean

@@ -4,14 +4,11 @@ import Lean.Meta.Offset
 def foo (x : Nat) : Nat :=
   x + 10
 
-open Lean Meta Simp
-@[simproc foo _]
-def simp_f : Simproc := fun e => do
-  let some n ← evalNat e.appArg! |>.run
-    | return none
+simproc reduce_f (foo _) := fun e => open Lean Meta in do
+  let some n ← evalNat e.appArg! |>.run | return none
   return some (.done { expr := mkNatLit (n+10) })
 
 example : x + foo 2 = 12 + x := by
-  fail_if_success simp (config := { simproc := false })
-  simp (config := { simproc := true })
+  fail_if_success simp (config := { «simproc» := false })
+  simp (config := { «simproc» := true })
   rw [Nat.add_comm]