85fde4c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Update export qualifiers.

commit85fde4ce6baacab038a6f7487a9e098d017ebce1 authorMatus Tejiscak <ziman@functor.sk> dateFri 12 Feb 2016, 10:45 (11 years ago) parent347fa38

2 files changed+42−23

compare with master

unifiedsplit

test/primitives006/Data/ByteArray.idr+14−14 test/primitives006/Data/Bytes.idr+28−9

test/primitives006/Data/ByteArray.idr+14−14

@@ -3,7 +3,7 @@ module Data.ByteArray

33%include C "array.h"

44%link C "array.o"

6−%access public

6+%access public export

77%default total

99namespace Byte

@@ -16,82 +16,82 @@ namespace Byte

1616 fromInt : Int -> Byte

1717 fromInt = prim__truncInt_B8

1818

19−abstract

19+export

2020record ByteArray where

2121 constructor BA

2222 ptr : CData

2323 sz : Int

2424

2525-- This needn't be precise; it just needs to be enough to be safe.

26−abstract

26+export

2727bytesPerInt : Int

2828bytesPerInt = 8

2929

30−abstract

30+export

3131allocate : Int -> IO ByteArray

3232allocate sz = do

3333 ptr <- foreign FFI_C "array_alloc" (Int -> IO CData) sz

3434 return $ BA ptr sz

3535

36−abstract

36+export

3737reallocate : Int -> ByteArray -> IO ()

3838reallocate newSz (BA ptr sz)

3939 = foreign FFI_C "array_realloc" (Int -> CData -> IO ()) sz ptr

4040

41−abstract

41+export

4242peek : Int -> ByteArray -> IO Byte

4343peek ofs (BA ptr sz)

4444 = if (ofs < 0 || ofs >= sz)

4545 then return 0

4646 else foreign FFI_C "array_peek" (Int -> CData -> IO Byte) ofs ptr

4747

48−abstract

48+export

4949peekInt : Int -> ByteArray -> IO Int

5050peekInt ofs (BA ptr sz)

5151 = if (ofs < 0 || ofs+bytesPerInt > sz)

5252 then return 0

5353 else foreign FFI_C "array_peek_int" (Int -> CData -> IO Int) ofs ptr

5454

55−abstract

55+export

5656poke : Int -> Byte -> ByteArray -> IO ()

5757poke ofs b (BA ptr sz)

5858 = if (ofs < 0 || ofs >= sz)

5959 then return ()

6060 else foreign FFI_C "array_poke" (Int -> Byte -> CData -> IO ()) ofs b ptr

6161

62−abstract

62+export

6363pokeInt : Int -> Int -> ByteArray -> IO ()

6464pokeInt ofs i (BA ptr sz)

6565 = if (ofs < 0 || ofs+bytesPerInt > sz)

6666 then return ()

6767 else foreign FFI_C "array_poke_int" (Int -> Int -> CData -> IO ()) ofs i ptr

6868

69−abstract

69+export

7070copy : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO ()

7171copy (BA srcPtr srcSz, srcIx) (BA dstPtr dstSz, dstIx) count

7272 = if (srcIx < 0 || dstIx < 0 || (srcIx+count) > srcSz || (dstIx+count) > dstSz)

7373 then return ()

7474 else foreign FFI_C "array_copy" (CData -> Int -> CData -> Int -> Int -> IO ()) srcPtr srcIx dstPtr dstIx count

7575

76−abstract

76+export

7777fill : Int -> Int -> Byte -> ByteArray -> IO ()

7878fill ofs count b (BA ptr sz)

7979 = if (ofs < 0 || ofs+count > sz)

8080 then return ()

8181 else foreign FFI_C "array_fill" (Int -> Int -> Byte -> CData -> IO ()) ofs count b ptr

8282

83−abstract

83+export

8484size : ByteArray -> Int

8585size (BA ptr sz) = sz

8686

87−abstract

87+export

8888compare : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO Int

8989compare (BA ptrL szL, ofsL) (BA ptrR szR, ofsR) count

9090 = if (ofsL < 0 || ofsL+count > szL || ofsR < 0 || ofsR+count > szR)

9191 then return 0

9292 else foreign FFI_C "array_compare" (CData -> Int -> CData -> Int -> Int -> IO Int) ptrL ofsL ptrR ofsR count

9393

94−abstract

94+export

9595find : Byte -> ByteArray -> Int -> Int -> IO (Maybe Int)

9696find b (BA ptr sz) ofs end = do

9797 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

33import Data.ByteArray as BA

5−%access public

5+%access public export

66%default total

88-- Structure of the allocated ByteArray

@@ -10,7 +10,7 @@ import Data.ByteArray as BA

1010-- used_size is an int and it takes up BA.bytesPerInt bytes

1111-- at the beginning of the array

1212

13−abstract

13+export

1414record Bytes where

1515 constructor B

1616 arr : ByteArray

@@ -32,15 +32,15 @@ allocate capacity = do

3232 BA.fill dataOfs capacity 0 arr -- zero the array

3333 return $ B arr dataOfs dataOfs

3434

35−abstract

35+export

3636length : Bytes -> Int

3737length (B arr ofs end) = end - ofs

