0 | module Data.Array
  1 |
  2 | import public Data.Array.Core
  3 | import public Data.Array.Index
  4 | import public Data.Array.Indexed
  5 |
  6 | %default total
  7 |
  8 | --------------------------------------------------------------------------------
  9 | --          Interfaces
 10 | --------------------------------------------------------------------------------
 11 |
 12 | export %inline
 13 | Eq a => Eq (Array a) where
 14 |   A _ a1 == A _ a2 = heq a1 a2
 15 |
 16 | export %inline
 17 | Ord a => Ord (Array a) where
 18 |   compare (A _ a1) (A _ a2) = hcomp a1 a2
 19 |
 20 | export
 21 | Show a => Show (Array a) where
 22 |   showPrec p (A size arr) = showCon p "A" (showArg size ++ showArg arr)
 23 |
 24 | export
 25 | Functor Array where
 26 |   map f (A s arr) = A s $ map f arr
 27 |
 28 | export
 29 | Foldable Array where
 30 |   foldr f x (A _ arr) = foldr f x arr
 31 |   foldl f x (A _ arr) = foldl f x arr
 32 |   toList (A _ arr)    = toList arr
 33 |   null   (A _ arr)    = null arr
 34 |
 35 | export
 36 | Traversable Array where
 37 |   traverse f (A s arr) = A s <$> traverse f arr
 38 |
 39 | export
 40 | Semigroup (Array a) where
 41 |   A m a1 <+> A n a2 = A (m+n) $ append a1 a2
 42 |
 43 | export
 44 | Monoid (Array a) where
 45 |   neutral = A 0 empty
 46 |
 47 | bind : Array a -> (a -> Array b) -> Array b
 48 | bind x f =
 49 |   let sb := foldl (\sa,v => sa :< f v) [<] x
 50 |    in A (SnocSize sb) (snocConcat sb)
 51 |
 52 | export
 53 | Applicative Array where
 54 |   pure v = A 1 $ fill 1 v
 55 |   af <*> av = bind af (\fun => map fun av)
 56 |
 57 | export
 58 | Monad Array where
 59 |   (>>=) = bind
 60 |
 61 | export
 62 | Alternative Array where
 63 |   empty = A 0 empty
 64 |   A 0 _ <|> ys = ys
 65 |   xs    <|> _  = xs
 66 |
 67 | --------------------------------------------------------------------------------
 68 | --          Initializing Arrays
 69 | --------------------------------------------------------------------------------
 70 |
 71 | export %inline
 72 | fromList : (ls : List a) -> Array a
 73 | fromList ls = A _ $ arrayL ls
 74 |
 75 | export %inline
 76 | fill : (n : Nat) -> a -> Array a
 77 | fill n v = A n $ fill n v
 78 |
 79 | export %inline
 80 | generate : (n : Nat) -> (Fin n -> a) -> Array a
 81 | generate n f = A n $ generate n f
 82 |
 83 | export %inline
 84 | iterate : (n : Nat) -> (a -> a) -> a -> Array a
 85 | iterate n f x = A n $ iterate n f x
 86 |
 87 | export %inline
 88 | force : Array a -> Array a
 89 | force (A s arr) = A s $ force arr
 90 |
 91 | --------------------------------------------------------------------------------
 92 | --          Subarrays
 93 | --------------------------------------------------------------------------------
 94 |
 95 | export %inline
 96 | take : Nat -> Array a -> Array a
 97 | take k (A size arr) with (k <= size) proof eq
 98 |   _ | True  = A k $ take k arr @{lteOpReflectsLTE _ _ eq}
 99 |   _ | False = A size arr
100 |
101 | export %inline
102 | drop : Nat -> Array a -> Array a
103 | drop n (A size arr) = A (size `minus` n) (drop n arr)
104 |
105 | export %inline
106 | filter : (a -> Bool) -> Array a -> Array a
107 | filter f (A size arr) = filter f arr
108 |
109 | export %inline
110 | mapMaybe : (a -> Maybe b) -> Array a -> Array b
111 | mapMaybe f (A size arr) = mapMaybe f arr
112 |