git.iko.soy/Idris-dev
on master help sign in
test basic021 type checks
3985928Rui Barreiro
libs/base/Data/IORef.idr+23−45
compare with master
unifiedsplit
@@ -1,14 +1,16 @@
1module Data.IORef
1module Data.IORef
2
2
3+export
4+data IORef a = MkIORef a
5+
3public export
6public export
4interface HasReference (ffi : FFI) where
7interface HasReference (ffi : FFI) where
5− IORef' : Type -> Type
6− newIORef' : a -> IO' ffi (IORef' a)
8+ newIORef' : a -> IO' ffi (IORef a)
7− readIORef' : IORef' a -> IO' ffi a
9+ readIORef' : IORef a -> IO' ffi a
8− writeIORef' : IORef' a -> a -> IO' ffi ()
10+ writeIORef' : IORef a -> a -> IO' ffi ()
9
11
10export
12export
11−modifyIORef': HasReference ffi => IORef' {ffi = ffi} a -> (a -> a) -> IO' ffi ()
13+modifyIORef': HasReference ffi => IORef a -> (a -> a) -> IO' ffi ()
12modifyIORef' ref fn =
14modifyIORef' ref fn =
13 do
15 do
14 val <- readIORef' ref
16 val <- readIORef' ref
@@ -16,20 +18,24 @@ modifyIORef' ref fn =
16
18
17export
19export
18implementation HasReference FFI_C where
20implementation HasReference FFI_C where
19− IORef' = Raw
20− newIORef' val =
21+ newIORef' val
21− foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)
22+ = do MkRaw ref <- foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)
23+ pure (MkIORef ref)
22− readIORef' ref =
24+ readIORef' (MkIORef ref)
23− do
24− MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) ref
25+ = do MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) (MkRaw ref)
25− pure val
26+ pure val
26− writeIORef' ref val =
27+ writeIORef' (MkIORef ref) val
27− foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())
28+ = foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())
28− ref (MkRaw val)
29+ (MkRaw ref) (MkRaw val)
29
30
30export
31export
31−IORef : Type -> Type
32+implementation HasReference FFI_JS where
32−IORef = IORef' {ffi = FFI_C}
33+ newIORef' val =
34+ (MkIORef . believe_me) <$> foreign FFI_JS "{val: %0}" (Ptr -> JS_IO Ptr) (believe_me val)
35+ readIORef' (MkIORef ref) =
36+ believe_me <$> foreign FFI_JS "%0.val" (Ptr -> JS_IO Ptr) (believe_me ref)
37+ writeIORef' (MkIORef ref) val =
38+ foreign FFI_JS "%0.val = %1" (Ptr -> Ptr -> JS_IO ()) (believe_me ref) (believe_me val)
33
39
34export
40export
35newIORef : a -> IO (IORef a)
41newIORef : a -> IO (IORef a)
@@ -46,31 +52,3 @@ writeIORef = writeIORef'
46export
52export
47modifyIORef : IORef a -> (a -> a) -> IO ()
53modifyIORef : IORef a -> (a -> a) -> IO ()
48modifyIORef = modifyIORef'
54modifyIORef = modifyIORef'
49−{-
50−export
51−data IORef a = MkIORef a
52−
53−export
54−newIORef : a -> IO (IORef a)
55−newIORef val
56− = do MkRaw ref <- foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)
57− pure (MkIORef ref)
58−
59−export
60−readIORef : IORef a -> IO a
61−readIORef (MkIORef ref)
62− = do MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) (MkRaw ref)
63− pure val
64−
65−export
66−writeIORef : IORef a -> a -> IO ()
67−writeIORef (MkIORef old) val
68− = foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())
69− (MkRaw old) (MkRaw val)
70−
71−export
72−modifyIORef : IORef a -> (a -> a) -> IO ()
73−modifyIORef ref fn
74− = do val <- readIORef ref
75− writeIORef ref (fn val)
76−-}