From f0232aeb5d8a1d6d88c0995a81048d0caea30ad2 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Tue, 21 Jan 2025 13:04:40 +0000 Subject: [PATCH] feat: set priority in monadic class instances --- doc/examples/widgets.lean | 2 +- src/Init/Control/Except.lean | 2 +- src/Init/Control/ExceptCps.lean | 2 +- src/Init/Control/Option.lean | 2 +- src/Init/Control/State.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 | 4 ++-- src/lake/Lake/Util/EStateT.lean | 4 ++-- tests/lean/run/catchThe.lean | 4 ++-- 11 files changed, 23 insertions(+), 22 deletions(-) diff --git a/doc/examples/widgets.lean b/doc/examples/widgets.lean index 506dca51a3ff..fa3f6a8b59bc 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 => throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩ Widget.ppExprTagged c.type /-! diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 961e2a99fa2f..6ab7ed0e6807 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 db30a57ef487..a810945b90af 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/Control/Option.lean b/src/Init/Control/Option.lean index 1df47eda77f6..5decf1a34b4b 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -63,7 +63,7 @@ instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩ let some a ← x | handle () pure a -instance : MonadExceptOf Unit (OptionT m) where +instance (priority := low) : MonadExceptOf Unit (OptionT m) where throw := fun _ => OptionT.fail tryCatch := OptionT.tryCatch diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean index c3e6e60b3066..2543519be7d2 100644 --- a/src/Init/Control/State.lean +++ b/src/Init/Control/State.lean @@ -113,7 +113,7 @@ def ForM.forIn [Monad m] [ForM (StateT β (ExceptT β m)) ρ α] section variable {σ : Type u} {m : Type u → Type v} -instance [Monad m] : MonadStateOf σ (StateT σ m) where +instance (priority := high) [Monad m] : MonadStateOf σ (StateT σ m) where get := StateT.get set := StateT.set modifyGet := StateT.modifyGet diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 040bb5bbf7a4..48ae9a35e799 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2997,7 +2997,8 @@ variable {ε : Type u} {m : Type v → Type w} @[inline] protected def orElse [MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : Unit → m α) : m α := tryCatch t₁ fun _ => t₂ () -instance [MonadExcept ε m] {α : Type v} : OrElse (m α) where +/- (priority := low) -/ +instance (priority := 100) [MonadExcept ε m] {α : Type v} : OrElse (m α) where orElse := MonadExcept.orElse end MonadExcept @@ -3027,7 +3028,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] @@ -3123,7 +3124,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 /-- @@ -3160,7 +3162,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) /-- @@ -3246,8 +3249,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 diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 9a3d2665b971..d2431a8fae76 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 @@ -346,9 +346,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 be32f60c7da0..3dc13642492d 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 9f308244186a..be81b2b1774a 100644 --- a/src/lake/Lake/Util/Cycle.lean +++ b/src/lake/Lake/Util/Cycle.lean @@ -58,14 +58,14 @@ 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 /-- A transformer that equips a monad with a `CallStack` to detect cycles. -/ abbrev CycleT κ m := CallStackT κ <| ExceptT (Cycle κ) m -instance [Monad m] : MonadCycleOf κ (CycleT κ m) where +instance (priority := high) [Monad m] : MonadCycleOf κ (CycleT κ m) where throwCycle := throw /-- diff --git a/src/lake/Lake/Util/EStateT.lean b/src/lake/Lake/Util/EStateT.lean index 5fcf982b4c65..c21ce7ed97bc 100644 --- a/src/lake/Lake/Util/EStateT.lean +++ b/src/lake/Lake/Util/EStateT.lean @@ -185,7 +185,7 @@ protected def get [Pure m] : EStateT ε σ m σ := fun s => protected def modifyGet [Pure m] (f : σ → Prod α σ) : EStateT ε σ m α := fun s => match f s with | (a, s) => pure <| .ok a s -instance [Pure m] : MonadStateOf σ (EStateT ε σ m) where +instance (priority := high) [Pure m] : MonadStateOf σ (EStateT ε σ m) where set := EStateT.set get := EStateT.get modifyGet := EStateT.modifyGet @@ -201,7 +201,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 4e6376af0406..2f2525d33ef9 100644 --- a/tests/lean/run/catchThe.lean +++ b/tests/lean/run/catchThe.lean @@ -14,7 +14,7 @@ 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 @@ -25,7 +25,7 @@ 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