@@ -0,0 +1,268 @@
1+module Data.Bytes
2+
3+import Data.ByteArray as BA
4+
5+%access public
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+abstract
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+abstract
36+length : Bytes -> Int
37+length (B arr ofs end) = end - ofs
38+
39+abstract
40+empty : Bytes
41+empty = unsafePerformIO $ allocate minimalCapacity
42+
43+abstract
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+abstract
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+(|>) : Bytes -> Byte -> Bytes
85+(|>) = snoc
86+
87+namespace SnocView
88+ data SnocView : Type where
89+ Nil : SnocView
90+ Snoc : (bs : Bytes) -> (b : Byte) -> SnocView
91+
92+ abstract
93+ snocView : Bytes -> SnocView
94+ snocView (B arr ofs end) =
95+ if end == ofs
96+ then SnocView.Nil
97+ else unsafePerformIO $ do
98+ last <- BA.peek (end-1) arr
99+ return $ SnocView.Snoc (B arr ofs (end-1)) last
100+
101+namespace ConsView
102+ data ConsView : Type where
103+ Nil : ConsView
104+ Cons : (b : Byte) -> (bs : Bytes) -> ConsView
105+
106+ abstract
107+ consView : Bytes -> ConsView
108+ consView (B arr ofs end) =
109+ if end == ofs
110+ then ConsView.Nil
111+ else unsafePerformIO $ do
112+ first <- BA.peek ofs arr
113+ return $ ConsView.Cons first (B arr (ofs+1) end)
114+
115+infixr 7 ++
116+%assert_total
117+abstract
118+(++) : Bytes -> Bytes -> Bytes
119+(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)
120+ = let countR = endR - ofsR in
121+ if endL + countR > BA.size arrL
122+ then unsafePerformIO $ do -- need more space
123+ grown <- grow 2 bsL
124+ return $ grown ++ bsR
125+ else unsafePerformIO $ do
126+ maxUsedL <- BA.peekInt 0 arrL
127+ if maxUsedL > endL
128+ then do -- headroom taken
129+ copyL <- grow 2 bsL
130+ return $ copyL ++ bsR
131+ else do -- can mutate
132+ BA.pokeInt 0 (endL + countR) arrL
133+ BA.copy (arrR, ofsR) (arrL, endL) countR
134+ return $ B arrL ofsL (endL + countR)
135+
136+dropPrefix : Int -> Bytes -> Bytes
137+dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end
138+
139+takePrefix : Int -> Bytes -> Bytes
140+takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)
141+
142+pack : List Byte -> Bytes
143+pack = fromList empty
144+ where
145+ fromList : Bytes -> List Byte -> Bytes
146+ fromList bs [] = bs
147+ fromList bs (x :: xs) = fromList (bs `snoc` x) xs
148+
149+unpack : Bytes -> List Byte
150+unpack bs with (consView bs)
151+ | Nil = []
152+ | Cons x xs = x :: unpack (assert_smaller bs xs)
153+
154+slice : Int -> Int -> Bytes -> Bytes
155+slice ofs' end' (B arr ofs end)
156+ = B arr
157+ (((ofs + ofs') `min` end) `max` dataOfs)
158+ (((ofs + end') `min` end) `max` dataOfs)
159+
160+-- Folds with early exit.
161+-- If Bytes were a Functor, this would be equivalent
162+-- to a Traversable implementation interpreted in the Either monad.
163+data Result : Type -> Type where
164+ Stop : (result : a) -> Result a
165+ Cont : (acc : a) -> Result a
166+
167+iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a
168+iterateR f acc bs with (snocView bs)
169+ | Nil = acc
170+ | Snoc ys y with (f y acc)
171+ | Stop result = result
172+ | Cont acc' = iterateR f acc' (assert_smaller bs ys)
173+
174+iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a
175+iterateL f acc bs with (consView bs)
176+ | Nil = acc
177+ | Cons y ys with (f acc y)
178+ | Stop result = result
179+ | Cont acc' = iterateL f acc' (assert_smaller bs ys)
180+
181+infixl 3 .:
182+private
183+(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)
184+(.:) g f x y = g (f x y)
185+
186+foldr : (Byte -> a -> a) -> a -> Bytes -> a
187+foldr f = iterateR (Cont .: f)
188+
189+foldl : (a -> Byte -> a) -> a -> Bytes -> a
190+foldl f = iterateL (Cont .: f)
191+
192+spanLength : (Byte -> Bool) -> Bytes -> Int
193+spanLength p = iterateL step 0
194+ where
195+ step : Int -> Byte -> Result Int
196+ step n b with (p b)
197+ | True = Cont (1 + n)
198+ | False = Stop n
199+
200+find : Byte -> Bytes -> Maybe Int
201+find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end
202+
203+splitAt : Int -> Bytes -> (Bytes, Bytes)
204+splitAt n bs = (takePrefix n bs, dropPrefix n bs)
205+
206+splitOn : Byte -> Bytes -> (Bytes, Bytes)
207+splitOn b bs with (find b bs)
208+ | Nothing = (bs, empty)
209+ | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)
210+
211+splitsOn : Byte -> Bytes -> List Bytes
212+splitsOn b bs with (find b bs)
213+ | Nothing = [bs]
214+ | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)
215+
216+asciiLines : Bytes -> List Bytes
217+asciiLines = splitsOn 0x0A
218+
219+span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
220+span p bs = splitAt (spanLength p bs) bs
221+
222+break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
223+break p bs = span (not . p) bs
224+
225+private
226+cmp : Bytes -> Bytes -> Ordering
227+cmp (B arrL ofsL endL) (B arrR ofsR endR) = unsafePerformIO $ do
228+ let countL = endL - ofsL
229+ let countR = endR - ofsR
230+ let commonCount = countL `min` countR
231+ result <- BA.compare (arrL, ofsL) (arrR, ofsR) commonCount
232+ return $
233+ if result /= 0
234+ then i2o result
235+ else compare countL countR
236+ where
237+ i2o : Int -> Ordering
238+ i2o 0 = EQ
239+ i2o i = if i < 0 then LT else GT
240+
241+implementation Eq Bytes where
242+ xs == ys = (Bytes.cmp xs ys == EQ)
243+
244+implementation Ord Bytes where
245+ compare = Bytes.cmp
246+
247+toString : Bytes -> String
248+toString = foldr (strCons . chr . toInt) ""
249+
250+fromString : String -> Bytes
251+fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack
252+
253+implementation Show Bytes where
254+ show = ("b" ++) . show . toString
255+
256+implementation Semigroup Bytes where
257+ (<+>) = (++)
258+
259+implementation Monoid Bytes where
260+ neutral = empty
261+
262+-- todo:
263+--
264+-- make indices Nats
265+-- Build a ByteString on top of Bytes?
266+-- migrate to (Bits 8)?
267+--
268+-- bidirectional growth?