0 | module Data.Buffer.Indexed
2 | import public Data.Array.Index
3 | import public Data.Array.Indexed
5 | import Data.Buffer.Mutable
8 | import Syntax.PreorderReasoning
18 | ix : IBuffer n -> (0 m : Nat) -> {auto x: Ix (S m) n} -> Bits8
19 | ix arr _ = at arr (ixToFin x)
23 | atNat : IBuffer n -> (m : Nat) -> {auto 0 lt : LT m n} -> Bits8
24 | atNat arr x = at arr (natToFinLT x)
28 | atByte : IBuffer 256 -> Bits8 -> Bits8
29 | atByte arr x = at arr (bits8ToFin x)
38 | empty = alloc 0 unsafeFreeze
42 | bufferL : (ls : List Bits8) -> IBuffer (length ls)
44 | alloc (length xs) $
\r,t =>
45 | let _ # t := writeList {xs} r xs t
50 | buffer : {n : _} -> Vect n Bits8 -> IBuffer n
53 | let _ # t := writeVect r xs t
62 | revBuffer : {n : _} -> Vect n Bits8 -> IBuffer n
65 | let _ # t := writeVectRev r n xs t
71 | generate : (n : Nat) -> (Fin n -> Bits8) -> IBuffer n
74 | let _ # t := genFrom r n f t
79 | fill : (n : Nat) -> Bits8 -> IBuffer n
80 | fill n = generate n . const
85 | iterate : (n : Nat) -> (f : Bits8 -> Bits8) -> Bits8 -> IBuffer n
88 | let _ # t := iterateFrom r n f v t
97 | force : {n : _} -> IBuffer n -> IBuffer n
98 | force buf = run1 $
\t => let r # t := thaw buf t in unsafeFreeze r t
106 | hcomp : {m,n : Nat} -> IBuffer m -> IBuffer n -> Ordering
107 | hcomp a1 a2 = go m n
110 | go : (k,l : Nat) -> {auto _ : Ix k m} -> {auto _ : Ix l n} -> Ordering
114 | go (S k) (S j) = case compare (ix a1 k) (ix a2 j) of
120 | heq : {m,n : Nat} -> IBuffer m -> IBuffer n -> Bool
124 | go : (k,l : Nat) -> {auto _ : Ix k m} -> {auto _ : Ix l n} -> Bool
126 | go (S k) (S j) = if ix a1 k == ix a2 j then go k j else False
130 | {n : Nat} -> Eq (IBuffer n) where
134 | go : (k : Nat) -> {auto 0 _ : LTE k n} -> Bool
136 | go (S k) = if atNat a1 k == atNat a2 k then go k else False
139 | {n : Nat} -> Ord (IBuffer n) where
140 | compare a1 a2 = go n
143 | go : (k : Nat) -> {auto _ : Ix k n} -> Ordering
145 | go (S k) = case compare (ix a1 k) (ix a2 k) of
156 | -> {auto 0 lte : LTE m n}
159 | ontoList xs 0 arr = xs
160 | ontoList xs (S k) arr = ontoList (atNat arr k :: xs) k arr
165 | -> {auto 0 lte : LTE m n}
167 | -> Vect (k + m) Bits8
168 | ontoVect xs 0 arr = rewrite plusZeroRightNeutral k in xs
169 | ontoVect xs (S v) arr =
170 | rewrite sym (plusSuccRightSucc k v) in ontoVect (atNat arr v :: xs) v arr
172 | ontoVectWithIndex :
173 | Vect k (Fin n, Bits8)
175 | -> {auto 0 lte : LTE m n}
177 | -> Vect (k + m) (Fin n, Bits8)
178 | ontoVectWithIndex xs 0 arr = rewrite plusZeroRightNeutral k in xs
179 | ontoVectWithIndex xs (S v) arr =
180 | rewrite sym (plusSuccRightSucc k v)
181 | in let x := natToFinLT v in ontoVectWithIndex ((x, at arr x) :: xs) v arr
185 | toVect : {n : _} -> IBuffer n -> Vect n Bits8
186 | toVect = ontoVect [] n
191 | toVectWithIndex : {n : _} -> IBuffer n -> Vect n (Fin n, Bits8)
192 | toVectWithIndex = ontoVectWithIndex [] n
196 | -> {auto 0 _ : LTE m n}
197 | -> (Bits8 -> a -> a)
201 | foldr_ 0 _ x arr = x
202 | foldr_ (S k) f x arr = foldr_ k f (f (atNat arr k) x) arr
206 | foldr : {n : _} -> (Bits8 -> a -> a) -> a -> IBuffer n -> a
210 | toList : {n : _} -> IBuffer n -> List Bits8
211 | toList = foldr (::) Nil
215 | -> {auto 0 prf : LTE m n}
216 | -> (Fin n -> Bits8 -> a -> a)
220 | foldrKV_ 0 _ x arr = x
221 | foldrKV_ (S k) f x arr =
222 | let fin := natToFinLT k @{prf} in foldrKV_ k f (f fin (at arr fin) x) arr
226 | foldrKV : {n : _} -> (Fin n -> Bits8 -> a -> a) -> a -> IBuffer n -> a
227 | foldrKV = foldrKV_ n
231 | -> {auto x : Ix m n}
232 | -> (a -> Bits8 -> a)
236 | foldl_ 0 _ v arr = v
237 | foldl_ (S k) f v arr = foldl_ k f (f v (ix arr k)) arr
241 | foldl : {n : _} -> (a -> Bits8 -> a) -> a -> IBuffer n -> a
245 | toSnocList : {n : _} -> IBuffer n -> SnocList Bits8
246 | toSnocList = foldl (:<) Lin
250 | -> {auto x : Ix m n}
251 | -> (Fin n -> a -> Bits8 -> a)
255 | foldlKV_ 0 _ v arr = v
256 | foldlKV_ (S k) f v arr =
257 | let fin := ixToFin x in foldlKV_ k f (f fin v (at arr fin)) arr
261 | foldlKV : {n : _} -> (Fin n -> a -> Bits8 -> a) -> a -> IBuffer n -> a
262 | foldlKV = foldlKV_ n
265 | {n : Nat} -> Show (IBuffer n) where
266 | showPrec p arr = showCon p "buffer" (showArg $
ontoList [] n arr)
270 | mapWithIndex : {n : _} -> (Fin n -> Bits8 -> Bits8) -> IBuffer n -> IBuffer n
271 | mapWithIndex f arr = generate n (\x => f x (at arr x))
275 | map : {n : _} -> (Bits8 -> Bits8) -> IBuffer n -> IBuffer n
276 | map f arr = generate n (f . at arr)
283 | updateAt : {n : _} -> Fin n -> (Bits8 -> Bits8) -> IBuffer n -> IBuffer n
284 | updateAt x f = mapWithIndex (\k,v => if x == k then f v else v)
290 | setAt : {n : _} -> Fin n -> Bits8 -> IBuffer n -> IBuffer n
291 | setAt x y = mapWithIndex (\k,v => if x == k then y else v)
300 | traverseWithIndex :
302 | -> {auto app : Applicative f}
303 | -> (Fin n -> Bits8 -> f Bits8)
306 | traverseWithIndex f arr =
307 | buffer <$> traverse (\(x,v) => f x v) (toVectWithIndex arr)
312 | -> {auto app : Applicative f}
313 | -> (Bits8 -> f Bits8)
316 | traverse = traverseWithIndex . const
324 | append : {m,n : _} -> IBuffer m -> IBuffer n -> IBuffer (m + n)
326 | alloc (m+n) $
\r,t =>
327 | let _ # t := icopy {n = m+n} src1 0 0 m @{reflexive} @{lteAddRight _} r t
328 | _ # t := icopy src2 0 m n @{reflexive} @{reflexive} r t
329 | in unsafeFreeze r t
337 | drop : {n : _} -> (m : Nat) -> IBuffer n -> IBuffer (n `minus` m)
338 | drop m buf = generate (n `minus` m) (\f => at buf (inc f))
346 | AB _ b1 == AB _ b2 = heq b1 b2
349 | Ord AnyBuffer where
350 | compare (AB _ b1) (AB _ b2) = hcomp b1 b2
353 | Semigroup AnyBuffer where
354 | AB _ b1 <+> AB _ b2 = AB _ $
append b1 b2
357 | Monoid AnyBuffer where
358 | neutral = AB 0 empty
361 | Show AnyBuffer where
362 | showPrec p (AB n ib) = showCon p "AB" (showArg n ++ showArg ib)
365 | FromString AnyBuffer where
366 | fromString s = AB _ $
fromString s
369 | Cast AnyBuffer String where
370 | cast (AB n ib) = toString ib 0 n
373 | pack : List Bits8 -> AnyBuffer
374 | pack bs = AB _ $
bufferL bs
377 | unpack : AnyBuffer -> List Bits8
378 | unpack (AB _ b) = toList b