feat: simproc sets

The command `register_simp_attr` now also declares a `simproc` set.

RELEASES.md

@@ -69,6 +69,10 @@ example : x + foo 2 = 12 + x := by
   fail_if_success simp [-reduceFoo]
   simp_arith
 ```
+The command `register_simp_attr <id>` now creates a `simp` **and** a `simproc` set with the name `<id>`. The following command instructs Lean to insert the `reduceFoo` simplification procedure into the set `my_simp`. If no set is specified, Lean uses the default `simp` set.
+```lean
+simproc [my_simp] reduceFoo (foo _) := ...
+```
 
 * The syntax of the `termination_by` and `decreasing_by` termination hints is overhauled:
 

src/Init/Simproc.lean

@@ -29,7 +29,7 @@ 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
+syntax (docComment)? attrKind "simproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command
 
 /--
 A user-defined simplification procedure declaration. To activate this procedure in `simp` tactic,
@@ -63,6 +63,11 @@ Auxiliary attribute for simplification procedures.
 -/
 syntax (name := simprocAttr) "simproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
 
+/--
+Auxiliary attribute for symbolic evaluation procedures.
+-/
+syntax (name := sevalAttr) "sevalproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
 /--
 Auxiliary attribute for builtin simplification procedures.
 -/
@@ -82,9 +87,26 @@ macro_rules
       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)
+  | `($[$doc?:docComment]? $kind:attrKind simproc $[$pre?]? $[ [ $ids?:ident,* ] ]? $n:ident ($pattern:term) := $body) => do
+     let mut cmds := #[(← `(simproc_decl $n ($pattern) := $body))]
+     let pushDefault (cmds : Array (TSyntax `command)) : MacroM (Array (TSyntax `command)) := do
+       return cmds.push (← `(attribute [$kind simproc $[$pre?]?] $n))
+     if let some ids := ids? then
+       for id in ids.getElems do
+         let idName := id.getId
+         let (attrName, attrKey) :=
+           if idName == `simp then
+             (`simprocAttr, "simproc")
+           else if idName == `seval then
+             (`sevalAttr, "sevalproc")
+           else
+             let idName := idName.appendAfter "_proc"
+             (`Parser.Attr ++ idName, idName.toString)
+         let attrStx : TSyntax `attr := ⟨mkNode attrName #[mkAtom attrKey, mkOptionalNode pre?]⟩
+         cmds := cmds.push (← `(attribute [$kind $attrStx] $n))
+     else
+       cmds ← pushDefault cmds
+     return mkNullNode cmds
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind builtin_simproc $[$pre?]? $n:ident ($pattern:term) := $body) => do

src/Lean/Elab/Tactic/Simp.lean

@@ -130,21 +130,21 @@ private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (p
 
 structure ElabSimpArgsResult where
   ctx      : Simp.Context
-  simprocs : Simprocs
+  simprocs : Simp.SimprocsArray
   starArg  : Bool := false
 
 inductive ResolveSimpIdResult where
   | none
   | expr (e : Expr)
   | simproc (declName : Name)
-  | ext  (ext : SimpExtension)
+  | ext  (ext₁ : SimpExtension) (ext₂ : Simp.SimprocExtension)
 
 /--
   Elaborate extra simp theorems provided to `simp`. `stx` is of the form `"[" simpTheorem,* "]"`
   If `eraseLocal == true`, then we consider local declarations when resolving names for erased theorems (`- id`),
   this option only makes sense for `simp_all` or `*` is used.
 -/
-def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simprocs) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
+def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
   if stx.isNone then
     return { ctx, simprocs }
   else
