
   0 | module Data.Vect.Dependent
   1 | 
   2 | import Data.Either
   3 | import Data.Fin.Split
   4 | import Data.Fin.ToFin
   5 | import Data.Vect
   6 | 
   7 | %default total
   8 | 
   9 | public export
  10 | data DVect : (n : Nat) -> (Fin n -> Type) -> Type where
  11 |   Nil  : DVect Z ty
  12 |   (::) : (a : ty FZ) -> DVect n (ty . FS) -> DVect (S n) ty
  13 | 
  14 | %name DVect xs, ys, zs
  15 | 
  16 | --- Indexing ---
  17 | 
  18 | public export
  19 | index : (i : Fin n) -> DVect n a -> a i
  20 | index FZ     (x::_ ) = x
  21 | index (FS i) (_::xs) = index i xs
  22 | 
  23 | --- Creation ---
  24 | 
  25 | public export
  26 | tabulateI : {n : Nat} -> {0 a : Fin n -> Type} -> ((i : Fin n) -> a i) -> DVect n a
  27 | tabulateI {n=Z}   _ = []
  28 | tabulateI {n=S n} f = f FZ :: tabulateI (\i => f $ FS i)
  29 | 
  30 | public export %inline
  31 | tabulate : {n : Nat} -> {0 a : Fin n -> Type} -> ({i : Fin n} -> a i) -> DVect n a
  32 | tabulate f = tabulateI (\i => f {i})
  33 | 
  34 | --- Concating ---
  35 | 
  36 | public export
  37 | (++) : DVect n a -> DVect m b -> DVect (n + m) $ either a b . Split.splitSum
  38 | (++) []      ys = ys
  39 | (++) (x::xs) ys = x :: rewrite funext $ \x => eitherBimapFusion a b FS id $ splitSum x in (xs ++ ys) where
  40 |   0 funext : ((x : _) -> f x = g x) -> f = g
  41 |   funext _ = believe_me $ the (Z = Z) Refl
  42 | 
  43 | --- Changes ---
  44 | 
  45 | public export
  46 | replaceAt : (i : Fin n) -> a i -> DVect n a -> DVect n a
  47 | replaceAt FZ     w (_::xs) = w :: xs
  48 | replaceAt (FS i) w (x::xs) = x :: replaceAt i w xs
  49 | 
  50 | public export
  51 | updateAt : (i : Fin n) -> (a i -> a i) -> DVect n a -> DVect n a
  52 | updateAt FZ     f (x::xs) = f x :: xs
  53 | updateAt (FS i) f (x::xs) = x :: updateAt i f xs
  54 | 
  55 | --- Mappings ---
  56 | 
  57 | public export
  58 | mapI : ((i : Fin n) -> a i -> b i) -> DVect n a -> DVect n b
  59 | mapI f []      = []
  60 | mapI f (x::xs) = f FZ x :: mapI (\i => f $ FS i) xs
  61 | 
  62 | public export %inline
  63 | map : ({i : Fin n} -> a i -> b i) -> DVect n a -> DVect n b
  64 | map f = mapI (\i => f {i})
  65 | 
  66 | public export %inline
  67 | (<$>) : ({i : Fin n} -> a i -> b i) -> DVect n a -> DVect n b
  68 | (<$>) = map
  69 | 
  70 | public export %inline
  71 | (<&>) : DVect n a -> ({i : Fin n} -> a i -> b i) -> DVect n b
  72 | (<&>) = flip map
  73 | 
  74 | public export
  75 | mapPreI : ((i : Fin n) -> DVect (finToNat i) (b . weakenToSuper {i}) -> a i -> b i) -> DVect n a -> DVect n b
  76 | mapPreI f []      = []
  77 | mapPreI f (x::xs) = let y = f FZ [] x in y :: mapPreI (\i, ys => f (FS i) (y::ys)) xs
  78 | 
  79 | public export %inline
  80 | mapPre : ({i : Fin n} -> DVect (finToNat i) (b . weakenToSuper {i}) -> a i -> b i) -> DVect n a -> DVect n b
  81 | mapPre f = mapPreI (\i => f {i})
  82 | 
  83 | --- Conversions ---
  84 | 
  85 | public export
  86 | downmapI : ((i : Fin n) -> a i -> b) -> DVect n a -> Vect n b
  87 | downmapI f []      = []
  88 | downmapI f (x::xs) = f FZ x :: downmapI (\i => f $ FS i) xs
  89 | 
  90 | public export %inline
  91 | downmap : ({i : Fin n} -> a i -> b) -> DVect n a -> Vect n b
  92 | downmap f = downmapI (\i => f {i})
  93 | 
  94 | public export
  95 | upmapI : ((i : Fin n) -> a -> b i) -> Vect n a -> DVect n b
  96 | upmapI f []      = []
  97 | upmapI f (x::xs) = f FZ x :: upmapI (\i => f $ FS i) xs
  98 | 
  99 | public export
 100 | upmap : ({i : Fin n} -> a -> b i) -> Vect n a -> DVect n b
 101 | upmap f = upmapI (\i => f {i})
 102 | 
 103 | --- Zippings ---
 104 | 
 105 | public export
 106 | zip : DVect n a -> DVect n b -> DVect n $ \i => (a i, b i)
 107 | zip []      []      = []
 108 | zip (x::xs) (y::ys) = (x, y) :: zip xs ys
 109 | 
 110 | public export
 111 | zipWithI : ((i : Fin n) -> a i -> b i -> c i) -> DVect n a -> DVect n b -> DVect n c
 112 | zipWithI _ []      []      = []
 113 | zipWithI f (x::xs) (y::ys) = f FZ x y :: zipWithI (\i => f $ FS i) xs ys
 114 | 
 115 | public export %inline
 116 | zipWith : ({i : Fin n} -> a i -> b i -> c i) -> DVect n a -> DVect n b -> DVect n c
 117 | zipWith f = zipWithI (\i => f {i})
 118 | 
 119 | public export
 120 | (<*>) : DVect n (\i => a i -> b i) -> DVect n a -> DVect n b
 121 | (<*>) []      []      = []
 122 | (<*>) (f::fs) (y::ys) = f y :: (fs <*> ys)
 123 | 
 124 | --- Restructuring ---
 125 | 
 126 | public export
 127 | transpose : {m : _} -> {0 a : Fin n -> Fin m -> Type} -> DVect n (\i => DVect m $ \j => a i j) -> DVect m (\j => DVect n $ \i => a i j)
 128 | transpose []      = tabulate []
 129 | transpose (x::xs) = zipWith (::) x $ transpose xs
 130 | 
 131 | --- Foldings ---
 132 | 
 133 | public export
 134 | foldlI : ((i : Fin n) -> acc -> a i -> acc) -> acc -> DVect n a -> acc
 135 | foldlI _ init [] = init
 136 | foldlI f init (x::xs) = foldlI (\i => f $ FS i) (f FZ init x) xs
 137 | 
 138 | public export %inline
 139 | foldl : ({i : Fin n} -> acc -> a i -> acc) -> acc -> DVect n a -> acc
 140 | foldl f = foldlI (\i => f {i})
 141 | 
 142 | public export
 143 | foldrI : ((i : Fin n) -> a i -> Lazy acc -> acc) -> acc -> DVect n a -> acc
 144 | foldrI _ init []      = init
 145 | foldrI f init (x::xs) = f FZ x $ foldrI (\i => f $ FS i) init xs
 146 | 
 147 | public export %inline
 148 | foldr : ({i : Fin n} -> a i -> Lazy acc -> acc) -> acc -> DVect n a -> acc
 149 | foldr f = foldrI (\i => f {i})
 150 | 
 151 | public export
 152 | foldlMI : Monad m => ((i : Fin n) -> acc -> a i -> m acc) -> acc -> DVect n a -> m acc
 153 | foldlMI fm = foldlI (\i, ma, b => ma >>= flip (fm i) b) . pure
 154 | 
 155 | public export
 156 | foldlM : Monad m => ({i : Fin n} -> acc -> a i -> m acc) -> acc -> DVect n a -> m acc
 157 | foldlM f = foldlMI (\i => f {i})
 158 | 
 159 | --- Traversals ---
 160 | 
 161 | public export
 162 | traverseI : Applicative f => ((i : Fin n) -> a i -> f (b i)) -> DVect n a -> f (DVect n b)
 163 | traverseI f []      = pure []
 164 | traverseI f (x::xs) = [| f FZ x :: traverseI (\i => f $ FS i) xs |]
 165 | 
 166 | public export %inline
 167 | traverse : Applicative f => ({i : Fin n} -> a i -> f (b i)) -> DVect n a -> f (DVect n b)
 168 | traverse f = traverseI (\i => f {i})
 169 | 
 170 | public export
 171 | sequence : Applicative f => DVect n (f . a) -> f (DVect n a)
 172 | sequence = traverse id
 173 | 
 174 | public export %inline
 175 | forI : Applicative f => DVect n a -> ((i : Fin n) -> a i -> f (b i)) -> f (DVect n b)
 176 | forI = flip traverseI
 177 | 
 178 | public export %inline
 179 | for : Applicative f => DVect n a -> ({i : Fin n} -> a i -> f (b i)) -> f (DVect n b)
 180 | for = flip traverse
 181 | 
 182 | --- Standard interfaces' implementations ---
 183 | 
 184 | public export
 185 | ({i : Fin n} -> Eq (a i)) => Eq (DVect n a) where
 186 |   (==) = all id .: downmap id .: zipWith (==)
 187 | 
 188 | public export
 189 | ({i : Fin n} -> Ord (a i)) => Ord (DVect n a) where
 190 |   compare = concat .: downmap id .: zipWith compare
 191 | 
 192 | public export
 193 | ({i : Fin n} -> Show (a i)) => Show (DVect n a) where
 194 |   show = concat . ("[" ::) . (`snoc` "]") . intersperse ", " . downmap show
 195 |   -- if you do `show = show . downmap show`, all elements will be wrapped in odd `"`s because of `Show String` instance.
 196 | 
 197 | public export
 198 | ({i : Fin n} -> Semigroup (a i)) => Semigroup (DVect n a) where
 199 |   (<+>) = zipWith (<+>)
 200 | 
 201 | public export
 202 | {n : Nat} -> {0 a : Fin n -> Type} ->
 203 | ({i : Fin n} -> Monoid (a i)) => Monoid (DVect n a) where
 204 |   neutral = tabulate neutral
 205 |