0 | module Control.RIO.State
 1 |
 2 | import Data.IORef
 3 |
 4 | %default total
 5 |
 6 | --------------------------------------------------------------------------------
 7 | --          Reader
 8 | --------------------------------------------------------------------------------
 9 |
10 | ||| Effectful getter, yielding values of type `a` and tagged
11 | ||| with label `lbl`.
12 | public export
13 | data Read : (lbl : l) -> (a : Type) -> Type where
14 |   [search lbl]
15 |   MkRead :  (read_  : IO a) -> Read lbl a
16 |
17 | ||| Read the current value of a getter.
18 | export %inline
19 | readAt : (0 lbl : l) -> {auto r : Read lbl a} -> HasIO io => io a
20 | readAt _ @{MkRead g} = liftIO g
21 |
22 | namespace Read
23 |
24 |   ||| Read the current value of a getter.
25 |   |||
26 |   ||| Use this if you experience slowdowns with `readAt` durcing compilation.
27 |   export %inline
28 |   (.read) : HasIO io => Read lbl a -> io a
29 |   (.read) (MkRead r) = liftIO r
30 |
31 | --------------------------------------------------------------------------------
32 | --          State
33 | --------------------------------------------------------------------------------
34 |
35 | ||| Mutable state holding values of type `a` and tagged
36 | ||| with label `lbl`.
37 | public export
38 | data ST : (lbl : l) -> (a : Type) -> Type where
39 |   [search lbl]
40 |   MkST :
41 |        (read_  : IO a)
42 |     -> (write_ : a -> IO ())
43 |     -> (mod_   : (a -> a) -> IO ())
44 |     -> ST lbl a
45 |
46 | export
47 | mkST : HasIO io => a -> io (ST lbl a)
48 | mkST v = do
49 |   ref <- newIORef v
50 |   pure $ MkST (readIORef ref) (writeIORef ref) (modifyIORef ref)
51 |
52 | export %hint %inline
53 | stToRead : ST lbl a => Read lbl a
54 | stToRead @{MkST r _ _} = MkRead r
55 |
56 | ||| Viewing a mutable state through a getter and a setter.
57 | export
58 | mapST : (a -> b) -> (b -> a -> a) -> ST lbl a -> ST lbl2 b
59 | mapST f g (MkST r w m) =
60 |   MkST (map f r) (\v => m (g v)) (\h => m (\va => g (h $ f va) va))
61 |
62 | ||| Modify the value stored in a mutable reference.
63 | export %inline
64 | modifyAt : (0 lbl : l) -> {auto st : ST lbl a} -> HasIO io => (a -> a) -> io ()
65 | modifyAt _ @{MkST _ _ m} f = liftIO (m f)
66 |
67 | ||| Write a value to a mutable reference.
68 | export %inline
69 | getAt : (0 lbl : l) -> {auto set : ST lbl a} -> HasIO io => io a
70 | getAt _ @{MkST r _ _} = liftIO r
71 |
72 | ||| Write a value to a mutable reference.
73 | export %inline
74 | setAt : (0 lbl : l) -> {auto set : ST lbl a} -> HasIO io => a -> io ()
75 | setAt _ @{MkST _ w _} v = liftIO (w v)
76 |
77 | ||| Read the current value of some mutable state.
78 | |||
79 | ||| Use this if you experience slowdowns with `getAt` durcing compilation.
80 | export %inline
81 | (.get) : HasIO io => ST lbl a -> io a
82 | (.get) (MkST r _ _) = liftIO r
83 |
84 | ||| Overwrite the current value of some mutable state.
85 | |||
86 | ||| Use this if you experience slowdowns with `setAt` durcing compilation.
87 | export %inline
88 | (.set) : HasIO io => ST lbl a -> a -> io ()
89 | (.set) (MkST _ w _) v = liftIO $ w v
90 |
91 | ||| Modify the current value of some mutable state.
92 | |||
93 | ||| Use this if you experience slowdowns with `setAt` durcing compilation.
94 | export %inline
95 | (.mod) : HasIO io => ST lbl a -> (a -> a) -> io ()
96 | (.mod) (MkST _ _ m) f = liftIO $ m f
97 |