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 -> 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 | ||| Mutate the contents of an IORef, combining readIORef and writeIORef.
41 | ||| This is not an atomic update, consider using atomically when operating in a multithreaded environment.
42 | export
43 | modifyIORef : HasIO io => IORef a -> (a -> a) -> io ()
44 | modifyIORef ref f
45 |     = do val <- readIORef ref
46 |          writeIORef ref (f val)
47 |
48 | ||| This function atomically runs its argument according to the provided mutex.
49 | ||| It can for instance be used to modify the contents of an IORef `ref` with a function `f`
50 | ||| in a safe way in a multithreaded program by using `atomically lock (modifyIORef ref f)`
51 | ||| provided that other threads also rely on the same `lock` to modify `ref`.
52 | export
53 | atomically : HasIO io => Mutex -> io () -> io ()
54 | atomically lock act
55 |     = do mutexAcquire lock
56 |          act
57 |          mutexRelease lock
58 |