-
Notifications
You must be signed in to change notification settings - Fork 642
/
Copy pathIORef.idr
59 lines (50 loc) · 1.6 KB
/
IORef.idr
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
module Data.IORef
||| A mutable variable in the IO monad.
export
data IORef a = MkIORef a
public export
interface HasReference (ffi : FFI) where
newIORef' : a -> IO' ffi (IORef a)
readIORef' : IORef a -> IO' ffi a
writeIORef' : IORef a -> a -> IO' ffi ()
export
modifyIORef': HasReference ffi => IORef a -> (a -> a) -> IO' ffi ()
modifyIORef' ref fn =
do
val <- readIORef' ref
writeIORef' ref (fn val)
export
implementation HasReference FFI_C where
newIORef' val
= do MkRaw ref <- foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)
pure (MkIORef ref)
readIORef' (MkIORef ref)
= do MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) (MkRaw ref)
pure val
writeIORef' (MkIORef ref) val
= foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())
(MkRaw ref) (MkRaw val)
export
implementation HasReference FFI_JS where
newIORef' val =
(MkIORef . believe_me) <$> foreign FFI_JS "{val: %0}" (Ptr -> JS_IO Ptr) (believe_me val)
readIORef' (MkIORef ref) =
believe_me <$> foreign FFI_JS "%0.val" (Ptr -> JS_IO Ptr) (believe_me ref)
writeIORef' (MkIORef ref) val =
foreign FFI_JS "%0.val = %1" (Ptr -> Ptr -> JS_IO ()) (believe_me ref) (believe_me val)
||| Build a new IORef
export
newIORef : a -> IO (IORef a)
newIORef = newIORef'
||| read the value of an IORef
export
readIORef : IORef a -> IO a
readIORef = readIORef'
||| write the value of an IORef
export
writeIORef : IORef a -> a -> IO ()
writeIORef = writeIORef'
||| mutate the contents of an IORef
export
modifyIORef : IORef a -> (a -> a) -> IO ()
modifyIORef = modifyIORef'