feat: simproc sets
The command `register_simp_attr` now also declares a `simproc` set.
This commit is contained in:
Leonardo de Moura
Scott Morrison
parent
755b59c2cf
commit
de886c617d
13 changed files with 231 additions and 99 deletions
|
|
@ -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:
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
28
src/Lean/Meta/Tactic/Simp/RegisterCommand.lean
Normal file
28
src/Lean/Meta/Tactic/Simp/RegisterCommand.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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 {}
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue