feat: simp only should not use default simproc set
This commit is contained in:
Leonardo de Moura
Sebastian Ullrich
parent
a2aadee28f
commit
5edd59806c
12 changed files with 101 additions and 78 deletions
|
|
@ -42,7 +42,7 @@ where
|
|||
go mvarId
|
||||
else if let some mvarId ← whnfReducibleLHS? mvarId then
|
||||
go mvarId
|
||||
else match (← simpTargetStar mvarId {}).1 with
|
||||
else match (← simpTargetStar mvarId {} (simprocs := {})).1 with
|
||||
| TacticResultCNM.closed => return ()
|
||||
| TacticResultCNM.modified mvarId => go mvarId
|
||||
| TacticResultCNM.noChange =>
|
||||
|
|
|
|||
|
|
@ -89,7 +89,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
|
|||
go mvarId
|
||||
else if let some mvarId ← whnfReducibleLHS? mvarId then
|
||||
go mvarId
|
||||
else match (← simpTargetStar mvarId { config.dsimp := false }).1 with
|
||||
else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
|
||||
| TacticResultCNM.closed => return ()
|
||||
| TacticResultCNM.modified mvarId => go mvarId
|
||||
| TacticResultCNM.noChange =>
|
||||
|
|
|
|||
|
|
@ -17,9 +17,9 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
|
|||
updateLhs result.expr (← result.getProof)
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.Conv.simp] def evalSimp : Tactic := fun stx => withMainContext do
|
||||
let { ctx, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
|
||||
let { ctx, simprocs, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
|
||||
let lhs ← getLhs
|
||||
let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (discharge? := d?)
|
||||
let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (simprocs := simprocs) (discharge? := d?)
|
||||
applySimpResult result
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do
|
||||
|
|
|
|||
|
|
@ -88,7 +88,7 @@ def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM Meta.Simp.
|
|||
| .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
|
||||
| .dsimp => return { (← elabDSimpConfigCore optConfig) with }
|
||||
|
||||
private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM Meta.SimpTheorems := do
|
||||
private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM SimpTheorems := do
|
||||
if e.isConst then
|
||||
let declName := e.constName!
|
||||
let info ← getConstInfo declName
|
||||
|
|
@ -129,8 +129,9 @@ private def addSimpTheorem (thms : Meta.SimpTheorems) (id : Origin) (stx : Synta
|
|||
thms.add id levelParams proof (post := post) (inv := inv)
|
||||
|
||||
structure ElabSimpArgsResult where
|
||||
ctx : Simp.Context
|
||||
starArg : Bool := false
|
||||
ctx : Simp.Context
|
||||
simprocs : Simprocs
|
||||
starArg : Bool := false
|
||||
|
||||
inductive ResolveSimpIdResult where
|
||||
| none
|
||||
|
|
@ -142,9 +143,9 @@ inductive ResolveSimpIdResult where
|
|||
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) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
|
||||
def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simprocs) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
|
||||
if stx.isNone then
|
||||
return { ctx }
|
||||
return { ctx, simprocs }
|
||||
else
|
||||
/-
|
||||
syntax simpPre := "↓"
|
||||
|
|
@ -191,7 +192,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
|
|||
starArg := true
|
||||
else
|
||||
throwUnsupportedSyntax
|
||||
return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, starArg }
|
||||
return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
|
||||
where
|
||||
resolveSimpIdTheorem? (simpArgTerm : Term) : TacticM ResolveSimpIdResult := do
|
||||
let resolveExt (n : Name) : TacticM ResolveSimpIdResult := do
|
||||
|
|
@ -218,6 +219,7 @@ where
|
|||
|
||||
structure MkSimpContextResult where
|
||||
ctx : Simp.Context
|
||||
simprocs : Simprocs
|
||||
dischargeWrapper : Simp.DischargeWrapper
|
||||
|
||||
/--
|
||||
|
|
@ -238,8 +240,9 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
|
|||
simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
|
||||
else
|
||||
getSimpTheorems
|
||||
let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
|
||||
let congrTheorems ← getSimpCongrTheorems
|
||||
let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) {
|
||||
let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := simprocs) {
|
||||
config := (← elabSimpConfig stx[1] (kind := kind))
|
||||
simpTheorems := #[simpTheorems], congrTheorems
|
||||
}
|
||||
|
|
@ -247,6 +250,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
|
|||
return { r with dischargeWrapper }
|
||||
else
|
||||
let ctx := r.ctx
|
||||
let simprocs := r.simprocs
|
||||
let mut simpTheorems := ctx.simpTheorems
|
||||
/-
|
||||
When using `zeta := false`, we do not expand let-declarations when using `[*]`.
|
||||
|
|
@ -257,7 +261,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
|
|||
unless simpTheorems.isErased (.fvar h) do
|
||||
simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
|
||||
let ctx := { ctx with simpTheorems }
|
||||
return { ctx, dischargeWrapper }
|
||||
return { ctx, simprocs, dischargeWrapper }
|
||||
|
||||
register_builtin_option tactic.simp.trace : Bool := {
|
||||
defValue := false
|
||||
|
|
@ -331,7 +335,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) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
|
||||
def simpLocation (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
|
||||
match loc with
|
||||
| Location.targets hyps simplifyTarget =>
|
||||
withMainContext do
|
||||
|
|
@ -343,7 +347,7 @@ def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := non
|
|||
where
|
||||
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM UsedSimps := do
|
||||
let mvarId ← getMainGoal
|
||||
let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
|
||||
let (result?, usedSimps) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
|
||||
match result? with
|
||||
| none => replaceMainGoal []
|
||||
| some (_, mvarId) => replaceMainGoal [mvarId]
|
||||
|
|
@ -353,15 +357,15 @@ where
|
|||
"simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)?
|
||||
-/
|
||||
@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do
|
||||
let { ctx, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
|
||||
let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
|
||||
let usedSimps ← dischargeWrapper.with fun discharge? =>
|
||||
simpLocation ctx discharge? (expandOptLocation stx[5])
|
||||
simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
|
||||
if tactic.simp.trace.get (← getOptions) then
|
||||
traceSimpCall stx usedSimps
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do
|
||||
let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
|
||||
let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
|
||||
let { ctx, simprocs, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
|
||||
let (result?, usedSimps) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
|
||||
match result? with
|
||||
| none => replaceMainGoal []
|
||||
| some mvarId => replaceMainGoal [mvarId]
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ where
|
|||
let sizeOfEq ← mkLT sizeOf_lhs sizeOf_rhs
|
||||
let hlt ← mkFreshExprSyntheticOpaqueMVar sizeOfEq
|
||||
-- TODO: we only need the `sizeOf` simp theorems
|
||||
match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] }).1 with
|
||||
match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] } {}).1 with
|
||||
| some _ => return false
|
||||
| none =>
|
||||
let heq ← mkCongrArg sizeOf_lhs.appFn! (← mkEqSymm h)
|
||||
|
|
|
|||
|
|
@ -666,23 +666,23 @@ def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods
|
|||
if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex
|
||||
|
||||
end Simp
|
||||
open Simp (UsedSimps)
|
||||
open Simp (UsedSimps Simprocs)
|
||||
|
||||
def simp (e : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
|
||||
def simp (e : Expr) (ctx : Simp.Context) (simprocs : Simprocs) (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.methodsDefault)
|
||||
| some d => Simp.main e ctx usedSimps (methods := Simp.mkMethods d)
|
||||
| none => Simp.main e ctx usedSimps (methods := Simp.methodsDefault simprocs)
|
||||
| some d => Simp.main e ctx usedSimps (methods := Simp.mkMethods simprocs d)
|
||||
|
||||
def dsimp (e : Expr) (ctx : Simp.Context)
|
||||
(usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do
|
||||
Simp.dsimpMain e ctx usedSimps (methods := Simp.methodsDefault)
|
||||
Simp.dsimpMain e ctx usedSimps (methods := Simp.methodsDefault {})
|
||||
|
||||
/-- 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) (discharge? : Option Simp.Discharge := none)
|
||||
def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (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 discharge? usedSimps
|
||||
let (r, usedSimps) ← simp target ctx simprocs discharge? usedSimps
|
||||
if mayCloseGoal && r.expr.consumeMData.isConstOf ``True then
|
||||
match r.proof? with
|
||||
| some proof => mvarId.assign (← mkOfEqTrue proof)
|
||||
|
|
@ -694,11 +694,11 @@ def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option S
|
|||
/--
|
||||
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) (discharge? : Option Simp.Discharge := none)
|
||||
def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
|
||||
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
|
||||
mvarId.withContext do
|
||||
mvarId.checkNotAssigned `simp
|
||||
simpTargetCore mvarId ctx discharge? mayCloseGoal usedSimps
|
||||
simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal usedSimps
|
||||
|
||||
/--
|
||||
Apply the result `r` for `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
|
||||
|
|
@ -729,9 +729,9 @@ 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) (discharge? : Option Simp.Discharge := none)
|
||||
def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
|
||||
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do
|
||||
let (r, usedSimps) ← simp prop ctx discharge? usedSimps
|
||||
let (r, usedSimps) ← simp prop ctx simprocs discharge? usedSimps
|
||||
return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
|
||||
|
||||
def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do
|
||||
|
|
@ -762,15 +762,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) (discharge? : Option Simp.Discharge := none)
|
||||
def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : Simprocs) (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 discharge? mayCloseGoal usedSimps
|
||||
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) (discharge? : Option Simp.Discharge := none)
|
||||
def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
|
||||
(simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
|
||||
(usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
|
||||
mvarId.withContext do
|
||||
|
|
@ -783,7 +783,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
|
|||
let localDecl ← fvarId.getDecl
|
||||
let type ← instantiateMVars localDecl.type
|
||||
let ctx := { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId) }
|
||||
let (r, usedSimps') ← simp type ctx discharge? usedSimps
|
||||
let (r, usedSimps') ← simp type ctx simprocs discharge? usedSimps
|
||||
usedSimps := usedSimps'
|
||||
match r.proof? with
|
||||
| some _ => match (← applySimpResultToProp mvarIdNew (mkFVar fvarId) type r) with
|
||||
|
|
@ -798,7 +798,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
|
|||
mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId r.expr
|
||||
replaced := replaced.push fvarId
|
||||
if simplifyTarget then
|
||||
match (← simpTarget mvarIdNew ctx discharge? (usedSimps := usedSimps)) with
|
||||
match (← simpTarget mvarIdNew ctx simprocs discharge? (usedSimps := usedSimps)) with
|
||||
| (none, usedSimps') => return (none, usedSimps')
|
||||
| (some mvarIdNew', usedSimps') => mvarIdNew := mvarIdNew'; usedSimps := usedSimps'
|
||||
let (fvarIdsNew, mvarIdNew') ← mvarIdNew.assertHypotheses toAssert
|
||||
|
|
@ -809,7 +809,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
|
|||
throwError "simp made no progress"
|
||||
return (some (fvarIdsNew, mvarIdNew), usedSimps)
|
||||
|
||||
def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
|
||||
def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
|
||||
(usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
|
||||
let mut ctx := ctx
|
||||
for h in (← getPropHyps) do
|
||||
|
|
@ -817,7 +817,7 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option S
|
|||
let proof := localDecl.toExpr
|
||||
let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
|
||||
ctx := { ctx with simpTheorems }
|
||||
match (← simpTarget mvarId ctx discharge? (usedSimps := usedSimps)) with
|
||||
match (← simpTarget mvarId ctx simprocs discharge? (usedSimps := usedSimps)) with
|
||||
| (none, usedSimps) => return (TacticResultCNM.closed, usedSimps)
|
||||
| (some mvarId', usedSimps') =>
|
||||
if (← mvarId.getType) == (← mvarId'.getType) then
|
||||
|
|
|
|||
|
|
@ -404,13 +404,14 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
|
|||
|
||||
abbrev Discharge := Expr → SimpM (Option Expr)
|
||||
|
||||
def mkMethods (discharge? : Discharge) : Methods := {
|
||||
def mkMethods (simprocs : Simprocs) (discharge? : Discharge) : Methods := {
|
||||
pre := (preDefault · discharge?)
|
||||
post := (postDefault · discharge?)
|
||||
discharge? := discharge?
|
||||
simprocs := simprocs
|
||||
}
|
||||
|
||||
def methodsDefault : Methods :=
|
||||
mkMethods dischargeDefault?
|
||||
def methodsDefault (simprocs : Simprocs) : Methods :=
|
||||
mkMethods simprocs dischargeDefault?
|
||||
|
||||
end Lean.Meta.Simp
|
||||
|
|
|
|||
|
|
@ -27,6 +27,7 @@ structure State where
|
|||
mvarId : MVarId
|
||||
entries : Array Entry := #[]
|
||||
ctx : Simp.Context
|
||||
simprocs : Simprocs
|
||||
usedSimps : UsedSimps := {}
|
||||
|
||||
abbrev M := StateRefT State MetaM
|
||||
|
|
@ -52,6 +53,7 @@ private abbrev getSimpTheorems : M SimpTheoremsArray :=
|
|||
|
||||
private partial def loop : M Bool := do
|
||||
modify fun s => { s with modified := false }
|
||||
let simprocs := (← get).simprocs
|
||||
-- simplify entries
|
||||
for i in [:(← get).entries.size] do
|
||||
let entry := (← get).entries[i]!
|
||||
|
|
@ -59,7 +61,7 @@ private partial def loop : M Bool := do
|
|||
-- We disable the current entry to prevent it to be simplified to `True`
|
||||
let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
|
||||
let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
|
||||
let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx (usedSimps := (← get).usedSimps)
|
||||
let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (usedSimps := (← get).usedSimps)
|
||||
modify fun s => { s with usedSimps }
|
||||
match r with
|
||||
| none => return true -- closed the goal
|
||||
|
|
@ -99,7 +101,7 @@ private partial def loop : M Bool := do
|
|||
}
|
||||
-- simplify target
|
||||
let mvarId := (← get).mvarId
|
||||
let (r, usedSimps) ← simpTarget mvarId (← get).ctx (usedSimps := (← get).usedSimps)
|
||||
let (r, usedSimps) ← simpTarget mvarId (← get).ctx simprocs (usedSimps := (← get).usedSimps)
|
||||
modify fun s => { s with usedSimps }
|
||||
match r with
|
||||
| none => return true
|
||||
|
|
@ -140,9 +142,9 @@ def main : M (Option MVarId) := do
|
|||
|
||||
end SimpAll
|
||||
|
||||
def simpAll (mvarId : MVarId) (ctx : Simp.Context) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
|
||||
def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
|
||||
mvarId.withContext do
|
||||
let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps }
|
||||
let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
|
||||
if let .some mvarIdNew := r then
|
||||
if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
|
||||
throwError "simp_all made no progress"
|
||||
|
|
|
|||
|
|
@ -65,43 +65,18 @@ def registerSimproc (declName : Name) (keys : Array SimpTheoremKey) : CoreM Unit
|
|||
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
|
||||
keys : Array SimpTheoremKey := #[]
|
||||
deriving Inhabited
|
||||
|
||||
structure SimprocEntry extends SimprocOLeanEntry where
|
||||
/--
|
||||
Recall that we cannot store `Simproc` into .olean files because it is a closure.
|
||||
Given `SimprocOLeanEntry.declName`, we convert it into a `Simproc` by using the unsafe function `evalConstCheck`.
|
||||
-/
|
||||
proc : Simproc
|
||||
|
||||
instance : BEq SimprocEntry where
|
||||
beq e₁ e₂ := e₁.declName == e₂.declName
|
||||
|
||||
instance : ToFormat SimprocEntry where
|
||||
format e := format e.declName
|
||||
|
||||
abbrev SimprocTree := DiscrTree SimprocEntry
|
||||
|
||||
structure SimprocState where
|
||||
pre : SimprocTree := DiscrTree.empty
|
||||
post : SimprocTree := DiscrTree.empty
|
||||
simprocNames : PHashSet Name := {}
|
||||
erased : PHashSet Name := {}
|
||||
deriving Inhabited
|
||||
|
||||
def SimprocState.erase (s : SimprocState) (declName : Name) : SimprocState :=
|
||||
def Simprocs.erase (s : Simprocs) (declName : Name) : Simprocs :=
|
||||
{ s with erased := s.erased.insert declName, simprocNames := s.simprocNames.erase declName }
|
||||
|
||||
builtin_initialize builtinSimprocsRef : IO.Ref SimprocState ← IO.mkRef {}
|
||||
builtin_initialize builtinSimprocsRef : IO.Ref Simprocs ← IO.mkRef {}
|
||||
|
||||
abbrev SimprocExtension := ScopedEnvExtension SimprocOLeanEntry SimprocEntry SimprocState
|
||||
abbrev SimprocExtension := ScopedEnvExtension SimprocOLeanEntry SimprocEntry Simprocs
|
||||
|
||||
unsafe def getSimprocFromDeclImpl (declName : Name) : ImportM Simproc := do
|
||||
let ctx ← read
|
||||
|
|
@ -140,7 +115,7 @@ def addSimprocAttr (declName : Name) (kind : AttributeKind) (post : Bool) : Meta
|
|||
throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
|
||||
simprocExtension.add { declName, post, keys, proc } kind
|
||||
|
||||
def getSimprocState : CoreM SimprocState :=
|
||||
def getSimprocs : CoreM Simprocs :=
|
||||
return simprocExtension.getState (← getEnv)
|
||||
|
||||
def SimprocEntry.try? (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM (Option Step) := do
|
||||
|
|
@ -169,12 +144,12 @@ def simproc? (tag : String) (s : SimprocTree) (erased : PHashSet Name) (e : Expr
|
|||
|
||||
def preSimproc? (e : Expr) : SimpM (Option Step) := do
|
||||
if !(← getConfig).simproc then return none
|
||||
let s := simprocExtension.getState (← getEnv)
|
||||
let s ← simprocs
|
||||
simproc? "pre" s.pre s.erased e
|
||||
|
||||
def postSimproc? (e : Expr) : SimpM (Option Step) := do
|
||||
if !(← getConfig).simproc then return none
|
||||
let s := simprocExtension.getState (← getEnv)
|
||||
let s ← simprocs
|
||||
simproc? "post" s.post s.erased e
|
||||
|
||||
end Lean.Meta.Simp
|
||||
|
|
|
|||
|
|
@ -71,10 +71,42 @@ def Step.updateResult : Step → Result → Step
|
|||
| Step.visit _, r => Step.visit r
|
||||
| Step.done _, r => Step.done r
|
||||
|
||||
abbrev Simproc := Expr → SimpM (Option Step)
|
||||
|
||||
/--
|
||||
`Simproc` .olean entry.
|
||||
-/
|
||||
structure SimprocOLeanEntry where
|
||||
/-- Name of a declaration stored in the environment which has type `Simproc`. -/
|
||||
declName : Name
|
||||
post : Bool := true
|
||||
keys : Array SimpTheoremKey := #[]
|
||||
deriving Inhabited
|
||||
|
||||
/--
|
||||
`Simproc` entry. It is the .olean entry plus the actual function.
|
||||
-/
|
||||
structure SimprocEntry extends SimprocOLeanEntry where
|
||||
/--
|
||||
Recall that we cannot store `Simproc` into .olean files because it is a closure.
|
||||
Given `SimprocOLeanEntry.declName`, we convert it into a `Simproc` by using the unsafe function `evalConstCheck`.
|
||||
-/
|
||||
proc : Simproc
|
||||
|
||||
abbrev SimprocTree := DiscrTree SimprocEntry
|
||||
|
||||
structure Simprocs where
|
||||
pre : SimprocTree := DiscrTree.empty
|
||||
post : SimprocTree := DiscrTree.empty
|
||||
simprocNames : PHashSet Name := {}
|
||||
erased : PHashSet Name := {}
|
||||
deriving Inhabited
|
||||
|
||||
structure Methods where
|
||||
pre : Expr → SimpM Step := fun e => return Step.visit { expr := e }
|
||||
post : Expr → SimpM Step := fun e => return Step.done { expr := e }
|
||||
discharge? : Expr → SimpM (Option Expr) := fun _ => return none
|
||||
simprocs : Simprocs := {}
|
||||
deriving Inhabited
|
||||
|
||||
unsafe def Methods.toMethodsRefImpl (m : Methods) : MethodsRef :=
|
||||
|
|
@ -98,6 +130,9 @@ def pre (e : Expr) : SimpM Step := do
|
|||
def post (e : Expr) : SimpM Step := do
|
||||
(← getMethods).post e
|
||||
|
||||
def simprocs : SimpM Simprocs := do
|
||||
return (← getMethods).simprocs
|
||||
|
||||
def discharge? (e : Expr) : SimpM (Option Expr) := do
|
||||
(← getMethods).discharge? e
|
||||
|
||||
|
|
@ -355,7 +390,7 @@ def Step.addExtraArgs (s : Step) (extraArgs : Array Expr) : MetaM Step := do
|
|||
|
||||
end Simp
|
||||
|
||||
export Simp (SimpM)
|
||||
export Simp (SimpM Simprocs)
|
||||
|
||||
/--
|
||||
Auxiliary method.
|
||||
|
|
|
|||
|
|
@ -82,14 +82,14 @@ open SplitIf
|
|||
|
||||
def simpIfTarget (mvarId : MVarId) (useDecide := false) : MetaM MVarId := do
|
||||
let mut ctx ← getSimpContext
|
||||
if let (some mvarId', _) ← simpTarget mvarId ctx (discharge? useDecide) (mayCloseGoal := false) then
|
||||
if let (some mvarId', _) ← simpTarget mvarId ctx {} (discharge? useDecide) (mayCloseGoal := false) then
|
||||
return mvarId'
|
||||
else
|
||||
unreachable!
|
||||
|
||||
def simpIfLocalDecl (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
|
||||
let mut ctx ← getSimpContext
|
||||
if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx discharge? (mayCloseGoal := false) then
|
||||
if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx {} discharge? (mayCloseGoal := false) then
|
||||
return mvarId'
|
||||
else
|
||||
unreachable!
|
||||
|
|
|
|||
|
|
@ -12,3 +12,9 @@ example : x + foo 2 = 12 + x := by
|
|||
fail_if_success simp (config := { «simproc» := false })
|
||||
simp (config := { «simproc» := true })
|
||||
rw [Nat.add_comm]
|
||||
|
||||
example : x + foo 2 = 12 + x := by
|
||||
-- `simp only` must not use the default simproc set
|
||||
fail_if_success simp (config := { «simproc» := true }) only
|
||||
simp (config := { «simproc» := true })
|
||||
rw [Nat.add_comm]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue