2d3bbcc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

wip

commit2d3bbccaa2684748c8173f179322feabbdab6e91 authorNiklas Larsson <niklas@mm.st> dateSun 14 Feb 2016, 02:01 (11 years ago) parentd82f489

5 files changed+51−29

compare with master

unifiedsplit

libs/contrib/CFFI/Memory.idr+23−13 libs/contrib/Data/HList.idr−13 test/ffi008/ffi008.c+5 test/ffi008/ffi008.h+3 test/ffi008/ffi008.idr+20−3

libs/contrib/CFFI/Memory.idr+23−13

@@ -30,20 +30,30 @@ alloc t = return $ CPt !(malloc (sizeOf t)) 0 t

3030free : CPtr -> IO ()

3131free (CPt p _ _) = mfree p

3232

33+withAlloc : CType -> (CPtr -> IO ()) -> IO ()

34+withAlloc t f = do m <- alloc t

35+ f m

36+ free m

37+

38+infixl 1 ~~>

39+

40+(~~>) : CType -> (CPtr -> IO ()) -> IO ()

41+(~~>) = withAlloc

42+

3343ctype : CPtr -> CType

3444ctype (CPt _ _ t) = t

3545mutual

36− peekArray : (c : CPtr) -> IO (translate (ctype c))

37− peekArray (CPt p o a@(ARRAY n t)) = do

38− os <- return $ fromList (offsets a)

39− return $ map (\x => peek (CPt p x t)) os

40−

41− pokeArray : (c : CPtr) -> translate (ctype c) -> IO ()

42− pokeArray (CPt p o a@(ARRAY n t)) x = do

43− os <- fromList $ offsets a

44− ox <- zip os x

45− map (\(x, y)=>poke (CPt p x t) y) ox

46− return ()

46+ -- peekArray : (c : CPtr) -> IO (translate (ctype c))

47+ -- peekArray (CPt p o a@(ARRAY n t)) = do

48+ -- os <- return $ fromList (offsets a)

49+ -- map (\x => peek (CPt p x t)) os

50+

51+ -- pokeArray : (c : CPtr) -> translate (ctype c) -> IO ()

52+ -- pokeArray (CPt p o a@(ARRAY n t)) x = do

53+ -- os <- fromList $ offsets a

54+ -- ox <- zip os x

55+ -- map (\(x, y)=>poke (CPt p x t) y) ox

56+ -- return ()

4757

4858 peek : (p : CPtr) -> IO (translate (ctype p))

4959 peek (CPt p o I8) = prim_peek8 p o

@@ -53,7 +63,7 @@ mutual

5363 peek (CPt p o FLOAT) = prim_peekSingle p o

5464 peek (CPt p o DOUBLE) = prim_peekDouble p o

5565 peek (CPt p o PTR) = prim_peekPtr p o

56− peek cp@(CPt p o (ARRAY n t)) = peekArray cp

66+ -- peek cp@(CPt p o (ARRAY n t)) = peekArray cp

5767 -- peek (CPt p o (UNION xs)) = ?peekUnion

5868 -- peek (CPt p o (STRUCT xs)) = ?peekStruct

5969 -- peek (CPt p o (PACKEDSTRUCT xs)) = ?peekPacked

@@ -74,7 +84,7 @@ mutual

7484 return ()

7585 poke (CPt p o DOUBLE) x = do _ <- prim_pokeDouble p o x

7686 return ()

77− poke cp@(CPt p o (ARRAY n t)) x = pokeArray cp x

87+ -- poke cp@(CPt p o (ARRAY n t)) x = pokeArray cp x

7888 -- poke (CPt p o (UNION xs)) x = ?pokeUnion

7989 -- poke (CPt p o (STRUCT xs)) x = ?pokeStruct

8090 -- poke (CPt p o (PACKEDSTRUCT xs)) x = ?pokePacked

libs/contrib/Data/HList.idrdeleted−13

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

1−||| A heterogenous list

2−module Data.HList

3−

4−%access public export

5−

6−data HList : List Type -> Type where

7− Nil : HList []

8− (::) : a -> HList xs -> HList (a :: xs)

9−

10−||| Extract an element from an HList

11−index : (i : Nat) -> HList ts -> {auto ok : InBounds i ts } -> List.index i ts

12−index Z (x::xs) {ok} = x

13−index (S j) (x::xs) {ok = InLater p}= index j xs

test/ffi008/ffi008.c+5

@@ -1,4 +1,5 @@

11#include "ffi008.h"

2+#include <stdio.h>

34int size1(void) {

45 return sizeof(struct test1);

@@ -7,3 +8,7 @@ int size1(void) {

78int size2(void) {

89 return sizeof(struct test2);

910}

11+

12+void print_mystruct(void) {

13+ printf("a: %d b: %d\n", mystruct.a, mystruct.b);

14+}

test/ffi008/ffi008.h+3

@@ -10,5 +10,8 @@ struct test2 {

1010 int16_t b;

1111};

1212

13+struct test2 mystruct;

14+

1315int size1(void);

1416int size2(void);

17+void print_mystruct();

test/ffi008/ffi008.idr+20−3

@@ -12,6 +12,12 @@ size1 = foreign FFI_C "size1" (IO Int)

1212size2 : IO Int

1313size2 = foreign FFI_C "size2" (IO Int)

1414

15+mystruct : IO Ptr

16+mystruct = foreign FFI_C "&mystruct" (IO Ptr)

17+

18+print_mystruct : IO ()

19+print_mystruct = foreign FFI_C "print_mystruct" (IO ())

20+

1521test1 : CType

1622test1 = STRUCT [I8, I64]

1723

@@ -19,16 +25,27 @@ test2 : CType

1925test2 = STRUCT [I32, I16]

2026

2127test3 : CType

22−test3 = STRUCT [I8, I8, I8, I64]

28+test3 = STRUCT [DOUBLE, DOUBLE, I8, I64]

2329

2430test4 : CType

2531test4 = PACKEDSTRUCT [I8, I8, I8, I64]

2632

2733printMore : IO ()

2834printMore = do

29− p <- alloc I8

30− a <- get p

35+ p <- alloc test3

36+ f3 <- return $ p # 1

37+ a <- peek f3

38+ printLn p

39+ printLn f3

3140 free p

41+ ms <- mystruct

42+ cms <- return $ CPt ms 0 (STRUCT [I32, I16])

43+ f1 <- return $ cms # 0

44+ printLn f1

45+ prim_poke32 f1 0 122

46+

47+ print_mystruct

48+ printLn test4

3249 printLn !size1

3350 printLn !size2

3451 printLn $ fields test3