ff9e9fa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added Data.IOArray for mutable array primitives

The interface provides only 'unsafe' reading and writing. This gives primtive access without bounds checking. Safe interfaces should be built on top of this, but it's up to the implementer whether bounds checking is at compile time (e.g. via a proof of bounds safety with the index mapping to an integer location) or at runtime (e.g. returning a Maybe)

commitff9e9fa8128014d8d8d1d565256b626d3421475b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 19 Oct 2017, 09:49 (9 years ago) parent9e1c9a3

6 files changed+114−5

compare with master

unifiedsplit

CHANGELOG.md+1 libs/contrib/Data/IOArray.idr+47 libs/contrib/contrib.ipkg+1 rts/idris_gc.c+15−3 rts/idris_rts.c+28−1 rts/idris_rts.h+22−1

CHANGELOG.md+1

@@ -18,6 +18,7 @@

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

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

2020+ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.

21++ Added `Data.IOArray`, containing primitives for mutable arrays.

2122

2223## Tool Updates

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

libs/contrib/Data/IOArray.idrnew file+47

@@ -0,0 +1,47 @@

1+module Data.IOArray

3+-- Raw access to IOArrays. This interface is unsafe because there's no

4+-- bounds checking, and is merely intended to provide primitive access via

5+-- the RTS. Safe interfaces (either with run time or compile time

6+-- bounds checking) can be implemented on top of this

8+-- Implemented entirely by the array primitives in the RTS

9+data ArrayData : Type -> Type where

10+

11+export

12+data IOArray elem = MkIOArray (ArrayData elem)

13+

14+||| Create a new array of the given size, with all entries set to the

15+||| given default element.

16+export

17+newArray : Int -> elem -> IO (IOArray elem)

18+newArray size default

19+ = do vm <- getMyVM

20+ MkRaw p <- foreign FFI_C "idris_newArray"

21+ (Ptr -> Int -> Raw elem -> IO (Raw (ArrayData elem)))

22+ vm size (MkRaw default)

23+ pure (MkIOArray p)

24+

25+||| Write an element at a location in an array.

26+||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can

27+||| be implemented on top of this, either with a run time or compile time

28+||| check.

29+export

30+unsafeWriteArray : IOArray elem -> Int -> elem -> IO ()

31+unsafeWriteArray (MkIOArray p) i val

32+ = foreign FFI_C "idris_arraySet"

33+ (Raw (ArrayData elem) -> Int -> Raw elem -> IO ())

34+ (MkRaw p) i (MkRaw val)

35+

36+||| Read the element at a location in an array.

37+||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can

38+||| be implemented on top of this, either with a run time or compile time

39+||| check.

40+export

41+unsafeReadArray : IOArray elem -> Int -> IO elem

42+unsafeReadArray (MkIOArray p) i

43+ = do MkRaw val <- foreign FFI_C "idris_arrayGet"

44+ (Raw (ArrayData elem) -> Int -> IO (Raw elem))

45+ (MkRaw p) i

46+ pure val

47+

libs/contrib/contrib.ipkg+1

@@ -26,6 +26,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory,

2626 Data.List.Zipper,

2727 Data.Pairs.Implicit,

2828 Data.Combinators, Data.Combinators.Applicative, Data.Combinators.Arrow,

29+ Data.IOArray,

2930

3031 Decidable.Decidable, Decidable.Order,

3132

rts/idris_gc.c+15−3

@@ -5,7 +5,7 @@

55#include <assert.h>

