on master help sign in
test basic021 type checks
commit3985928569b34b4e1eea53fbb68daf5331e1e75b authorRui Barreiro <rui.barreiro@gmail.com> dateWed 4 Oct 2017, 18:57 (9 years ago) parentbf432a1
1 file changed+23−45
libs/base/Data/IORef.idr+23−45
libs/base/Data/IORef.idr+23−45
@@ -1,14 +1,16 @@
11module Data.IORef
22
3+export
4+data IORef a = MkIORef a
5+
36public export
47interface HasReference (ffi : FFI) where
5− IORef' : Type -> Type
6− newIORef' : a -> IO' ffi (IORef' a)
7− readIORef' : IORef' a -> IO' ffi a
8− writeIORef' : IORef' a -> a -> IO' ffi ()
8+ newIORef' : a -> IO' ffi (IORef a)
9+ readIORef' : IORef a -> IO' ffi a
10+ writeIORef' : IORef a -> a -> IO' ffi ()
911
1012export
11−modifyIORef': HasReference ffi => IORef' {ffi = ffi} a -> (a -> a) -> IO' ffi ()
13+modifyIORef': HasReference ffi => IORef a -> (a -> a) -> IO' ffi ()
1214modifyIORef' ref fn =
1315 do
1416 val <- readIORef' ref
@@ -16,20 +18,24 @@ modifyIORef' ref fn =
1618
1719export
1820implementation HasReference FFI_C where
19− IORef' = Raw
20− newIORef' val =
21− foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)
22− readIORef' ref =
23− do
24− MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) ref
25− pure val
26− writeIORef' ref val =
27− foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())
28− ref (MkRaw val)
21+ newIORef' val
22+ = do MkRaw ref <- foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)
23+ pure (MkIORef ref)
24+ readIORef' (MkIORef ref)
25+ = do MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) (MkRaw ref)
26+ pure val
27+ writeIORef' (MkIORef ref) val
28+ = foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())
29+ (MkRaw ref) (MkRaw val)
2930
3031export
31−IORef : Type -> Type
32−IORef = IORef' {ffi = FFI_C}
32+implementation HasReference FFI_JS where
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)
3339
3440export
3541newIORef : a -> IO (IORef a)
@@ -46,31 +52,3 @@ writeIORef = writeIORef'
4652export
4753modifyIORef : IORef a -> (a -> a) -> IO ()
4854modifyIORef = 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−-}