max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: sort simp lemmas by application order

Browse source
This commit is contained in:
Mario Carneiro 2022-09-21 17:13:44 -04:00 • committed by Leonardo de Moura
parent afca560bda
commit 84497c1d09
4 changed files with 26 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Elab/Tactic/Simp.lean
View file

@ -14,7 +14,7 @@ import Lean.Elab.Tactic.Config
namespace Lean.Elab.Tactic
open Meta
open TSyntax.Compat
open Simp (OriginSet)
open Simp (UsedSimps)
declare_config_elab elabSimpConfigCore Meta.Simp.Config
declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx
@ -249,7 +249,7 @@ register_builtin_option tactic.simp.trace : Bool := {
descr := "When tracing is enabled, calls to `simp` or `dsimp` will print an equivalent `simp only` call."
}
def traceSimpCall (stx : Syntax) (usedSimps : OriginSet) : MetaM Unit := do
def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
let mut stx := stx
if stx[3].isNone then
stx := stx.setArg 3 (mkNullNode #[mkAtom "only"])
@ -257,7 +257,7 @@ def traceSimpCall (stx : Syntax) (usedSimps : OriginSet) : MetaM Unit := do
let mut localsOrStar := some #[]
let lctx ← getLCtx
let env ← getEnv
for thm in usedSimps do
for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
match thm with
| .decl declName => -- global definitions in the environment
if env.contains declName && !simpOnlyBuiltins.contains declName then
@ -298,7 +298,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 OriginSet := do
def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
match loc with
| Location.targets hyps simplifyTarget =>
withMainContext do
@ -308,7 +308,7 @@ def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := non
withMainContext do
go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
where
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM OriginSet := do
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM UsedSimps := do
let mvarId ← getMainGoal
let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
match result? with

26
src/Lean/Meta/Tactic/Simp/Main.lean
View file

@ -690,7 +690,7 @@ where
modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
return r
def main (e : Expr) (ctx : Context) (usedSimps : OriginSet := {}) (methods : Methods := {}) : MetaM (Result × OriginSet) := do
def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do
let ctx := { ctx with config := (← ctx.config.updateArith) }
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
try
@ -699,7 +699,7 @@ def main (e : Expr) (ctx : Context) (usedSimps : OriginSet := {}) (methods : Met
catch ex =>
if ex.isMaxHeartbeat then throwNestedTacticEx `simp ex else throw ex
def dsimpMain (e : Expr) (ctx : Context) (usedSimps : OriginSet := {}) (methods : Methods := {}) : MetaM (Expr × OriginSet) := do
def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Expr × UsedSimps) := do
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
try
let (r, s) ← dsimp e methods ctx |>.run { usedTheorems := usedSimps }
@ -810,16 +810,16 @@ def methods : Methods :=
end DefaultMethods
end Simp
open Simp (OriginSet)
open Simp (UsedSimps)
def simp (e : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(usedSimps : OriginSet := {}) : MetaM (Simp.Result × OriginSet) := do profileitM Exception "simp" (← getOptions) do
(usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" (← getOptions) do
match discharge? with
| none => Simp.main e ctx usedSimps (methods := Simp.DefaultMethods.methods)
| some d => Simp.main e ctx usedSimps (methods := { pre := (Simp.preDefault · d), post := (Simp.postDefault · d), discharge? := d })
def dsimp (e : Expr) (ctx : Simp.Context)
(usedSimps : OriginSet := {}) : MetaM (Expr × OriginSet) := do profileitM Exception "dsimp" (← getOptions) do
(usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do
Simp.dsimpMain e ctx usedSimps (methods := Simp.DefaultMethods.methods)
/--
@ -837,7 +837,7 @@ def applySimpResultToTarget (mvarId : MVarId) (target : Expr) (r : Simp.Result)
/-- 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)
(mayCloseGoal := true) (usedSimps : OriginSet := {}) : MetaM (Option MVarId × OriginSet) := do
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
let target ← instantiateMVars (← mvarId.getType)
let (r, usedSimps) ← simp target ctx discharge? usedSimps
if mayCloseGoal && r.expr.isConstOf ``True then
@ -852,7 +852,7 @@ 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)
(mayCloseGoal := true) (usedSimps : OriginSet := {}) : MetaM (Option MVarId × OriginSet) :=
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
mvarId.withContext do
mvarId.checkNotAssigned `simp
simpTargetCore mvarId ctx discharge? mayCloseGoal usedSimps
@ -887,7 +887,7 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
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)
(mayCloseGoal := true) (usedSimps : OriginSet := {}) : MetaM (Option (Expr × Expr) × OriginSet) := do
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do
let (r, usedSimps) ← simp prop ctx discharge? usedSimps
return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
@ -920,7 +920,7 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(mayCloseGoal := true) (usedSimps : OriginSet := {}) : MetaM (Option (FVarId × MVarId) × OriginSet) := do
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do
mvarId.withContext do
mvarId.checkNotAssigned `simp
let type ← instantiateMVars (← fvarId.getType)
@ -929,7 +929,7 @@ def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (disc
def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
(usedSimps : OriginSet := {}) : MetaM (Option (Array FVarId × MVarId) × OriginSet) := do
(usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
mvarId.withContext do
mvarId.checkNotAssigned `simp
let mut mvarId := mvarId
@ -964,7 +964,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
return (some (fvarIdsNew, mvarIdNew), usedSimps)
def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(usedSimps : OriginSet := {}) : MetaM (TacticResultCNM × OriginSet) := mvarId.withContext do
(usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
let mut ctx := ctx
for h in (← getPropHyps) do
let localDecl ← h.getDecl
@ -980,11 +980,11 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option S
return (TacticResultCNM.modified mvarId', usedSimps')
def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
(usedSimps : OriginSet := {}) : MetaM (Option MVarId × OriginSet) := do
(usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
mvarId.withContext do
mvarId.checkNotAssigned `simp
let mut mvarId := mvarId
let mut usedSimps : OriginSet := usedSimps
let mut usedSimps : UsedSimps := usedSimps
for fvarId in fvarIdsToSimp do
let type ← instantiateMVars (← fvarId.getType)
let (typeNew, usedSimps') ← dsimp type ctx

6
src/Lean/Meta/Tactic/Simp/SimpAll.lean
View file

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

8
src/Lean/Meta/Tactic/Simp/Types.lean
View file

@ -35,12 +35,12 @@ def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
def Context.mkDefault : MetaM Context :=
return { config := {}, simpTheorems := #[(← getSimpTheorems)], congrTheorems := (← getSimpCongrTheorems) }
abbrev OriginSet := Std.HashSet Origin
abbrev UsedSimps := Std.HashMap Origin Nat
structure State where
cache : Cache := {}
congrCache : CongrCache := {}
usedTheorems : OriginSet := {}
usedTheorems : UsedSimps := {}
numSteps : Nat := 0
abbrev SimpM := ReaderT Context $ StateRefT State MetaM
@ -101,7 +101,9 @@ def getSimpCongrTheorems : M SimpCongrTheorems :=
modify fun s => { s with cache := cacheSaved }
def recordSimpTheorem (thmId : Origin) : SimpM Unit :=
modify fun s => { s with usedTheorems := s.usedTheorems.insert thmId }
modify fun s => if s.usedTheorems.contains thmId then s else
let n := s.usedTheorems.size
{ s with usedTheorems := s.usedTheorems.insert thmId n }
end Simp