0 | module Data.Vect
   1 |
   2 | import Data.DPair
   3 | import Data.List
   4 | import Data.Nat
   5 | import public Data.Fin
   6 | import public Data.Zippable
   7 |
   8 | import Control.Function
   9 | import Decidable.Equality
  10 | import Syntax.PreorderReasoning
  11 |
  12 | %default total
  13 |
  14 | public export
  15 | data Vect : (len : Nat) -> (elem : Type) -> Type where
  16 |   ||| Empty vector
  17 |   Nil  : Vect Z elem
  18 |   ||| A non-empty vector of length `S len`, consisting of a head element and
  19 |   ||| the rest of the list, of length `len`.
  20 |   (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
  21 |
  22 | -- Hints for interactive editing
  23 | %name Vect xs, ys, zs, ws
  24 |
  25 | public export
  26 | length : (xs : Vect len elem) -> Nat
  27 | length [] = 0
  28 | length (_::xs) = 1 + length xs
  29 |
  30 | ||| Show that the length function on vectors in fact calculates the length
  31 | export
  32 | lengthCorrect : (xs : Vect len elem) -> length xs = len
  33 | lengthCorrect []        = Refl
  34 | lengthCorrect (_ :: xs) = rewrite lengthCorrect xs in Refl
  35 |
  36 | export
  37 | {x : a} -> Injective (Vect.(::) x) where
  38 |   injective Refl = Refl
  39 |
  40 | export
  41 | {xs : Vect n a} -> Injective (\x => Vect.(::) x xs) where
  42 |   injective Refl = Refl
  43 |
  44 | export
  45 | Biinjective Vect.(::) where
  46 |   biinjective Refl = (Refl, Refl)
  47 |
  48 | --------------------------------------------------------------------------------
  49 | -- Indexing into vectors
  50 | --------------------------------------------------------------------------------
  51 |
  52 | export
  53 | invertVectZ : (xs : Vect Z a) -> xs === []
  54 | invertVectZ [] = Refl
  55 |
  56 |
  57 | ||| All but the first element of the vector
  58 | |||
  59 | ||| ```idris example
  60 | ||| tail [1,2,3,4]
  61 | ||| ```
  62 | public export
  63 | tail : Vect (S len) elem -> Vect len elem
  64 | tail (_::xs) = xs
  65 |
  66 | ||| Only the first element of the vector
  67 | |||
  68 | ||| ```idris example
  69 | ||| head [1,2,3,4]
  70 | ||| ```
  71 | public export
  72 | head : Vect (S len) elem -> elem
  73 | head (x::_) = x
  74 |
  75 | export
  76 | invertVectS : (xs : Vect (S n) a) -> xs === head xs :: tail xs
  77 | invertVectS (_ :: _) = Refl
  78 |
  79 | ||| The last element of the vector
  80 | |||
  81 | ||| ```idris example
  82 | ||| last [1,2,3,4]
  83 | ||| ```
  84 | public export
  85 | last : Vect (S len) elem -> elem
  86 | last [x]        = x
  87 | last (_::y::ys) = last $ y::ys
  88 |
  89 | ||| All but the last element of the vector
  90 | |||
  91 | ||| ```idris example
  92 | ||| init [1,2,3,4]
  93 | ||| ```
  94 | public export
  95 | init : Vect (S len) elem -> Vect len elem
  96 | init [_]        = []
  97 | init (x::y::ys) = x :: init (y::ys)
  98 |
  99 | ||| Extract the first `n` elements of a Vect.
 100 | public export
 101 | take : (n  : Nat)
 102 |     -> (  xs : Vect (n + m) type)
 103 |     -> Vect n type
 104 | take 0 xs = Nil
 105 | take (S k) (x :: xs) = x :: take k xs
 106 |
 107 | namespace Stream
 108 |   ||| Take precisely n elements from the stream.
 109 |   ||| @ n how many elements to take
 110 |   ||| @ xs the stream
 111 |   public export
 112 |   take : (n : Nat) -> (xs : Stream a) -> Vect n a
 113 |   take Z xs = []
 114 |   take (S k) (x :: xs) = x :: take k xs
 115 |
 116 | ||| Drop the first `n` elements of a Vect.
 117 | public export
 118 | drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
 119 | drop 0 xs = xs
 120 | drop (S k) (x :: xs) = drop k xs
 121 |
 122 | ||| Drop up to the first `n` elements of a Vect.
 123 | public export
 124 | drop' : (n : Nat) -> Vect l elem -> Vect (l `minus` n) elem
 125 | drop' 0 xs = rewrite minusZeroRight l in xs
 126 | drop' (S k) [] = rewrite minusZeroLeft (S k) in []
 127 | drop' (S k) (x :: xs) = drop' k xs
 128 |
 129 | ||| Generate all of the Fin elements as a Vect whose length is the number of
 130 | ||| elements.
 131 | |||
 132 | ||| Useful, for example, when one wants all the indices for specific Vect.
 133 | public export
 134 | allFins : (n : Nat) -> Vect n (Fin n)
 135 | -- implemented using `map`, so the definition is further down
 136 |
 137 | ||| Extract a particular element from a vector
 138 | |||
 139 | ||| ```idris example
 140 | ||| index 1 [1,2,3,4]
 141 | ||| ```
 142 | public export
 143 | index : Fin len -> Vect len elem -> elem
 144 | index FZ     (x::_)  = x
 145 | index (FS k) (_::xs) = index k xs
 146 |
 147 | ||| Insert an element at a particular index
 148 | |||
 149 | ||| ```idris example
 150 | ||| insertAt 1 8 [1,2,3,4]
 151 | ||| ```
 152 | public export
 153 | insertAt : (idx : Fin (S len)) -> (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
 154 | insertAt FZ     y xs      = y :: xs
 155 | insertAt (FS k) y (x::xs) = x :: insertAt k y xs
 156 |
 157 | ||| Construct a new vector consisting of all but the indicated element
 158 | |||
 159 | ||| ```idris example
 160 | ||| deleteAt 1 [1,2,3,4]
 161 | ||| ```
 162 | public export
 163 | deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
 164 | deleteAt FZ     (_::xs)        = xs
 165 | deleteAt (FS k) [x]            = absurd k
 166 | deleteAt (FS k) (x::xs@(_::_)) = x :: deleteAt k xs
 167 |
 168 | ||| Replace an element at a particular index with another
 169 | |||
 170 | ||| ```idris example
 171 | ||| replaceAt 1 8 [1,2,3,4]
 172 | ||| ```
 173 | public export
 174 | replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
 175 | replaceAt FZ     y (_::xs) = y :: xs
 176 | replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
 177 |
 178 | ||| Replace the element at a particular index with the result of applying a function to it
 179 | ||| @ i the index to replace at
 180 | ||| @ f the update function
 181 | ||| @ xs the vector to replace in
 182 | |||
 183 | ||| ```idris example
 184 | ||| updateAt 1 (+10) [1,2,3,4]
 185 | ||| ```
 186 | public export
 187 | updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
 188 | updateAt FZ     f (x::xs) = f x :: xs
 189 | updateAt (FS k) f (x::xs) = x :: updateAt k f xs
 190 |
 191 | ||| Append two vectors
 192 | |||
 193 | ||| ```idris example
 194 | ||| [1,2,3,4] ++ [5,6]
 195 | ||| ```
 196 | public export
 197 | (++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
 198 | (++) []      ys = ys
 199 | (++) (x::xs) ys = x :: xs ++ ys
 200 |
 201 | ||| Add an element at the end of the vector.
 202 | ||| The main use case for it is to get the expected type signature
 203 | ||| `Vect n a -> a -> Vect (S n) a` instead of
 204 | ||| `Vect n a -> a -> Vect (n + 1) a` which you get by using `++ [x]`
 205 | |||
 206 | ||| Snoc gets its name by reversing `cons`, indicating we are
 207 | ||| tacking on the element at the end rather than the beginning.
 208 | ||| `append` would also be a suitable name.
 209 | |||
 210 | ||| @ xs The vector to be appended
 211 | ||| @ v The value to append
 212 | public export
 213 | snoc : (xs : Vect n a) -> (v : a) -> Vect (S n) a
 214 | snoc [] v = [v]
 215 | snoc (x :: xs) v = x :: snoc xs v
 216 |
 217 | ||| Pop the last element from a vector. This is the opposite of `snoc`, in that
 218 | ||| `(uncurry snoc) unsnoc xs` is `xs`. It is equivalent to `(init xs, last xs)`,
 219 | ||| but traverses the vector once.
 220 | |||
 221 | ||| @ xs The vector to pop the element from.
 222 | public export
 223 | unsnoc : (xs : Vect (S n) a) -> (Vect n a, a)
 224 | unsnoc [x] = ([], x)
 225 | unsnoc (x :: xs@(_ :: _)) = let (ini, lst) = unsnoc xs in (x :: ini, lst)
 226 |
 227 | ||| Repeat some value some number of times.
 228 | |||
 229 | ||| @ len the number of times to repeat it
 230 | ||| @ x the value to repeat
 231 | |||
 232 | ||| ```idris example
 233 | ||| replicate 4 1
 234 | ||| ```
 235 | public export
 236 | replicate : (len : Nat) -> (x : elem) -> Vect len elem
 237 | replicate Z     _ = []
 238 | replicate (S k) x = x :: replicate k x
 239 |
 240 | ||| Merge two ordered vectors
 241 | |||
 242 | ||| ```idris example
 243 | ||| mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])
 244 | ||| ```
 245 | export
 246 | mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
 247 | mergeBy _ [] ys = ys
 248 | mergeBy _ xs [] = rewrite plusZeroRightNeutral n in xs
 249 | mergeBy {n = S k} {m = S k'} order (x :: xs) (y :: ys)
 250 |      = case order x y of
 251 |             LT => x :: mergeBy order xs (y :: ys)
 252 |             _  => rewrite sym (plusSuccRightSucc k k') in
 253 |                              y :: mergeBy order (x :: xs) ys
 254 |
 255 | export
 256 | merge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elem
 257 | merge = mergeBy compare
 258 |
 259 | -- Properties for functions in this section --
 260 |
 261 | export
 262 | replaceAtSameIndex : (xs : Vect n a) -> (i : Fin n) -> (0 y : a) -> index i (replaceAt i y xs) = y
 263 | replaceAtSameIndex (_::_) FZ     _ = Refl
 264 | replaceAtSameIndex (_::_) (FS _) _ = replaceAtSameIndex _ _ _
 265 |
 266 | export
 267 | replaceAtDiffIndexPreserves : (xs : Vect n a) -> (i, j : Fin n) -> Not (i = j) -> (0 y : a) -> index i (replaceAt j y xs) = index i xs
 268 | replaceAtDiffIndexPreserves (_::_) FZ     FZ     co _ = absurd $ co Refl
 269 | replaceAtDiffIndexPreserves (_::_) FZ     (FS _) _  _ = Refl
 270 | replaceAtDiffIndexPreserves (_::_) (FS _) FZ     _  _ = Refl
 271 | replaceAtDiffIndexPreserves (_::_) (FS z) (FS w) co y = replaceAtDiffIndexPreserves _ z w (\zw => co $ cong FS zw) y
 272 |
 273 | --------------------------------------------------------------------------------
 274 | -- Transformations
 275 | --------------------------------------------------------------------------------
 276 |
 277 | ||| Reverse the second vector, prepending the result to the first.
 278 | |||
 279 | ||| ```idris example
 280 | ||| reverseOnto [0, 1] [10, 11, 12]
 281 | ||| ```
 282 | public export
 283 | reverseOnto : Vect n elem -> Vect m elem -> Vect (n+m) elem
 284 | reverseOnto {n}         acc []        = rewrite plusZeroRightNeutral n in acc
 285 | reverseOnto {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
 286 |                                         in reverseOnto (x::acc) xs
 287 |
 288 | ||| Reverse the order of the elements of a vector
 289 | |||
 290 | ||| ```idris example
 291 | ||| reverse [1,2,3,4]
 292 | ||| ```
 293 | public export
 294 | reverse : (xs : Vect len elem) -> Vect len elem
 295 | reverse = reverseOnto []
 296 |
 297 | ||| Alternate an element between the other elements of a vector
 298 | ||| @ sep the element to intersperse
 299 | ||| @ xs the vector to separate with `sep`
 300 | |||
 301 | ||| ```idris example
 302 | ||| intersperse 0 [1,2,3,4]
 303 | ||| ```
 304 | export
 305 | intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
 306 | intersperse sep []      = []
 307 | intersperse sep (x::xs) = x :: intersperse' sep xs
 308 |   where
 309 |     intersperse' : elem -> Vect n elem -> Vect (n + n) elem
 310 |     intersperse'         sep []      = []
 311 |     intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
 312 |                                        in sep :: x :: intersperse' sep xs
 313 |
 314 | --------------------------------------------------------------------------------
 315 | -- Conversion from list (toList is provided by Foldable)
 316 | --------------------------------------------------------------------------------
 317 |
 318 | public export
 319 | toVect : (n : Nat) -> List a -> Maybe (Vect n a)
 320 | toVect Z [] = Just []
 321 | toVect (S k) (x :: xs)
 322 |     = do xs' <- toVect k xs
 323 |          pure (x :: xs')
 324 | toVect _ _ = Nothing
 325 |
 326 | ||| Convert a list to a vector.
 327 | |||
 328 | ||| The length of the list should be statically known.
 329 | |||
 330 | ||| ```idris example
 331 | ||| fromList [1,2,3,4]
 332 | ||| ```
 333 | public export
 334 | fromList : (xs : List elem) -> Vect (length xs) elem
 335 | fromList []      = []
 336 | fromList (v::vs) = v :: fromList vs
 337 |
 338 | public export
 339 | fromList' : (xs : Vect len elem) -> (l : List elem) -> Vect (length l + len) elem
 340 | fromList' ys [] = ys
 341 | fromList' ys (x::xs) =
 342 |   rewrite (plusSuccRightSucc (length xs) len) in
 343 |   fromList' (x::ys) xs
 344 |
 345 | --------------------------------------------------------------------------------
 346 | -- Equality
 347 | --------------------------------------------------------------------------------
 348 |
 349 | public export
 350 | Eq a => Eq (Vect n a) where
 351 |   (==) []      []      = True
 352 |   (==) (x::xs) (y::ys) = x == y && xs == ys
 353 |
 354 | public export
 355 | DecEq a => DecEq (Vect n a) where
 356 |   decEq []      []      = Yes Refl
 357 |   decEq (x::xs) (y::ys) = decEqCong2 (decEq x y) (decEq xs ys)
 358 |
 359 | --------------------------------------------------------------------------------
 360 | -- Order
 361 | --------------------------------------------------------------------------------
 362 |
 363 | public export
 364 | implementation Ord elem => Ord (Vect len elem) where
 365 |   compare []      []      = EQ
 366 |   compare (x::xs) (y::ys)
 367 |       = case compare x y of
 368 |              EQ => compare xs ys
 369 |              x => x
 370 |
 371 | --------------------------------------------------------------------------------
 372 | -- Maps
 373 | --------------------------------------------------------------------------------
 374 |
 375 | public export
 376 | implementation Functor (Vect n) where
 377 |   map f []        = []
 378 |   map f (x::xs) = f x :: map f xs
 379 |
 380 | ||| Map a partial function across a vector, returning those elements for which
 381 | ||| the function had a value.
 382 | |||
 383 | ||| The first projection of the resulting pair (ie the length) will always be
 384 | ||| at most the length of the input vector. This is not, however, guaranteed
 385 | ||| by the type.
 386 | |||
 387 | ||| @ f the partial function (expressed by returning `Maybe`)
 388 | ||| @ xs the vector to check for results
 389 | |||
 390 | ||| ```idris example
 391 | ||| mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])
 392 | ||| ```
 393 | export
 394 | mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
 395 | mapMaybe f []      = (_ ** [])
 396 | mapMaybe f (x::xs) =
 397 |   let (len ** ys) = mapMaybe f xs
 398 |   in case f x of
 399 |        Just y  => (S len ** y :: ys)
 400 |        Nothing => (  len **      ys)
 401 |
 402 | -- now that we have `map`, we can finish implementing `allFins`
 403 | allFins 0 = []
 404 | allFins (S k) = FZ :: map FS (allFins k)
 405 |
 406 | --------------------------------------------------------------------------------
 407 | -- Folds
 408 | --------------------------------------------------------------------------------
 409 |
 410 | public export
 411 | foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
 412 | foldrImpl f e go [] = go e
 413 | foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
 414 |
 415 | export
 416 | foldrImplGoLemma
 417 |   :  (x : a) -> (xs : Vect n a) -> (f : a -> b -> b) -> (e : b) -> (go : b -> b)
 418 |   -> go (foldrImpl f e (f x) xs) === foldrImpl f e (go . (f x)) xs
 419 | foldrImplGoLemma z []        f e go = Refl
 420 | foldrImplGoLemma z (y :: ys) f e go = Calc $
 421 |   |~ go (foldrImpl f e ((f z) . (f y)) ys)
 422 |   ~~ go ((f z) (foldrImpl f e (f y) ys))   ... (cong go (sym (foldrImplGoLemma y ys f e (f z))))
 423 |   ~~ (go . (f z)) (foldrImpl f e (f y) ys) ... (cong go Refl)
 424 |   ~~ foldrImpl f e (go . (f z) . (f y)) ys ... (foldrImplGoLemma y ys f e (go . (f z)))
 425 |
 426 | public export
 427 | implementation Foldable (Vect n) where
 428 |   foldr f e xs = foldrImpl f e id xs
 429 |   foldl f z [] = z
 430 |   foldl f z (x :: xs) = foldl f (f z x) xs
 431 |
 432 |   null [] = True
 433 |   null _ = False
 434 |
 435 |   toList [] = []
 436 |   toList (x :: xs) = x :: toList xs
 437 |
 438 |   foldMap f = foldl (\acc, elem => acc <+> f elem) neutral
 439 |
 440 | --------------------------------------------------------------------------------
 441 | -- Special folds
 442 | --------------------------------------------------------------------------------
 443 |
 444 | ||| Flatten a vector of equal-length vectors
 445 | |||
 446 | ||| ```idris example
 447 | ||| concat [[1,2,3], [4,5,6]]
 448 | ||| ```
 449 | public export
 450 | concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
 451 | concat []      = []
 452 | concat (v::vs) = v ++ Vect.concat vs
 453 |
 454 | ||| Foldr without seeding the accumulator
 455 | |||
 456 | ||| ```idris example
 457 | ||| foldr1 (-) (fromList [1,2,3])
 458 | ||| ```
 459 | public export
 460 | foldr1 : (t -> t -> t) -> Vect (S n) t -> t
 461 | foldr1 f [x]        = x
 462 | foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))
 463 |
 464 | ||| Foldl without seeding the accumulator
 465 | |||
 466 | ||| ```idris example
 467 | ||| foldl1 (-) (fromList [1,2,3])
 468 | ||| ```
 469 | public export
 470 | foldl1 : (t -> t -> t) -> Vect (S n) t -> t
 471 | foldl1 f (x::xs) = foldl f x xs
 472 |
 473 | --------------------------------------------------------------------------------
 474 | -- Scans
 475 | --------------------------------------------------------------------------------
 476 |
 477 | ||| The scanr function is similar to foldr, but returns all the intermediate
 478 | ||| accumulator states in the form of a vector. Note the intermediate accumulator
 479 | ||| states appear in the result in reverse order - the first state appears last
 480 | ||| in the result.
 481 | |||
 482 | ||| ```idris example
 483 | ||| scanr (-) 0 (fromList [1,2,3])
 484 | ||| ```
 485 | public export
 486 | scanr : (elem -> res -> res) -> res -> Vect len elem -> Vect (S len) res
 487 | scanr _ q [] = [q]
 488 | scanr f q (x :: xs) = let qs'@(q' :: _) = scanr f q xs in f x q' :: qs'
 489 |
 490 | ||| The scanr1 function is a variant of scanr that doesn't require an explicit
 491 | ||| starting value.
 492 | ||| It assumes the last element of the vector to be the starting value and then
 493 | ||| starts the fold with the element preceding it.
 494 | |||
 495 | ||| ```idris example
 496 | ||| scanr1 (-) (fromList [1,2,3])
 497 | ||| ```
 498 | public export
 499 | scanr1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
 500 | scanr1 _ [] = []
 501 | scanr1 f xs@(_ :: _) = let (ini, lst) = unsnoc xs in scanr f lst ini
 502 |
 503 | ||| The scanl function is similar to foldl, but returns all the intermediate
 504 | ||| accumulator states in the form of a vector.
 505 | |||
 506 | ||| ```idris example
 507 | ||| scanl (-) 0 (fromList [1,2,3])
 508 | ||| ```
 509 | public export
 510 | scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
 511 | scanl f q []      = [q]
 512 | scanl f q (x::xs) = q :: scanl f (f q x) xs
 513 |
 514 | ||| The scanl1 function is a variant of scanl that doesn't require an explicit
 515 | ||| starting value.
 516 | ||| It assumes the first element of the vector to be the starting value and then
 517 | ||| starts the fold with the element following it.
 518 | |||
 519 | ||| ```idris example
 520 | ||| scanl1 (-) (fromList [1,2,3])
 521 | ||| ```
 522 | public export
 523 | scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
 524 | scanl1 f [] = []
 525 | scanl1 f (x::xs) = scanl f x xs
 526 |
 527 | --------------------------------------------------------------------------------
 528 | -- Membership tests
 529 | --------------------------------------------------------------------------------
 530 |
 531 | ||| Find the association of some key with a user-provided comparison
 532 | ||| @ p the comparison operator for keys (True if they match)
 533 | ||| @ e the key to look for
 534 | |||
 535 | ||| ```idris example
 536 | ||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
 537 | ||| ```
 538 | public export
 539 | lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
 540 | lookupBy p e []           = Nothing
 541 | lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
 542 |
 543 | ||| Find the association of some key using the default Boolean equality test
 544 | |||
 545 | ||| ```idris example
 546 | ||| lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]
 547 | ||| ```
 548 | public export
 549 | lookup : Eq key => key -> Vect n (key, val) -> Maybe val
 550 | lookup = lookupBy (==)
 551 |
 552 | ||| Check if any element of xs is found in elems by a user-provided comparison
 553 | ||| @ p the comparison operator
 554 | ||| @ elems the vector to search
 555 | ||| @ xs what to search for
 556 | |||
 557 | ||| ```idris example
 558 | ||| hasAnyBy (==) [2,5] [1,2,3,4]
 559 | ||| ```
 560 | public export
 561 | hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
 562 | hasAnyBy p elems []      = False
 563 | hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
 564 |
 565 | ||| Check if any element of xs is found in elems using the default Boolean equality test
 566 | |||
 567 | ||| ```idris example
 568 | ||| hasAny [2,5] [1,2,3,4]
 569 | ||| ```
 570 | public export
 571 | hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
 572 | hasAny = hasAnyBy (==)
 573 |
 574 | --------------------------------------------------------------------------------
 575 | -- Searching with a predicate
 576 | --------------------------------------------------------------------------------
 577 |
 578 | ||| Find the first element of the vector that satisfies some test
 579 | ||| @ p the test to satisfy
 580 | |||
 581 | ||| ```idris example
 582 | ||| find (== 3) [1,2,3,4]
 583 | ||| ```
 584 | public export
 585 | find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
 586 | find p []      = Nothing
 587 | find p (x::xs) = if p x then Just x else find p xs
 588 |
 589 | ||| Find the index of the first element of the vector that satisfies some test
 590 | |||
 591 | ||| ```idris example
 592 | ||| findIndex (== 3) [1,2,3,4]
 593 | ||| ```
 594 | public export
 595 | findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
 596 | findIndex p []        = Nothing
 597 | findIndex p (x :: xs) = if p x then Just FZ else FS <$> findIndex p xs
 598 |
 599 | ||| Find the indices of all elements that satisfy some test
 600 | |||
 601 | ||| ```idris example
 602 | ||| findIndices (< 3) [1,2,3,4]
 603 | ||| ```
 604 | public export
 605 | findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
 606 | findIndices p []        = []
 607 | findIndices p (x :: xs)
 608 |      = let is = FS <$> findIndices p xs in
 609 |            if p x then FZ :: is else is
 610 |
 611 | ||| Find the index of the first element of the vector that satisfies some test
 612 | |||
 613 | ||| ```idris example
 614 | ||| elemIndexBy (==) 3 [1,2,3,4]
 615 | ||| ```
 616 | public export
 617 | elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
 618 | elemIndexBy p e = findIndex $ p e
 619 |
 620 | ||| Find the index of the first element of the vector equal to the given one.
 621 | |||
 622 | ||| ```idris example
 623 | ||| elemIndex 3 [1,2,3,4]
 624 | ||| ```
 625 | public export
 626 | elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
 627 | elemIndex = elemIndexBy (==)
 628 |
 629 | ||| Find the indices of all elements that satisfy some test
 630 | |||
 631 | ||| ```idris example
 632 | ||| elemIndicesBy (<=) 3 [1,2,3,4]
 633 | ||| ```
 634 | public export
 635 | elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
 636 | elemIndicesBy p e = findIndices $ p e
 637 |
 638 | ||| Find the indices of all elements equal to the given one
 639 | |||
 640 | ||| ```idris example
 641 | ||| elemIndices 3 [1,2,3,4,3]
 642 | ||| ```
 643 | public export
 644 | elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
 645 | elemIndices = elemIndicesBy (==)
 646 |
 647 | --------------------------------------------------------------------------------
 648 | -- Filters
 649 | --------------------------------------------------------------------------------
 650 |
 651 | ||| Find all elements of a vector that satisfy some test
 652 | |||
 653 | ||| ```idris example
 654 | ||| filter (< 3) (fromList [1,2,3,4])
 655 | ||| ```
 656 | public export
 657 | filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
 658 | filter p []      = ( _ ** [] )
 659 | filter p (x::xs) =
 660 |   let (_ ** tail) = filter p xs
 661 |    in if p x then
 662 |         (_ ** x::tail)
 663 |       else
 664 |         (_ ** tail)
 665 |
 666 | public export
 667 | nubByImpl : Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
 668 | nubByImpl acc p []      = (_ ** [])
 669 | nubByImpl acc p (x::xs) with (elemBy p x acc)
 670 |   nubByImpl acc p (x :: xs) | True  = nubByImpl acc p xs
 671 |   nubByImpl acc p (x :: xs) | False with (nubByImpl (x::acc) p xs)
 672 |     nubByImpl acc p (x :: xs) | False | (_ ** tail) = (_ ** x::tail)
 673 |
 674 | ||| Make the elements of some vector unique by some test
 675 | |||
 676 | ||| ```idris example
 677 | ||| nubBy (==) (fromList [1,2,2,3,4,4])
 678 | ||| ```
 679 | public export
 680 | nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
 681 | nubBy = nubByImpl []
 682 |
 683 | ||| Make the elements of some vector unique by the default Boolean equality
 684 | |||
 685 | ||| ```idris example
 686 | ||| nub (fromList [1,2,2,3,4,4])
 687 | ||| ```
 688 | public export
 689 | nub : Eq elem => Vect len elem -> (p ** Vect p elem)
 690 | nub = nubBy (==)
 691 |
 692 | ||| Delete first element from list according to some test
 693 | |||
 694 | ||| ```idris example
 695 | ||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])
 696 | ||| ```
 697 | public export
 698 | deleteBy : {len : _} -> -- needed for the dependent pair
 699 |            (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
 700 | deleteBy _  _ []      = (_ ** [])
 701 | deleteBy eq x (y::ys) =
 702 |   let (len ** zs) = deleteBy eq x ys
 703 |   in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
 704 |
 705 | ||| Delete first element from list equal to the given one
 706 | |||
 707 | ||| ```idris example
 708 | ||| delete 2 (fromList [1,2,2,3,4,4])
 709 | ||| ```
 710 | public export
 711 | delete : {len : _} ->
 712 |          Eq elem => elem -> Vect len elem -> (p ** Vect p elem)
 713 | delete = deleteBy (==)
 714 |
 715 | --------------------------------------------------------------------------------
 716 | -- Splitting and breaking vects
 717 | --------------------------------------------------------------------------------
 718 |
 719 | ||| A tuple where the first element is a `Vect` of the `n` first elements and
 720 | ||| the second element is a `Vect` of the remaining elements of the original.
 721 | ||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
 722 | ||| but is more efficient.
 723 | |||
 724 | ||| @ n   the index to split at
 725 | ||| @ xs  the `Vect` to split in two
 726 | |||
 727 | ||| ```idris example
 728 | ||| splitAt 2 (fromList [1,2,3,4])
 729 | ||| ```
 730 | public export
 731 | splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
 732 | splitAt Z xs = ([], xs)
 733 | splitAt (S k) (x :: xs) with (splitAt k {m} xs)
 734 |   splitAt (S k) (x :: xs) | (tk, dr) = (x :: tk, dr)
 735 |
 736 | ||| A tuple where the first element is a `Vect` of the `n` elements passing given test
 737 | ||| and the second element is a `Vect` of the remaining elements of the original.
 738 | |||
 739 | ||| ```idris example
 740 | ||| partition (== 2) (fromList [1,2,3,2,4])
 741 | ||| ```
 742 | public export
 743 | partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
 744 | partition p []      = ((_ ** []), (_ ** []))
 745 | partition p (x::xs) =
 746 |   let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
 747 |     if p x then
 748 |       ((S leftLen ** x::lefts), (rightLen ** rights))
 749 |     else
 750 |       ((leftLen ** lefts), (S rightLen ** x::rights))
 751 |
 752 | ||| Split a vector whose length is a multiple of two numbers, k times n, into k
 753 | ||| sections of length n.
 754 | |||
 755 | ||| ```idris example
 756 | ||| > kSplits 2 4 [1, 2, 3, 4, 5, 6, 7, 8]
 757 | ||| [[1, 2, 3, 4], [5, 6, 7, 8]]
 758 | ||| ```
 759 | public export
 760 | kSplits : (k, n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
 761 | kSplits 0     n xs = []
 762 | kSplits (S k) n xs = let (ys, zs) = splitAt n xs
 763 |                      in ys :: kSplits k n zs
 764 |
 765 | ||| Split a vector whose length is a multiple of two numbers, k times n, into n
 766 | ||| sections of length k.
 767 | |||
 768 | ||| ```idris example
 769 | ||| > nSplits 2 4 [1, 2, 3, 4, 5, 6, 7, 8]
 770 | ||| [[1, 5], [2, 6], [3, 7], [4, 8]]
 771 | ||| ```
 772 | public export
 773 | nSplits : (k, n : Nat) -> Vect (k * n) a -> Vect n (Vect k a)
 774 | -- implemented via matrix transposition, so the definition is further down
 775 |
 776 | --------------------------------------------------------------------------------
 777 | -- Predicates
 778 | --------------------------------------------------------------------------------
 779 |
 780 | ||| Verify vector prefix
 781 | |||
 782 | ||| ```idris example
 783 | ||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
 784 | ||| ```
 785 | public export
 786 | isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
 787 | isPrefixOfBy p [] right        = True
 788 | isPrefixOfBy p left []         = False
 789 | isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
 790 |
 791 | ||| Verify vector prefix
 792 | |||
 793 | ||| ```idris example
 794 | ||| isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])
 795 | ||| ```
 796 | public export
 797 | isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
 798 | isPrefixOf = isPrefixOfBy (==)
 799 |
 800 | ||| Verify vector suffix
 801 | |||
 802 | ||| ```idris example
 803 | ||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
 804 | ||| ```
 805 | public export
 806 | isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
 807 | isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
 808 |
 809 | ||| Verify vector suffix
 810 | |||
 811 | ||| ```idris example
 812 | ||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
 813 | ||| ```
 814 | public export
 815 | isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
 816 | isSuffixOf = isSuffixOfBy (==)
 817 |
 818 | --------------------------------------------------------------------------------
 819 | -- Conversions
 820 | --------------------------------------------------------------------------------
 821 |
 822 | ||| Convert Maybe type into Vect
 823 | |||
 824 | ||| ```idris example
 825 | ||| maybeToVect (Just 2)
 826 | ||| ```
 827 | public export
 828 | maybeToVect : Maybe elem -> (p ** Vect p elem)
 829 | maybeToVect Nothing  = (_ ** [])
 830 | maybeToVect (Just j) = (_ ** [j])
 831 |
 832 | ||| Convert first element of Vect (if exists) into Maybe.
 833 | |||
 834 | ||| ```idris example
 835 | ||| vectToMaybe [2]
 836 | ||| ```
 837 | public export
 838 | vectToMaybe : Vect len elem -> Maybe elem
 839 | vectToMaybe []      = Nothing
 840 | vectToMaybe (x::xs) = Just x
 841 |
 842 | --------------------------------------------------------------------------------
 843 | -- Misc
 844 | --------------------------------------------------------------------------------
 845 |
 846 | ||| Filter out Nothings from Vect and unwrap the Justs
 847 | |||
 848 | ||| ```idris example
 849 | ||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
 850 | ||| ```
 851 | public export
 852 | catMaybes : (xs : Vect n (Maybe elem)) -> (p ** Vect p elem)
 853 | catMaybes []             = (_ ** [])
 854 | catMaybes (Nothing::xs)  = catMaybes xs
 855 | catMaybes ((Just j)::xs) =
 856 |   let (_ ** tail) = catMaybes xs
 857 |    in (_ ** j::tail)
 858 |
 859 | ||| Get diagonal elements
 860 | |||
 861 | ||| ```idris example
 862 | ||| diag [[1,2,3], [4,5,6], [7,8,9]]
 863 | ||| ```
 864 | public export
 865 | diag : Vect len (Vect len elem) -> Vect len elem
 866 | diag []             = []
 867 | diag ((x::xs)::xss) = x :: diag (map tail xss)
 868 |
 869 | namespace Fin
 870 |
 871 |   public export
 872 |   tabulate : {len : Nat} -> (Fin len -> a) -> Vect len a
 873 |   tabulate {len = Z} f = []
 874 |   tabulate {len = S _} f = f FZ :: tabulate (f . FS)
 875 |
 876 |   public export
 877 |   range : {len : Nat} -> Vect len (Fin len)
 878 |   range = tabulate id
 879 |
 880 | namespace Subset
 881 |
 882 |   public export
 883 |   tabulate : {len : Nat} -> (Subset Nat (`LT` len) -> a) -> Vect len a
 884 |   tabulate {len = Z} f = []
 885 |   tabulate {len = S _} f
 886 |     = f (Element Z ltZero)
 887 |     :: Subset.tabulate (\ (Element n prf) => f (Element (S n) (LTESucc prf)))
 888 |
 889 |   public export
 890 |   range : {len : Nat} -> Vect len (Subset Nat (`LT` len))
 891 |   range = tabulate id
 892 |
 893 | --------------------------------------------------------------------------------
 894 | -- Zippable
 895 | --------------------------------------------------------------------------------
 896 |
 897 | public export
 898 | Zippable (Vect k) where
 899 |   zipWith _ [] [] = []
 900 |   zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
 901 |
 902 |   zipWith3 _ [] [] [] = []
 903 |   zipWith3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3 f xs ys zs
 904 |
 905 |   unzipWith f [] = ([], [])
 906 |   unzipWith f (x :: xs) = let (b, c) = f x
 907 |                               (bs, cs) = unzipWith f xs in
 908 |                               (b :: bs, c :: cs)
 909 |
 910 |   unzipWith3 f [] = ([], [], [])
 911 |   unzipWith3 f (x :: xs) = let (b, c, d) = f x
 912 |                                (bs, cs, ds) = unzipWith3 f xs in
 913 |                                (b :: bs, c :: cs, d :: ds)
 914 |
 915 | export
 916 | zipWithIndexLinear : (0 f : _) -> (xs, ys : Vect n a) -> (i : Fin n) -> index i (zipWith f xs ys) = f (index i xs) (index i ys)
 917 | zipWithIndexLinear _ (_::xs) (_::ys) FZ     = Refl
 918 | zipWithIndexLinear f (_::xs) (_::ys) (FS i) = zipWithIndexLinear f xs ys i
 919 |
 920 | export
 921 | zipWith3IndexLinear : (0 f : _) -> (xs, ys, zs : Vect n a) -> (i : Fin n) -> index i (zipWith3 f xs ys zs) = f (index i xs) (index i ys) (index i zs)
 922 | zipWith3IndexLinear _ (_::xs) (_::ys) (_::zs) FZ     = Refl
 923 | zipWith3IndexLinear f (_::xs) (_::ys) (_::zs) (FS i) = zipWith3IndexLinear f xs ys zs i
 924 |
 925 | --------------------------------------------------------------------------------
 926 | -- Permutation
 927 | --------------------------------------------------------------------------------
 928 |
 929 | ||| Rearrange the elements of a vector according to some permutation of its
 930 | ||| indices.
 931 | ||| @ v the vector whose elements to rearrange
 932 | ||| @ p the permutation to apply
 933 | |||
 934 | ||| ```idris example
 935 | ||| > permute ['a', 'b', 'c', 'd'] [0, 3, 2, 1]
 936 | ||| ['a', 'd' , 'c' ,'b']
 937 | ||| ```
 938 | export
 939 | permute : (v : Vect len a) -> (p : Vect len (Fin len)) -> Vect len a
 940 | permute v p = (`index` v) <$> p
 941 |
 942 | --------------------------------------------------------------------------------
 943 | -- Matrix transposition
 944 | --------------------------------------------------------------------------------
 945 |
 946 | ||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
 947 | |||
 948 | ||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
 949 | |||
 950 | ||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
 951 | |||
 952 | ||| ```idris example
 953 | ||| transpose [[1,2], [3,4], [5,6], [7,8]]
 954 | ||| ```
 955 | public export
 956 | transpose : {n : _} -> (array : Vect m (Vect n elem)) -> Vect n (Vect m elem)
 957 | transpose []        = replicate _ []                 -- = [| [] |]
 958 | transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
 959 |
 960 | -- nSplits from earlier on
 961 | nSplits k n = transpose . kSplits k n
 962 |
 963 | --------------------------------------------------------------------------------
 964 | -- Applicative/Monad/Traversable
 965 | --------------------------------------------------------------------------------
 966 | -- These only work if the length is known at run time!
 967 |
 968 | public export
 969 | implementation {k : Nat} -> Applicative (Vect k) where
 970 |     pure = replicate _
 971 |     fs <*> vs = zipWith apply fs vs
 972 |
 973 | -- ||| This monad is different from the List monad, (>>=)
 974 | -- ||| uses the diagonal.
 975 | public export
 976 | implementation {k : Nat} -> Monad (Vect k) where
 977 |     m >>= f = diag (map f m)
 978 |
 979 | public export
 980 | implementation Traversable (Vect k) where
 981 |     traverse f []        = pure []
 982 |     traverse f (x :: xs) = [| f x :: traverse f xs |]
 983 |
 984 | --------------------------------------------------------------------------------
 985 | -- Semigroup/Monoid
 986 | --------------------------------------------------------------------------------
 987 |
 988 | public export
 989 | Semigroup a => Semigroup (Vect k a) where
 990 |   (<+>) = zipWith (<+>)
 991 |
 992 | public export
 993 | {k : Nat} -> Monoid a => Monoid (Vect k a) where
 994 |   neutral = replicate k neutral
 995 |
 996 | --------------------------------------------------------------------------------
 997 | -- Show
 998 | --------------------------------------------------------------------------------
 999 |
1000 | export
1001 | implementation Show elem => Show (Vect len elem) where
1002 |     show = show . toList
1003 |
1004 | -- Some convenience functions for testing lengths
1005 |
1006 | -- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
1007 | -- only know we don't know how to make a Vect n a, not that one can't exist.
1008 | export
1009 | exactLength : {m : Nat} -> -- expected at run-time
1010 |               (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
1011 | exactLength {m} len xs with (decEq m len)
1012 |   exactLength {m = m} m xs | (Yes Refl) = Just xs
1013 |   exactLength {m = m} len xs | (No contra) = Nothing
1014 |
1015 | ||| If the given Vect is at least the required length, return a Vect with
1016 | ||| at least that length in its type, otherwise return Nothing
1017 | ||| @len the required length
1018 | ||| @xs the vector with the desired length
1019 | export
1020 | overLength : {m : Nat} -> -- expected at run-time
1021 |              (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)
1022 | overLength n xs with (cmp m n)
1023 |   overLength {m}   (plus m (S y)) xs | (CmpLT y) = Nothing
1024 |   overLength {m}                m xs | CmpEQ     = Just (0 ** xs)
1025 |   overLength {m = plus n (S x)} n xs | (CmpGT x)
1026 |          = Just (S x ** rewrite plusCommutative (S x) n in xs)
1027 |