e4a16c7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add a little documentation

Make some stuff private

commite4a16c7630a3f812a0b5898164c802ced618d801 authorNiklas Larsson <niklas@mm.st> dateMon 7 Mar 2016, 14:17 (11 years ago) parent3f8b424

2 files changed+31−3

compare with master

unifiedsplit

libs/contrib/CFFI/Memory.idr+12−2 libs/contrib/CFFI/Types.idr+19−1

libs/contrib/CFFI/Memory.idr+12−2

@@ -9,33 +9,40 @@ import Data.Vect

99%access public export

1010%default partial

1111

12+

1213data CPtr = CPt Ptr Int

1314

1415implicit toCPtr : Ptr -> CPtr

1516toCPtr p = CPt p 0

1617

18+||| Import of malloc from the C standard library.

1719malloc : Int -> IO Ptr

1820malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size

1921

22+||| Import of free from the C standard library.

2023mfree : Ptr -> IO ()

2124mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr

2225

26+||| Allocate enough memory to hold an instance of a C typr

2327alloc : Composite -> IO CPtr

2428alloc t = return $ CPt !(malloc (sizeOf t)) 0

2529

30+||| Free memory allocated with alloc

2631free : CPtr -> IO ()

2732free (CPt p _ ) = mfree p

2833

34+||| Perform an IO action with memory that is freed afterwards

2935withAlloc : Composite -> (CPtr -> IO ()) -> IO ()

3036withAlloc t f = do m <- alloc t

3137 f m

3238 free m

3339

3440infixl 1 ~~>

35−

41+||| Perform an IO action with memory that is freed afterwards

3642(~~>) : Composite-> (CPtr -> IO ()) -> IO ()

3743(~~>) = withAlloc

3844

45+||| Read from memory

3946peek : (t: CType) -> CPtr -> IO (translate t)

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

4148peek I16 (CPt p o) = prim_peek16 p o

@@ -45,6 +52,7 @@ peek FLOAT (CPt p o) = prim_peekSingle p o

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

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

4754

55+||| Write to memory

4856poke : (t : CType) -> CPtr -> translate t -> IO ()

4957poke I8 (CPt p o) x = do _ <- prim_poke8 p o x

5058 return ()

@@ -61,12 +69,13 @@ poke FLOAT (CPt p o) x = do _ <- prim_pokeSingle p o x

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

6270 return ()

6371

72+||| Update memory with a function.

6473update : (t: CType) -> CPtr -> (translate t -> translate t) -> IO ()

6574update ty cp f = do val <- peek ty cp

6675 out <- return $ f val

6776 poke ty cp out

6877

69−-- TODO : Fix bounds checking

78+||| Get a pointer to a field in a composite value

7079field : Composite -> Nat -> CPtr -> CPtr

7180field arr@(ARRAY n t) i (CPt p o ) = CPt p (o + offset arr i)

7281field un@(UNION xs) i (CPt p o ) = CPt p o

@@ -76,5 +85,6 @@ field (T t) Z p = p

7685

7786infixl 10 #

7887

88+||| Get a pointer to a field in a composite value

