Init.Control.Except

source

@[inline]

def Except.pure {ε : Type u} {α : Type u_1} (a : α) :

Except ε α

Equations

Except.pure a = Except.ok a

source

@[inline]

def Except.map {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) :

Except ε α → Except ε β

Equations

Except.map f _fun_discr = match _fun_discr with | Except.error err => Except.error err | Except.ok v => Except.ok (f v)

source

@[simp]

theorem Except.map_id {ε : Type u} {α : Type u_1} :

Except.map id = id

source

@[inline]

def Except.mapError {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : ε → ε') :

Except ε α → Except ε' α

Equations

Except.mapError f _fun_discr = match _fun_discr with | Except.error err => Except.error (f err) | Except.ok v => Except.ok v

source

@[inline]

def Except.bind {ε : Type u} {α : Type u_1} {β : Type u_2} (ma : Except ε α) (f : α → Except ε β) :

Except ε β

Equations

Except.bind ma f = match ma with | Except.error err => Except.error err | Except.ok v => f v

source

@[inline]

def Except.toBool {ε : Type u} {α : Type u_1} :

Except ε α → Bool

Equations

Except.toBool _fun_discr = match _fun_discr with | Except.ok a => true | Except.error a => false

source

@[inline]

def Except.toOption {ε : Type u} {α : Type u_1} :

Except ε α → Option α

Equations

Except.toOption _fun_discr = match _fun_discr with | Except.ok a => some a | Except.error a => none

source

@[inline]

def Except.tryCatch {ε : Type u} {α : Type u_1} (ma : Except ε α) (handle : ε → Except ε α) :

Except ε α

Equations

Except.tryCatch ma handle = match ma with | Except.ok a => Except.ok a | Except.error e => handle e

source

def Except.orElseLazy {ε : Type u} {α : Type u_1} (x : Except ε α) (y : Unit → Except ε α) :

Except ε α

Equations

Except.orElseLazy x y = match x with | Except.ok a => Except.ok a | Except.error a => y ()

source

instance Except.instMonadExcept {ε : Type u} :

Monad (Except ε)

Equations

Except.instMonadExcept = Monad.mk

source

def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) :

Type v

Equations

ExceptT ε m α = m (Except ε α)

source

@[inline]

def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) :

ExceptT ε m α

Equations

ExceptT.mk x = x

source

@[inline]

def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) :

m (Except ε α)

Equations

ExceptT.run x = x

source

@[inline]

