git.iko.soy/Idris-dev
on master help sign in
wip
2d3bbccNiklas Larsson
libs/contrib/CFFI/Memory.idr+23−13
compare with master
unifiedsplit
@@ -30,20 +30,30 @@ alloc t = return $ CPt !(malloc (sizeOf t)) 0 t
30free : CPtr -> IO ()
30free : CPtr -> IO ()
31free (CPt p _ _) = mfree p
31free (CPt p _ _) = mfree p
32
32
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+
33ctype : CPtr -> CType
43ctype : CPtr -> CType
34ctype (CPt _ _ t) = t
44ctype (CPt _ _ t) = t
35mutual
45mutual
36− peekArray : (c : CPtr) -> IO (translate (ctype c))
46+ -- peekArray : (c : CPtr) -> IO (translate (ctype c))
37− peekArray (CPt p o a@(ARRAY n t)) = do
47+ -- peekArray (CPt p o a@(ARRAY n t)) = do
38− os <- return $ fromList (offsets a)
48+ -- os <- return $ fromList (offsets a)
39− return $ map (\x => peek (CPt p x t)) os
49+ -- map (\x => peek (CPt p x t)) os
40−
50+
41− pokeArray : (c : CPtr) -> translate (ctype c) -> IO ()
51+ -- pokeArray : (c : CPtr) -> translate (ctype c) -> IO ()
42− pokeArray (CPt p o a@(ARRAY n t)) x = do
52+ -- pokeArray (CPt p o a@(ARRAY n t)) x = do
43− os <- fromList $ offsets a
53+ -- os <- fromList $ offsets a
44− ox <- zip os x
54+ -- ox <- zip os x
45− map (\(x, y)=>poke (CPt p x t) y) ox
55+ -- map (\(x, y)=>poke (CPt p x t) y) ox
46− return ()
56+ -- return ()
47
57
48 peek : (p : CPtr) -> IO (translate (ctype p))
58 peek : (p : CPtr) -> IO (translate (ctype p))
49 peek (CPt p o I8) = prim_peek8 p o
59 peek (CPt p o I8) = prim_peek8 p o
@@ -53,7 +63,7 @@ mutual
53 peek (CPt p o FLOAT) = prim_peekSingle p o
63 peek (CPt p o FLOAT) = prim_peekSingle p o
54 peek (CPt p o DOUBLE) = prim_peekDouble p o
64 peek (CPt p o DOUBLE) = prim_peekDouble p o
55 peek (CPt p o PTR) = prim_peekPtr p o
65 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
57 -- peek (CPt p o (UNION xs)) = ?peekUnion
67 -- peek (CPt p o (UNION xs)) = ?peekUnion
58 -- peek (CPt p o (STRUCT xs)) = ?peekStruct
68 -- peek (CPt p o (STRUCT xs)) = ?peekStruct
59 -- peek (CPt p o (PACKEDSTRUCT xs)) = ?peekPacked
69 -- peek (CPt p o (PACKEDSTRUCT xs)) = ?peekPacked
@@ -74,7 +84,7 @@ mutual
74 return ()
84 return ()
75 poke (CPt p o DOUBLE) x = do _ <- prim_pokeDouble p o x
85 poke (CPt p o DOUBLE) x = do _ <- prim_pokeDouble p o x
76 return ()
86 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
78 -- poke (CPt p o (UNION xs)) x = ?pokeUnion
88 -- poke (CPt p o (UNION xs)) x = ?pokeUnion
79 -- poke (CPt p o (STRUCT xs)) x = ?pokeStruct
89 -- poke (CPt p o (STRUCT xs)) x = ?pokeStruct
80 -- poke (CPt p o (PACKEDSTRUCT xs)) x = ?pokePacked
90 -- 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 @@
1#include "ffi008.h"
1#include "ffi008.h"
2+#include <stdio.h>
2
3
3int size1(void) {
4int size1(void) {
4 return sizeof(struct test1);
5 return sizeof(struct test1);
@@ -7,3 +8,7 @@ int size1(void) {
7int size2(void) {
8int size2(void) {
8 return sizeof(struct test2);
9 return sizeof(struct test2);
9}
10}
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 {
10 int16_t b;
10 int16_t b;
11};
11};
12
12
13+struct test2 mystruct;
14+
13int size1(void);
15int size1(void);
14int size2(void);
16int size2(void);
17+void print_mystruct();
test/ffi008/ffi008.idr+20−3
@@ -12,6 +12,12 @@ size1 = foreign FFI_C "size1" (IO Int)
12size2 : IO Int
12size2 : IO Int
13size2 = foreign FFI_C "size2" (IO Int)
13size2 = foreign FFI_C "size2" (IO Int)
14
14
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+
15test1 : CType
21test1 : CType
16test1 = STRUCT [I8, I64]
22test1 = STRUCT [I8, I64]
17
23
@@ -19,16 +25,27 @@ test2 : CType
19test2 = STRUCT [I32, I16]
25test2 = STRUCT [I32, I16]
20
26
21test3 : CType
27test3 : CType
22−test3 = STRUCT [I8, I8, I8, I64]
28+test3 = STRUCT [DOUBLE, DOUBLE, I8, I64]
23
29
24test4 : CType
30test4 : CType
25test4 = PACKEDSTRUCT [I8, I8, I8, I64]
31test4 = PACKEDSTRUCT [I8, I8, I8, I64]
26
32
27printMore : IO ()
33printMore : IO ()
28printMore = do
34printMore = do
29− p <- alloc I8
35+ p <- alloc test3
30− a <- get p
36+ f3 <- return $ p # 1
37+ a <- peek f3
38+ printLn p
39+ printLn f3
31 free p
40 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
32 printLn !size1
49 printLn !size1
33 printLn !size2
50 printLn !size2
34 printLn $ fields test3
51 printLn $ fields test3