From de886c617d0cc08c43976e89c3e9b835455c956d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Jan 2024 17:19:29 -0800 Subject: [PATCH] feat: simproc sets The command `register_simp_attr` now also declares a `simproc` set. --- RELEASES.md | 4 + src/Init/Simproc.lean | 30 +++- src/Lean/Elab/Tactic/Simp.lean | 22 +-- src/Lean/Elab/Tactic/Simproc.lean | 30 ---- src/Lean/Linter/MissingDocs.lean | 2 +- src/Lean/Meta/Tactic/Simp.lean | 1 + src/Lean/Meta/Tactic/Simp/Main.lean | 16 +- .../Meta/Tactic/Simp/RegisterCommand.lean | 28 ++++ src/Lean/Meta/Tactic/Simp/Rewrite.lean | 10 +- src/Lean/Meta/Tactic/Simp/SimpAll.lean | 6 +- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 12 +- src/Lean/Meta/Tactic/Simp/Simproc.lean | 156 +++++++++++++++--- tests/pkg/user_attr/UserAttr/Tst.lean | 13 ++ 13 files changed, 231 insertions(+), 99 deletions(-) create mode 100644 src/Lean/Meta/Tactic/Simp/RegisterCommand.lean diff --git a/RELEASES.md b/RELEASES.md index 219c129819..df138cb6a2 100644 --- a/RELEASES.md +++ b/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 ` now creates a `simp` **and** a `simproc` set with the name ``. 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: diff --git a/src/Init/Simproc.lean b/src/Init/Simproc.lean index 03ed09b902..e0859df328 100644 --- a/src/Init/Simproc.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index f4018ac34f..8f3bc9eb35 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Simproc.lean b/src/Lean/Elab/Tactic/Simproc.lean index 91caacec0e..0d6bef5840 100644 --- a/src/Lean/Elab/Tactic/Simproc.lean +++ b/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 diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index 672f896cdf..a06ee655f6 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp.lean b/src/Lean/Meta/Tactic/Simp.lean index d6796dcfac..9b40225b31 100644 --- a/src/Lean/Meta/Tactic/Simp.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index e255986980..0cec05a995 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/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,7 +742,7 @@ 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 @@ -750,7 +750,7 @@ def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simp 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 diff --git a/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean b/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean new file mode 100644 index 0000000000..65497836de --- /dev/null +++ b/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +import Lean.Meta.Tactic.Simp.SimpTheorems +import Lean.Meta.Tactic.Simp.Simproc + +namespace Lean.Meta.Simp + +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}")) + let procId := mkIdentFrom id (simpAttrNameToSimprocAttrName id.getId) + let procStr := procId.getId.toString + let procIdParser := mkIdentFrom procId (`Parser.Attr ++ procId.getId) + let procDescr := quote s!"simproc set for {procId.getId.toString}" + -- TODO: better docDomment for simprocs + `($[$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 + /-- Simplification procedure -/ + initialize extProc : SimprocExtension ← registerSimprocAttr $(quote procId.getId) $procDescr none $(quote procId.getId) + /-- Simplification procedure -/ + syntax (name := $procIdParser:ident) $(quote procStr):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? : attr) + +end Lean.Meta.Simp diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index d397e10212..1ca22f5129 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/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 {} diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean index 4f62f90775..662c3a537f 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index c7ae577b19..52130da8a0 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean index de39a2a286..f6fd8b6f59 100644 --- a/src/Lean/Meta/Tactic/Simp/Simproc.lean +++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.ScopedEnvExtension +import Lean.Compiler.InitAttr import Lean.Meta.DiscrTree import Lean.Meta.Tactic.Simp.Types @@ -86,6 +87,8 @@ def Simprocs.erase (s : Simprocs) (declName : Name) : Simprocs := builtin_initialize builtinSimprocsRef : IO.Ref Simprocs ← IO.mkRef {} +builtin_initialize builtinSimprocsSEvalRef : IO.Ref Simprocs ← IO.mkRef {} + abbrev SimprocExtension := ScopedEnvExtension SimprocOLeanEntry SimprocEntry Simprocs unsafe def getSimprocFromDeclImpl (declName : Name) : ImportM Simproc := do @@ -100,30 +103,17 @@ opaque getSimprocFromDecl (declName: Name) : ImportM Simproc def toSimprocEntry (e : SimprocOLeanEntry) : ImportM SimprocEntry := do return { toSimprocOLeanEntry := e, proc := (← getSimprocFromDecl e.declName) } -builtin_initialize simprocExtension : SimprocExtension ← - registerScopedEnvExtension { - name := `simproc - mkInitial := builtinSimprocsRef.get - ofOLeanEntry := fun _ => toSimprocEntry - toOLeanEntry := fun e => e.toSimprocOLeanEntry - addEntry := fun s e => - if e.post then - { s with post := s.post.insertCore e.keys e } - else - { s with pre := s.pre.insertCore e.keys e } - } - -def eraseSimprocAttr (declName : Name) : AttrM Unit := do - let s := simprocExtension.getState (← getEnv) +def eraseSimprocAttr (ext : SimprocExtension) (declName : Name) : AttrM Unit := do + let s := ext.getState (← getEnv) unless s.simprocNames.contains declName do throwError "'{declName}' does not have [simproc] attribute" - modifyEnv fun env => simprocExtension.modifyState env fun s => s.erase declName + modifyEnv fun env => ext.modifyState env fun s => s.erase declName -def addSimprocAttr (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do +def addSimprocAttr (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do let proc ← getSimprocFromDecl declName let some keys ← getSimprocDeclKeys? declName | throwError "invalid [simproc] attribute, '{declName}' is not a simproc" - simprocExtension.add { declName, post, keys, proc } kind + ext.add { declName, post, keys, proc } kind def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit := do let some keys := (← builtinSimprocDeclsRef.get).keys.find? declName | @@ -133,9 +123,6 @@ def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO else builtinSimprocsRef.modify fun s => { s with pre := s.pre.insertCore keys { declName, keys, post, proc } } -def getSimprocs : CoreM Simprocs := - return simprocExtension.getState (← getEnv) - def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs := do let proc ← try @@ -186,30 +173,145 @@ def simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Ex trace[Debug.Meta.Tactic.simp] "simproc result {e} => {r.expr}" recordSimpTheorem (.decl simprocEntry.declName post) return .done (← mkEqTransOptProofResult proof? r) - | Step.continue (some r) => + | .continue (some r) => trace[Debug.Meta.Tactic.simp] "simproc result {e} => {r.expr}" recordSimpTheorem (.decl simprocEntry.declName post) e := r.expr proof? ← mkEqTrans? proof? r.proof? found := true - | Step.continue none => + | .continue none => pure () if found then return .continue (some { expr := e, proof? }) else return .continue +abbrev SimprocsArray := Array Simprocs + +def SimprocsArray.add (ss : SimprocsArray) (declName : Name) (post : Bool) : CoreM SimprocsArray := + if ss.isEmpty then + let s : Simprocs := {} + return #[ (← s.add declName post) ] + else + ss.modifyM 0 fun s => s.add declName post + +def SimprocsArray.erase (ss : SimprocsArray) (declName : Name) : SimprocsArray := + ss.map fun s => s.erase declName + +def SimprocsArray.isErased (ss : SimprocsArray) (declName : Name) : Bool := + ss.any fun s => s.erased.contains declName + +def simprocArrayCore (post : Bool) (ss : SimprocsArray) (e : Expr) : SimpM Step := do + let mut found := false + let mut e := e + let mut proof? : Option Expr := none + for s in ss do + match (← simprocCore (post := post) (if post then s.post else s.pre) s.erased e) with + | .visit r => return .visit (← mkEqTransOptProofResult proof? r) + | .done r => return .done (← mkEqTransOptProofResult proof? r) + | .continue none => pure () + | .continue (some r) => + e := r.expr + proof? ← mkEqTrans? proof? r.proof? + found := true + if found then + return .continue (some { expr := e, proof? }) + else + return .continue + register_builtin_option simprocs : Bool := { defValue := true descr := "Enable/disable `simproc`s (simplification procedures)." } -def userPreSimprocs (s : Simprocs) : Simproc := fun e => do +def userPreSimprocs (s : SimprocsArray) : Simproc := fun e => do unless simprocs.get (← getOptions) do return .continue - simprocCore (post := false) s.pre s.erased e + simprocArrayCore (post := false) s e -def userPostSimprocs (s : Simprocs) : Simproc := fun e => do +def userPostSimprocs (s : SimprocsArray) : Simproc := fun e => do unless simprocs.get (← getOptions) do return .continue - simprocCore (post := true) s.post s.erased e + simprocArrayCore (post := true) s e + +def mkSimprocExt (name : Name := by exact decl_name%) (ref? : Option (IO.Ref Simprocs)) : IO SimprocExtension := + registerScopedEnvExtension { + name := name + mkInitial := + if let some ref := ref? then + ref.get + else + return {} + ofOLeanEntry := fun _ => toSimprocEntry + toOLeanEntry := fun e => e.toSimprocOLeanEntry + addEntry := fun s e => + if e.post then + { s with post := s.post.insertCore e.keys e } + else + { s with pre := s.pre.insertCore e.keys e } + } + +def mkSimprocAttr (attrName : Name) (attrDescr : String) (ext : SimprocExtension) (name : Name) : IO Unit := do + registerBuiltinAttribute { + ref := name + name := attrName + descr := attrDescr + applicationTime := AttributeApplicationTime.afterCompilation + add := fun declName stx attrKind => + let go : MetaM Unit := do + let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost + addSimprocAttr ext declName attrKind post + discard <| go.run {} {} + erase := eraseSimprocAttr ext + } + +abbrev SimprocExtensionMap := HashMap Name SimprocExtension + +builtin_initialize simprocExtensionMapRef : IO.Ref SimprocExtensionMap ← IO.mkRef {} + +def registerSimprocAttr (attrName : Name) (attrDescr : String) (ref? : Option (IO.Ref Simprocs)) + (name : Name := by exact decl_name%) : IO SimprocExtension := do + let ext ← mkSimprocExt name ref? + mkSimprocAttr attrName attrDescr ext name + simprocExtensionMapRef.modify fun map => map.insert attrName ext + return ext + +builtin_initialize simprocExtension : SimprocExtension ← registerSimprocAttr `simprocAttr "Simplification procedure" (some builtinSimprocsRef) + +builtin_initialize simprocSEvalExtension : SimprocExtension ← registerSimprocAttr `sevalprocAttr "Symbolic evaluator procedure" (some builtinSimprocsSEvalRef) + +builtin_initialize + registerBuiltinAttribute { + ref := by exact decl_name% + name := `simprocBuiltinAttr + descr := "Builtin simplification procedure" + erase := fun _ => pure () -- FIX: 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 + } + +def getSimprocs : CoreM Simprocs := + return simprocExtension.getState (← getEnv) + +def getSEvalSimprocs : CoreM Simprocs := + return simprocSEvalExtension.getState (← getEnv) + +def getSimprocExtensionCore? (attrName : Name) : IO (Option SimprocExtension) := + return (← simprocExtensionMapRef.get).find? attrName + +def simpAttrNameToSimprocAttrName (attrName : Name) : Name := + if attrName == `simp then `simprocAttr + else if attrName == `seval then `sevalprocAttr + else attrName.appendAfter "_proc" + +def getSimprocExtension? (simpAttrName : Name) : IO (Option SimprocExtension) := + getSimprocExtensionCore? (simpAttrNameToSimprocAttrName simpAttrName) + +def SimprocExtension.getSimprocs (ext : SimprocExtension) : CoreM Simprocs := + return ext.getState (← getEnv) end Lean.Meta.Simp diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean index 53b664d876..6830fe7f7a 100644 --- a/tests/pkg/user_attr/UserAttr/Tst.lean +++ b/tests/pkg/user_attr/UserAttr/Tst.lean @@ -75,3 +75,16 @@ def showThmsOf (simpAttrName : Name) : MetaM Unit := do IO.println thmName #eval showThmsOf `my_simp + +def boo (x : Nat) : Nat := + x + 10 + +open Lean Meta in +simproc [my_simp] reduceBoo (boo _) := fun e => do + unless e.isAppOfArity ``boo 1 do return .continue + let some n ← Nat.fromExpr? e.appArg! | return .continue + return .done { expr := mkNatLit (n+10) } + +example : f x + boo 2 = id (x + 2) + 12 := by + simp + simp [my_simp] -- Applies the simp and simproc sets