ff9e9fa · Idris-dev · git.iko.soy

CHANGELOG.md+1

compare with master

unifiedsplit

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

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

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

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

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

21

22

22## Tool Updates

23## Tool Updates

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

24+ 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

2+

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

7+

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,

26 Data.List.Zipper,

27 Data.Pairs.Implicit,

28 Data.Combinators, Data.Combinators.Applicative, Data.Combinators.Arrow,

29+ Data.IOArray,

29

30

30 Decidable.Decidable, Decidable.Order,

31 Decidable.Decidable, Decidable.Order,

31

32

rts/idris_gc.c+15−3

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

5#include <assert.h>

6

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

8− int ar;

8+ int ar, len;

9 Closure* cl = NULL;

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

11 return x;

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

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

21 }

22 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;

23 case CT_FLOAT:

28 case CT_FLOAT:

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

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

25 break;

30 break;

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

58 case CT_RAWDATA:

63 case CT_RAWDATA:

59 {

64 {

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

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

61− cl = allocate(size, 0);

66+ cl = allocate(size, 1);

62 memcpy(cl, x, size);

67 memcpy(cl, x, size);

63 }

68 }

64 break;

69 break;

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

76

81

77void cheney(VM *vm) {

82void cheney(VM *vm) {

78 int i;

83 int i;

79− int ar;

84+ int ar, len;

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

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

81

86

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

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

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

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

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

92 }

97 }

93 break;

98 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;

94 case CT_REF:

106 case CT_REF:

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

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

96 break;

108 break;

rts/idris_rts.c+28−1

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

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

797}

798

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+

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

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

800 int i = GETINT(index);

817 int i = GETINT(index);

801 switch(i) {

818 switch(i) {

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

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

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

878

895

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

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

880− int i, ar;

897+ int i, ar, len;

881 VAL* argptr;

898 VAL* argptr;

882 Closure* cl;

899 Closure* cl;

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

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

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

898 }

915 }

899 }

916 }

900 break;

917 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;

901 case CT_FLOAT:

928 case CT_FLOAT:

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

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

903 break;

930 break;

rts/idris_rts.h+22−1

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

25

26// Closures

27typedef 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,

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

30 CT_FWD, CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA

31} ClosureType;

32

33typedef struct Closure *VAL;

34

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

36+// tag_arity field) and arguments

35typedef struct {

37typedef struct {

36 uint32_t tag_arity;

38 uint32_t tag_arity;

37 VAL args[];

39 VAL args[];

38} con;

40} con;

39

41

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+

40typedef struct {

50typedef struct {

41 VAL str;

51 VAL str;

42 size_t offset;

52 size_t offset;

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

62 uint32_t ty;

72 uint32_t ty;

63 union {

73 union {

64 con c;

74 con c;

75+ array arr;

65 int i;

76 int i;

66 double f;

77 double f;

67 String str;

78 String str;

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

312

323

313#define NULL_CON(x) nullary_cons[x]

324#define NULL_CON(x) nullary_cons[x]

314

325

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+

315int idris_errno(void);

331int idris_errno(void);

316char* idris_showerror(int err);

332char* idris_showerror(int err);

317

333

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

407void idris_writeRef(VAL ref, VAL x);

423void idris_writeRef(VAL ref, VAL x);

408VAL idris_readRef(VAL ref);

424VAL idris_readRef(VAL ref);

409

425

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+

410// system infox

431// system infox

411// used indices:

432// used indices:

412// 0 returns backend

433// 0 returns backend