0 | module Data.IORef
 1 |
 2 | import System.Concurrency
 3 | import System.Info
 4 |
 5 | %default total
 6 |
 7 | -- Implemented externally
 8 | -- e.g., in Scheme, passed around as a box
 9 | data Mut : Type -> Type where [external]
10 |
11 | %extern prim__newIORef : forall a . a -> (1 x : %World) -> IORes (Mut a)
12 | %extern prim__readIORef : forall a . Mut a -> (1 x : %World) -> IORes a
13 | %extern prim__writeIORef : forall a . Mut a -> (1 val : a) -> (1 x : %World) -> IORes ()
14 |
15 | export
16 | data IORef : Type -> Type where
17 |      MkRef : Mut a -> IORef a
18 |
19 | ||| Create a new IORef.
20 | export
21 | newIORef : HasIO io => a -> io (IORef a)
22 | newIORef val
23 |     = do m <- primIO (prim__newIORef val)
24 |          pure (MkRef m)
25 |
26 | ||| Read the value of an IORef.
27 | %inline
28 | export
29 | readIORef : HasIO io => IORef a -> io a
30 | readIORef (MkRef m) = primIO (prim__readIORef m)
31 |
32 | ||| Write a new value into an IORef.
33 | ||| This function does not create a memory barrier and can be reordered with other independent reads and writes within a thread,
34 | ||| which may cause issues for multithreaded execution.
35 | %inline
36 | export
37 | writeIORef : HasIO io => IORef a -> (val : a) -> io ()
38 | writeIORef (MkRef m) val = primIO (prim__writeIORef m val)
39 |
40 | ||| Write a new value into an IORef.
41 | ||| This function does not create a memory barrier and can be reordered with other independent reads and writes within a thread,
42 | ||| which may cause issues for multithreaded execution.
43 | %inline
44 | export
45 | writeIORef1 : HasLinearIO io => IORef a -> (1 val : a) -> io ()
46 | writeIORef1 (MkRef m) val = primIO1 (prim__writeIORef m val)
47 |
48 | ||| Mutate the contents of an IORef, combining readIORef and writeIORef.
49 | ||| This is not an atomic update, consider using atomically when operating in a multithreaded environment.
50 | export
51 | modifyIORef : HasIO io => IORef a -> (a -> a) -> io ()
52 | modifyIORef ref f
53 |     = do val <- readIORef ref
54 |          writeIORef ref (f val)
55 |
56 | ||| This function atomically runs its argument according to the provided mutex.
57 | ||| It can for instance be used to modify the contents of an IORef `ref` with a function `f`
58 | ||| in a safe way in a multithreaded program by using `atomically lock (modifyIORef ref f)`
59 | ||| provided that other threads also rely on the same `lock` to modify `ref`.
60 | export
61 | atomically : HasIO io => Mutex -> io () -> io ()
62 | atomically lock act
63 |     = do mutexAcquire lock
64 |          act
65 |          mutexRelease lock
66 |