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 | public export
 327 | fromList' : (xs : Vect len elem) -> (l : List elem) -> Vect (length l + len) elem
 328 | fromList' ys [] = ys
 329 | fromList' ys (x::xs) =
 330 |   rewrite (plusSuccRightSucc (length xs) len) in
 331 |   fromList' (x::ys) xs
 332 |
 333 | ||| Convert a list to a vector.
 334 | |||
 335 | ||| The length of the list should be statically known.
 336 | |||
 337 | ||| ```idris example
 338 | ||| fromList [1,2,3,4]
 339 | ||| ```
 340 | public export
 341 | fromList : (xs : List elem) -> Vect (length xs) elem
 342 | fromList l =
 343 |   rewrite (sym $ plusZeroRightNeutral (length l)) in
 344 |   reverse $ fromList' [] l
 345 |
 346 | --------------------------------------------------------------------------------
 347 | -- Equality
 348 | --------------------------------------------------------------------------------
 349 |
 350 | public export
 351 | Eq a => Eq (Vect n a) where
 352 |   (==) []      []      = True
 353 |   (==) (x::xs) (y::ys) = x == y && xs == ys
 354 |
 355 | public export
 356 | DecEq a => DecEq (Vect n a) where
 357 |   decEq []      []      = Yes Refl
 358 |   decEq (x::xs) (y::ys) = decEqCong2 (decEq x y) (decEq xs ys)
 359 |
 360 | --------------------------------------------------------------------------------
 361 | -- Order
 362 | --------------------------------------------------------------------------------
 363 |
 364 | public export
 365 | implementation Ord elem => Ord (Vect len elem) where
 366 |   compare []      []      = EQ
 367 |   compare (x::xs) (y::ys)
 368 |       = case compare x y of
 369 |              EQ => compare xs ys
 370 |              x => x
 371 |
 372 | --------------------------------------------------------------------------------
 373 | -- Maps
 374 | --------------------------------------------------------------------------------
 375 |
 376 | public export
 377 | implementation Functor (Vect n) where
 378 |   map f []        = []
 379 |   map f (x::xs) = f x :: map f xs
 380 |
 381 | ||| Map a partial function across a vector, returning those elements for which
 382 | ||| the function had a value.
 383 | |||
 384 | ||| The first projection of the resulting pair (ie the length) will always be
 385 | ||| at most the length of the input vector. This is not, however, guaranteed
 386 | ||| by the type.
 387 | |||
 388 | ||| @ f the partial function (expressed by returning `Maybe`)
 389 | ||| @ xs the vector to check for results
 390 | |||
 391 | ||| ```idris example
 392 | ||| mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])
 393 | ||| ```
 394 | export
 395 | mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
 396 | mapMaybe f []      = (_ ** [])
 397 | mapMaybe f (x::xs) =
 398 |   let (len ** ys) = mapMaybe f xs
 399 |   in case f x of
 400 |        Just y  => (S len ** y :: ys)
 401 |        Nothing => (  len **      ys)
 402 |
 403 | -- now that we have `map`, we can finish implementing `allFins`
 404 | allFins 0 = []
 405 | allFins (S k) = FZ :: map FS (allFins k)
 406 |
 407 | --------------------------------------------------------------------------------
 408 | -- Folds
 409 | --------------------------------------------------------------------------------
 410 |
 411 | public export
 412 | foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
 413 | foldrImpl f e go [] = go e
 414 | foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
 415 |
 416 | export
 417 | foldrImplGoLemma
 418 |   :  (x : a) -> (xs : Vect n a) -> (f : a -> b -> b) -> (e : b) -> (go : b -> b)
 419 |   -> go (foldrImpl f e (f x) xs) === foldrImpl f e (go . (f x)) xs
 420 | foldrImplGoLemma z []        f e go = Refl
 421 | foldrImplGoLemma z (y :: ys) f e go = Calc $
 422 |   |~ go (foldrImpl f e ((f z) . (f y)) ys)
 423 |   ~~ go ((f z) (foldrImpl f e (f y) ys))   ... (cong go (sym (foldrImplGoLemma y ys f e (f z))))
 424 |   ~~ (go . (f z)) (foldrImpl f e (f y) ys) ... (cong go Refl)
 425 |   ~~ foldrImpl f e (go . (f z) . (f y)) ys ... (foldrImplGoLemma y ys f e (go . (f z)))
 426 |
 427 | public export
 428 | implementation Foldable (Vect n) where
 429 |   foldr f e xs = foldrImpl f e id xs
 430 |   foldl f z [] = z
 431 |   foldl f z (x :: xs) = foldl f (f z x) xs
 432 |
 433 |   null [] = True
 434 |   null _ = False
 435 |
 436 |   foldMap f = foldl (\acc, elem => acc <+> f elem) neutral
 437 |
 438 | --------------------------------------------------------------------------------
 439 | -- Special folds
 440 | --------------------------------------------------------------------------------
 441 |
 442 | ||| Flatten a vector of equal-length vectors
 443 | |||
 444 | ||| ```idris example
 445 | ||| concat [[1,2,3], [4,5,6]]
 446 | ||| ```
 447 | public export
 448 | concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
 449 | concat []      = []
 450 | concat (v::vs) = v ++ Vect.concat vs
 451 |
 452 | ||| Foldr without seeding the accumulator
 453 | |||
 454 | ||| ```idris example
 455 | ||| foldr1 (-) (fromList [1,2,3])
 456 | ||| ```
 457 | public export
 458 | foldr1 : (t -> t -> t) -> Vect (S n) t -> t
 459 | foldr1 f [x]        = x
 460 | foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))
 461 |
 462 | ||| Foldl without seeding the accumulator
 463 | |||
 464 | ||| ```idris example
 465 | ||| foldl1 (-) (fromList [1,2,3])
 466 | ||| ```
 467 | public export
 468 | foldl1 : (t -> t -> t) -> Vect (S n) t -> t
 469 | foldl1 f (x::xs) = foldl f x xs
 470 |
 471 | --------------------------------------------------------------------------------
 472 | -- Scans
 473 | --------------------------------------------------------------------------------
 474 |
 475 | ||| The scanr function is similar to foldr, but returns all the intermediate
 476 | ||| accumulator states in the form of a vector. Note the intermediate accumulator
 477 | ||| states appear in the result in reverse order - the first state appears last
 478 | ||| in the result.
 479 | |||
 480 | ||| ```idris example
 481 | ||| scanr (-) 0 (fromList [1,2,3])
 482 | ||| ```
 483 | public export
 484 | scanr : (elem -> res -> res) -> res -> Vect len elem -> Vect (S len) res
 485 | scanr _ q [] = [q]
 486 | scanr f q (x :: xs) = let qs'@(q' :: _) = scanr f q xs in f x q' :: qs'
 487 |
 488 | ||| The scanr1 function is a variant of scanr that doesn't require an explicit
 489 | ||| starting value.
 490 | ||| It assumes the last element of the vector to be the starting value and then
 491 | ||| starts the fold with the element preceding it.
 492 | |||
 493 | ||| ```idris example
 494 | ||| scanr1 (-) (fromList [1,2,3])
 495 | ||| ```
 496 | public export
 497 | scanr1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
 498 | scanr1 _ [] = []
 499 | scanr1 f xs@(_ :: _) = let (ini, lst) = unsnoc xs in scanr f lst ini
 500 |
 501 | ||| The scanl function is similar to foldl, but returns all the intermediate
 502 | ||| accumulator states in the form of a vector.
 503 | |||
 504 | ||| ```idris example
 505 | ||| scanl (-) 0 (fromList [1,2,3])
 506 | ||| ```
 507 | public export
 508 | scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
 509 | scanl f q []      = [q]
 510 | scanl f q (x::xs) = q :: scanl f (f q x) xs
 511 |
 512 | ||| The scanl1 function is a variant of scanl that doesn't require an explicit
 513 | ||| starting value.
 514 | ||| It assumes the first element of the vector to be the starting value and then
 515 | ||| starts the fold with the element following it.
 516 | |||
 517 | ||| ```idris example
 518 | ||| scanl1 (-) (fromList [1,2,3])
 519 | ||| ```
 520 | public export
 521 | scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
 522 | scanl1 f [] = []
 523 | scanl1 f (x::xs) = scanl f x xs
 524 |
 525 | --------------------------------------------------------------------------------
 526 | -- Membership tests
 527 | --------------------------------------------------------------------------------
 528 |
 529 | ||| Find the association of some key with a user-provided comparison
 530 | ||| @ p the comparison operator for keys (True if they match)
 531 | ||| @ e the key to look for
 532 | |||
 533 | ||| ```idris example
 534 | ||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
 535 | ||| ```
 536 | public export
 537 | lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
 538 | lookupBy p e []           = Nothing
 539 | lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
 540 |
 541 | ||| Find the association of some key using the default Boolean equality test
 542 | |||
 543 | ||| ```idris example
 544 | ||| lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]
 545 | ||| ```
 546 | public export
 547 | lookup : Eq key => key -> Vect n (key, val) -> Maybe val
 548 | lookup = lookupBy (==)
 549 |
 550 | ||| Check if any element of xs is found in elems by a user-provided comparison
 551 | ||| @ p the comparison operator
 552 | ||| @ elems the vector to search
 553 | ||| @ xs what to search for
 554 | |||
 555 | ||| ```idris example
 556 | ||| hasAnyBy (==) [2,5] [1,2,3,4]
 557 | ||| ```
 558 | public export
 559 | hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
 560 | hasAnyBy p elems []      = False
 561 | hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
 562 |
 563 | ||| Check if any element of xs is found in elems using the default Boolean equality test
 564 | |||
 565 | ||| ```idris example
 566 | ||| hasAny [2,5] [1,2,3,4]
 567 | ||| ```
 568 | public export
 569 | hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
 570 | hasAny = hasAnyBy (==)
 571 |
 572 | --------------------------------------------------------------------------------
 573 | -- Searching with a predicate
 574 | --------------------------------------------------------------------------------
 575 |
 576 | ||| Find the first element of the vector that satisfies some test
 577 | ||| @ p the test to satisfy
 578 | |||
 579 | ||| ```idris example
 580 | ||| find (== 3) [1,2,3,4]
 581 | ||| ```
 582 | public export
 583 | find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
 584 | find p []      = Nothing
 585 | find p (x::xs) = if p x then Just x else find p xs
 586 |
 587 | ||| Find the index of the first element of the vector that satisfies some test
 588 | |||
 589 | ||| ```idris example
 590 | ||| findIndex (== 3) [1,2,3,4]
 591 | ||| ```
 592 | public export
 593 | findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
 594 | findIndex p []        = Nothing
 595 | findIndex p (x :: xs) = if p x then Just FZ else FS <$> findIndex p xs
 596 |
 597 | ||| Find the indices of all elements that satisfy some test
 598 | |||
 599 | ||| ```idris example
 600 | ||| findIndices (< 3) [1,2,3,4]
 601 | ||| ```
 602 | public export
 603 | findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
 604 | findIndices p []        = []
 605 | findIndices p (x :: xs)
 606 |      = let is = FS <$> findIndices p xs in
 607 |            if p x then FZ :: is else is
 608 |
 609 | ||| Find the index of the first element of the vector that satisfies some test
 610 | |||
 611 | ||| ```idris example
 612 | ||| elemIndexBy (==) 3 [1,2,3,4]
 613 | ||| ```
 614 | public export
 615 | elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
 616 | elemIndexBy p e = findIndex $ p e
 617 |
 618 | ||| Find the index of the first element of the vector equal to the given one.
 619 | |||
 620 | ||| ```idris example
 621 | ||| elemIndex 3 [1,2,3,4]
 622 | ||| ```
 623 | public export
 624 | elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
 625 | elemIndex = elemIndexBy (==)
 626 |
 627 | ||| Find the indices of all elements that satisfy some test
 628 | |||
 629 | ||| ```idris example
 630 | ||| elemIndicesBy (<=) 3 [1,2,3,4]
 631 | ||| ```
 632 | public export
 633 | elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
 634 | elemIndicesBy p e = findIndices $ p e
 635 |
 636 | ||| Find the indices of all elements equal to the given one
 637 | |||
 638 | ||| ```idris example
 639 | ||| elemIndices 3 [1,2,3,4,3]
 640 | ||| ```
 641 | public export
 642 | elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
 643 | elemIndices = elemIndicesBy (==)
 644 |
 645 | --------------------------------------------------------------------------------
 646 | -- Filters
 647 | --------------------------------------------------------------------------------
 648 |
 649 | ||| Find all elements of a vector that satisfy some test
 650 | |||
 651 | ||| ```idris example
 652 | ||| filter (< 3) (fromList [1,2,3,4])
 653 | ||| ```
 654 | public export
 655 | filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
 656 | filter p []      = ( _ ** [] )
 657 | filter p (x::xs) =
 658 |   let (_ ** tail) = filter p xs
 659 |    in if p x then
 660 |         (_ ** x::tail)
 661 |       else
 662 |         (_ ** tail)
 663 |
 664 | public export
 665 | nubByImpl : Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
 666 | nubByImpl acc p []      = (_ ** [])
 667 | nubByImpl acc p (x::xs) with (elemBy p x acc)
 668 |   nubByImpl acc p (x :: xs) | True  = nubByImpl acc p xs
 669 |   nubByImpl acc p (x :: xs) | False with (nubByImpl (x::acc) p xs)
 670 |     nubByImpl acc p (x :: xs) | False | (_ ** tail) = (_ ** x::tail)
 671 |
 672 | ||| Make the elements of some vector unique by some test
 673 | |||
 674 | ||| ```idris example
 675 | ||| nubBy (==) (fromList [1,2,2,3,4,4])
 676 | ||| ```
 677 | public export
 678 | nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
 679 | nubBy = nubByImpl []
 680 |
 681 | ||| Make the elements of some vector unique by the default Boolean equality
 682 | |||
 683 | ||| ```idris example
 684 | ||| nub (fromList [1,2,2,3,4,4])
 685 | ||| ```
 686 | public export
 687 | nub : Eq elem => Vect len elem -> (p ** Vect p elem)
 688 | nub = nubBy (==)
 689 |
 690 | ||| Delete first element from list according to some test
 691 | |||
 692 | ||| ```idris example
 693 | ||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])
 694 | ||| ```
 695 | public export
 696 | deleteBy : {len : _} -> -- needed for the dependent pair
 697 |            (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
 698 | deleteBy _  _ []      = (_ ** [])
 699 | deleteBy eq x (y::ys) =
 700 |   let (len ** zs) = deleteBy eq x ys
 701 |   in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
 702 |
 703 | ||| Delete first element from list equal to the given one
 704 | |||
 705 | ||| ```idris example
 706 | ||| delete 2 (fromList [1,2,2,3,4,4])
 707 | ||| ```
 708 | public export
 709 | delete : {len : _} ->
 710 |          Eq elem => elem -> Vect len elem -> (p ** Vect p elem)
 711 | delete = deleteBy (==)
 712 |
 713 | --------------------------------------------------------------------------------
 714 | -- Splitting and breaking vects
 715 | --------------------------------------------------------------------------------
 716 |
 717 | ||| A tuple where the first element is a `Vect` of the `n` first elements and
 718 | ||| the second element is a `Vect` of the remaining elements of the original.
 719 | ||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
 720 | ||| but is more efficient.
 721 | |||
 722 | ||| @ n   the index to split at
 723 | ||| @ xs  the `Vect` to split in two
 724 | |||
 725 | ||| ```idris example
 726 | ||| splitAt 2 (fromList [1,2,3,4])
 727 | ||| ```
 728 | public export
 729 | splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
 730 | splitAt Z xs = ([], xs)
 731 | splitAt (S k) (x :: xs) with (splitAt k {m} xs)
 732 |   splitAt (S k) (x :: xs) | (tk, dr) = (x :: tk, dr)
 733 |
 734 | ||| A tuple where the first element is a `Vect` of the `n` elements passing given test
 735 | ||| and the second element is a `Vect` of the remaining elements of the original.
 736 | |||
 737 | ||| ```idris example
 738 | ||| partition (== 2) (fromList [1,2,3,2,4])
 739 | ||| ```
 740 | public export
 741 | partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
 742 | partition p []      = ((_ ** []), (_ ** []))
 743 | partition p (x::xs) =
 744 |   let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
 745 |     if p x then
 746 |       ((S leftLen ** x::lefts), (rightLen ** rights))
 747 |     else
 748 |       ((leftLen ** lefts), (S rightLen ** x::rights))
 749 |
 750 | ||| Split a vector whose length is a multiple of two numbers, k times n, into k
 751 | ||| sections of length n.
 752 | |||
 753 | ||| ```idris example
 754 | ||| > kSplits 2 4 [1, 2, 3, 4, 5, 6, 7, 8]
 755 | ||| [[1, 2, 3, 4], [5, 6, 7, 8]]
 756 | ||| ```
 757 | public export
 758 | kSplits : (k, n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
 759 | kSplits 0     n xs = []
 760 | kSplits (S k) n xs = let (ys, zs) = splitAt n xs
 761 |                      in ys :: kSplits k n zs
 762 |
 763 | ||| Split a vector whose length is a multiple of two numbers, k times n, into n
 764 | ||| sections of length k.
 765 | |||
 766 | ||| ```idris example
 767 | ||| > nSplits 2 4 [1, 2, 3, 4, 5, 6, 7, 8]
 768 | ||| [[1, 5], [2, 6], [3, 7], [4, 8]]
 769 | ||| ```
 770 | public export
 771 | nSplits : (k, n : Nat) -> Vect (k * n) a -> Vect n (Vect k a)
 772 | -- implemented via matrix transposition, so the definition is further down
 773 |
 774 | --------------------------------------------------------------------------------
 775 | -- Predicates
 776 | --------------------------------------------------------------------------------
 777 |
 778 | ||| Verify vector prefix
 779 | |||
 780 | ||| ```idris example
 781 | ||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
 782 | ||| ```
 783 | public export
 784 | isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
 785 | isPrefixOfBy p [] right        = True
 786 | isPrefixOfBy p left []         = False
 787 | isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
 788 |
 789 | ||| Verify vector prefix
 790 | |||
 791 | ||| ```idris example
 792 | ||| isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])
 793 | ||| ```
 794 | public export
 795 | isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
 796 | isPrefixOf = isPrefixOfBy (==)
 797 |
 798 | ||| Verify vector suffix
 799 | |||
 800 | ||| ```idris example
 801 | ||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
 802 | ||| ```
 803 | public export
 804 | isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
 805 | isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
 806 |
 807 | ||| Verify vector suffix
 808 | |||
 809 | ||| ```idris example
 810 | ||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
 811 | ||| ```
 812 | public export
 813 | isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
 814 | isSuffixOf = isSuffixOfBy (==)
 815 |
 816 | --------------------------------------------------------------------------------
 817 | -- Conversions
 818 | --------------------------------------------------------------------------------
 819 |
 820 | ||| Convert Maybe type into Vect
 821 | |||
 822 | ||| ```idris example
 823 | ||| maybeToVect (Just 2)
 824 | ||| ```
 825 | public export
 826 | maybeToVect : Maybe elem -> (p ** Vect p elem)
 827 | maybeToVect Nothing  = (_ ** [])
 828 | maybeToVect (Just j) = (_ ** [j])
 829 |
 830 | ||| Convert first element of Vect (if exists) into Maybe.
 831 | |||
 832 | ||| ```idris example
 833 | ||| vectToMaybe [2]
 834 | ||| ```
 835 | public export
 836 | vectToMaybe : Vect len elem -> Maybe elem
 837 | vectToMaybe []      = Nothing
 838 | vectToMaybe (x::xs) = Just x
 839 |
 840 | --------------------------------------------------------------------------------
 841 | -- Misc
 842 | --------------------------------------------------------------------------------
 843 |
 844 | ||| Filter out Nothings from Vect and unwrap the Justs
 845 | |||
 846 | ||| ```idris example
 847 | ||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
 848 | ||| ```
 849 | public export
 850 | catMaybes : (xs : Vect n (Maybe elem)) -> (p ** Vect p elem)
 851 | catMaybes []             = (_ ** [])
 852 | catMaybes (Nothing::xs)  = catMaybes xs
 853 | catMaybes ((Just j)::xs) =
 854 |   let (_ ** tail) = catMaybes xs
 855 |    in (_ ** j::tail)
 856 |
 857 | ||| Get diagonal elements
 858 | |||
 859 | ||| ```idris example
 860 | ||| diag [[1,2,3], [4,5,6], [7,8,9]]
 861 | ||| ```
 862 | public export
 863 | diag : Vect len (Vect len elem) -> Vect len elem
 864 | diag []             = []
 865 | diag ((x::xs)::xss) = x :: diag (map tail xss)
 866 |
 867 | namespace Fin
 868 |
 869 |   public export
 870 |   tabulate : {len : Nat} -> (Fin len -> a) -> Vect len a
 871 |   tabulate {len = Z} f = []
 872 |   tabulate {len = S _} f = f FZ :: tabulate (f . FS)
 873 |
 874 |   public export
 875 |   range : {len : Nat} -> Vect len (Fin len)
 876 |   range = tabulate id
 877 |
 878 | namespace Subset
 879 |
 880 |   public export
 881 |   tabulate : {len : Nat} -> (Subset Nat (`LT` len) -> a) -> Vect len a
 882 |   tabulate {len = Z} f = []
 883 |   tabulate {len = S _} f
 884 |     = f (Element Z ltZero)
 885 |     :: Subset.tabulate (\ (Element n prf) => f (Element (S n) (LTESucc prf)))
 886 |
 887 |   public export
 888 |   range : {len : Nat} -> Vect len (Subset Nat (`LT` len))
 889 |   range = tabulate id
 890 |
 891 | --------------------------------------------------------------------------------
 892 | -- Zippable
 893 | --------------------------------------------------------------------------------
 894 |
 895 | public export
 896 | Zippable (Vect k) where
 897 |   zipWith _ [] [] = []
 898 |   zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
 899 |
 900 |   zipWith3 _ [] [] [] = []
 901 |   zipWith3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3 f xs ys zs
 902 |
 903 |   unzipWith f [] = ([], [])
 904 |   unzipWith f (x :: xs) = let (b, c) = f x
 905 |                               (bs, cs) = unzipWith f xs in
 906 |                               (b :: bs, c :: cs)
 907 |
 908 |   unzipWith3 f [] = ([], [], [])
 909 |   unzipWith3 f (x :: xs) = let (b, c, d) = f x
 910 |                                (bs, cs, ds) = unzipWith3 f xs in
 911 |                                (b :: bs, c :: cs, d :: ds)
 912 |
 913 | export
 914 | zipWithIndexLinear : (0 f : _) -> (xs, ys : Vect n a) -> (i : Fin n) -> index i (zipWith f xs ys) = f (index i xs) (index i ys)
 915 | zipWithIndexLinear _ (_::xs) (_::ys) FZ     = Refl
 916 | zipWithIndexLinear f (_::xs) (_::ys) (FS i) = zipWithIndexLinear f xs ys i
 917 |
 918 | export
 919 | 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)
 920 | zipWith3IndexLinear _ (_::xs) (_::ys) (_::zs) FZ     = Refl
 921 | zipWith3IndexLinear f (_::xs) (_::ys) (_::zs) (FS i) = zipWith3IndexLinear f xs ys zs i
 922 |
 923 | --------------------------------------------------------------------------------
 924 | -- Permutation
 925 | --------------------------------------------------------------------------------
 926 |
 927 | ||| Rearrange the elements of a vector according to some permutation of its
 928 | ||| indices.
 929 | ||| @ v the vector whose elements to rearrange
 930 | ||| @ p the permutation to apply
 931 | |||
 932 | ||| ```idris example
 933 | ||| > permute ['a', 'b', 'c', 'd'] [0, 3, 2, 1]
 934 | ||| ['a', 'd' , 'c' ,'b']
 935 | ||| ```
 936 | export
 937 | permute : (v : Vect len a) -> (p : Vect len (Fin len)) -> Vect len a
 938 | permute v p = (`index` v) <$> p
 939 |
 940 | --------------------------------------------------------------------------------
 941 | -- Matrix transposition
 942 | --------------------------------------------------------------------------------
 943 |
 944 | ||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
 945 | |||
 946 | ||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
 947 | |||
 948 | ||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
 949 | |||
 950 | ||| ```idris example
 951 | ||| transpose [[1,2], [3,4], [5,6], [7,8]]
 952 | ||| ```
 953 | public export
 954 | transpose : {n : _} -> (array : Vect m (Vect n elem)) -> Vect n (Vect m elem)
 955 | transpose []        = replicate _ []                 -- = [| [] |]
 956 | transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
 957 |
 958 | -- nSplits from earlier on
 959 | nSplits k n = transpose . kSplits k n
 960 |
 961 | --------------------------------------------------------------------------------
 962 | -- Applicative/Monad/Traversable
 963 | --------------------------------------------------------------------------------
 964 | -- These only work if the length is known at run time!
 965 |
 966 | public export
 967 | implementation {k : Nat} -> Applicative (Vect k) where
 968 |     pure = replicate _
 969 |     fs <*> vs = zipWith apply fs vs
 970 |
 971 | -- ||| This monad is different from the List monad, (>>=)
 972 | -- ||| uses the diagonal.
 973 | public export
 974 | implementation {k : Nat} -> Monad (Vect k) where
 975 |     m >>= f = diag (map f m)
 976 |
 977 | public export
 978 | implementation Traversable (Vect k) where
 979 |     traverse f []        = pure []
 980 |     traverse f (x :: xs) = [| f x :: traverse f xs |]
 981 |
 982 | --------------------------------------------------------------------------------
 983 | -- Semigroup/Monoid
 984 | --------------------------------------------------------------------------------
 985 |
 986 | public export
 987 | Semigroup a => Semigroup (Vect k a) where
 988 |   (<+>) = zipWith (<+>)
 989 |
 990 | public export
 991 | {k : Nat} -> Monoid a => Monoid (Vect k a) where
 992 |   neutral = replicate k neutral
 993 |
 994 | --------------------------------------------------------------------------------
 995 | -- Show
 996 | --------------------------------------------------------------------------------
 997 |
 998 | export
 999 | implementation Show elem => Show (Vect len elem) where
1000 |     show = show . toList
1001 |
1002 | -- Some convenience functions for testing lengths
1003 |
1004 | -- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
1005 | -- only know we don't know how to make a Vect n a, not that one can't exist.
1006 | export
1007 | exactLength : {m : Nat} -> -- expected at run-time
1008 |               (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
1009 | exactLength {m} len xs with (decEq m len)
1010 |   exactLength {m = m} m xs | (Yes Refl) = Just xs
1011 |   exactLength {m = m} len xs | (No contra) = Nothing
1012 |
1013 | ||| If the given Vect is at least the required length, return a Vect with
1014 | ||| at least that length in its type, otherwise return Nothing
1015 | ||| @len the required length
1016 | ||| @xs the vector with the desired length
1017 | export
1018 | overLength : {m : Nat} -> -- expected at run-time
1019 |              (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)
1020 | overLength n xs with (cmp m n)
1021 |   overLength {m}   (plus m (S y)) xs | (CmpLT y) = Nothing
1022 |   overLength {m}                m xs | CmpEQ     = Just (0 ** xs)
1023 |   overLength {m = plus n (S x)} n xs | (CmpGT x)
1024 |          = Just (S x ** rewrite plusCommutative (S x) n in xs)
1025 |