@@ -0,0 +1,287 @@
1+module Data.Bytes
2+
3+import Data.ByteArray as BA
4+
5+%access public export
6+%default total
7+
8+-- Structure of the allocated ByteArray
9+-- [used_size][.....data.....]
10+-- used_size is an int and it takes up BA.bytesPerInt bytes
11+-- at the beginning of the array
12+
13+export
14+record Bytes where
15+ constructor B
16+ arr : ByteArray
17+ ofs : Int
18+ end : Int -- first offset not included in the array
19+
20+minimalCapacity : Int
21+minimalCapacity = 16
22+
23+private
24+dataOfs : Int
25+dataOfs = 1 * BA.bytesPerInt
26+
27+private
28+allocate : Int -> IO Bytes
29+allocate capacity = do
30+ arr <- BA.allocate (BA.bytesPerInt + capacity)
31+ BA.pokeInt 0 dataOfs arr
32+ BA.fill dataOfs capacity 0 arr -- zero the array
33+ return $ B arr dataOfs dataOfs
34+
35+export
36+length : Bytes -> Int
37+length (B arr ofs end) = end - ofs
38+
39+export
40+empty : Bytes
41+empty = unsafePerformIO $ allocate minimalCapacity
42+
43+export
44+null : Bytes -> Bool
45+null (B arr ofs end) = (ofs == end)
46+
47+%freeze empty
48+
49+-- factor=1 ~ copy
50+-- factor=2 ~ grow
51+private
52+grow : Int -> Bytes -> IO Bytes
53+grow factor (B arr ofs end) = do
54+ maxUsed <- BA.peekInt 0 arr
55+ let bytesUsed = end - ofs
56+ let bytesAvailable =
57+ if maxUsed > end
58+ then bytesUsed
59+ else BA.size arr - ofs
60+ B arr' ofs' end' <- allocate $ (factor*bytesAvailable) `max` minimalCapacity
61+ BA.copy (arr, ofs) (arr', ofs') bytesUsed
62+ return $ B arr' ofs' (ofs' + bytesUsed)
63+
64+%assert_total
65+export
66+snoc : Bytes -> Byte -> Bytes
67+snoc bs@(B arr ofs end) byte
68+ = if end >= BA.size arr
69+ then unsafePerformIO $ do -- need more space
70+ grown <- grow 2 bs
71+ return $ snoc grown byte
72+ else unsafePerformIO $ do
73+ maxUsed <- BA.peekInt 0 arr
74+ if maxUsed > end
75+ then do -- someone already took the headroom, need copying
76+ copy <- grow 2 bs
77+ return $ snoc copy byte
78+ else do -- can mutate
79+ BA.pokeInt 0 (end+1) arr
80+ BA.poke end byte arr
81+ return $ B arr ofs (end+1)
82+
83+infixl 7 |>
84+export
85+(|>) : Bytes -> Byte -> Bytes
86+(|>) = snoc
87+
88+namespace SnocView
89+ data SnocView : Type where
90+ Nil : SnocView
91+ Snoc : (bs : Bytes) -> (b : Byte) -> SnocView
92+
93+ export
94+ snocView : Bytes -> SnocView
95+ snocView (B arr ofs end) =
96+ if end == ofs
97+ then SnocView.Nil
98+ else unsafePerformIO $ do
99+ last <- BA.peek (end-1) arr
100+ return $ SnocView.Snoc (B arr ofs (end-1)) last
101+
102+namespace ConsView
103+ data ConsView : Type where
104+ Nil : ConsView
105+ Cons : (b : Byte) -> (bs : Bytes) -> ConsView
106+
107+ export
108+ consView : Bytes -> ConsView
109+ consView (B arr ofs end) =
110+ if end == ofs
111+ then ConsView.Nil
112+ else unsafePerformIO $ do
113+ first <- BA.peek ofs arr
114+ return $ ConsView.Cons first (B arr (ofs+1) end)
115+
116+infixr 7 ++
117+%assert_total
118+export
119+(++) : Bytes -> Bytes -> Bytes
120+(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)
121+ = let countR = endR - ofsR in
122+ if endL + countR > BA.size arrL
123+ then unsafePerformIO $ do -- need more space
124+ grown <- grow 2 bsL
125+ return $ grown ++ bsR
126+ else unsafePerformIO $ do
127+ maxUsedL <- BA.peekInt 0 arrL
128+ if maxUsedL > endL
129+ then do -- headroom taken
130+ copyL <- grow 2 bsL
131+ return $ copyL ++ bsR
132+ else do -- can mutate
133+ BA.pokeInt 0 (endL + countR) arrL
134+ BA.copy (arrR, ofsR) (arrL, endL) countR
135+ return $ B arrL ofsL (endL + countR)
136+
137+export
138+dropPrefix : Int -> Bytes -> Bytes
139+dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end
140+
141+export
142+takePrefix : Int -> Bytes -> Bytes
143+takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)
144+
145+export
146+pack : List Byte -> Bytes
147+pack = fromList empty
148+ where
149+ fromList : Bytes -> List Byte -> Bytes
150+ fromList bs [] = bs
151+ fromList bs (x :: xs) = fromList (bs `snoc` x) xs
152+
153+export
154+unpack : Bytes -> List Byte
155+unpack bs with (consView bs)
156+ | Nil = []
157+ | Cons x xs = x :: unpack (assert_smaller bs xs)
158+
159+export
160+slice : Int -> Int -> Bytes -> Bytes
161+slice ofs' end' (B arr ofs end)
162+ = B arr
163+ (((ofs + ofs') `min` end) `max` dataOfs)
164+ (((ofs + end') `min` end) `max` dataOfs)
165+
166+-- Folds with early exit.
167+-- If Bytes were a Functor, this would be equivalent
168+-- to a Traversable implementation interpreted in the Either monad.
169+data Result : Type -> Type where
170+ Stop : (result : a) -> Result a
171+ Cont : (acc : a) -> Result a
172+
173+export
174+iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a
175+iterateR f acc bs with (snocView bs)
176+ | Nil = acc
177+ | Snoc ys y with (f y acc)
178+ | Stop result = result
179+ | Cont acc' = iterateR f acc' (assert_smaller bs ys)
180+
181+export
182+iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a
183+iterateL f acc bs with (consView bs)
184+ | Nil = acc
185+ | Cons y ys with (f acc y)
186+ | Stop result = result
187+ | Cont acc' = iterateL f acc' (assert_smaller bs ys)
188+
189+infixl 3 .:
190+private
191+(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)
192+(.:) g f x y = g (f x y)
193+
194+export
195+foldr : (Byte -> a -> a) -> a -> Bytes -> a
196+foldr f = iterateR (Cont .: f)
197+
198+export
199+foldl : (a -> Byte -> a) -> a -> Bytes -> a
200+foldl f = iterateL (Cont .: f)
201+
202+export
203+spanLength : (Byte -> Bool) -> Bytes -> Int
204+spanLength p = iterateL step 0
205+ where
206+ step : Int -> Byte -> Result Int
207+ step n b with (p b)
208+ | True = Cont (1 + n)
209+ | False = Stop n
210+
211+find : Byte -> Bytes -> Maybe Int
212+find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end
213+
214+export
215+splitAt : Int -> Bytes -> (Bytes, Bytes)
216+splitAt n bs = (takePrefix n bs, dropPrefix n bs)
217+
218+export
219+splitOn : Byte -> Bytes -> (Bytes, Bytes)
220+splitOn b bs with (find b bs)
221+ | Nothing = (bs, empty)
222+ | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)
223+
224+export
225+splitsOn : Byte -> Bytes -> List Bytes
226+splitsOn b bs with (find b bs)
227+ | Nothing = [bs]
228+ | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)
229+
230+export
231+asciiLines : Bytes -> List Bytes
232+asciiLines = splitsOn 0x0A
233+
234+export
235+span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
236+span p bs = splitAt (spanLength p bs) bs
237+
238+export
239+break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
240+break p bs = span (not . p) bs
241+
242+private
243+cmp : Bytes -> Bytes -> Ordering
244+cmp (B arrL ofsL endL) (B arrR ofsR endR) = unsafePerformIO $ do
245+ let countL = endL - ofsL
246+ let countR = endR - ofsR
247+ let commonCount = countL `min` countR
248+ result <- BA.compare (arrL, ofsL) (arrR, ofsR) commonCount
249+ return $
250+ if result /= 0
251+ then i2o result
252+ else compare countL countR
253+ where
254+ i2o : Int -> Ordering
255+ i2o 0 = EQ
256+ i2o i = if i < 0 then LT else GT
257+
258+implementation Eq Bytes where
259+ xs == ys = (Bytes.cmp xs ys == EQ)
260+
261+implementation Ord Bytes where
262+ compare = Bytes.cmp
263+
264+export
265+toString : Bytes -> String
266+toString = foldr (strCons . chr . toInt) ""
267+
268+export
269+fromString : String -> Bytes
270+fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack
271+
272+implementation Show Bytes where
273+ show = ("b" ++) . show . toString
274+
275+implementation Semigroup Bytes where
276+ (<+>) = (++)
277+
278+implementation Monoid Bytes where
279+ neutral = empty
280+
281+-- todo:
282+--
283+-- make indices Nats
284+-- Build a ByteString on top of Bytes?
285+-- migrate to (Bits 8)?
286+--
287+-- bidirectional growth?