@@ -188,8 +188,9 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simprocs) (eras
             thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
           | .simproc declName =>
             simprocs ← simprocs.add declName post
-          | .ext ext =>
-            thmsArray := thmsArray.push (← ext.getTheorems)
+          | .ext ext₁ ext₂ =>
+            thmsArray := thmsArray.push (← ext₁.getTheorems)
+            simprocs  := simprocs.push (← ext₂.getSimprocs)
           | .none    =>
             let name ← mkFreshId
             thms ← addSimpTheorem thms (.stx name arg) term post inv
@@ -206,8 +207,9 @@ where
 
   resolveSimpIdTheorem? (simpArgTerm : Term) : TacticM ResolveSimpIdResult := do
     let resolveExt (n : Name) : TacticM ResolveSimpIdResult := do
-      if let some ext ← getSimpExtension? n then
-        return .ext ext
+      if let some ext₁ ← getSimpExtension? n then
+        let some ext₂ ← Simp.getSimprocExtension? n | throwError "simproc set associated with simp set '{n}' was not found"
+        return .ext ext₁ ext₂
       else
         return .none
     match simpArgTerm with
@@ -236,7 +238,7 @@ where
 
 structure MkSimpContextResult where
   ctx              : Simp.Context
-  simprocs         : Simprocs
+  simprocs         : Simp.SimprocsArray
   dischargeWrapper : Simp.DischargeWrapper
 
 /--
@@ -259,7 +261,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
     getSimpTheorems
   let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := simprocs) {
+  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {
     config      := (← elabSimpConfig stx[1] (kind := kind))
     simpTheorems := #[simpTheorems], congrTheorems
   }
@@ -361,7 +363,7 @@ For many tactics other than the simplifier,
 one should use the `withLocation` tactic combinator
 when working with a `location`.
 -/
-def simpLocation (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
+def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do

src/Lean/Elab/Tactic/Simproc.lean

@@ -52,34 +52,4 @@ namespace Command
 
 end Command
 
-builtin_initialize
-  registerBuiltinAttribute {
-    ref             := by exact decl_name%
-    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
-        addSimprocAttr declName attrKind post
-      go.run' {}
-    applicationTime := AttributeApplicationTime.afterCompilation
-  }
-
-builtin_initialize
-  registerBuiltinAttribute {
-    ref             := by exact decl_name%
-    name            := `simprocBuiltinAttr
-    descr           := "Builtin simplification procedure"
-    erase           := eraseSimprocAttr
-    add             := fun declName stx _ => do
-      let go : MetaM Unit := do
-        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-        let val := mkAppN (mkConst ``addSimprocBuiltinAttr) #[toExpr declName, toExpr post, mkConst declName]
-        let initDeclName ← mkFreshUserName (declName ++ `declare)
-        declareBuiltin initDeclName val
-      go.run' {}
-    applicationTime := AttributeApplicationTime.afterCompilation
-  }
-
 end Lean.Elab

src/Lean/Linter/MissingDocs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Mario Carneiro
 -/
-import Lean.Meta.Tactic.Simp.SimpTheorems
+import Lean.Meta.Tactic.Simp.RegisterCommand
 import Lean.Elab.Command
 import Lean.Elab.SetOption
 import Lean.Linter.Util

src/Lean/Meta/Tactic/Simp.lean

@@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Simp.Rewrite
 import Lean.Meta.Tactic.Simp.SimpAll
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs
+import Lean.Meta.Tactic.Simp.RegisterCommand
 
 namespace Lean
 

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

@@ -646,9 +646,9 @@ def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods
       if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex
 
 end Simp
-open Simp (UsedSimps Simprocs)
+open Simp (UsedSimps SimprocsArray)
 
-def simp (e : Expr) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" (← getOptions) do
   match discharge? with
   | none   => Simp.main e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs)
@@ -659,7 +659,7 @@ def dsimp (e : Expr) (ctx : Simp.Context)
   Simp.dsimpMain e ctx usedSimps (methods := Simp.mkDefaultMethodsCore {})
 
 /-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
-def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   let target ← instantiateMVars (← mvarId.getType)
   let (r, usedSimps) ← simp target ctx simprocs discharge? usedSimps
@@ -674,7 +674,7 @@ def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs :
 /--
   Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
   where `mvarId'` is the simplified new goal. -/
-def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
@@ -709,7 +709,7 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
   otherwise, where `proof' : prop'` and `prop'` is the simplified `prop`.
 
   This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
