0 | module Data.ArrayVect
2 | import Data.Array.Core as Core
3 | import Data.Array.Indexed as Array
5 | import Data.Vect as Vect
16 | data ArrayVect : Nat -> Type -> Type where
18 | (::) : a -> ArrayVect n a -> ArrayVect (S n) a
20 | %name ArrayVect
xs, ys, zs
23 | unsafeFromArray : Core.IArray n a -> ArrayVect n a
24 | unsafeFromArray = believe_me
27 | unsafeToArray : ArrayVect n a -> Core.IArray n a
28 | unsafeToArray = believe_me
32 | fromVect : {n : Nat} -> Vect n a -> ArrayVect n a
34 | fromVect (x :: xs) = x :: fromVect xs
37 | fromVectArray : {n : Nat} -> Vect n a -> ArrayVect n a
38 | fromVectArray xs = unsafeFromArray (Array.array xs)
40 | %transform "arrayVectFromVect"
Data.ArrayVect.fromVect = Data.ArrayVect.fromVectArray
44 | toVect : {n : Nat} -> ArrayVect n a -> Vect n a
46 | toVect (x :: xs) = x :: toVect xs
49 | toVectArray : {n : Nat} -> ArrayVect n a -> Vect n a
50 | toVectArray xs = Array.toVect (unsafeToArray xs)
52 | %transform "arrayVectToVect"
Data.ArrayVect.toVect = Data.ArrayVect.toVectArray
56 | fromList : (xs : List a) -> ArrayVect (length xs) a
57 | fromList xs = fromVect (Vect.fromList xs)
60 | fromListArray : (xs : List a) -> ArrayVect (length xs) a
61 | fromListArray xs = unsafeFromArray (Array.arrayL xs)
63 | %transform "arrayVectFromList"
Data.ArrayVect.fromList = Data.ArrayVect.fromListArray
67 | toList : {n : Nat} -> ArrayVect n a -> List a
69 | toList (x :: xs) = x :: toList xs
72 | toListArray : {n : Nat} -> ArrayVect n a -> List a
73 | toListArray xs = Prelude.toList (unsafeToArray xs)
75 | %transform "arrayVectToList"
Data.ArrayVect.toList = Data.ArrayVect.toListArray
79 | empty : ArrayVect 0 a
83 | emptyArray : ArrayVect 0 a
84 | emptyArray = unsafeFromArray Array.empty
86 | %transform "arrayVectEmpty"
Data.ArrayVect.empty = Data.ArrayVect.emptyArray
90 | singleton : a -> ArrayVect 1 a
91 | singleton x = x :: []
94 | singletonArray : a -> ArrayVect 1 a
95 | singletonArray x = unsafeFromArray (Array.fill 1 x)
97 | %transform "arrayVectSingleton"
Data.ArrayVect.singleton = Data.ArrayVect.singletonArray
101 | replicate : (n : Nat) -> a -> ArrayVect n a
103 | replicate (S k) x = x :: replicate k x
106 | replicateArray : (n : Nat) -> a -> ArrayVect n a
107 | replicateArray n x = unsafeFromArray (Array.fill n x)
109 | %transform "arrayVectReplicate"
Data.ArrayVect.replicate = Data.ArrayVect.replicateArray
113 | generate : (n : Nat) -> (Fin n -> a) -> ArrayVect n a
114 | generate n f = fromVect (Vect.Fin.tabulate f)
117 | generateArray : (n : Nat) -> (Fin n -> a) -> ArrayVect n a
118 | generateArray n f = unsafeFromArray (Array.generate n f)
120 | %transform "arrayVectGenerate"
Data.ArrayVect.generate = Data.ArrayVect.generateArray
122 | iterVect : (n : Nat) -> (a -> a) -> a -> Vect n a
123 | iterVect 0 _ x = []
124 | iterVect (S k) f x = x :: iterVect k f (f x)
128 | iterate : (n : Nat) -> (a -> a) -> a -> ArrayVect n a
129 | iterate n f x = fromVect (iterVect n f x)
132 | iterateArray : (n : Nat) -> (a -> a) -> a -> ArrayVect n a
133 | iterateArray n f x = unsafeFromArray (Array.iterate n f x)
135 | %transform "arrayVectIterate"
Data.ArrayVect.iterate = Data.ArrayVect.iterateArray
139 | length : {n : Nat} -> ArrayVect n a -> Nat
141 | length (_ :: xs) = S (length xs)
144 | lengthArray : {n : Nat} -> ArrayVect n a -> Nat
145 | lengthArray {n} _ = n
147 | %transform "arrayVectLength"
Data.ArrayVect.length = Data.ArrayVect.lengthArray
151 | null : {n : Nat} -> ArrayVect n a -> Bool
153 | null (_ :: _) = False
156 | nullArray : {n : Nat} -> ArrayVect n a -> Bool
157 | nullArray {n} _ = n == 0
159 | %transform "arrayVectNull"
Data.ArrayVect.null = Data.ArrayVect.nullArray
163 | index : {n : Nat} -> Fin n -> ArrayVect n a -> a
164 | index FZ (x :: _) = x
165 | index (FS k) (_ :: xs) = index k xs
168 | indexArray : {n : Nat} -> Fin n -> ArrayVect n a -> a
169 | indexArray i xs = Core.at (unsafeToArray xs) i
171 | %transform "arrayVectIndex"
Data.ArrayVect.index = Data.ArrayVect.indexArray
175 | head : {n : Nat} -> ArrayVect (S n) a -> a
179 | headArray : {n : Nat} -> ArrayVect (S n) a -> a
180 | headArray xs = Core.at (unsafeToArray xs) FZ
182 | %transform "arrayVectHead"
Data.ArrayVect.head = Data.ArrayVect.headArray
187 | tail : {n : Nat} -> ArrayVect (S n) a -> ArrayVect n a
188 | tail (_ :: xs) = xs
191 | tailArray : {n : Nat} -> ArrayVect (S n) a -> ArrayVect n a
193 | rewrite sym (minusZeroRight n) in unsafeFromArray (Array.drop 1 (unsafeToArray xs))
195 | %transform "arrayVectTail"
Data.ArrayVect.tail = Data.ArrayVect.tailArray
199 | map : {n : Nat} -> (a -> b) -> ArrayVect n a -> ArrayVect n b
201 | map f (x :: xs) = f x :: map f xs
204 | mapArray : {n : Nat} -> (a -> b) -> ArrayVect n a -> ArrayVect n b
205 | mapArray f xs = unsafeFromArray (Prelude.map f (unsafeToArray xs))
207 | %transform "arrayVectMap"
Data.ArrayVect.map = Data.ArrayVect.mapArray
211 | mapWithIndex : {n : Nat} -> (Fin n -> a -> b) -> ArrayVect n a -> ArrayVect n b
212 | mapWithIndex f xs = generate n (\i => f i (index i xs))
215 | mapWithIndexArray : {n : Nat} -> (Fin n -> a -> b) -> ArrayVect n a -> ArrayVect n b
216 | mapWithIndexArray f xs = unsafeFromArray (Array.mapWithIndex f (unsafeToArray xs))
218 | %transform "arrayVectMapWithIndex"
Data.ArrayVect.mapWithIndex = Data.ArrayVect.mapWithIndexArray
223 | updateAt : {n : Nat} -> Fin n -> (a -> a) -> ArrayVect n a -> ArrayVect n a
224 | updateAt FZ f (x :: xs) = f x :: xs
225 | updateAt (FS k) f (x :: xs) = x :: updateAt k f xs
228 | updateAtArray : {n : Nat} -> Fin n -> (a -> a) -> ArrayVect n a -> ArrayVect n a
229 | updateAtArray i f xs = unsafeFromArray (Array.updateAt i f (unsafeToArray xs))
231 | %transform "arrayVectUpdateAt"
Data.ArrayVect.updateAt = Data.ArrayVect.updateAtArray
236 | replaceAt : {n : Nat} -> Fin n -> a -> ArrayVect n a -> ArrayVect n a
237 | replaceAt i x xs = updateAt i (const x) xs
240 | replaceAtArray : {n : Nat} -> Fin n -> a -> ArrayVect n a -> ArrayVect n a
241 | replaceAtArray i x xs = unsafeFromArray (Array.setAt i x (unsafeToArray xs))
243 | %transform "arrayVectReplaceAt"
Data.ArrayVect.replaceAt = Data.ArrayVect.replaceAtArray
247 | (++) : {m, n : Nat} -> ArrayVect m a -> ArrayVect n a -> ArrayVect (m + n) a
249 | (x :: xs) ++ ys = x :: (xs ++ ys)
252 | appendArray : {m, n : Nat} -> ArrayVect m a -> ArrayVect n a -> ArrayVect (m + n) a
253 | appendArray xs ys = unsafeFromArray (Array.append (unsafeToArray xs) (unsafeToArray ys))
255 | %transform "arrayVectAppend"
Data.ArrayVect.(++) = Data.ArrayVect.appendArray
259 | take : {n : Nat} -> (m : Nat) -> ArrayVect (m + n) a -> ArrayVect m a
261 | take (S k) (x :: xs) = x :: take k xs
264 | takeArray : {n : Nat} -> (m : Nat) -> ArrayVect (m + n) a -> ArrayVect m a
265 | takeArray m xs = unsafeFromArray (Core.take m (unsafeToArray xs) @{lteAddRight m})
267 | %transform "arrayVectTake"
Data.ArrayVect.take = Data.ArrayVect.takeArray
271 | drop : {n : Nat} -> (m : Nat) -> ArrayVect n a -> ArrayVect (n `minus` m) a
272 | drop 0 xs = rewrite minusZeroRight n in xs
274 | drop (S k) (_ :: xs) = drop k xs
277 | dropArray : {n : Nat} -> (m : Nat) -> ArrayVect n a -> ArrayVect (n `minus` m) a
278 | dropArray m xs = unsafeFromArray (Array.drop m (unsafeToArray xs))
280 | %transform "arrayVectDrop"
Data.ArrayVect.drop = Data.ArrayVect.dropArray
284 | zipWith : {n : Nat} -> (a -> b -> c) -> ArrayVect n a -> ArrayVect n b -> ArrayVect n c
285 | zipWith f [] [] = []
286 | zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
289 | zipWithArray : {n : Nat} -> (a -> b -> c) -> ArrayVect n a -> ArrayVect n b -> ArrayVect n c
290 | zipWithArray f xs ys =
291 | unsafeFromArray (Array.generate n (\i => f (Core.at (unsafeToArray xs) i) (Core.at (unsafeToArray ys) i)))
293 | %transform "arrayVectZipWith"
Data.ArrayVect.zipWith = Data.ArrayVect.zipWithArray
297 | foldr : {n : Nat} -> (a -> acc -> acc) -> acc -> ArrayVect n a -> acc
299 | foldr f z (x :: xs) = f x (foldr f z xs)
302 | foldrArray : {n : Nat} -> (a -> acc -> acc) -> acc -> ArrayVect n a -> acc
303 | foldrArray f z xs = Prelude.foldr f z (unsafeToArray xs)
305 | %transform "arrayVectFoldr"
Data.ArrayVect.foldr = Data.ArrayVect.foldrArray
309 | foldl : {n : Nat} -> (acc -> a -> acc) -> acc -> ArrayVect n a -> acc
311 | foldl f z (x :: xs) = foldl f (f z x) xs
314 | foldlArray : {n : Nat} -> (acc -> a -> acc) -> acc -> ArrayVect n a -> acc
315 | foldlArray f z xs = Prelude.foldl f z (unsafeToArray xs)
317 | %transform "arrayVectFoldl"
Data.ArrayVect.foldl = Data.ArrayVect.foldlArray
322 | filter : {n : Nat} -> (a -> Bool) -> ArrayVect n a -> (
m ** ArrayVect m a)
323 | filter p [] = (
_ ** [])
324 | filter p (x :: xs) =
325 | let (
m ** ys)
= filter p xs in
326 | if p x then (
S m ** x :: ys)
else (
m ** ys)
329 | filterArray : {n : Nat} -> (a -> Bool) -> ArrayVect n a -> (
m ** ArrayVect m a)
331 | case Array.filter p (unsafeToArray xs) of
332 | A m ys => (
m ** unsafeFromArray ys)
334 | %transform "arrayVectFilter"
Data.ArrayVect.filter = Data.ArrayVect.filterArray
339 | mapMaybe : {n : Nat} -> (a -> Maybe b) -> ArrayVect n a -> (
m ** ArrayVect m b)
340 | mapMaybe f [] = (
_ ** [])
341 | mapMaybe f (x :: xs) =
342 | let (
m ** ys)
= mapMaybe f xs in
344 | Just y => (
S m ** y :: ys)
345 | Nothing => (
m ** ys)
348 | mapMaybeArray : {n : Nat} -> (a -> Maybe b) -> ArrayVect n a -> (
m ** ArrayVect m b)
349 | mapMaybeArray f xs =
350 | case Array.mapMaybe f (unsafeToArray xs) of
351 | A m ys => (
m ** unsafeFromArray ys)
353 | %transform "arrayVectMapMaybe"
Data.ArrayVect.mapMaybe = Data.ArrayVect.mapMaybeArray
357 | equals : {n : Nat} -> Eq a => ArrayVect n a -> ArrayVect n a -> Bool
358 | equals [] [] = True
359 | equals (x :: xs) (y :: ys) = x == y && equals xs ys
362 | equalsArray : {n : Nat} -> Eq a => ArrayVect n a -> ArrayVect n a -> Bool
363 | equalsArray xs ys = unsafeToArray xs == unsafeToArray ys
365 | %transform "arrayVectEquals"
Data.ArrayVect.equals = Data.ArrayVect.equalsArray
369 | compare : {n : Nat} -> Ord a => ArrayVect n a -> ArrayVect n a -> Ordering
371 | compare (x :: xs) (y :: ys) =
372 | case Prelude.compare x y of
373 | EQ => compare xs ys
377 | compareArray : {n : Nat} -> Ord a => ArrayVect n a -> ArrayVect n a -> Ordering
378 | compareArray xs ys = Prelude.compare (unsafeToArray xs) (unsafeToArray ys)
380 | %transform "arrayVectCompare"
Data.ArrayVect.compare = Data.ArrayVect.compareArray
384 | showPrecAV : {n : Nat} -> Show a => Prec -> ArrayVect n a -> String
385 | showPrecAV p xs = showPrec p (toVect xs)
388 | showPrecAVArray : {n : Nat} -> Show a => Prec -> ArrayVect n a -> String
389 | showPrecAVArray p xs = showPrec p (Array.toVect (unsafeToArray xs))
391 | %transform "arrayVectShowPrec"
Data.ArrayVect.showPrecAV = Data.ArrayVect.showPrecAVArray
395 | {n : Nat} -> Eq a => Eq (ArrayVect n a) where
400 | {n : Nat} -> Ord a => Ord (ArrayVect n a) where
401 | compare = Data.ArrayVect.compare
406 | {n : Nat} -> Show a => Show (ArrayVect n a) where
407 | showPrec = showPrecAV
412 | {n : Nat} -> Functor (ArrayVect n) where
413 | map = Data.ArrayVect.map
418 | {n : Nat} -> Foldable (ArrayVect n) where
419 | foldr = Data.ArrayVect.foldr
420 | foldl = Data.ArrayVect.foldl
421 | toList = Data.ArrayVect.toList
422 | null = Data.ArrayVect.null
427 | {n : Nat} -> Applicative (ArrayVect n) where
429 | fs <*> xs = zipWith apply fs xs