0 | module Control.Eff.State
 1 |
 2 | import Control.Eff.Internal
 3 |
 4 | %default total
 5 |
 6 | public export
 7 | data StateL : (lbl : k) -> (s : Type) -> (a : Type) -> Type where
 8 |   [search lbl]
 9 |   Get : StateL lbl s s
10 |   Put : (vs : s) -> StateL lbl s ()
11 |
12 | public export
13 | State : (s,a : Type) -> Type
14 | State = StateL ()
15 |
16 | export
17 | getAt : (0 lbl : k) -> Has (StateL lbl s) fs => Eff fs s
18 | getAt lbl = send $ Get {lbl}
19 |
20 | export %inline
21 | get : Has (State s) fs => Eff fs s
22 | get = getAt ()
23 |
24 | export
25 | putAt : (0 lbl : k) -> Has (StateL lbl s) fs => s -> Eff fs ()
26 | putAt lbl vs = send $ Put {lbl} vs
27 |
28 | export %inline
29 | put : Has (State s) fs => s -> Eff fs ()
30 | put = putAt ()
31 |
32 | export
33 | modifyAt : (0 lbl : k) -> Has (StateL lbl s) fs => (s -> s) -> Eff fs ()
34 | modifyAt lbl f = getAt lbl >>= putAt lbl . f
35 |
36 | export %inline
37 | modify : Has (State s) fs => (s -> s) -> Eff fs ()
38 | modify = modifyAt ()
39 |
40 | --------------------------------------------------------------------------------
41 | --          Running State
42 | --------------------------------------------------------------------------------
43 |
44 | export
45 | handleState :
46 |      {0 m : Type -> Type}
47 |   -> (get : m s)
48 |   -> (put : s -> m ())
49 |   -> StateL lbl s a
50 |   -> m a
51 | handleState get _   Get      = get
52 | handleState _   put (Put vs) = put vs
53 |
54 | unState : s -> StateL lbl s a -> (a,s)
55 | unState vs Get     = (vs,vs)
56 | unState _ (Put s2) = ((),s2)
57 |
58 | export
59 | runStateAt :
60 |      (0 lbl : k)
61 |   -> {auto _ : Has (StateL lbl s) fs}
62 |   -> s
63 |   -> Eff fs t
64 |   -> Eff (fs - StateL lbl s) (t,s)
65 | runStateAt _ vs =
66 |   handleRelayS vs (\x,y => pure (y,x)) $ \vs2,st,f =>
67 |     let (vv,vs3) := unState vs2 st
68 |      in f vs3 vv
69 |
70 | export %inline
71 | runState : Has (State s) fs => s -> Eff fs t -> Eff (fs - State s) (t,s)
72 | runState = runStateAt ()
73 |