From 6c234daad7664bc6d7364b8ec22fc87e4359ab45 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Aug 2020 09:28:23 -0700 Subject: [PATCH] chore: `MonadExceptCore` => `MonadExceptOf` --- src/Init/Control/EState.lean | 2 +- src/Init/Control/Except.lean | 20 ++++++++++---------- src/Init/Control/Option.lean | 2 +- src/Init/Control/Reader.lean | 2 +- src/Init/Control/State.lean | 2 +- src/Init/System/IO.lean | 4 ++-- 6 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean index 896d15e458..17d000d605 100644 --- a/src/Init/Control/EState.lean +++ b/src/Init/Control/EState.lean @@ -116,7 +116,7 @@ instance {δ} [Backtrackable δ σ] : HasOrelse (EStateM ε σ α) := instance : MonadState σ (EStateM ε σ) := { set := @EStateM.set _ _, get := @EStateM.get _ _, modifyGet := @EStateM.modifyGet _ _ } -instance {δ} [Backtrackable δ σ] : MonadExceptCore ε (EStateM ε σ) := +instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) := { throw := @EStateM.throw _ _, catch := @EStateM.catch _ _ _ _ } @[inline] def adaptState {σ₁ σ₂} (split : σ → σ₁ × σ₂) (merge : σ₁ → σ₂ → σ) (x : EStateM ε σ₁ α) : EStateM ε σ α := diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 3eec7af6e9..bbb0bc9a70 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -126,36 +126,36 @@ fun x => ExceptT.mk $ Except.mapError f <$> x end ExceptT /-- An implementation of [MonadError](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError) -/ -class MonadExceptCore (ε : Type u) (m : Type v → Type w) := +class MonadExceptOf (ε : Type u) (m : Type v → Type w) := (throw {α : Type v} : ε → m α) (catch {α : Type v} : m α → (ε → m α) → m α) -abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadExceptCore ε m] {α : Type v} (e : ε) : m α := -MonadExceptCore.throw e +abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (e : ε) : m α := +MonadExceptOf.throw e -abbrev catchThe (ε : Type u) {m : Type v → Type w} [MonadExceptCore ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α := -MonadExceptCore.catch x handle +abbrev catchThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α := +MonadExceptOf.catch x handle -instance ExceptT.monadExceptParent (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptCore ε₁ m] : MonadExceptCore ε₁ (ExceptT ε₂ m) := +instance ExceptT.monadExceptParent (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) := { throw := fun α e => ExceptT.mk $ throwThe ε₁ e, catch := fun α x handle => ExceptT.mk $ catchThe ε₁ x handle } -instance ExceptT.monadExceptSelf (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptCore ε (ExceptT ε m) := +instance ExceptT.monadExceptSelf (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) := { throw := fun α e => ExceptT.mk $ pure (Except.error e), catch := @ExceptT.catch ε _ _ } -instance (ε) : MonadExceptCore ε (Except ε) := +instance (ε) : MonadExceptOf ε (Except ε) := { throw := fun α => Except.error, catch := @Except.catch _ } -/-- Similar to `MonadExceptCore`, but `ε` is an outParam for convenience -/ +/-- Similar to `MonadExceptOf`, but `ε` is an outParam for convenience -/ class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) := (throw {α : Type v} : ε → m α) (catch {α : Type v} : m α → (ε → m α) → m α) export MonadExcept (throw catch) -instance MonadExceptCore.isMonadExcept (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptCore ε m] : MonadExcept ε m := +instance MonadExceptOf.isMonadExcept (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m := { throw := fun _ e => throwThe ε e, catch := fun _ x handle => catchThe ε x handle } diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index b1d63170ec..3f9cd15715 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -63,7 +63,7 @@ namespace OptionT (do { some a ← ma | (handle ()); pure a } : m (Option α)) - instance : MonadExceptCore Unit (OptionT m) := + instance : MonadExceptOf Unit (OptionT m) := { throw := fun _ _ => OptionT.fail, catch := @OptionT.catch _ _ } instance (m out) [MonadRun out m] : MonadRun (fun α => out (Option α)) (OptionT m) := diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean index a8c8021d69..f1650bf165 100644 --- a/src/Init/Control/Reader.lean +++ b/src/Init/Control/Reader.lean @@ -64,7 +64,7 @@ instance [Alternative m] : Alternative (ReaderT ρ m) := failure := @ReaderT.failure _ _ _ _, orelse := @ReaderT.orelse _ _ _ _ } -instance (ε) [Monad m] [MonadExceptCore ε m] : MonadExceptCore ε (ReaderT ρ m) := +instance (ε) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) := { throw := fun α => ReaderT.lift ∘ throwThe ε, catch := fun α x c r => catchThe ε (x r) (fun e => (c e) r) } diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean index 97f8be57cb..b80f0b2cf3 100644 --- a/src/Init/Control/State.lean +++ b/src/Init/Control/State.lean @@ -80,7 +80,7 @@ fun st => do (a, st') ← x st; pure (a, join st' ctx) -instance (ε) [MonadExceptCore ε m] : MonadExceptCore ε (StateT σ m) := +instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := { throw := fun α => StateT.lift ∘ throwThe ε, catch := fun α x c s => catchThe ε (x s) (fun e => c e s) } diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 2cfa222249..2a8fa09483 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -35,7 +35,7 @@ fun s => match x s with | EStateM.Result.error ex s => h ex s instance (ε : Type) : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld)) -instance (ε : Type) : MonadExceptCore ε (EIO ε) := inferInstanceAs (MonadExceptCore ε (EStateM ε IO.RealWorld)) +instance (ε : Type) : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EStateM ε IO.RealWorld)) instance (α ε : Type) : HasOrelse (EIO ε α) := ⟨MonadExcept.orelse⟩ instance {ε : Type} {α : Type} [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α)) @@ -68,7 +68,7 @@ constant allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α := arbitra @[extern "lean_io_initializing"] constant IO.initializing : IO Bool := arbitrary _ -class MonadIO (m : Type → Type) extends HasMonadLiftT IO m, MonadExceptCore IO.Error m +class MonadIO (m : Type → Type) extends HasMonadLiftT IO m, MonadExceptOf IO.Error m instance : MonadIO IO := {}