7989(#) : Composite -> Nat -> CPtr -> CPtr

8090(#) = field

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

@@ -15,6 +15,7 @@ data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR

1515data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)

1616 | PACKEDSTRUCT (List Composite)

1717

18+||| Implicit conversion of primitive C types to composites

1819implicit mkComposite : CType -> Composite

1920mkComposite x = T x

2021

@@ -34,6 +35,7 @@ Show Composite where

3435 show (UNION xs) = "UNION " ++ show xs

3536 show (PACKEDSTRUCT xs) = "PACKEDSTRUCT " ++ show xs

3637

38+||| What Idris type the C type is marshalled to

3739translate : CType -> Type

3840translate I8 = Bits8

3941translate I16 = Bits16

@@ -44,6 +46,7 @@ translate DOUBLE = Double

4446translate PTR = Ptr

4547

4648mutual

49+ private

4750 sizeOfCT : CType -> Int

4851 sizeOfCT I8 = 1

4952 sizeOfCT I16 = 2

@@ -53,6 +56,8 @@ mutual

5356 sizeOfCT DOUBLE = 8

5457 sizeOfCT PTR = prim__sizeofPtr

5558

59+ ||| Size of value of the type in bytes

60+ export

5661 sizeOf : Composite -> Int

5762 sizeOf (T ct) = sizeOfCT ct

5863 sizeOf (ARRAY n t) = n * sizeOf t

@@ -60,6 +65,7 @@ mutual

6065 sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs

6166 sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs

6267

68+ private

6369 alignOfCT : CType -> Int

6470 alignOfCT I8 = 1

6571 alignOfCT I16 = 2

@@ -69,6 +75,8 @@ mutual

6975 alignOfCT DOUBLE = prim__sizeofPtr

7076 alignOfCT PTR = prim__sizeofPtr

7177

78+ ||| Alignment requirement of the type

79+ export

7280 alignOf : Composite -> Int

7381 alignOf (T t) = alignOfCT t

7482 alignOf (ARRAY n t) = alignOf t

@@ -76,12 +84,15 @@ mutual

7684 alignOf (UNION xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs

7785 alignOf (PACKEDSTRUCT xs) = 1

7886

87+ private

7988 pad : Int -> Int -> Int

8089 pad pos align = let c = pos `mod` align in if c == 0 then 0 else align - c

8190

91+ private

8292 nextOffset : Composite -> Int -> Int

8393 nextOffset ty pos = pos + pad pos (alignOf ty)

8494

95+ private

8596 offsetsStruct : List Composite -> List Int

8697 offsetsStruct xs = offsets' xs 0

8798 where

@@ -89,6 +100,7 @@ mutual

89100 offsets' [] _ = []

90101 offsets' (x::xs) pos = (nextOffset x pos)::(offsets' xs (nextOffset x pos + sizeOf x))

91102

103+ private

92104 sizeOfStruct : List Composite -> Int

93105 sizeOfStruct xs = sizeStruct' xs 0 1

94106 where

@@ -97,6 +109,8 @@ mutual

97109 sizeStruct' (x::xs) pos maxAlign = sizeStruct' xs (nextOffset x pos + sizeOf x)

98110 (max maxAlign (alignOf x))

99111

112+||| Number of fields in a composite type

113+export

100114fields : Composite -> Nat

101115fields (STRUCT xs) = length xs

102116fields (PACKEDSTRUCT xs) = length xs

@@ -104,6 +118,7 @@ fields (UNION xs) = length xs

104118fields (ARRAY n _) = toNat n

105119fields (T _) = 1

106120

121+private

107122offsetsPacked : List Composite -> List Int

108123offsetsPacked xs = offsets' xs [] 0

109124 where

@@ -117,6 +132,7 @@ indexOrFail i xs = case index' i xs of

117132 Just x => x

118133 Nothing => error "Out of bounds access"

119134

135+||| The offset of a firld in a composite type

120136export

121137offset : Composite -> Nat -> Int

122138offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)

@@ -124,6 +140,8 @@ offset (PACKEDSTRUCT xs) i = indexOrFail i (offsetsPacked xs)

124140offset (ARRAY _ t) i = sizeOf t * toIntNat i

125141offset (T _) _ = 0

126142

143+||| All offsets of a composite type

144+export

127145offsets : Composite -> List Int

128146offsets (STRUCT xs) = offsetsStruct xs

129147offsets (PACKEDSTRUCT xs) = offsetsPacked xs

@@ -131,7 +149,7 @@ offsets (UNION xs) = replicate (length xs) 0

131149offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]

132150offsets (T _) = [0]

133151

134−

152+||| The type of a field in a composite type.

135153export

136154fieldType : Composite -> Nat -> Composite

137155fieldType (STRUCT xs@(y::_)) i = indexOrFail i xs