-
Notifications
You must be signed in to change notification settings - Fork 350
/
Option.lean
80 lines (58 loc) · 2.25 KB
/
Option.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Init.Data.Option.Basic
import Init.Control.Basic
import Init.Control.Except
universe u v
instance {α} : ToBool (Option α) := ⟨Option.toBool⟩
def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
m (Option α)
@[inline] def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) : m (Option α) :=
x
namespace OptionT
variable {m : Type u → Type v} [Monad m] {α β : Type u}
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 α := OptionT.mk do
pure (some a)
instance : Monad (OptionT m) where
pure := OptionT.pure
bind := OptionT.bind
@[inline] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
match (← x) with
| some a => pure (some a)
| _ => y ()
@[inline] protected def fail : OptionT m α := OptionT.mk do
pure none
instance : Alternative (OptionT m) where
failure := OptionT.fail
orElse := OptionT.orElse
@[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 α := OptionT.mk do
let some a ← x | handle ()
pure a
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
abbrev OptionM (α : Type u) := OptionT Id α
abbrev OptionM.run (x : OptionM α) : Option α :=
x
instance [Monad m] : MonadControl m (OptionT m) where
stM := Option
liftWith f := liftM <| f fun x => x.run
restoreM x := x