
  0 | module Data.Vect.Ex
  1 | 
  2 | import Data.Fin.Minus
  3 | import Data.List1
  4 | import Data.SortedMap
  5 | import Data.SortedSet
  6 | import Data.Vect
  7 | 
  8 | %default total
  9 | 
 10 | public export
 11 | mapI : (f : Fin n -> a -> b) -> Vect n a -> Vect n b
 12 | mapI f []      = []
 13 | mapI f (x::xs) = f FZ x :: mapI (f . FS) xs
 14 | 
 15 | export
 16 | toListI : Vect n a -> List (a, Fin n)
 17 | toListI []      = []
 18 | toListI (x::xs) = (x, FZ) :: (map FS <$> toListI xs)
 19 | 
 20 | export %inline
 21 | withIndex : Vect n a -> Vect n (Fin n, a)
 22 | withIndex = mapI (,)
 23 | 
 24 | public export
 25 | drop'' : (xs : Vect n a) -> (count : Fin $ S n) -> Vect (n - count) a
 26 | drop'' xs      FZ     = xs
 27 | drop'' (_::xs) (FS c) = drop'' xs c
 28 | 
 29 | export
 30 | mapPre : ((i : Fin n) -> Vect (finToNat i) b -> a -> b) -> Vect n a -> Vect n b
 31 | mapPre f []      = []
 32 | mapPre f (x::xs) = let y = f FZ [] x in y :: mapPre (\i, ys => f (FS i) (y::ys)) xs
 33 | 
 34 | export
 35 | fromMap : {n : _} -> SortedMap (Fin n) a -> Vect n (Maybe a)
 36 | fromMap = foldl (flip . uncurry $ \i => replaceAt i . Just) (replicate _ Nothing) . SortedMap.toList
 37 | 
 38 | export
 39 | presenceVect : {n : _} -> SortedSet (Fin n) -> Vect n Bool
 40 | presenceVect = tabulate . flip contains
 41 | 
 42 | public export
 43 | reverseMapping : Ord a => Vect n a -> SortedMap a $ List1 $ Fin n
 44 | reverseMapping = concat . mapI (\idx, x => singleton x $ singleton idx)
 45 |