max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add missing OptionT instance

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-31 16:37:18 -07:00
parent 4062dee864
commit 97ac231138
1 changed files with 16 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/Init/Control/Option.lean
View file

@ -21,47 +21,51 @@ def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
namespace OptionT
variable {m : Type u → Type v} [Monad m] {α β : Type u}
@[inline] protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := id (α := m (Option β)) do
protected def mk (x : m (Option α)) : OptionT m α :=
x
@[inline] protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := OptionT.mk do
match (← x) with
| some a => f a
| none => pure none
@[inline] protected def pure (a : α) : OptionT m α := id (α := m (Option α)) do
@[inline] protected def pure (a : α) : OptionT m α := OptionT.mk do
pure (some a)
instance : Monad (OptionT m) := {
instance : Monad (OptionT m) where
pure := OptionT.pure
bind := OptionT.bind
}
@[inline] protected def orElse (x : OptionT m α) (y : OptionT m α) : OptionT m α := id (α := m (Option α)) do
@[inline] protected def orElse (x : OptionT m α) (y : OptionT m α) : OptionT m α := OptionT.mk do
match (← x) with
| some a => pure (some a)
| _ => y
@[inline] protected def fail : OptionT m α := id (α := m (Option α)) do
@[inline] protected def fail : OptionT m α := OptionT.mk do
pure none
instance : Alternative (OptionT m) := {
instance : Alternative (OptionT m) where
failure := OptionT.fail
orElse := OptionT.orElse
}
@[inline] protected def lift (x : m α) : OptionT m α := id (α := m (Option α)) do
@[inline] protected def lift (x : m α) : OptionT m α := OptionT.mk do
return some (← x)
instance : MonadLift m (OptionT m) := ⟨OptionT.lift⟩
instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
@[inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := id (α := m (Option α)) do
@[inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := OptionT.mk do
let some a ← x | handle ()
pure a
instance : MonadExceptOf Unit (OptionT m) := {
instance : MonadExceptOf Unit (OptionT m) where
throw := fun _ => OptionT.fail
tryCatch := OptionT.tryCatch
}
instance (ε : Type u) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
throw e := OptionT.mk <| throwThe ε e
tryCatch x handle := OptionT.mk <| tryCatchThe ε x handle
end OptionT