From a2aadee28f9cba171139dccfd10cc4b37efc989c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Dec 2023 11:40:28 -0800 Subject: [PATCH] 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 | 1 + src/Init/Simproc.lean | 89 +++++++++++++++++++ src/Init/Tactics.lean | 23 ----- src/Lean/Elab/Tactic.lean | 2 +- .../Tactic/{SimprocAttr.lean => Simproc.lean} | 31 ++++--- src/Lean/Meta/Tactic/Simp/Simproc.lean | 65 ++++++++++++-- tests/lean/run/simproc1.lean | 11 +-- 7 files changed, 175 insertions(+), 47 deletions(-) create mode 100644 src/Init/Simproc.lean rename src/Lean/Elab/Tactic/{SimprocAttr.lean => Simproc.lean} (60%) diff --git a/src/Init.lean b/src/Init.lean index aea7d2ca94..d23607ad4b 100644 --- a/src/Init.lean +++ b/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 diff --git a/src/Init/Simproc.lean b/src/Init/Simproc.lean new file mode 100644 index 0000000000..9da05c9764 --- /dev/null +++ b/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 diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index b0dae4c89d..fb313ba9d2 100644 --- a/src/Init/Tactics.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index 10a9738ca0..b58a9fd159 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/SimprocAttr.lean b/src/Lean/Elab/Tactic/Simproc.lean similarity index 60% rename from src/Lean/Elab/Tactic/SimprocAttr.lean rename to src/Lean/Elab/Tactic/Simproc.lean index a4cc7a37fe..03034036d9 100644 --- a/src/Lean/Elab/Tactic/SimprocAttr.lean +++ b/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 } diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean index 50ce50e7bc..4321a88c7e 100644 --- a/src/Lean/Meta/Tactic/Simp/Simproc.lean +++ b/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 diff --git a/tests/lean/run/simproc1.lean b/tests/lean/run/simproc1.lean index 9b3fcbc4f7..4bfdd08d6b 100644 --- a/tests/lean/run/simproc1.lean +++ b/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]