From ea23ab6fef31d59773c54132b0dfb9b66d10d73c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 22 Apr 2024 08:55:41 +0200 Subject: [PATCH] refactor: make throwTacticEx parameter `msg` optional (#3951) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit previously, the empty `MessageData` (`m!""`) was used to indicate “no message”, and `throwTacticEx` would format the message differently then. But the semantics of `MessageData.isEmpty` isn't entirely clear in the presence of lazy message data (e.g. `.ofPPFormat`). So to avoid wondering what `isEmpty` should do there, let's simply use an optional argument to `throwTacticEx` and get rid of `MessageData.isEmpty`. --- src/Lean/Elab/Tactic/Split.lean | 6 +++--- src/Lean/Message.lean | 11 ----------- src/Lean/Meta/Tactic/Assumption.lean | 2 +- src/Lean/Meta/Tactic/Contradiction.lean | 2 +- src/Lean/Meta/Tactic/Refl.lean | 2 +- src/Lean/Meta/Tactic/Util.lean | 9 ++++----- 6 files changed, 10 insertions(+), 22 deletions(-) diff --git a/src/Lean/Elab/Tactic/Split.lean b/src/Lean/Elab/Tactic/Split.lean index e01aa81bbc..fd27465d4c 100644 --- a/src/Lean/Elab/Tactic/Split.lean +++ b/src/Lean/Elab/Tactic/Split.lean @@ -21,12 +21,12 @@ open Meta throwErrorAt stx[2] "'split' tactic failed, select a single target to split" if simplifyTarget then liftMetaTactic fun mvarId => do - let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "" + let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId return mvarIds else let fvarId ← getFVarId hyps[0]! liftMetaTactic fun mvarId => do - let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId "" + let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId return mvarIds | Location.wildcard => liftMetaTactic fun mvarId => do @@ -34,7 +34,7 @@ open Meta for fvarId in fvarIds do if let some mvarIds ← splitLocalDecl? mvarId fvarId then return mvarIds - let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "" + let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId return mvarIds end Lean.Elab.Tactic diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index f347b6308c..b65775423c 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -82,17 +82,6 @@ inductive MessageData where namespace MessageData -/-- Determines whether the message contains any content. -/ -def isEmpty : MessageData → Bool - | ofFormat f => f.isEmpty - | withContext _ m => m.isEmpty - | withNamingContext _ m => m.isEmpty - | nest _ m => m.isEmpty - | group m => m.isEmpty - | compose m₁ m₂ => m₁.isEmpty && m₂.isEmpty - | tagged _ m => m.isEmpty - | _ => false - variable (p : Name → Bool) in /-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag` is true. -/ partial def hasTag : MessageData → Bool diff --git a/src/Lean/Meta/Tactic/Assumption.lean b/src/Lean/Meta/Tactic/Assumption.lean index 629ff573cc..e3dd9b2922 100644 --- a/src/Lean/Meta/Tactic/Assumption.lean +++ b/src/Lean/Meta/Tactic/Assumption.lean @@ -33,7 +33,7 @@ def assumptionCore (mvarId : MVarId) : MetaM Bool := /-- Close goal `mvarId` using an assumption. Throw error message if failed. -/ def _root_.Lean.MVarId.assumption (mvarId : MVarId) : MetaM Unit := unless (← mvarId.assumptionCore) do - throwTacticEx `assumption mvarId "" + throwTacticEx `assumption mvarId @[deprecated MVarId.assumption] def assumption (mvarId : MVarId) : MetaM Unit := diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean index a296d92fb8..507dffdb94 100644 --- a/src/Lean/Meta/Tactic/Contradiction.lean +++ b/src/Lean/Meta/Tactic/Contradiction.lean @@ -224,7 +224,7 @@ Throw exception if goal failed to be closed. -/ def _root_.Lean.MVarId.contradiction (mvarId : MVarId) (config : Contradiction.Config := {}) : MetaM Unit := unless (← mvarId.contradictionCore config) do - throwTacticEx `contradiction mvarId "" + throwTacticEx `contradiction mvarId @[deprecated MVarId.contradiction] def contradiction (mvarId : MVarId) (config : Contradiction.Config := {}) : MetaM Unit := diff --git a/src/Lean/Meta/Tactic/Refl.lean b/src/Lean/Meta/Tactic/Refl.lean index 13c61a1881..4bca1e0f58 100644 --- a/src/Lean/Meta/Tactic/Refl.lean +++ b/src/Lean/Meta/Tactic/Refl.lean @@ -67,6 +67,6 @@ Close given goal using `HEq.refl`. def _root_.Lean.MVarId.hrefl (mvarId : MVarId) : MetaM Unit := do mvarId.withContext do let some [] ← observing? do mvarId.apply (mkConst ``HEq.refl [← mkFreshLevelMVar]) - | throwTacticEx `hrefl mvarId "" + | throwTacticEx `hrefl mvarId end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index c95ad6b34f..bc754350c9 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -36,11 +36,10 @@ def appendTagSuffix (mvarId : MVarId) (suffix : Name) : MetaM Unit := do def mkFreshExprSyntheticOpaqueMVar (type : Expr) (tag : Name := Name.anonymous) : MetaM Expr := mkFreshExprMVar type MetavarKind.syntheticOpaque tag -def throwTacticEx (tacticName : Name) (mvarId : MVarId) (msg : MessageData) : MetaM α := - if msg.isEmpty then - throwError "tactic '{tacticName}' failed\n{mvarId}" - else - throwError "tactic '{tacticName}' failed, {msg}\n{mvarId}" +def throwTacticEx (tacticName : Name) (mvarId : MVarId) (msg? : Option MessageData := none) : MetaM α := + match msg? with + | none => throwError "tactic '{tacticName}' failed\n{mvarId}" + | some msg => throwError "tactic '{tacticName}' failed, {msg}\n{mvarId}" def throwNestedTacticEx {α} (tacticName : Name) (ex : Exception) : MetaM α := do throwError "tactic '{tacticName}' failed, nested error:\n{ex.toMessageData}"