From 283587987ab2eb3b56fbc3a19d5f33ab9e04a2ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 30 Apr 2024 14:11:34 -0700 Subject: [PATCH] feat: diagnostic information for `simp` --- src/Lean/Elab/Tactic/Simp.lean | 66 +++++++++---- src/Lean/Elab/Tactic/SimpTrace.lean | 29 +++--- src/Lean/Elab/Tactic/Simpa.lean | 26 ++--- src/Lean/Meta/Diagnostics.lean | 6 +- src/Lean/Meta/Tactic/Simp/Main.lean | 100 ++++++++++---------- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 1 + src/Lean/Meta/Tactic/Simp/SimpAll.lean | 29 +++--- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 3 + src/Lean/Meta/Tactic/Simp/Types.lean | 24 +++++ 9 files changed, 176 insertions(+), 108 deletions(-) diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index c51b1cf43b..7115a8c0ed 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -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 ` 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) diff --git a/src/Lean/Elab/Tactic/SimpTrace.lean b/src/Lean/Elab/Tactic/SimpTrace.lean index 76d2a7ece4..3342fc35dd 100644 --- a/src/Lean/Elab/Tactic/SimpTrace.lean +++ b/src/Lean/Elab/Tactic/SimpTrace.lean @@ -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 diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean index 3e8cf1e459..ab4717e4b4 100644 --- a/src/Lean/Elab/Tactic/Simpa.lean +++ b/src/Lean/Elab/Tactic/Simpa.lean @@ -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 diff --git a/src/Lean/Meta/Diagnostics.lean b/src/Lean/Meta/Diagnostics.lean index e6806ae9b3..269c214927 100644 --- a/src/Lean/Meta/Diagnostics.lean +++ b/src/Lean/Meta/Diagnostics.lean @@ -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 diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 6163f14fce..8af723e5fa 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -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 diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 93ffe0c3fb..6f484502f0 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -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 diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean index fa363c2534..6b69893369 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean @@ -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 diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index 92df535ef2..91c316e3e2 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -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, diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 323ca1d35c..f9c2a5a4de 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -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.