3838

39−abstract

39+export

4040empty : Bytes

4141empty = unsafePerformIO $ allocate minimalCapacity

4242

43−abstract

43+export

4444null : Bytes -> Bool

4545null (B arr ofs end) = (ofs == end)

4646

@@ -62,7 +62,7 @@ grow factor (B arr ofs end) = do

6262 return $ B arr' ofs' (ofs' + bytesUsed)

6363

6464%assert_total

65−abstract

65+export

6666snoc : Bytes -> Byte -> Bytes

6767snoc bs@(B arr ofs end) byte

6868 = if end >= BA.size arr

@@ -81,6 +81,7 @@ snoc bs@(B arr ofs end) byte

8181 return $ B arr ofs (end+1)

8282

8383infixl 7 |>

84+export

8485(|>) : Bytes -> Byte -> Bytes

8586(|>) = snoc

8687

@@ -89,7 +90,7 @@ namespace SnocView

8990 Nil : SnocView

9091 Snoc : (bs : Bytes) -> (b : Byte) -> SnocView

9192

92− abstract

93+ export

9394 snocView : Bytes -> SnocView

9495 snocView (B arr ofs end) =

9596 if end == ofs

@@ -103,7 +104,7 @@ namespace ConsView

103104 Nil : ConsView

104105 Cons : (b : Byte) -> (bs : Bytes) -> ConsView

105106

106− abstract

107+ export

107108 consView : Bytes -> ConsView

108109 consView (B arr ofs end) =

109110 if end == ofs

@@ -114,7 +115,7 @@ namespace ConsView

114115

115116infixr 7 ++

116117%assert_total

117−abstract

118+export

118119(++) : Bytes -> Bytes -> Bytes

119120(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)

120121 = let countR = endR - ofsR in

@@ -133,12 +134,15 @@ abstract

133134 BA.copy (arrR, ofsR) (arrL, endL) countR

134135 return $ B arrL ofsL (endL + countR)

135136

137+export

136138dropPrefix : Int -> Bytes -> Bytes

137139dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end

138140

141+export

139142takePrefix : Int -> Bytes -> Bytes

140143takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)

141144

145+export

142146pack : List Byte -> Bytes

143147pack = fromList empty

144148 where

@@ -146,11 +150,13 @@ pack = fromList empty

146150 fromList bs [] = bs

147151 fromList bs (x :: xs) = fromList (bs `snoc` x) xs

148152

153+export

149154unpack : Bytes -> List Byte

150155unpack bs with (consView bs)

151156 | Nil = []

152157 | Cons x xs = x :: unpack (assert_smaller bs xs)

153158

159+export

154160slice : Int -> Int -> Bytes -> Bytes

155161slice ofs' end' (B arr ofs end)

156162 = B arr

@@ -164,6 +170,7 @@ data Result : Type -> Type where

164170 Stop : (result : a) -> Result a

165171 Cont : (acc : a) -> Result a

166172

173+export

167174iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a

168175iterateR f acc bs with (snocView bs)

169176 | Nil = acc

@@ -171,6 +178,7 @@ iterateR f acc bs with (snocView bs)

171178 | Stop result = result

172179 | Cont acc' = iterateR f acc' (assert_smaller bs ys)

173180

181+export

174182iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a

175183iterateL f acc bs with (consView bs)

176184 | Nil = acc

@@ -183,12 +191,15 @@ private

183191(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)

184192(.:) g f x y = g (f x y)

185193

194+export

186195foldr : (Byte -> a -> a) -> a -> Bytes -> a

187196foldr f = iterateR (Cont .: f)

188197

198+export

189199foldl : (a -> Byte -> a) -> a -> Bytes -> a

190200foldl f = iterateL (Cont .: f)

191201

202+export

192203spanLength : (Byte -> Bool) -> Bytes -> Int

193204spanLength p = iterateL step 0

194205 where

@@ -200,25 +211,31 @@ spanLength p = iterateL step 0

200211find : Byte -> Bytes -> Maybe Int

201212find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end

202213

214+export

203215splitAt : Int -> Bytes -> (Bytes, Bytes)

204216splitAt n bs = (takePrefix n bs, dropPrefix n bs)

205217

218+export

206219splitOn : Byte -> Bytes -> (Bytes, Bytes)

207220splitOn b bs with (find b bs)

208221 | Nothing = (bs, empty)

209222 | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)

210223

224+export

211225splitsOn : Byte -> Bytes -> List Bytes

212226splitsOn b bs with (find b bs)

213227 | Nothing = [bs]

214228 | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)

215229

230+export

216231asciiLines : Bytes -> List Bytes

217232asciiLines = splitsOn 0x0A

218233

234+export

219235span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)

220236span p bs = splitAt (spanLength p bs) bs

221237

238+export

222239break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)

223240break p bs = span (not . p) bs

224241

@@ -244,9 +261,11 @@ implementation Eq Bytes where

244261implementation Ord Bytes where

245262 compare = Bytes.cmp

246263

264+export

247265toString : Bytes -> String

248266toString = foldr (strCons . chr . toInt) ""

249267

268+export

250269fromString : String -> Bytes

251270fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack

252271