d2c0907 · Idris-dev · git.iko.soy

libs/contrib/CFFI/Memory.idr+6−6

compare with master

unifiedsplit

@@ -30,8 +30,8 @@ get (CPt p o I8) = prim_peek8 p o

30get (CPt p o I16) = prim_peek16 p o

31get (CPt p o I32) = prim_peek32 p o

32get (CPt p o I64) = prim_peek64 p o

33−get (CPt p o FLOAT) = prim_peek32 p o

33+get (CPt p o FLOAT) = prim_peekSingle p o

34−get (CPt p o DOUBLE) = cast $ prim_peek64 p o

34+get (CPt p o DOUBLE) = prim_peekDouble p o

35get (CPt p o PTR) = prim_peekPtr p o

36

37

@@ -41,8 +41,8 @@ put _ _ = putStrLn "putting"

41-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()

42

43field : CPtr -> (i : Nat) -> CPtr

44−field (Cpt p o arr@(ARRAY n t)) = CPt p (o + index i (offsets arr)) t

44+field (CPt p o arr@(ARRAY n t)) = CPt p (o + index i (offsets arr)) t

45−field (Cpt p o (UNION xs)) = CPt p o (index i xs)

45+field (CPt p o (UNION xs)) = CPt p o (index i xs)

46−field (Cpt p o st@(STRUCT xs)) = CPt p (o + index i (offsets st)) (index i xs)

46+field (CPt p o st@(STRUCT xs)) = CPt p (o + index i (offsets st)) (index i xs)

47−field (Cpt p o ps@(PACKEDSTRUCT xs)) = CPt p (o + index i (offsets st)) (index i xs)

47+field (CPt p o ps@(PACKEDSTRUCT xs)) = CPt p (o + index i (offsets st)) (index i xs)

48field p Z = p

libs/contrib/CFFI/Types.idr+1−1

@@ -17,7 +17,7 @@ translate I8 = Bits8

17translate I16 = Bits16

18translate I32 = Bits32

19translate I64 = Bits64

20−translate FLOAT = Bits32

20+translate FLOAT = Double

21translate DOUBLE = Double

22translate PTR = Ptr

23translate (ARRAY n t) = Vect (toNat n) (translate t)

libs/prelude/Builtins.idr+5

@@ -214,3 +214,8 @@ export data CData : Type

214

215%extern prim__peekPtr : prim__WorldType -> Ptr -> Int -> Ptr

216%extern prim__pokePtr : prim__WorldType -> Ptr -> Int -> Ptr -> Int

217+

218+%extern prim__peekDouble : prim__WorldType -> Ptr -> Int -> Double

219+%extern prim__pokeDouble : prim__WorldType -> Ptr -> Int -> Double -> Int

220+%extern prim__peekSingle : prim__WorldType -> Ptr -> Int -> Double

221+%extern prim__pokeSingle : prim__WorldType -> Ptr -> Int -> Double -> Int

libs/prelude/IO.idr+16

@@ -349,3 +349,19 @@ prim_peekPtr ptr offset = MkIO (\w => prim_io_return (prim__peekPtr (world w) pt

349prim_pokePtr : Ptr -> Int -> Ptr -> IO Int

350prim_pokePtr ptr offset val = MkIO (\w => prim_io_return (

351 prim__pokePtr (world w) ptr offset val))

352+

353+prim_peekDouble : Ptr -> Int -> IO Double

354+prim_peekDouble ptr offset = MkIO (\w => prim_io_return (prim__peekDouble (world w) ptr offset))

355+

356+prim_pokeDouble : Ptr -> Int -> Double -> IO Int

357+prim_pokeDouble ptr offset val = MkIO (\w => prim_io_return (

358+ prim__pokeDouble (world w) ptr offset val))

359+

360+||| Single precision floats are marshalled to Doubles

361+prim_peekSingle : Ptr -> Int -> IO Double

362+prim_peekSingle ptr offset = MkIO (\w => prim_io_return (prim__peekSingle (world w) ptr offset))

363+

364+||| Single precision floats are marshalled to Doubles

365+prim_pokeSingle : Ptr -> Int -> Double -> IO Int

366+prim_pokeSingle ptr offset val = MkIO (\w => prim_io_return (

367+ prim__pokeSingle (world w) ptr offset val))

rts/idris_rts.c+18

@@ -464,6 +464,24 @@ VAL idris_pokePtr(VAL ptr, VAL offset, VAL data) {

464 return MKINT(0);

465}

466

467+VAL idris_peekDouble(VM* vm, VAL ptr, VAL offset) {

468+ return MKFLOAT(vm, *(double*)(GETPTR(ptr) + GETINT(offset)));

469+}

470+

471+VAL idris_pokeDouble(VAL ptr, VAL offset, VAL data) {

472+ *(double*)(GETPTR(ptr) + GETINT(offset)) = GETFLOAT(data);

473+ return MKINT(0);

474+}

475+

476+VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset) {

477+ return MKFLOAT(vm, *(float*)(GETPTR(ptr) + GETINT(offset)));

478+}

479+

480+VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data) {

481+ *(float*)(GETPTR(ptr) + GETINT(offset)) = GETFLOAT(data);

482+ return MKINT(0);

483+}

484+

467void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size) {

485void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size) {

468 memmove(dest + dest_offset, src + src_offset, size);

486 memmove(dest + dest_offset, src + src_offset, size);

469}

487}

rts/idris_rts.h+4

@@ -348,6 +348,10 @@ void idris_poke(void* ptr, i_int offset, uint8_t data);

348

349VAL idris_peekPtr(VM* vm, VAL ptr, VAL offset);

350VAL idris_pokePtr(VAL ptr, VAL offset, VAL data);

351+VAL idris_peekDouble(VM* vm, VAL ptr, VAL offset);

352+VAL idris_pokeDouble(VAL ptr, VAL offset, VAL data);

353+VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset);

354+VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data);

351

355

352// String primitives

356// String primitives

353VAL idris_concat(VM* vm, VAL l, VAL r);

357VAL idris_concat(VM* vm, VAL l, VAL r);

src/IRTS/CodegenC.hs+8

@@ -653,6 +653,14 @@ doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peekPtr"

653 = v ++ "idris_peekPtr(vm," ++ creg p ++ "," ++ creg o ++")"

654doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokePtr"

655 = v ++ "idris_pokePtr(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"

656+doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokeDouble"

657+ = v ++ "idris_pokeDouble(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"

658+doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peekDouble"

659+ = v ++ "idris_peekDouble(vm," ++ creg p ++ "," ++ creg o ++")"

660+doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokeSingle"

661+ = v ++ "idris_pokeSingle(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"

662+doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peekSingle"

663+ = v ++ "idris_peekSingle(vm," ++ creg p ++ "," ++ creg o ++")"

656doOp v (LExternal pk) [] | pk == sUN "prim__sizeofPtr"

664doOp v (LExternal pk) [] | pk == sUN "prim__sizeofPtr"

657 = v ++ "MKINT(sizeof(void*))"

665 = v ++ "MKINT(sizeof(void*))"

658doOp v (LExternal mpt) [p] | mpt == sUN "prim__asPtr" = v ++ "MKPTR(vm, GETMPTR("++ creg p ++"))"

666doOp v (LExternal mpt) [p] | mpt == sUN "prim__asPtr" = v ++ "MKPTR(vm, GETMPTR("++ creg p ++"))"