def ExceptT.pure {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (a : α) :

ExceptT ε m α

Equations

ExceptT.pure a = ExceptT.mk (pure (Except.ok a))

source

@[inline]

def ExceptT.bindCont {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} {β : Type u} (f : α → ExceptT ε m β) :

Except ε α → m (Except ε β)

Equations

ExceptT.bindCont f _fun_discr = match _fun_discr with | Except.ok a => f a | Except.error e => pure (Except.error e)

source

@[inline]

def ExceptT.bind {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} {β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) :

ExceptT ε m β

Equations

ExceptT.bind ma f = ExceptT.mk (ma >>= ExceptT.bindCont f)

source

@[inline]

def ExceptT.map {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} {β : Type u} (f : α → β) (x : ExceptT ε m α) :

ExceptT ε m β

Equations

ExceptT.map f x = ExceptT.mk do let a ← x match a with | Except.ok a => pure (Except.ok (f a)) | Except.error e => pure (Except.error e)

source

@[inline]

def ExceptT.lift {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (t : m α) :

ExceptT ε m α

Equations

ExceptT.lift t = ExceptT.mk (Except.ok <$> t)

source

instance ExceptT.instMonadLiftExceptExceptT {ε : Type u} {m : Type u → Type v} [inst : Monad m] :

MonadLift (Except ε) (ExceptT ε m)

Equations

ExceptT.instMonadLiftExceptExceptT = { monadLift := fun {α} e => ExceptT.mk (pure e) }

source

instance ExceptT.instMonadLiftExceptT {ε : Type u} {m : Type u → Type v} [inst : Monad m] :

MonadLift m (ExceptT ε m)

Equations

ExceptT.instMonadLiftExceptT = { monadLift := fun {α} => ExceptT.lift }

source

@[inline]

def ExceptT.tryCatch {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) :

ExceptT ε m α

Equations

ExceptT.tryCatch ma handle = ExceptT.mk do let res ← ma match res with | Except.ok a => pure (Except.ok a) | Except.error e => handle e

source

instance ExceptT.instMonadFunctorExceptT {ε : Type u} {m : Type u → Type v} :

MonadFunctor m (ExceptT ε m)

Equations

ExceptT.instMonadFunctorExceptT = { monadMap := fun {α} f x => f (Except ε α) x }

source

instance ExceptT.instMonadExceptT {ε : Type u} {m : Type u → Type v} [inst : Monad m] :

Monad (ExceptT ε m)

Equations

ExceptT.instMonadExceptT = Monad.mk

source

@[inline]

def ExceptT.adapt {ε : Type u} {m : Type u → Type v} [inst : Monad m] {ε' : Type u} {α : Type u} (f : ε → ε') :

ExceptT ε m α → ExceptT ε' m α

Equations

ExceptT.adapt f x = ExceptT.mk (Except.mapError f <$> x)

source

instance instMonadExceptOfExceptT (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [inst : Monad m] [inst : MonadExceptOf ε₁ m] :

MonadExceptOf ε₁ (ExceptT ε₂ m)

Equations

instMonadExceptOfExceptT m ε₁ ε₂ = { throw := fun {α} e => ExceptT.mk (throwThe ε₁ e), tryCatch := fun {α} x handle => ExceptT.mk (tryCatchThe ε₁ x handle) }

source

instance instMonadExceptOfExceptT_1 (m : Type u → Type v) (ε : Type u) [inst : Monad m] :

MonadExceptOf ε (ExceptT ε m)

Equations

instMonadExceptOfExceptT_1 m ε = { throw := fun {α} e => ExceptT.mk (pure (Except.error e)), tryCatch := fun {α} => ExceptT.tryCatch }

source

instance instInhabitedExceptT {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} [inst : Monad m] [inst : Inhabited ε] :

Inhabited (ExceptT ε m α)

Equations

instInhabitedExceptT = { default := throw default }

source

instance instMonadExceptOfExcept (ε : Type u_1) :

MonadExceptOf ε (Except ε)

Equations

instMonadExceptOfExcept ε = { throw := fun {α} => Except.error, tryCatch := fun {α} => Except.tryCatch }

source

@[inline]

def MonadExcept.orelse' {ε : Type u} {m : Type v → Type w} [inst : MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : m α) (useFirstEx : optParam Bool true) :

m α

Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard orelse uses the second.

Equations

MonadExcept.orelse' t₁ t₂ useFirstEx = tryCatch t₁ fun e₁ => tryCatch t₂ fun e₂ => throw (if useFirstEx = true then e₁ else e₂)

source

@[inline]

def observing {ε : Type u} {α : Type u} {m : Type u → Type v} [inst : Monad m] [inst : MonadExcept ε m] (x : m α) :

m (Except ε α)

Equations

observing x = tryCatch (do let a ← x pure (Except.ok a)) fun ex => pure (Except.error ex)

source

def liftExcept {ε : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} [inst : MonadExceptOf ε m] [inst : Pure m] :

Except ε α → m α

Equations

liftExcept _fun_discr = match _fun_discr with | Except.ok a => pure a | Except.error e => throw e

source

instance instMonadControlExceptT (ε : Type u) (m : Type u → Type v) [inst : Monad m] :

MonadControl m (ExceptT ε m)

Equations

instMonadControlExceptT ε m = { stM := Except ε, liftWith := fun {α} f => liftM (f fun {β} x => ExceptT.run x), restoreM := fun {α} x => x }

source

class MonadFinally (m : Type u → Type v) :

Type (max (u + 1) v)

tryFinally' x f runs x and then the "finally" computation f. When x succeeds with a : α, f (some a) is returned. If x fails for m's definition of failure, f none is returned. Hence tryFinally' can be thought of as performing the same role as a finally block in an imperative programming language.
tryFinally' : {α β : Type u} → m α → (Option α → m β) → m (α × β)

Instances

source

@[inline]

def tryFinally {m : Type u → Type v} {α : Type u} {β : Type u} [inst : MonadFinally m] [inst : Functor m] (x : m α) (finalizer : m β) :

m α

Execute x and then execute finalizer even if x threw an exception

Equations

tryFinally x finalizer = let y := tryFinally' x fun x => finalizer; (fun a => a.fst) <$> y

source

instance Id.finally:

MonadFinally Id

Equations

Id.finally = { tryFinally' := fun {α β} x h => let a := x; let b := h (some x); pure (a, b) }

source

instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [inst : MonadFinally m] [inst : Monad m] :

MonadFinally (ExceptT ε m)

Equations

One or more equations did not get rendered due to their size.