921ac8f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added Data.IORef

This is intended for simple mutable state in IO, which is sometimes useful for efficiency of global state. STRef could work similarly, at some point.

commit921ac8fd76d1a8ff46a6f40e3b6d6a3cc76803ec authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 17 Sep 2017, 13:06 (9 years ago) parent8fb1be9

10 files changed+91−6

compare with master

unifiedsplit

CHANGELOG.md+7−2 libs/base/Data/IORef.idr+28 libs/base/base.ipkg+1 rts/idris_gc.c+7−1 rts/idris_rts.c+20 rts/idris_rts.h+8−2 test/TestData.hs+2−1 test/basic021/basic021.idr+13 test/basic021/expected+1 test/basic021/run+4

CHANGELOG.md+7−2

@@ -1,13 +1,18 @@

11# New in 1.1.*

3−+ Addition of `Text.Literate`, a module for working with literate

4− source files.

3+## Language updates

55+ In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side

66 of any definitions in `where` clauses, provided the left-hand side of the

77 definition does not shadow it.

88+ Private functions are no longer visible in the REPL except for modules

99 that are explicitly loaded.

1010

11+## Library Updates

12+

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

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

15+

1116# New in 1.1.1

1217

1318+ Erasure analysis is now faster thanks to a bit smarter constraint solving.

libs/base/Data/IORef.idrnew file+28

@@ -0,0 +1,28 @@

1+module Data.IORef

3+export

4+data IORef a = MkIORef a

6+export

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

8+newIORef val

9+ = do MkRaw ref <- foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)

10+ pure (MkIORef ref)

11+

12+export

13+readIORef : IORef a -> IO a

14+readIORef (MkIORef ref)

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

16+ pure val

17+

18+export

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

20+writeIORef (MkIORef old) val

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

22+ (MkRaw old) (MkRaw val)

23+

24+export

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

26+modifyIORef ref fn

27+ = do val <- readIORef ref

28+ writeIORef ref (fn val)

libs/base/base.ipkg+1

@@ -21,6 +21,7 @@ modules = System,

2121 Data.HVect,

2222 Data.Complex,

2323 Data.Erased,

24+ Data.IORef,

2425 Data.List,

2526 Data.List.Views,

2627 Data.List.Quantifiers,

rts/idris_gc.c+7−1

@@ -50,6 +50,9 @@ VAL copy(VM* vm, VAL x) {

5050 case CT_BITS64:

5151 cl = idris_b64CopyForGC(vm, x);

5252 break;

53+ case CT_REF:

54+ cl = idris_newRefLock((VAL)(x->info.ptr), 1);

55+ break;

5356 case CT_FWD:

5457 return x->info.ptr;

5558 case CT_RAWDATA:

@@ -79,7 +82,7 @@ void cheney(VM *vm) {

7982 while(scan < vm->heap.next) {

8083 size_t inc = *((size_t*)scan);

8184 VAL heap_item = (VAL)(scan+sizeof(size_t));

82− // If it's a CT_CON or CT_STROFFSET, copy its arguments

85+ // If it's a CT_CON, CT_REF or CT_STROFFSET, copy its arguments

8386 switch(GETTY(heap_item)) {

8487 case CT_CON:

8588 ar = ARITY(heap_item);

@@ -88,6 +91,9 @@ void cheney(VM *vm) {

8891 heap_item->info.c.args[i] = newptr;

8992 }

9093 break;

94+ case CT_REF:

95+ heap_item->info.ptr = copy(vm, (VAL)(heap_item->info.ptr));

96+ break;

9197 case CT_STROFFSET:

9298 heap_item->info.str_offset->str

9399 = copy(vm, heap_item->info.str_offset->str);

rts/idris_rts.c+20

@@ -776,6 +776,26 @@ VAL idris_strRev(VM* vm, VAL str) {

776776 return cl;

777777}

778778

779+VAL idris_newRefLock(VAL x, int outerlock) {

780+ Closure* cl = allocate(sizeof(Closure), outerlock);

781+ SETTY(cl, CT_REF);

782+ cl->info.ptr = (void*)x;

783+ return cl;

784+}

785+

786+VAL idris_newRef(VAL x) {

787+ return idris_newRefLock(x, 0);

788+}

789+

790+void idris_writeRef(VAL ref, VAL x) {

791+ ref->info.ptr = (void*)x;

792+ SETTY(ref, CT_REF);

793+}

794+

795+VAL idris_readRef(VAL ref) {

796+ return (VAL)(ref->info.ptr);

797+}

798+

779799VAL idris_systemInfo(VM* vm, VAL index) {

780800 int i = GETINT(index);

781801 switch(i) {

rts/idris_rts.h+8−2

@@ -26,8 +26,8 @@

2626// Closures

2727typedef enum {

2828 CT_CON, CT_INT, CT_BIGINT, CT_FLOAT, CT_STRING, CT_STROFFSET,

29− CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_FWD,

30− CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA

29+ CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_REF,

30+ CT_FWD, CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA

3131} ClosureType;

3232

3333typedef struct Closure *VAL;

@@ -401,6 +401,12 @@ VAL idris_strIndex(VM* vm, VAL str, VAL i);

401401VAL idris_strRev(VM* vm, VAL str);

402402VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str);

403403

404+// Support for IORefs

405+VAL idris_newRefLock(VAL x, int outerlock);

406+VAL idris_newRef(VAL x);

407+void idris_writeRef(VAL ref, VAL x);

408+VAL idris_readRef(VAL ref);

409+

404410// system infox

405411// used indices:

406412// 0 returns backend

test/TestData.hs+2−1

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

7272 ( 17, ANY ),

7373 ( 18, ANY ),

7474 ( 19, ANY ),

75− ( 20, ANY )]),

75+ ( 20, ANY ),

76+ ( 21, ANY )]),

7677 ("bignum", "Bignum",

7778 [ ( 1, ANY ),

7879 ( 2, ANY )]),

test/basic021/basic021.idrnew file+13

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

1+import Data.IORef

3+count : Nat -> IORef Integer -> IO ()

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 1000000 r

test/basic021/expectednew file+1

@@ -0,0 +1 @@

1+1000000

test/basic021/runnew file+4

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

1+#!/usr/bin/env bash

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

3+./basic021

4+rm -f basic021 *.ibc