From d9ea0925853818660ff4869ef11bcacfaec9b7d7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 May 2024 19:22:24 +0200 Subject: [PATCH] feat: include congruence theorems at `simp` diagnostic information (#4043) --- src/Lean/Meta/Diagnostics.lean | 15 ++++++--------- src/Lean/Meta/Tactic/Simp/Diagnostics.lean | 2 ++ src/Lean/Meta/Tactic/Simp/Main.lean | 1 + src/Lean/Meta/Tactic/Simp/Types.lean | 16 ++++++++++++---- 4 files changed, 21 insertions(+), 13 deletions(-) diff --git a/src/Lean/Meta/Diagnostics.lean b/src/Lean/Meta/Diagnostics.lean index 18fdf03c6b..baf77a8ef3 100644 --- a/src/Lean/Meta/Diagnostics.lean +++ b/src/Lean/Meta/Diagnostics.lean @@ -35,7 +35,8 @@ structure DiagSummary where 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 +def mkDiagSummary (counters : PHashMap Name Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do + let threshold := diagnostics.threshold.get (← getOptions) let entries := collectAboveThreshold counters threshold p Name.lt if entries.isEmpty then return {} @@ -46,21 +47,18 @@ def mkDiagSummary (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → return { data, max := entries[0]!.2 } def mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances := false) : MetaM DiagSummary := do - let threshold := diagnostics.threshold.get (← getOptions) let env ← getEnv - mkDiagSummary counters threshold fun declName => + mkDiagSummary counters fun declName => getReducibilityStatusCore env declName matches .semireducible && isInstanceCore env declName == instances def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM DiagSummary := do - let threshold := diagnostics.threshold.get (← getOptions) let env ← getEnv - mkDiagSummary counters threshold fun declName => + mkDiagSummary counters fun declName => getReducibilityStatusCore env declName matches .reducible def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do - let threshold := diagnostics.threshold.get (← getOptions) - mkDiagSummary (← get).diag.heuristicCounter threshold + mkDiagSummary (← get).diag.heuristicCounter def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) : MessageData := if s.isEmpty then @@ -71,12 +69,11 @@ def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSumm def reportDiag : MetaM Unit := do if (← isDiagnosticsEnabled) then - let threshold := diagnostics.threshold.get (← getOptions) let unfoldCounter := (← get).diag.unfoldCounter let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true) let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter - let heu ← mkDiagSummary (← get).diag.heuristicCounter threshold + let heu ← mkDiagSummary (← get).diag.heuristicCounter let inst ← mkDiagSummaryForUsedInstances unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty do let m := MessageData.nil diff --git a/src/Lean/Meta/Tactic/Simp/Diagnostics.lean b/src/Lean/Meta/Tactic/Simp/Diagnostics.lean index ad19383bb1..766c8b8fc2 100644 --- a/src/Lean/Meta/Tactic/Simp/Diagnostics.lean +++ b/src/Lean/Meta/Tactic/Simp/Diagnostics.lean @@ -36,6 +36,7 @@ def reportDiag (diag : Simp.Diagnostics) (diagOrig : Meta.Diagnostics) : MetaM U if (← isDiagnosticsEnabled) then let used ← mkSimpDiagSummary diag.usedThmCounter let tried ← mkSimpDiagSummary diag.triedThmCounter diag.usedThmCounter + let congr ← mkDiagSummary diag.congrThmCounter let unfoldCounter := subCounters (← get).diag.unfoldCounter diagOrig.unfoldCounter let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true) @@ -44,6 +45,7 @@ def reportDiag (diag : Simp.Diagnostics) (diagOrig : Meta.Diagnostics) : MetaM U let m := MessageData.nil let m := appendSection m `simp "used theorems" used let m := appendSection m `simp "tried theorems" tried + let m := appendSection m `simp "tried congruence theorems" congr let m := appendSection m `reduction "unfolded declarations" unfoldDefault let m := appendSection m `reduction "unfolded instances" unfoldInstance let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index a651d882a5..8ee496f282 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -520,6 +520,7 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do /-- Try to rewrite `e` children using the given congruence theorem -/ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do + recordCongrTheorem c.theoremName trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}" let thm ← mkConstWithFreshMVarLevels c.theoremName let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm) diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index f9c2a5a4de..b1325fd54b 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -90,6 +90,7 @@ structure Context where -/ parent? : Option Expr := none dischargeDepth : UInt32 := 0 + deriving Inhabited def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool := @@ -103,6 +104,8 @@ structure Diagnostics where usedThmCounter : PHashMap Origin Nat := {} /-- Number of times each simp theorem has been tried. -/ triedThmCounter : PHashMap Origin Nat := {} + /-- Number of times each congr theorem has been tried. -/ + congrThmCounter : PHashMap Name Nat := {} deriving Inhabited structure State where @@ -308,14 +311,14 @@ Save current cache, reset it, execute `x`, and then restore original cache. withFreshCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do - modifyDiag fun { usedThmCounter, triedThmCounter } => + modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } => let cNew := if let some c := triedThmCounter.find? thmId then c + 1 else 1 - { usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew } + { usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew, congrThmCounter } def recordSimpTheorem (thmId : Origin) : SimpM Unit := do - modifyDiag fun { usedThmCounter, triedThmCounter } => + modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } => let cNew := if let some c := usedThmCounter.find? thmId then c + 1 else 1 - { usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter } + { usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter, congrThmCounter } /- If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead. See issue #3547. @@ -335,6 +338,11 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit := do let n := s.usedTheorems.size { s with usedTheorems := s.usedTheorems.insert thmId n } +def recordCongrTheorem (declName : Name) : SimpM Unit := do + modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } => + let cNew := if let some c := congrThmCounter.find? declName then c + 1 else 1 + { congrThmCounter := congrThmCounter.insert declName cNew, triedThmCounter, usedThmCounter } + def Result.getProof (r : Result) : MetaM Expr := do match r.proof? with | some p => return p