-def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do
   let (r, usedSimps) ← simp prop ctx simprocs discharge? usedSimps
   return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
@@ -742,15 +742,15 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
   else
     applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
 
-def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let type ← instantiateMVars (← fvarId.getType)
     let (r, usedSimps) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal usedSimps
     return (← applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps)
 
-def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
   mvarId.withContext do
@@ -789,7 +789,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {})
       throwError "simp made no progress"
     return (some (fvarIdsNew, mvarIdNew), usedSimps)
 
-def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
   let mut ctx := ctx
   for h in (← getPropHyps) do

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

@@ -308,13 +308,13 @@ def simpGround (discharge? : Expr → SimpM (Option Expr)) : Simproc := fun e =>
   trace[Meta.Tactic.simp.ground] "delta, {e} => {eNew}"
   return .visit { expr := eNew }
 
-partial def preDefault (s : Simprocs) (discharge? : Expr → SimpM (Option Expr)) : Simproc :=
+partial def preDefault (s : SimprocsArray) (discharge? : Expr → SimpM (Option Expr)) : Simproc :=
   rewritePre discharge? >>
   simpMatch discharge? >>
   userPreSimprocs s >>
   simpUsingDecide
 
-def postDefault (s : Simprocs) (discharge? : Expr → SimpM (Option Expr)) : Simproc :=
+def postDefault (s : SimprocsArray) (discharge? : Expr → SimpM (Option Expr)) : Simproc :=
   rewritePost discharge? >>
   userPostSimprocs s >>
   simpGround discharge? >>
@@ -410,18 +410,18 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
 
 abbrev Discharge := Expr → SimpM (Option Expr)
 
-def mkMethods (s : Simprocs) (discharge? : Discharge) : Methods := {
+def mkMethods (s : SimprocsArray) (discharge? : Discharge) : Methods := {
   pre        := preDefault s discharge?
   post       := postDefault s discharge?
   discharge? := discharge?
 }
 
-def mkDefaultMethodsCore (simprocs : Simprocs) : Methods :=
+def mkDefaultMethodsCore (simprocs : SimprocsArray) : Methods :=
   mkMethods simprocs dischargeDefault?
 
 def mkDefaultMethods : CoreM Methods := do
   if simprocs.get (← getOptions) then
-    return mkDefaultMethodsCore (← getSimprocs)
+    return mkDefaultMethodsCore #[(← getSimprocs)]
   else
     return mkDefaultMethodsCore {}
 

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

@@ -9,7 +9,7 @@ import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 
-open Simp (UsedSimps)
+open Simp (UsedSimps SimprocsArray)
 
 namespace SimpAll
 
@@ -27,7 +27,7 @@ structure State where
   mvarId    : MVarId
   entries   : Array Entry := #[]
   ctx       : Simp.Context
-  simprocs  : Simprocs
+  simprocs  : SimprocsArray
   usedSimps : UsedSimps := {}
 
 abbrev M := StateRefT State MetaM
@@ -142,7 +142,7 @@ def main : M (Option MVarId) := do
 
 end SimpAll
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   mvarId.withContext do
     let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
     if let .some mvarIdNew := r then

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

@@ -491,14 +491,4 @@ def SimpTheoremsArray.isDeclToUnfold (thmsArray : SimpTheoremsArray) (declName :
 def SimpTheoremsArray.isLetDeclToUnfold (thmsArray : SimpTheoremsArray) (fvarId : FVarId) : Bool :=
 thmsArray.any fun thms => thms.isLetDeclToUnfold fvarId
 
-macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc:(docComment)?
-  "register_simp_attr" id:ident : command => do
-  let str := id.getId.toString
-  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
-  let descr := quote (removeLeadingSpaces (doc.map (·.getDocString) |>.getD s!"simp set for {id.getId.toString}"))
-  `($[$doc:docComment]? initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr $(quote id.getId)
-    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? (prio)? : attr)
-
-end Meta
-
-end Lean
+end Lean.Meta