-
Notifications
You must be signed in to change notification settings - Fork 334
/
StateRef.lean
61 lines (45 loc) · 2.47 KB
/
StateRef.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
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
The State monad transformer using IO references.
-/
prelude
import Init.System.IO
import Init.Control.State
def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
/- Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/
@[inline] def StateRefT'.run {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m (α × σ) := do
let ref ← ST.mkRef s
let a ← x ref
let s ← ref.get
pure (a, s)
@[inline] def StateRefT'.run' {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m α := do
let (a, _) ← x.run s
pure a
namespace StateRefT'
variable {ω σ : Type} {m : Type → Type} {α : Type}
@[inline] protected def lift (x : m α) : StateRefT' ω σ m α :=
fun _ => x
instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩
instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
instance [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))
@[inline] protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
fun ref => ref.get
@[inline] protected def set [Monad m] [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
fun ref => ref.set s
@[inline] protected def modifyGet [Monad m] [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
fun ref => ref.modifyGet f
instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) where
get := StateRefT'.get
set := StateRefT'.set
modifyGet := StateRefT'.modifyGet
instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateRefT' ω σ m) where
throw := StateRefT'.lift ∘ throwThe ε
tryCatch := fun x c s => tryCatchThe ε (x s) (fun e => c e s)
end StateRefT'
instance (ω σ : Type) (m : Type → Type) : MonadControl m (StateRefT' ω σ m) :=
inferInstanceAs (MonadControl m (ReaderT _ _))
instance {m : Type → Type} {ω σ : Type} [MonadFinally m] [Monad m] : MonadFinally (StateRefT' ω σ m) :=
inferInstanceAs (MonadFinally (ReaderT _ _))