713e485 · Idris-dev · git.iko.soy

libs/base/Data/Buffer.idr+5−4

compare with master

unifiedsplit

@@ -21,11 +21,12 @@ record Buffer where

21||| fails

22export

23newBuffer : (size : Int) -> IO (Maybe Buffer)

24+newBuffer size = do vm <- getMyVM

24−newBuffer size = do bptr <- foreign FFI_C "idris_newBuffer" (Int -> IO Ptr)

25+ bptr <- foreign FFI_C "idris_newBuffer" (Ptr -> Int -> IO ManagedPtr)

25− size

26+ vm size

26− bad <- nullPtr bptr

27+ bad <- nullManagedPtr bptr

27 if bad then pure Nothing

28 if bad then pure Nothing

28− else pure (Just (MkBuffer (prim__registerPtr bptr (size + 8)) size 0))

29+ else pure (Just (MkBuffer bptr size 0))

29

30

30||| Reset the 'next location' pointer of the buffer to 0.

31||| Reset the 'next location' pointer of the buffer to 0.

31||| The 'next location' pointer gives the location for the next file read/write

32||| The 'next location' pointer gives the location for the next file read/write

libs/prelude/Builtins.idr+1

@@ -206,6 +206,7 @@ export data CData : Type

206%extern prim__stderr : Ptr

207

208%extern prim__null : Ptr

209+%extern prim__managedNull : ManagedPtr

209%extern prim__eqPtr : Ptr -> Ptr -> Int

210%extern prim__eqPtr : Ptr -> Ptr -> Int

210%extern prim__eqManagedPtr : ManagedPtr -> ManagedPtr -> Int

211%extern prim__eqManagedPtr : ManagedPtr -> ManagedPtr -> Int

211%extern prim__registerPtr : Ptr -> Int -> ManagedPtr

212%extern prim__registerPtr : Ptr -> Int -> ManagedPtr

libs/prelude/Prelude/Strings.idr+8

@@ -146,6 +146,9 @@ reverse = prim__strRev

146null : Ptr

147null = prim__null

148

149+managedNull : ManagedPtr

150+managedNull = prim__managedNull

151+

149-- Some more complex string operations

152-- Some more complex string operations

150

153

151data StrM : String -> Type where

154data StrM : String -> Type where

@@ -398,6 +401,11 @@ nullPtr : Ptr -> IO Bool

398nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p

401nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p

399 pure (ok /= 0)

402 pure (ok /= 0)

400

403

404+partial

405+nullManagedPtr : ManagedPtr -> IO Bool

406+nullManagedPtr p = do ok <- foreign FFI_C "isNull" (ManagedPtr -> IO Int) p

407+ pure (ok /= 0)

408+

401||| Check if a supposed string was actually a null pointer

409||| Check if a supposed string was actually a null pointer

402partial

410partial

403nullStr : String -> IO Bool

411nullStr : String -> IO Bool

rts/idris_buffer.c+7−3

@@ -6,8 +6,10 @@ typedef struct {

6 uint8_t data[0];

7} Buffer;

8

9−void* idris_newBuffer(int bytes) {

9+VAL idris_newBuffer(VM* vm, int bytes) {

10+ size_t size = sizeof(Buffer) + bytes*sizeof(uint8_t);

11+

10− Buffer* buf = malloc(sizeof(Buffer) + bytes*sizeof(uint8_t));

12+ Buffer* buf = malloc(size);

11 if (buf == NULL) {

13 if (buf == NULL) {

12 return NULL;

14 return NULL;

13 }

15 }

@@ -15,7 +17,9 @@ void* idris_newBuffer(int bytes) {

15 buf->size = bytes;

17 buf->size = bytes;

16 memset(buf->data, 0, bytes);

18 memset(buf->data, 0, bytes);

17

19

20+ void* retbuf = MKMPTR(vm, buf, size);

21+ free(buf);

18− return buf;

22+ return retbuf;

19}

23}

20

24

21void idris_copyBuffer(void* from, int start, int len,

25void idris_copyBuffer(void* from, int start, int len,

rts/idris_buffer.h+1−1

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

6#include <stdint.h>

7#include "idris_rts.h"

8

9−void* idris_newBuffer(int bytes);

9+VAL idris_newBuffer(VM* vm, int bytes);

10

11int idris_getBufferSize(void* buffer);

12

src/IRTS/CodegenC.hs+2−1

@@ -389,7 +389,7 @@ c_irts (FArith (ATInt (ITFixed ity))) l x

389c_irts FString l x = l ++ "MKSTR(vm, " ++ x ++ ")"

390c_irts FUnit l x = x

391c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"

392−c_irts FManagedPtr l x = l ++ "MKMPTR(vm, " ++ x ++ ")"

392+c_irts FManagedPtr l x = l ++ x

393c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"

394c_irts FCData l x = l ++ "MKCDATA(vm, " ++ x ++ ")"

395c_irts FAny l x = l ++ x

@@ -644,6 +644,7 @@ doOp v (LExternal se) [] | se == sUN "prim__stderr" = v ++ "MKPTR(vm, stderr)"

644

645doOp v (LExternal vm) [_] | vm == sUN "prim__vm" = v ++ "MKPTR(vm, vm)"

646doOp v (LExternal nul) [] | nul == sUN "prim__null" = v ++ "MKPTR(vm, NULL)"

647+doOp v (LExternal nul) [] | nul == sUN "prim__managedNull" = v ++ "MKPTR(vm, NULL)"

647doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqPtr"

648doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqPtr"

648 = v ++ "MKINT((i_int)(GETPTR(" ++ creg x ++ ") == GETPTR(" ++ creg y ++ ")))"

649 = v ++ "MKINT((i_int)(GETPTR(" ++ creg x ++ ") == GETPTR(" ++ creg y ++ ")))"

649doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqManagedPtr"

650doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqManagedPtr"