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