c3113e7 · Idris-dev · git.iko.soy

CHANGELOG.md+1−1

compare with master

unifiedsplit

@@ -12,7 +12,7 @@

12## Library Updates

13

14+ Added `Text.Literate`, a module for working with literate source files.

15−+ Added `Data.IORef`, for working with mutable references in `IO`.

15++ Added `Data.IORef`, for working with mutable references in `IO` and `JS_IO`.

16+ Added `discriminate` and `construct` tactics to Pruviloj.

17

18## Tool Updates

libs/base/Data/IORef.idr+37−11

@@ -3,26 +3,52 @@ module Data.IORef

3export

4data IORef a = MkIORef a

5

6+public export

7+interface HasReference (ffi : FFI) where

8+ newIORef' : a -> IO' ffi (IORef a)

9+ readIORef' : IORef a -> IO' ffi a

10+ writeIORef' : IORef a -> a -> IO' ffi ()

11+

6export

12export

7−newIORef : a -> IO (IORef a)

13+modifyIORef': HasReference ffi => IORef a -> (a -> a) -> IO' ffi ()

14+modifyIORef' ref fn =

15+ do

16+ val <- readIORef' ref

17+ writeIORef' ref (fn val)

18+

19+export

20+implementation HasReference FFI_C where

8−newIORef val

21+ newIORef' val

9 = do MkRaw ref <- 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)

10 pure (MkIORef ref)

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)

30+

31+export

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)

39+

40+export

41+newIORef : a -> IO (IORef a)

42+newIORef = newIORef'

11

43

12export

44export

13readIORef : IORef a -> IO a

45readIORef : IORef a -> IO a

14−readIORef (MkIORef ref)

46+readIORef = readIORef'

15− = do MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) (MkRaw ref)

16− pure val

17

47

18export

48export

19writeIORef : IORef a -> a -> IO ()

49writeIORef : IORef a -> a -> IO ()

20−writeIORef (MkIORef old) val

50+writeIORef = writeIORef'

21− = foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())

22− (MkRaw old) (MkRaw val)

23

51

24export

52export

25modifyIORef : IORef a -> (a -> a) -> IO ()

53modifyIORef : IORef a -> (a -> a) -> IO ()

26−modifyIORef ref fn

54+modifyIORef = modifyIORef'

27− = do val <- readIORef ref

28− writeIORef ref (fn val)

test/TestData.hs+2−1

@@ -72,7 +72,8 @@ testFamiliesData = [

72 ( 18, ANY ),

73 ( 19, ANY ),

74 ( 20, ANY ),

75− ( 21, C_CG )]),

75+ ( 21, C_CG ),

76+ ( 22, NODE_CG )]),

76 ("bignum", "Bignum",

77 ("bignum", "Bignum",

77 [ ( 1, ANY ),

78 [ ( 1, ANY ),

78 ( 2, ANY )]),

79 ( 2, ANY )]),

test/basic021/basic021_2.idrnew file+13

@@ -0,0 +1,13 @@

1+import Data.IORef

2+

3+count : HasReference ffi => Nat -> IORef Integer -> IO' ffi ()

4+count Z ref

5+ = do x <- readIORef' ref

6+ printLn' x

7+count (S k) ref

8+ = do modifyIORef' ref (+1)

9+ count k ref

10+

11+main : IO ()

12+main = do r <- newIORef' 0

13+ count 1000 r

test/basic021/expected+1

@@ -1 +1,2 @@

11000000

2+1000

test/basic021/run+3−1

@@ -1,4 +1,6 @@

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ basic021.idr -o basic021

3+${IDRIS:-idris} $@ basic021_2.idr -o basic021_2

3./basic021

4./basic021

5+./basic021_2

4−rm -f basic021 *.ibc

6+rm -f basic021 basic021_2 *.ibc

test/basic022/basic022.idrnew file+13

@@ -0,0 +1,13 @@

1+import Data.IORef

2+

3+count : HasReference ffi => Nat -> IORef Integer -> IO' ffi ()

4+count Z ref

5+ = do x <- readIORef' ref

6+ printLn' x

7+count (S k) ref

8+ = do modifyIORef' ref (+1)

9+ count k ref

10+

11+main : JS_IO ()

12+main = do r <- newIORef' 0

13+ count 1000 r

test/basic022/expectednew file+1

@@ -0,0 +1 @@

1+1000

test/basic022/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ basic022.idr -o basic022

3+./basic022

4+rm -f basic022 *.ibc