77VAL copy(VM* vm, VAL x) {

8− int ar;

8+ int ar, len;

99 Closure* cl = NULL;

1010 if (x==NULL || ISINT(x)) {

1111 return x;

@@ -20,6 +20,11 @@ VAL copy(VM* vm, VAL x) {

2020 memcpy(&(cl->info.c.args), &(x->info.c.args), sizeof(VAL)*ar);

2121 }

2222 break;

23+ case CT_ARRAY:

24+ len = x->info.arr.length;

25+ allocArray(cl, vm, len, 1);

26+ memcpy(&(cl->info.arr.content), &(x->info.arr.content), sizeof(VAL)*len);

27+ break;

2328 case CT_FLOAT:

2429 cl = MKFLOATc(vm, x->info.f);

2530 break;

@@ -58,7 +63,7 @@ VAL copy(VM* vm, VAL x) {

5863 case CT_RAWDATA:

5964 {

6065 size_t size = x->info.size + sizeof(Closure);

61− cl = allocate(size, 0);

66+ cl = allocate(size, 1);

6267 memcpy(cl, x, size);

6368 }

6469 break;

@@ -76,7 +81,7 @@ VAL copy(VM* vm, VAL x) {

7681

7782void cheney(VM *vm) {

7883 int i;

79− int ar;

84+ int ar, len;

8085 char* scan = aligned_heap_pointer(vm->heap.heap);

8186

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

@@ -91,6 +96,13 @@ void cheney(VM *vm) {

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

9297 }

9398 break;

99+ case CT_ARRAY:

100+ len = heap_item->info.arr.length;

101+ for(i = 0; i < len; ++i) {

102+ VAL newptr = copy(vm, heap_item->info.arr.content[i]);

103+ heap_item->info.arr.content[i] = newptr;

104+ }

105+ break;

94106 case CT_REF:

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

96108 break;

rts/idris_rts.c+28−1

@@ -796,6 +796,23 @@ VAL idris_readRef(VAL ref) {

796796 return (VAL)(ref->info.ptr);

797797}

798798

799+VAL idris_newArray(VM* vm, int size, VAL def) {

800+ Closure* cl;

801+ allocArray(cl, vm, size, 0);

802+ for(int i=0; i<size; ++i) {

803+ cl->info.arr.content[i] = def;

804+ }

805+ return cl;

806+}

807+

808+void idris_arraySet(VAL arr, int index, VAL newval) {

809+ arr->info.arr.content[index] = newval;

810+}

811+

812+VAL idris_arrayGet(VAL arr, int index) {

813+ return arr->info.arr.content[index];

814+}

815+

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

800817 int i = GETINT(index);

801818 switch(i) {

@@ -877,7 +894,7 @@ void* idris_stopThread(VM* vm) {

877894// VM is assumed to be a different vm from the one x lives on

878895

879896VAL doCopyTo(VM* vm, VAL x) {

880− int i, ar;

897+ int i, ar, len;

881898 VAL* argptr;

882899 Closure* cl;

883900 if (x==NULL || ISINT(x)) {

@@ -898,6 +915,16 @@ VAL doCopyTo(VM* vm, VAL x) {

898915 }

899916 }

900917 break;

918+ case CT_ARRAY:

919+ len = x->info.arr.length;

920+ allocArray(cl, vm, len, 1);

921+

922+ argptr = (VAL*)(cl->info.arr.content);

923+ for(i = 0; i < len; ++i) {

924+ *argptr = doCopyTo(vm, *((VAL*)(x->info.arr.content)+i)); // recursive version

925+ argptr++;

926+ }

927+ break;

901928 case CT_FLOAT:

902929 cl = MKFLOATc(vm, x->info.f);

903930 break;

rts/idris_rts.h+22−1

@@ -25,18 +25,28 @@

2525

2626// Closures

2727typedef enum {

28− CT_CON, CT_INT, CT_BIGINT, CT_FLOAT, CT_STRING, CT_STROFFSET,

28+ CT_CON, CT_ARRAY, CT_INT, CT_BIGINT, CT_FLOAT, CT_STRING, CT_STROFFSET,

2929 CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_REF,

3030 CT_FWD, CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA

3131} ClosureType;

3232

3333typedef struct Closure *VAL;

3434

35+// A constructor, consisting of a tag, an arity (16 bits each of the

36+// tag_arity field) and arguments

3537typedef struct {

3638 uint32_t tag_arity;

3739 VAL args[];

3840} con;

3941

42+// An array; similar to a constructor but with a length, and contents

43+// initialised to NULL (high level Idris programs are responsible for

44+// initialising them properly)

45+typedef struct {

46+ uint32_t length;

47+ VAL content[];

48+} array;

49+

4050typedef struct {

4151 VAL str;

4252 size_t offset;

@@ -62,6 +72,7 @@ typedef struct Closure {

6272 uint32_t ty;

6373 union {

6474 con c;

75+ array arr;

6576 int i;

6677 double f;

6778 String str;

@@ -312,6 +323,11 @@ void idris_free(void* ptr, size_t size);

312323

313324#define NULL_CON(x) nullary_cons[x]

314325

326+#define allocArray(cl, vm, len, o) \

327+ cl = allocate(sizeof(Closure) + sizeof(VAL)*len, o); \

328+ SETTY(cl, CT_ARRAY); \

329+ cl->info.arr.length = len;

330+

315331int idris_errno(void);

316332char* idris_showerror(int err);

317333

@@ -407,6 +423,11 @@ VAL idris_newRef(VAL x);

407423void idris_writeRef(VAL ref, VAL x);

408424VAL idris_readRef(VAL ref);

409425

426+// Support for IOArrays

427+VAL idris_newArray(VM* vm, int size, VAL def);

428+void idris_arraySet(VAL arr, int index, VAL newval);

429+VAL idris_arrayGet(VAL arr, int index);

430+

410431// system infox

411432// used indices:

412433// 0 returns backend