git.iko.soy/Idris-dev
on master help sign in
first try, example basic021 gives a type error
bf432a1Rui Barreiro
libs/base/Data/IORef.idr+48
compare with master
unifiedsplit
@@ -1,5 +1,52 @@
1module Data.IORef
1module Data.IORef
2
2
3+public export
4+interface 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 ()
9+
10+export
11+modifyIORef': HasReference ffi => IORef' {ffi = ffi} a -> (a -> a) -> IO' ffi ()
12+modifyIORef' ref fn =
13+ do
14+ val <- readIORef' ref
15+ writeIORef' ref (fn val)
16+
17+export
18+implementation 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)
29+
30+export
31+IORef : Type -> Type
32+IORef = IORef' {ffi = FFI_C}
33+
34+export
35+newIORef : a -> IO (IORef a)
36+newIORef = newIORef'
37+
38+export
39+readIORef : IORef a -> IO a
40+readIORef = readIORef'
41+
42+export
43+writeIORef : IORef a -> a -> IO ()
44+writeIORef = writeIORef'
45+
46+export
47+modifyIORef : IORef a -> (a -> a) -> IO ()
48+modifyIORef = modifyIORef'
49+{-
3export
50export
4data IORef a = MkIORef a
51data IORef a = MkIORef a
5
52
@@ -26,3 +73,4 @@ modifyIORef : IORef a -> (a -> a) -> IO ()
26modifyIORef ref fn
73modifyIORef ref fn
27 = do val <- readIORef ref
74 = do val <- readIORef ref
28 writeIORef ref (fn val)
75 writeIORef ref (fn val)
76+-}