git.iko.soy/Idris-dev
on master help sign in
Update export qualifiers.
85fde4cMatus Tejiscak
test/primitives006/Data/ByteArray.idr+14−14
compare with master
unifiedsplit
@@ -3,7 +3,7 @@ module Data.ByteArray
3%include C "array.h"
3%include C "array.h"
4%link C "array.o"
4%link C "array.o"
5
5
6−%access public
6+%access public export
7%default total
7%default total
8
8
9namespace Byte
9namespace Byte
@@ -16,82 +16,82 @@ namespace Byte
16 fromInt : Int -> Byte
16 fromInt : Int -> Byte
17 fromInt = prim__truncInt_B8
17 fromInt = prim__truncInt_B8
18
18
19−abstract
19+export
20record ByteArray where
20record ByteArray where
21 constructor BA
21 constructor BA
22 ptr : CData
22 ptr : CData
23 sz : Int
23 sz : Int
24
24
25-- This needn't be precise; it just needs to be enough to be safe.
25-- This needn't be precise; it just needs to be enough to be safe.
26−abstract
26+export
27bytesPerInt : Int
27bytesPerInt : Int
28bytesPerInt = 8
28bytesPerInt = 8
29
29
30−abstract
30+export
31allocate : Int -> IO ByteArray
31allocate : Int -> IO ByteArray
32allocate sz = do
32allocate sz = do
33 ptr <- foreign FFI_C "array_alloc" (Int -> IO CData) sz
33 ptr <- foreign FFI_C "array_alloc" (Int -> IO CData) sz
34 return $ BA ptr sz
34 return $ BA ptr sz
35
35
36−abstract
36+export
37reallocate : Int -> ByteArray -> IO ()
37reallocate : Int -> ByteArray -> IO ()
38reallocate newSz (BA ptr sz)
38reallocate newSz (BA ptr sz)
39 = foreign FFI_C "array_realloc" (Int -> CData -> IO ()) sz ptr
39 = foreign FFI_C "array_realloc" (Int -> CData -> IO ()) sz ptr
40
40
41−abstract
41+export
42peek : Int -> ByteArray -> IO Byte
42peek : Int -> ByteArray -> IO Byte
43peek ofs (BA ptr sz)
43peek ofs (BA ptr sz)
44 = if (ofs < 0 || ofs >= sz)
44 = if (ofs < 0 || ofs >= sz)
45 then return 0
45 then return 0
46 else foreign FFI_C "array_peek" (Int -> CData -> IO Byte) ofs ptr
46 else foreign FFI_C "array_peek" (Int -> CData -> IO Byte) ofs ptr
47
47
48−abstract
48+export
49peekInt : Int -> ByteArray -> IO Int
49peekInt : Int -> ByteArray -> IO Int
50peekInt ofs (BA ptr sz)
50peekInt ofs (BA ptr sz)
51 = if (ofs < 0 || ofs+bytesPerInt > sz)
51 = if (ofs < 0 || ofs+bytesPerInt > sz)
52 then return 0
52 then return 0
53 else foreign FFI_C "array_peek_int" (Int -> CData -> IO Int) ofs ptr
53 else foreign FFI_C "array_peek_int" (Int -> CData -> IO Int) ofs ptr
54
54
55−abstract
55+export
56poke : Int -> Byte -> ByteArray -> IO ()
56poke : Int -> Byte -> ByteArray -> IO ()
57poke ofs b (BA ptr sz)
57poke ofs b (BA ptr sz)
58 = if (ofs < 0 || ofs >= sz)
58 = if (ofs < 0 || ofs >= sz)
59 then return ()
59 then return ()
60 else foreign FFI_C "array_poke" (Int -> Byte -> CData -> IO ()) ofs b ptr
60 else foreign FFI_C "array_poke" (Int -> Byte -> CData -> IO ()) ofs b ptr
61
61
62−abstract
62+export
63pokeInt : Int -> Int -> ByteArray -> IO ()
63pokeInt : Int -> Int -> ByteArray -> IO ()
64pokeInt ofs i (BA ptr sz)
64pokeInt ofs i (BA ptr sz)
65 = if (ofs < 0 || ofs+bytesPerInt > sz)
65 = if (ofs < 0 || ofs+bytesPerInt > sz)
66 then return ()
66 then return ()
67 else foreign FFI_C "array_poke_int" (Int -> Int -> CData -> IO ()) ofs i ptr
67 else foreign FFI_C "array_poke_int" (Int -> Int -> CData -> IO ()) ofs i ptr
68
68
69−abstract
69+export
70copy : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO ()
70copy : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO ()
71copy (BA srcPtr srcSz, srcIx) (BA dstPtr dstSz, dstIx) count
71copy (BA srcPtr srcSz, srcIx) (BA dstPtr dstSz, dstIx) count
72 = if (srcIx < 0 || dstIx < 0 || (srcIx+count) > srcSz || (dstIx+count) > dstSz)
72 = if (srcIx < 0 || dstIx < 0 || (srcIx+count) > srcSz || (dstIx+count) > dstSz)
73 then return ()
73 then return ()
74 else foreign FFI_C "array_copy" (CData -> Int -> CData -> Int -> Int -> IO ()) srcPtr srcIx dstPtr dstIx count
74 else foreign FFI_C "array_copy" (CData -> Int -> CData -> Int -> Int -> IO ()) srcPtr srcIx dstPtr dstIx count
75
75
76−abstract
76+export
77fill : Int -> Int -> Byte -> ByteArray -> IO ()
77fill : Int -> Int -> Byte -> ByteArray -> IO ()
78fill ofs count b (BA ptr sz)
78fill ofs count b (BA ptr sz)
79 = if (ofs < 0 || ofs+count > sz)
79 = if (ofs < 0 || ofs+count > sz)
80 then return ()
80 then return ()
81 else foreign FFI_C "array_fill" (Int -> Int -> Byte -> CData -> IO ()) ofs count b ptr
81 else foreign FFI_C "array_fill" (Int -> Int -> Byte -> CData -> IO ()) ofs count b ptr
82
82
83−abstract
83+export
84size : ByteArray -> Int
84size : ByteArray -> Int
85size (BA ptr sz) = sz
85size (BA ptr sz) = sz
86
86
87−abstract
87+export
88compare : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO Int
88compare : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO Int
89compare (BA ptrL szL, ofsL) (BA ptrR szR, ofsR) count
89compare (BA ptrL szL, ofsL) (BA ptrR szR, ofsR) count
90 = if (ofsL < 0 || ofsL+count > szL || ofsR < 0 || ofsR+count > szR)
90 = if (ofsL < 0 || ofsL+count > szL || ofsR < 0 || ofsR+count > szR)
91 then return 0
91 then return 0
92 else foreign FFI_C "array_compare" (CData -> Int -> CData -> Int -> Int -> IO Int) ptrL ofsL ptrR ofsR count
92 else foreign FFI_C "array_compare" (CData -> Int -> CData -> Int -> Int -> IO Int) ptrL ofsL ptrR ofsR count
93
93
94−abstract
94+export
95find : Byte -> ByteArray -> Int -> Int -> IO (Maybe Int)
95find : Byte -> ByteArray -> Int -> Int -> IO (Maybe Int)
96find b (BA ptr sz) ofs end = do
96find b (BA ptr sz) ofs end = do
97 ofs <- foreign FFI_C "array_find" (Byte -> CData -> Int -> Int -> IO Int) b ptr ofs end
97 ofs <- foreign FFI_C "array_find" (Byte -> CData -> Int -> Int -> IO Int) b ptr ofs end
test/primitives006/Data/Bytes.idr+28−9
@@ -2,7 +2,7 @@ module Data.Bytes
2
2
3import Data.ByteArray as BA
3import Data.ByteArray as BA
4
4
5−%access public
5+%access public export
6%default total
6%default total
7
7
8-- Structure of the allocated ByteArray
8-- Structure of the allocated ByteArray
@@ -10,7 +10,7 @@ import Data.ByteArray as BA
10-- used_size is an int and it takes up BA.bytesPerInt bytes
10-- used_size is an int and it takes up BA.bytesPerInt bytes
11-- at the beginning of the array
11-- at the beginning of the array
12
12
13−abstract
13+export
14record Bytes where
14record Bytes where
15 constructor B
15 constructor B
16 arr : ByteArray
16 arr : ByteArray
@@ -32,15 +32,15 @@ allocate capacity = do
32 BA.fill dataOfs capacity 0 arr -- zero the array
32 BA.fill dataOfs capacity 0 arr -- zero the array
33 return $ B arr dataOfs dataOfs
33 return $ B arr dataOfs dataOfs
34
34
35−abstract
35+export
36length : Bytes -> Int
36length : Bytes -> Int
37length (B arr ofs end) = end - ofs
37length (B arr ofs end) = end - ofs
38
38
39−abstract
39+export
40empty : Bytes
40empty : Bytes
41empty = unsafePerformIO $ allocate minimalCapacity
41empty = unsafePerformIO $ allocate minimalCapacity
42
42
43−abstract
43+export
44null : Bytes -> Bool
44null : Bytes -> Bool
45null (B arr ofs end) = (ofs == end)
45null (B arr ofs end) = (ofs == end)
46
46
@@ -62,7 +62,7 @@ grow factor (B arr ofs end) = do
62 return $ B arr' ofs' (ofs' + bytesUsed)
62 return $ B arr' ofs' (ofs' + bytesUsed)
63
63
64%assert_total
64%assert_total
65−abstract
65+export
66snoc : Bytes -> Byte -> Bytes
66snoc : Bytes -> Byte -> Bytes
67snoc bs@(B arr ofs end) byte
67snoc bs@(B arr ofs end) byte
68 = if end >= BA.size arr
68 = if end >= BA.size arr
@@ -81,6 +81,7 @@ snoc bs@(B arr ofs end) byte
81 return $ B arr ofs (end+1)
81 return $ B arr ofs (end+1)
82
82
83infixl 7 |>
83infixl 7 |>
84+export
84(|>) : Bytes -> Byte -> Bytes
85(|>) : Bytes -> Byte -> Bytes
85(|>) = snoc
86(|>) = snoc
86
87
@@ -89,7 +90,7 @@ namespace SnocView
89 Nil : SnocView
90 Nil : SnocView
90 Snoc : (bs : Bytes) -> (b : Byte) -> SnocView
91 Snoc : (bs : Bytes) -> (b : Byte) -> SnocView
91
92
92− abstract
93+ export
93 snocView : Bytes -> SnocView
94 snocView : Bytes -> SnocView
94 snocView (B arr ofs end) =
95 snocView (B arr ofs end) =
95 if end == ofs
96 if end == ofs
@@ -103,7 +104,7 @@ namespace ConsView
103 Nil : ConsView
104 Nil : ConsView
104 Cons : (b : Byte) -> (bs : Bytes) -> ConsView
105 Cons : (b : Byte) -> (bs : Bytes) -> ConsView
105
106
106− abstract
107+ export
107 consView : Bytes -> ConsView
108 consView : Bytes -> ConsView
108 consView (B arr ofs end) =
109 consView (B arr ofs end) =
109 if end == ofs
110 if end == ofs
@@ -114,7 +115,7 @@ namespace ConsView
114
115
115infixr 7 ++
116infixr 7 ++
116%assert_total
117%assert_total
117−abstract
118+export
118(++) : Bytes -> Bytes -> Bytes
119(++) : Bytes -> Bytes -> Bytes
119(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)
120(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)
120 = let countR = endR - ofsR in
121 = let countR = endR - ofsR in
@@ -133,12 +134,15 @@ abstract
133 BA.copy (arrR, ofsR) (arrL, endL) countR
134 BA.copy (arrR, ofsR) (arrL, endL) countR
134 return $ B arrL ofsL (endL + countR)
135 return $ B arrL ofsL (endL + countR)
135
136
137+export
136dropPrefix : Int -> Bytes -> Bytes
138dropPrefix : Int -> Bytes -> Bytes
137dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end
139dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end
138
140
141+export
139takePrefix : Int -> Bytes -> Bytes
142takePrefix : Int -> Bytes -> Bytes
140takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)
143takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)
141
144
145+export
142pack : List Byte -> Bytes
146pack : List Byte -> Bytes
143pack = fromList empty
147pack = fromList empty
144 where
148 where
@@ -146,11 +150,13 @@ pack = fromList empty
146 fromList bs [] = bs
150 fromList bs [] = bs
147 fromList bs (x :: xs) = fromList (bs `snoc` x) xs
151 fromList bs (x :: xs) = fromList (bs `snoc` x) xs
148
152
153+export
149unpack : Bytes -> List Byte
154unpack : Bytes -> List Byte
150unpack bs with (consView bs)
155unpack bs with (consView bs)
151 | Nil = []
156 | Nil = []
152 | Cons x xs = x :: unpack (assert_smaller bs xs)
157 | Cons x xs = x :: unpack (assert_smaller bs xs)
153
158
159+export
154slice : Int -> Int -> Bytes -> Bytes
160slice : Int -> Int -> Bytes -> Bytes
155slice ofs' end' (B arr ofs end)
161slice ofs' end' (B arr ofs end)
156 = B arr
162 = B arr
@@ -164,6 +170,7 @@ data Result : Type -> Type where
164 Stop : (result : a) -> Result a
170 Stop : (result : a) -> Result a
165 Cont : (acc : a) -> Result a
171 Cont : (acc : a) -> Result a
166
172
173+export
167iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a
174iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a
168iterateR f acc bs with (snocView bs)
175iterateR f acc bs with (snocView bs)
169 | Nil = acc
176 | Nil = acc
@@ -171,6 +178,7 @@ iterateR f acc bs with (snocView bs)
171 | Stop result = result
178 | Stop result = result
172 | Cont acc' = iterateR f acc' (assert_smaller bs ys)
179 | Cont acc' = iterateR f acc' (assert_smaller bs ys)
173
180
181+export
174iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a
182iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a
175iterateL f acc bs with (consView bs)
183iterateL f acc bs with (consView bs)
176 | Nil = acc
184 | Nil = acc
@@ -183,12 +191,15 @@ private
183(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)
191(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)
184(.:) g f x y = g (f x y)
192(.:) g f x y = g (f x y)
185
193
194+export
186foldr : (Byte -> a -> a) -> a -> Bytes -> a
195foldr : (Byte -> a -> a) -> a -> Bytes -> a
187foldr f = iterateR (Cont .: f)
196foldr f = iterateR (Cont .: f)
188
197
198+export
189foldl : (a -> Byte -> a) -> a -> Bytes -> a
199foldl : (a -> Byte -> a) -> a -> Bytes -> a
190foldl f = iterateL (Cont .: f)
200foldl f = iterateL (Cont .: f)
191
201
202+export
192spanLength : (Byte -> Bool) -> Bytes -> Int
203spanLength : (Byte -> Bool) -> Bytes -> Int
193spanLength p = iterateL step 0
204spanLength p = iterateL step 0
194 where
205 where
@@ -200,25 +211,31 @@ spanLength p = iterateL step 0
200find : Byte -> Bytes -> Maybe Int
211find : Byte -> Bytes -> Maybe Int
201find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end
212find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end
202
213
214+export
203splitAt : Int -> Bytes -> (Bytes, Bytes)
215splitAt : Int -> Bytes -> (Bytes, Bytes)
204splitAt n bs = (takePrefix n bs, dropPrefix n bs)
216splitAt n bs = (takePrefix n bs, dropPrefix n bs)
205
217
218+export
206splitOn : Byte -> Bytes -> (Bytes, Bytes)
219splitOn : Byte -> Bytes -> (Bytes, Bytes)
207splitOn b bs with (find b bs)
220splitOn b bs with (find b bs)
208 | Nothing = (bs, empty)
221 | Nothing = (bs, empty)
209 | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)
222 | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)
210
223
224+export
211splitsOn : Byte -> Bytes -> List Bytes
225splitsOn : Byte -> Bytes -> List Bytes
212splitsOn b bs with (find b bs)
226splitsOn b bs with (find b bs)
213 | Nothing = [bs]
227 | Nothing = [bs]
214 | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)
228 | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)
215
229
230+export
216asciiLines : Bytes -> List Bytes
231asciiLines : Bytes -> List Bytes
217asciiLines = splitsOn 0x0A
232asciiLines = splitsOn 0x0A
218
233
234+export
219span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
235span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
220span p bs = splitAt (spanLength p bs) bs
236span p bs = splitAt (spanLength p bs) bs
221
237
238+export
222break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
239break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
223break p bs = span (not . p) bs
240break p bs = span (not . p) bs
224
241
@@ -244,9 +261,11 @@ implementation Eq Bytes where
244implementation Ord Bytes where
261implementation Ord Bytes where
245 compare = Bytes.cmp
262 compare = Bytes.cmp
246
263
264+export
247toString : Bytes -> String
265toString : Bytes -> String
248toString = foldr (strCons . chr . toInt) ""
266toString = foldr (strCons . chr . toInt) ""
249
267
268+export
250fromString : String -> Bytes
269fromString : String -> Bytes
251fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack
270fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack
252
271