From 6dbf937f43f1da8c60467917e2bbfeb3680d3b4f Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Mon, 9 Sep 2024 19:46:26 +0200 Subject: [PATCH] set high priority in monadic class instances --- doc/examples/widgets.lean | 2 +- doc/monads/transformers.lean | 4 ++-- src/Init/Control/Except.lean | 2 +- src/Init/Control/ExceptCps.lean | 2 +- src/Init/Prelude.lean | 13 +++++++------ src/Lean/Elab/Match.lean | 8 ++++---- src/Lean/Elab/PreDefinition/Eqns.lean | 2 +- src/lake/Lake/Util/Cycle.lean | 2 +- src/lake/Lake/Util/EStateT.lean | 2 +- tests/lean/run/catchThe.lean | 8 ++++---- 10 files changed, 23 insertions(+), 22 deletions(-) diff --git a/doc/examples/widgets.lean b/doc/examples/widgets.lean index 8e06c21080e15..75f010f860f9e 100644 --- a/doc/examples/widgets.lean +++ b/doc/examples/widgets.lean @@ -141,7 +141,7 @@ def getType (params : GetTypeParams) : RequestM (RequestTask CodeWithInfos) := runTermElabM snap do let name ← resolveGlobalConstNoOverloadCore params.name let c ← try getConstInfo name - catch _ => throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩ + catch _ : Exception => throw ⟨.invalidParams, s!"no constant named '{name}'"⟩ Widget.ppExprTagged c.type /-! diff --git a/doc/monads/transformers.lean b/doc/monads/transformers.lean index 3e6e907dfeb6a..d81df94aa8ec5 100644 --- a/doc/monads/transformers.lean +++ b/doc/monads/transformers.lean @@ -218,7 +218,7 @@ def liftTest2 (x : Except String Float) : The ReaderT monadLift is even simpler than the one for StateT: ```lean,ignore -instance : MonadLift m (ReaderT ρ m) where +instance : MonadLift m (ReaderT ρ m) where monadLift x := fun _ => x ``` @@ -313,4 +313,4 @@ truly master monads, you should know how to make your own, and there's one final should understand for that. This is the idea of type "laws". Each of the structures you've learned so far has a series of laws associated with it. And for your instances of these classes to make sense, they should follow the laws! Check out [Monad Laws](laws.lean.md). --/ \ No newline at end of file +-/ diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 961e2a99fa2fc..6ab7ed0e68077 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -136,7 +136,7 @@ instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [MonadExceptO tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle @[always_inline] -instance (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) where +instance (priority := high) (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) where throw e := ExceptT.mk <| pure (Except.error e) tryCatch := ExceptT.tryCatch diff --git a/src/Init/Control/ExceptCps.lean b/src/Init/Control/ExceptCps.lean index db30a57ef4876..a810945b90af5 100644 --- a/src/Init/Control/ExceptCps.lean +++ b/src/Init/Control/ExceptCps.lean @@ -36,7 +36,7 @@ instance : Monad (ExceptCpsT ε m) where instance : LawfulMonad (ExceptCpsT σ m) := by refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl -instance : MonadExceptOf ε (ExceptCpsT ε m) where +instance (priority := high) : MonadExceptOf ε (ExceptCpsT ε m) where throw e := fun _ _ k => k e tryCatch x handle := fun _ k₁ k₂ => x _ k₁ (fun e => handle e _ k₁ k₂) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index aa2a25ad5d0ab..7059d6d134cd4 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3016,7 +3016,7 @@ namespace ReaderT section variable {ρ : Type u} {m : Type u → Type v} {α : Type u} -instance : MonadLift m (ReaderT ρ m) where +instance : MonadLift m (ReaderT ρ m) where monadLift x := fun _ => x @[always_inline] @@ -3112,7 +3112,8 @@ instance (ρ : Type u) (m : Type u → Type v) [MonadReaderOf ρ m] : MonadReade instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [MonadReaderOf ρ m] : MonadReaderOf ρ n where read := liftM (m := m) read -instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (ReaderT ρ m) where +/- (priority := high) -/ +instance (priority := 10000) {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (ReaderT ρ m) where read := ReaderT.read /-- @@ -3149,7 +3150,8 @@ instance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadW instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [MonadFunctor m n] [MonadWithReaderOf ρ m] : MonadWithReaderOf ρ n where withReader f := monadMap (m := m) (withTheReader ρ f) -instance {ρ : Type u} {m : Type u → Type v} : MonadWithReaderOf ρ (ReaderT ρ m) where +/- (priority := high) -/ +instance (priority := 10000) {ρ : Type u} {m : Type u → Type v} : MonadWithReaderOf ρ (ReaderT ρ m) where withReader f x := fun ctx => x (f ctx) /-- @@ -3235,8 +3237,6 @@ of the state. It is equivalent to `get <* modify f` but may be more efficient. def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m σ := modifyGet fun s => (s, f s) --- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer --- will be picked first @[always_inline] instance {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [MonadStateOf σ m] : MonadStateOf σ n where get := liftM (m := m) MonadStateOf.get @@ -3373,7 +3373,8 @@ instance : MonadStateOf σ (EStateM ε σ) where get := EStateM.get modifyGet := EStateM.modifyGet -instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) where +/- (priority := high) -/ +instance (priority := 10000) {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) where throw := EStateM.throw tryCatch := EStateM.tryCatch diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index fdbe7a6c6b3a3..2b1e04371df37 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -165,7 +165,7 @@ open Lean.Elab.Term.Quotation in for (pats, rhs) in patss.zip rhss do let vars ← try getPatternsVars pats - catch | _ => return -- can happen in case of pattern antiquotations + catch _ => return -- can happen in case of pattern antiquotations Quotation.withNewLocals (getPatternVarNames vars) <| precheck rhs | _ => throwUnsupportedSyntax @@ -347,9 +347,9 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep | some path => restoreState s -- Wrap the type mismatch exception for the "discriminant refinement" feature. - throwThe PatternElabException { ex := ex, patternIdx := idx, pathToIndex := path } - | none => restoreState s; throw ex - | none => throw ex + throw { ex := ex, patternIdx := idx, pathToIndex := path } + | none => restoreState s; throwThe Exception ex + | none => throwThe Exception ex matchType := b.instantiate1 pattern patterns := patterns.push pattern | _ => throwError "unexpected match type" diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 62350a1556c60..e1f0486db673d 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -222,7 +222,7 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do let args := e.getAppArgs for discr in args[info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do if (← Meta.isConstructorApp discr) then - throwThe Unit () + throw () return (← (find e).run) matches .error _ partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do diff --git a/src/lake/Lake/Util/Cycle.lean b/src/lake/Lake/Util/Cycle.lean index 7187f2a111abe..36e5155538fdb 100644 --- a/src/lake/Lake/Util/Cycle.lean +++ b/src/lake/Lake/Util/Cycle.lean @@ -55,7 +55,7 @@ instance inhabitedOfMonadCycle [MonadCycle κ m] : Inhabited (m α) := ⟨throwC /-- A transformer that equips a monad with a `CallStack`. -/ abbrev CallStackT κ m := ReaderT (CallStack κ) m -instance [Monad m] : MonadCallStackOf κ (CallStackT κ m) where +instance (priority := high) [Monad m] : MonadCallStackOf κ (CallStackT κ m) where getCallStack := read withCallStack s x := x s diff --git a/src/lake/Lake/Util/EStateT.lean b/src/lake/Lake/Util/EStateT.lean index 36bc5eab9498a..31de108de8bd1 100644 --- a/src/lake/Lake/Util/EStateT.lean +++ b/src/lake/Lake/Util/EStateT.lean @@ -199,7 +199,7 @@ protected def tryCatch [Monad m] (x : EStateT ε σ m α) (handle : ε → EStat | .error e s => handle e s | ok => pure ok -instance [Monad m] : MonadExceptOf ε (EStateT ε σ m) where +instance (priority := high) [Monad m] : MonadExceptOf ε (EStateT ε σ m) where throw := EStateT.throw tryCatch := EStateT.tryCatch diff --git a/tests/lean/run/catchThe.lean b/tests/lean/run/catchThe.lean index 7b66206b44f85..5068d1263497c 100644 --- a/tests/lean/run/catchThe.lean +++ b/tests/lean/run/catchThe.lean @@ -14,11 +14,11 @@ def testM {α} [BEq α] [ToString α] (x : M α) (expected : α) : MetaM Unit : | Except.error e => throwError m!"FAILED: {e}" @[noinline] def act1 : M Nat := - throw <| Exception.error Syntax.missing "Error at act1" + throwThe Exception <| Exception.error Syntax.missing "Error at act1" def g1 : M Nat := tryCatchThe Exception - (tryCatchThe String act1 (fun ex => pure 100)) + (tryCatch act1 (fun ex => pure 100)) (fun ex => pure 200) /-- info: -/ @@ -26,11 +26,11 @@ def g1 : M Nat := #eval testM g1 200 @[noinline] def act2 : M Nat := - throwThe String "hello world" + throw "hello world" def g2 : M Nat := tryCatchThe Exception - (tryCatchThe String act2 (fun ex => pure 100)) + (tryCatch act2 (fun ex => pure 100)) (fun ex => pure 200) /-- info: -/