feat: diagnostic information for simp
This commit is contained in:
Leonardo de Moura
Leonardo de Moura
parent
99e652ab1c
commit
283587987a
9 changed files with 176 additions and 108 deletions
|
|
@ -15,7 +15,6 @@ import Lean.Elab.Tactic.Config
|
|||
namespace Lean.Elab.Tactic
|
||||
open Meta
|
||||
open TSyntax.Compat
|
||||
open Simp (UsedSimps)
|
||||
|
||||
declare_config_elab elabSimpConfigCore Meta.Simp.Config
|
||||
declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx
|
||||
|
|
@ -327,7 +326,7 @@ If `stx` is the syntax of a `simp`, `simp_all` or `dsimp` tactic invocation, and
|
|||
creates the syntax of an equivalent `simp only`, `simp_all only` or `dsimp only`
|
||||
invocation.
|
||||
-/
|
||||
def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
|
||||
def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
|
||||
let isSimpAll := stx.isOfKind ``Parser.Tactic.simpAll
|
||||
let mut stx := stx
|
||||
if stx[3].isNone then
|
||||
|
|
@ -379,7 +378,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
|
|||
let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
|
||||
return stx.setArg 4 (mkNullNode argsStx)
|
||||
|
||||
def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
|
||||
def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do
|
||||
logInfoAt stx[0] m!"Try this: {← mkSimpOnly stx usedSimps}"
|
||||
|
||||
/--
|
||||
|
|
@ -396,7 +395,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 : Simp.SimprocsArray) (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 Simp.Stats := do
|
||||
match loc with
|
||||
| Location.targets hyps simplifyTarget =>
|
||||
withMainContext do
|
||||
|
|
@ -406,33 +405,67 @@ def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge
|
|||
withMainContext do
|
||||
go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
|
||||
where
|
||||
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM UsedSimps := do
|
||||
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.Stats := do
|
||||
let mvarId ← getMainGoal
|
||||
let (result?, usedSimps) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
|
||||
let (result?, stats) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
|
||||
match result? with
|
||||
| none => replaceMainGoal []
|
||||
| some (_, mvarId) => replaceMainGoal [mvarId]
|
||||
return usedSimps
|
||||
return stats
|
||||
|
||||
def mkSimpDiagSummary (counters : PHashMap Origin Nat) : MetaM DiagSummary := do
|
||||
let threshold := diagnostics.threshold.get (← getOptions)
|
||||
let entries := collectAboveThreshold counters threshold (fun _ => true) (lt := (· < ·))
|
||||
if entries.isEmpty then
|
||||
return {}
|
||||
else
|
||||
let mut data := #[]
|
||||
for (thmId, counter) in entries do
|
||||
let key ← match thmId with
|
||||
| .decl declName _ _ => pure m!"{MessageData.ofConst (← mkConstWithLevelParams declName)}"
|
||||
| .fvar fvarId => pure m!"{mkFVar fvarId}"
|
||||
| _ => pure thmId.key
|
||||
data := data.push m!"{if data.isEmpty then " " else "\n"}{key} ↦ {counter}"
|
||||
return { data, max := entries[0]!.2 }
|
||||
|
||||
def reportDiag (diag : Simp.Diagnostics) : TacticM Unit := do
|
||||
if (← isDiagnosticsEnabled) then
|
||||
let used ← mkSimpDiagSummary diag.usedThmCounter
|
||||
let tried ← mkSimpDiagSummary diag.triedThmCounter
|
||||
unless used.isEmpty && tried.isEmpty do
|
||||
let m := MessageData.nil
|
||||
let m := appendSection m `simp "used theorems" used
|
||||
let m := appendSection m `simp "tried theorems" tried
|
||||
let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
|
||||
logInfo m
|
||||
|
||||
def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
|
||||
-- TODO: collect current unfolding diag info
|
||||
let stats ← x
|
||||
reportDiag stats
|
||||
return ()
|
||||
|
||||
/-
|
||||
"simp" (config)? (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
|
||||
(location)?
|
||||
-/
|
||||
@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do
|
||||
@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do
|
||||
let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
|
||||
let usedSimps ← dischargeWrapper.with fun discharge? =>
|
||||
let stats ← dischargeWrapper.with fun discharge? =>
|
||||
simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
|
||||
if tactic.simp.trace.get (← getOptions) then
|
||||
traceSimpCall stx usedSimps
|
||||
traceSimpCall stx stats.usedTheorems
|
||||
return stats.diag
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do
|
||||
@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do withSimpDiagnostics do
|
||||
let { ctx, simprocs, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
|
||||
let (result?, usedSimps) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
|
||||
let (result?, stats) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
|
||||
match result? with
|
||||
| none => replaceMainGoal []
|
||||
| some mvarId => replaceMainGoal [mvarId]
|
||||
if tactic.simp.trace.get (← getOptions) then
|
||||
traceSimpCall stx usedSimps
|
||||
traceSimpCall stx stats.usedTheorems
|
||||
return stats.diag
|
||||
|
||||
def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Location) : TacticM Unit := do
|
||||
match loc with
|
||||
|
|
@ -444,14 +477,15 @@ def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Lo
|
|||
withMainContext do
|
||||
go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
|
||||
where
|
||||
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do
|
||||
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := withSimpDiagnostics do
|
||||
let mvarId ← getMainGoal
|
||||
let (result?, usedSimps) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
|
||||
let (result?, stats) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
|
||||
match result? with
|
||||
| none => replaceMainGoal []
|
||||
| some mvarId => replaceMainGoal [mvarId]
|
||||
if tactic.simp.trace.get (← getOptions) then
|
||||
mvarId.withContext <| traceSimpCall (← getRef) usedSimps
|
||||
mvarId.withContext <| traceSimpCall (← getRef) stats.usedTheorems
|
||||
return stats.diag
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do
|
||||
let { ctx, simprocs, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
|
||||
|
|
|
|||
|
|
@ -25,39 +25,41 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
|
|||
@[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
|
||||
match stx with
|
||||
| `(tactic|
|
||||
simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do
|
||||
simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
|
||||
let stx ← if bang.isSome then
|
||||
`(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
else
|
||||
`(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
|
||||
let usedSimps ← dischargeWrapper.with fun discharge? =>
|
||||
let stats ← dischargeWrapper.with fun discharge? =>
|
||||
simpLocation ctx (simprocs := simprocs) discharge? <|
|
||||
(loc.map expandLocation).getD (.targets #[] true)
|
||||
let stx ← mkSimpCallStx stx usedSimps
|
||||
let stx ← mkSimpCallStx stx stats.usedTheorems
|
||||
addSuggestion tk stx (origSpan? := ← getRef)
|
||||
return stats.diag
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx =>
|
||||
match stx with
|
||||
| `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => do
|
||||
| `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
|
||||
let stx ← if bang.isSome then
|
||||
`(tactic| simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
|
||||
else
|
||||
`(tactic| simp_all%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
|
||||
let { ctx, .. } ← mkSimpContext stx (eraseLocal := true)
|
||||
(kind := .simpAll) (ignoreStarArg := true)
|
||||
let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
|
||||
let (result?, stats) ← simpAll (← getMainGoal) ctx
|
||||
match result? with
|
||||
| none => replaceMainGoal []
|
||||
| some mvarId => replaceMainGoal [mvarId]
|
||||
let stx ← mkSimpCallStx stx usedSimps
|
||||
let stx ← mkSimpCallStx stx stats.usedTheorems
|
||||
addSuggestion tk stx (origSpan? := ← getRef)
|
||||
return stats.diag
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
/-- Implementation of `dsimp?`. -/
|
||||
def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Location) :
|
||||
TacticM Simp.UsedSimps := do
|
||||
TacticM Simp.Stats := do
|
||||
match loc with
|
||||
| Location.targets hyps simplifyTarget =>
|
||||
withMainContext do
|
||||
|
|
@ -68,25 +70,26 @@ def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Locati
|
|||
go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
|
||||
where
|
||||
/-- Implementation of `dsimp?`. -/
|
||||
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
|
||||
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.Stats := do
|
||||
let mvarId ← getMainGoal
|
||||
let (result?, usedSimps) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
|
||||
let (result?, stats) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
|
||||
(fvarIdsToSimp := fvarIdsToSimp)
|
||||
match result? with
|
||||
| none => replaceMainGoal []
|
||||
| some mvarId => replaceMainGoal [mvarId]
|
||||
pure usedSimps
|
||||
pure stats
|
||||
|
||||
@[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx =>
|
||||
match stx with
|
||||
| `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => do
|
||||
| `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
|
||||
let stx ← if bang.isSome then
|
||||
`(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
else
|
||||
`(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
let { ctx, simprocs, .. } ←
|
||||
withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
|
||||
let usedSimps ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
|
||||
let stx ← mkSimpCallStx stx usedSimps
|
||||
let stats ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
|
||||
let stx ← mkSimpCallStx stx stats.usedTheorems
|
||||
addSuggestion tk stx (origSpan? := ← getRef)
|
||||
return stats.diag
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ deriving instance Repr for UseImplicitLambdaResult
|
|||
@[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do
|
||||
match stx with
|
||||
| `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
|
||||
$[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do
|
||||
$[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
|
||||
let stx ← `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?)
|
||||
let { ctx, simprocs, dischargeWrapper } ←
|
||||
withMainContext <| mkSimpContext stx (eraseLocal := false)
|
||||
|
|
@ -39,12 +39,13 @@ deriving instance Repr for UseImplicitLambdaResult
|
|||
-- TODO: have `simpa` fail if it doesn't use `simp`.
|
||||
let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
|
||||
dischargeWrapper.with fun discharge? => do
|
||||
let (some (_, g), usedSimps) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
|
||||
let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
|
||||
(simplifyTarget := true) (discharge? := discharge?)
|
||||
| if getLinterUnnecessarySimpa (← getOptions) then
|
||||
logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
|
||||
return {}
|
||||
g.withContext do
|
||||
let usedSimps ← if let some stx := usingArg then
|
||||
let stats ← if let some stx := usingArg then
|
||||
setGoals [g]
|
||||
g.withContext do
|
||||
let e ← Tactic.elabTerm stx none (mayPostpone := true)
|
||||
|
|
@ -52,8 +53,8 @@ deriving instance Repr for UseImplicitLambdaResult
|
|||
pure (h, g)
|
||||
else
|
||||
(← g.assert `h (← inferType e) e).intro1
|
||||
let (result?, usedSimps) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
|
||||
(simplifyTarget := false) (usedSimps := usedSimps) (discharge? := discharge?)
|
||||
let (result?, stats) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
|
||||
(simplifyTarget := false) (stats := stats) (discharge? := discharge?)
|
||||
match result? with
|
||||
| some (xs, g) =>
|
||||
let h := match xs with | #[h] | #[] => h | _ => unreachable!
|
||||
|
|
@ -66,18 +67,18 @@ deriving instance Repr for UseImplicitLambdaResult
|
|||
if (← getLCtx).getRoundtrippingUserName? h |>.isSome then
|
||||
logLint linter.unnecessarySimpa (← getRef)
|
||||
m!"try 'simp at {Expr.fvar h}' instead of 'simpa using {Expr.fvar h}'"
|
||||
pure usedSimps
|
||||
pure stats
|
||||
else if let some ldecl := (← getLCtx).findFromUserName? `this then
|
||||
if let (some (_, g), usedSimps) ← simpGoal g ctx (simprocs := simprocs)
|
||||
(fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (usedSimps := usedSimps)
|
||||
if let (some (_, g), stats) ← simpGoal g ctx (simprocs := simprocs)
|
||||
(fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (stats := stats)
|
||||
(discharge? := discharge?) then
|
||||
g.assumption; pure usedSimps
|
||||
g.assumption; pure stats
|
||||
else
|
||||
pure usedSimps
|
||||
pure stats
|
||||
else
|
||||
g.assumption; pure usedSimps
|
||||
g.assumption; pure stats
|
||||
if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
|
||||
let stx ← match ← mkSimpOnly stx usedSimps with
|
||||
let stx ← match ← mkSimpOnly stx stats.usedTheorems with
|
||||
| `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?) =>
|
||||
if unfold.isSome then
|
||||
`(tactic| simpa! $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
|
||||
|
|
@ -85,6 +86,7 @@ deriving instance Repr for UseImplicitLambdaResult
|
|||
`(tactic| simpa $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
|
||||
| _ => unreachable!
|
||||
TryThis.addSuggestion tk stx (origSpan? := ← getRef)
|
||||
return stats.diag
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
end Lean.Elab.Tactic.Simpa
|
||||
|
|
|
|||
|
|
@ -10,13 +10,13 @@ import Lean.Meta.Instances
|
|||
|
||||
namespace Lean.Meta
|
||||
|
||||
private def collectAboveThreshold (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool) : Array (Name × Nat) := Id.run do
|
||||
def collectAboveThreshold [BEq α] [Hashable α] (counters : PHashMap α Nat) (threshold : Nat) (p : α → Bool) (lt : α → α → Bool) : Array (α × Nat) := Id.run do
|
||||
let mut r := #[]
|
||||
for (declName, counter) in counters do
|
||||
if counter > threshold then
|
||||
if p declName then
|
||||
r := r.push (declName, counter)
|
||||
return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then d₁.lt d₂ else c₁ > c₂
|
||||
return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then lt d₁ d₂ else c₁ > c₂
|
||||
|
||||
structure DiagSummary where
|
||||
data : Array MessageData := #[]
|
||||
|
|
@ -27,7 +27,7 @@ def DiagSummary.isEmpty (s : DiagSummary) : Bool :=
|
|||
s.data.isEmpty
|
||||
|
||||
def mkDiagSummary (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do
|
||||
let entries := collectAboveThreshold counters threshold p
|
||||
let entries := collectAboveThreshold counters threshold p Name.lt
|
||||
if entries.isEmpty then
|
||||
return {}
|
||||
else
|
||||
|
|
|
|||
|
|
@ -655,60 +655,60 @@ where
|
|||
@[inline] def withSimpConfig (ctx : Context) (x : MetaM α) : MetaM α :=
|
||||
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
|
||||
|
||||
def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do
|
||||
def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
|
||||
let ctx := { ctx with config := (← ctx.config.updateArith) }
|
||||
withSimpConfig ctx do withCatchingRuntimeEx do
|
||||
try
|
||||
withoutCatchingRuntimeEx do
|
||||
let (r, s) ← simp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
|
||||
let (r, s) ← simp e methods.toMethodsRef ctx |>.run { stats with }
|
||||
trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
|
||||
return (r, s.usedTheorems)
|
||||
return (r, { s with })
|
||||
catch ex =>
|
||||
if ex.isRuntime then throwNestedTacticEx `simp ex else throw ex
|
||||
|
||||
def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Expr × UsedSimps) := do
|
||||
def dsimpMain (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Expr × Stats) := do
|
||||
withSimpConfig ctx do withCatchingRuntimeEx do
|
||||
try
|
||||
withoutCatchingRuntimeEx do
|
||||
let (r, s) ← dsimp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
|
||||
pure (r, s.usedTheorems)
|
||||
let (r, s) ← dsimp e methods.toMethodsRef ctx |>.run { stats with }
|
||||
pure (r, { s with })
|
||||
catch ex =>
|
||||
if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex
|
||||
|
||||
end Simp
|
||||
open Simp (UsedSimps SimprocsArray)
|
||||
open Simp (SimprocsArray Stats)
|
||||
|
||||
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
|
||||
(stats : Stats := {}) : MetaM (Simp.Result × Stats) := do profileitM Exception "simp" (← getOptions) do
|
||||
match discharge? with
|
||||
| none => Simp.main e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs)
|
||||
| some d => Simp.main e ctx usedSimps (methods := Simp.mkMethods simprocs d)
|
||||
| none => Simp.main e ctx stats (methods := Simp.mkDefaultMethodsCore simprocs)
|
||||
| some d => Simp.main e ctx stats (methods := Simp.mkMethods simprocs d)
|
||||
|
||||
def dsimp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[])
|
||||
(usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do
|
||||
Simp.dsimpMain e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs )
|
||||
(stats : Stats := {}) : MetaM (Expr × Stats) := do profileitM Exception "dsimp" (← getOptions) do
|
||||
Simp.dsimpMain e ctx stats (methods := Simp.mkDefaultMethodsCore simprocs )
|
||||
|
||||
/-- 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 : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
|
||||
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
|
||||
(mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
|
||||
let target ← instantiateMVars (← mvarId.getType)
|
||||
let (r, usedSimps) ← simp target ctx simprocs discharge? usedSimps
|
||||
let (r, stats) ← simp target ctx simprocs discharge? stats
|
||||
if mayCloseGoal && r.expr.isTrue then
|
||||
match r.proof? with
|
||||
| some proof => mvarId.assign (← mkOfEqTrue proof)
|
||||
| none => mvarId.assign (mkConst ``True.intro)
|
||||
return (none, usedSimps)
|
||||
return (none, stats)
|
||||
else
|
||||
return (← applySimpResultToTarget mvarId target r, usedSimps)
|
||||
return (← applySimpResultToTarget mvarId target r, stats)
|
||||
|
||||
/--
|
||||
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 : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
|
||||
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
|
||||
(mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) :=
|
||||
mvarId.withContext do
|
||||
mvarId.checkNotAssigned `simp
|
||||
simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal usedSimps
|
||||
simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal stats
|
||||
|
||||
/--
|
||||
Apply the result `r` for `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
|
||||
|
|
@ -740,9 +740,9 @@ 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) (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)
|
||||
(mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (Expr × Expr) × Stats) := do
|
||||
let (r, stats) ← simp prop ctx simprocs discharge? stats
|
||||
return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), stats)
|
||||
|
||||
def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do
|
||||
match r with
|
||||
|
|
@ -773,99 +773,99 @@ 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) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
|
||||
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do
|
||||
(mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (FVarId × MVarId) × Stats) := do
|
||||
mvarId.withContext do
|
||||
mvarId.checkNotAssigned `simp
|
||||
let type ← instantiateMVars (← fvarId.getType)
|
||||
let (r, usedSimps) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal usedSimps
|
||||
return (← applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps)
|
||||
let (r, stats) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal stats
|
||||
return (← applySimpResultToLocalDeclCore mvarId fvarId r, stats)
|
||||
|
||||
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
|
||||
(stats : Stats := {}) : MetaM (Option (Array FVarId × MVarId) × Stats) := do
|
||||
mvarId.withContext do
|
||||
mvarId.checkNotAssigned `simp
|
||||
let mut mvarIdNew := mvarId
|
||||
let mut toAssert := #[]
|
||||
let mut replaced := #[]
|
||||
let mut usedSimps := usedSimps
|
||||
let mut stats := stats
|
||||
for fvarId in fvarIdsToSimp do
|
||||
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 simprocs discharge? usedSimps
|
||||
usedSimps := usedSimps'
|
||||
let (r, stats') ← simp type ctx simprocs discharge? stats
|
||||
stats := stats'
|
||||
match r.proof? with
|
||||
| some _ => match (← applySimpResultToProp mvarIdNew (mkFVar fvarId) type r) with
|
||||
| none => return (none, usedSimps)
|
||||
| none => return (none, stats)
|
||||
| some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
|
||||
| none =>
|
||||
if r.expr.isFalse then
|
||||
mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
|
||||
return (none, usedSimps)
|
||||
return (none, stats)
|
||||
-- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
|
||||
-- Reason: it introduces a `mkExpectedTypeHint`
|
||||
mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId r.expr
|
||||
replaced := replaced.push fvarId
|
||||
if simplifyTarget then
|
||||
match (← simpTarget mvarIdNew ctx simprocs discharge? (usedSimps := usedSimps)) with
|
||||
| (none, usedSimps') => return (none, usedSimps')
|
||||
| (some mvarIdNew', usedSimps') => mvarIdNew := mvarIdNew'; usedSimps := usedSimps'
|
||||
match (← simpTarget mvarIdNew ctx simprocs discharge? (stats := stats)) with
|
||||
| (none, stats') => return (none, stats')
|
||||
| (some mvarIdNew', stats') => mvarIdNew := mvarIdNew'; stats := stats'
|
||||
let (fvarIdsNew, mvarIdNew') ← mvarIdNew.assertHypotheses toAssert
|
||||
mvarIdNew := mvarIdNew'
|
||||
let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
|
||||
mvarIdNew ← mvarIdNew.tryClearMany toClear
|
||||
if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
|
||||
throwError "simp made no progress"
|
||||
return (some (fvarIdsNew, mvarIdNew), usedSimps)
|
||||
return (some (fvarIdsNew, mvarIdNew), stats)
|
||||
|
||||
def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
|
||||
(usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
|
||||
(stats : Stats := {}) : MetaM (TacticResultCNM × Stats) := mvarId.withContext do
|
||||
let mut ctx := ctx
|
||||
for h in (← getPropHyps) do
|
||||
let localDecl ← h.getDecl
|
||||
let proof := localDecl.toExpr
|
||||
let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
|
||||
ctx := { ctx with simpTheorems }
|
||||
match (← simpTarget mvarId ctx simprocs discharge? (usedSimps := usedSimps)) with
|
||||
| (none, usedSimps) => return (TacticResultCNM.closed, usedSimps)
|
||||
| (some mvarId', usedSimps') =>
|
||||
match (← simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
|
||||
| (none, stats) => return (TacticResultCNM.closed, stats)
|
||||
| (some mvarId', stats') =>
|
||||
if (← mvarId.getType) == (← mvarId'.getType) then
|
||||
return (TacticResultCNM.noChange, usedSimps)
|
||||
return (TacticResultCNM.noChange, stats)
|
||||
else
|
||||
return (TacticResultCNM.modified mvarId', usedSimps')
|
||||
return (TacticResultCNM.modified mvarId', stats')
|
||||
|
||||
def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
|
||||
(usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
|
||||
(stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
|
||||
mvarId.withContext do
|
||||
mvarId.checkNotAssigned `simp
|
||||
let mut mvarIdNew := mvarId
|
||||
let mut usedSimps : UsedSimps := usedSimps
|
||||
let mut stats : Stats := stats
|
||||
for fvarId in fvarIdsToSimp do
|
||||
let type ← instantiateMVars (← fvarId.getType)
|
||||
let (typeNew, usedSimps') ← dsimp type ctx simprocs
|
||||
usedSimps := usedSimps'
|
||||
let (typeNew, stats') ← dsimp type ctx simprocs
|
||||
stats := stats'
|
||||
if typeNew.isFalse then
|
||||
mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
|
||||
return (none, usedSimps)
|
||||
return (none, stats)
|
||||
if typeNew != type then
|
||||
mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId typeNew
|
||||
if simplifyTarget then
|
||||
let target ← mvarIdNew.getType
|
||||
let (targetNew, usedSimps') ← dsimp target ctx simprocs usedSimps
|
||||
usedSimps := usedSimps'
|
||||
let (targetNew, stats') ← dsimp target ctx simprocs stats
|
||||
stats := stats'
|
||||
if targetNew.isTrue then
|
||||
mvarIdNew.assign (mkConst ``True.intro)
|
||||
return (none, usedSimps)
|
||||
return (none, stats)
|
||||
if let some (_, lhs, rhs) := targetNew.consumeMData.eq? then
|
||||
if (← withReducible <| isDefEq lhs rhs) then
|
||||
mvarIdNew.assign (← mkEqRefl lhs)
|
||||
return (none, usedSimps)
|
||||
return (none, stats)
|
||||
if target != targetNew then
|
||||
mvarIdNew ← mvarIdNew.replaceTargetDefEq targetNew
|
||||
pure () -- FIXME: bug in do notation if this is removed?
|
||||
if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
|
||||
throwError "dsimp made no progress"
|
||||
return (some mvarIdNew, usedSimps)
|
||||
return (some mvarIdNew, stats)
|
||||
|
||||
end Lean.Meta
|
||||
|
|
|
|||
|
|
@ -109,6 +109,7 @@ where
|
|||
return false
|
||||
|
||||
private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
|
||||
recordTriedSimpTheorem thm.origin
|
||||
let rec go (e : Expr) : SimpM (Option Result) := do
|
||||
if (← isDefEq lhs e) then
|
||||
unless (← synthesizeArgs thm.origin bis xs) do
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ import Lean.Meta.Tactic.Simp.Main
|
|||
|
||||
namespace Lean.Meta
|
||||
|
||||
open Simp (UsedSimps SimprocsArray)
|
||||
open Simp (Stats SimprocsArray)
|
||||
|
||||
namespace SimpAll
|
||||
|
||||
|
|
@ -24,12 +24,13 @@ structure Entry where
|
|||
deriving Inhabited
|
||||
|
||||
structure State where
|
||||
modified : Bool := false
|
||||
mvarId : MVarId
|
||||
entries : Array Entry := #[]
|
||||
ctx : Simp.Context
|
||||
simprocs : SimprocsArray
|
||||
usedSimps : UsedSimps := {}
|
||||
modified : Bool := false
|
||||
mvarId : MVarId
|
||||
entries : Array Entry := #[]
|
||||
ctx : Simp.Context
|
||||
simprocs : SimprocsArray
|
||||
usedTheorems : Simp.UsedSimps := {}
|
||||
diag : Simp.Diagnostics := {}
|
||||
|
||||
abbrev M := StateRefT State MetaM
|
||||
|
||||
|
|
@ -62,8 +63,8 @@ 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 simprocs (usedSimps := (← get).usedSimps)
|
||||
modify fun s => { s with usedSimps }
|
||||
let (r, stats) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (stats := { (← get) with })
|
||||
modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
|
||||
match r with
|
||||
| none => return true -- closed the goal
|
||||
| some (proofNew, typeNew) =>
|
||||
|
|
@ -102,8 +103,8 @@ private partial def loop : M Bool := do
|
|||
}
|
||||
-- simplify target
|
||||
let mvarId := (← get).mvarId
|
||||
let (r, usedSimps) ← simpTarget mvarId (← get).ctx simprocs (usedSimps := (← get).usedSimps)
|
||||
modify fun s => { s with usedSimps }
|
||||
let (r, stats) ← simpTarget mvarId (← get).ctx simprocs (stats := { (← get) with })
|
||||
modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
|
||||
match r with
|
||||
| none => return true
|
||||
| some mvarIdNew =>
|
||||
|
|
@ -143,12 +144,12 @@ def main : M (Option MVarId) := do
|
|||
|
||||
end SimpAll
|
||||
|
||||
def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
|
||||
def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
|
||||
mvarId.withContext do
|
||||
let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
|
||||
let (r, s) ← SimpAll.main.run { stats with mvarId, ctx, simprocs }
|
||||
if let .some mvarIdNew := r then
|
||||
if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
|
||||
throwError "simp_all made no progress"
|
||||
return (r, s.usedSimps)
|
||||
return (r, { s with })
|
||||
|
||||
end Lean.Meta
|
||||
|
|
|
|||
|
|
@ -50,6 +50,9 @@ def Origin.key : Origin → Name
|
|||
|
||||
instance : BEq Origin := ⟨(·.key == ·.key)⟩
|
||||
instance : Hashable Origin := ⟨(hash ·.key)⟩
|
||||
instance : LT Origin := ⟨(·.key.lt ·.key)⟩
|
||||
instance (a b : Origin) : Decidable (a < b) :=
|
||||
inferInstanceAs (Decidable (a.key.lt b.key = true))
|
||||
|
||||
/-
|
||||
Note: we want to use iota reduction when indexing instances. Otherwise,
|
||||
|
|
|
|||
|
|
@ -98,11 +98,23 @@ def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
|
|||
-- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
|
||||
abbrev UsedSimps := PHashMap Origin Nat
|
||||
|
||||
structure Diagnostics where
|
||||
/-- Number of times each simp theorem has been used/applied. -/
|
||||
usedThmCounter : PHashMap Origin Nat := {}
|
||||
/-- Number of times each simp theorem has been tried. -/
|
||||
triedThmCounter : PHashMap Origin Nat := {}
|
||||
deriving Inhabited
|
||||
|
||||
structure State where
|
||||
cache : Cache := {}
|
||||
congrCache : CongrCache := {}
|
||||
usedTheorems : UsedSimps := {}
|
||||
numSteps : Nat := 0
|
||||
diag : Diagnostics := {}
|
||||
|
||||
structure Stats where
|
||||
usedTheorems : UsedSimps := {}
|
||||
diag : Diagnostics := {}
|
||||
|
||||
private opaque MethodsRefPointed : NonemptyType.{0}
|
||||
|
||||
|
|
@ -118,6 +130,10 @@ opaque simp (e : Expr) : SimpM Result
|
|||
@[extern "lean_dsimp"]
|
||||
opaque dsimp (e : Expr) : SimpM Expr
|
||||
|
||||
@[inline] def modifyDiag (f : Diagnostics → Diagnostics) : SimpM Unit := do
|
||||
if (← isDiagnosticsEnabled) then
|
||||
modify fun { cache, congrCache, usedTheorems, numSteps, diag } => { cache, congrCache, usedTheorems, numSteps, diag := f diag }
|
||||
|
||||
/--
|
||||
Result type for a simplification procedure. We have `pre` and `post` simplication procedures.
|
||||
-/
|
||||
|
|
@ -291,7 +307,15 @@ Save current cache, reset it, execute `x`, and then restore original cache.
|
|||
@[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
|
||||
withFreshCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
|
||||
|
||||
def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do
|
||||
modifyDiag fun { usedThmCounter, triedThmCounter } =>
|
||||
let cNew := if let some c := triedThmCounter.find? thmId then c + 1 else 1
|
||||
{ usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew }
|
||||
|
||||
def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
|
||||
modifyDiag fun { usedThmCounter, triedThmCounter } =>
|
||||
let cNew := if let some c := usedThmCounter.find? thmId then c + 1 else 1
|
||||
{ usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter }
|
||||
/-
|
||||
If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead.
|
||||
See issue #3547.
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue