1 | module Data.DList

  3 | import Data.Singleton

  4 | import Data.DSum

  5 | import Data.Some

 11 | public export

 12 | data DList : (f : a -> Type) -> (ts : List a) -> Type where

 13 |   ||| The empty dependent list

 14 |   Nil : DList f Nil

 15 |   ||| Prepends a dependently typed element to a dependent list

 16 |   (::) : {0 x : a} -> f x -> DList f xs -> DList f (x :: xs)

 21 | public export

 22 | (++) : DList f xs -> DList f ys -> DList f (xs ++ ys)

 23 | Nil         ++ fys = fys

 24 | (fx :: fxs) ++ fys = fx :: fxs ++ fys

 28 | length : DList f xs -> Nat

 29 | length Nil = Z

 30 | length (x :: xs) = S (length xs)

 34 | head : DList f (x :: xs) -> f x

 35 | head (fx :: fxs) = fx

 39 | tail : DList f (x :: xs) -> DList f xs

 40 | tail (fx :: fxs) = fxs

 44 | split : {xs, xs' : List a} -> DList f (xs ++ xs') -> (DList f xs, DList f xs')

 45 | split {xs = Nil} dl = (Nil, dl)

 46 | split {xs = x :: xs''} (fx :: fxs''') = let (fxs'', fxs') = split (fxs''') in (fx :: fxs'', fxs')

 52 | pushToParams : DList (f . g) ts -> DList f (map g ts)

 59 | pushToParams xs = believe_me xs

 63 | pullFromParams : DList f (map g ts) -> DList (f . g) ts

 67 | pullFromParams xs = believe_me xs

 73 | dmap : ({0 x : t} -> a x -> b x) -> DList a xs -> DList b xs

 74 | dmap f Nil = Nil

 75 | dmap f (ax :: axs) = f ax :: dmap f axs

 80 | undmap : ({0 x : t} -> a x -> b) -> DList a xs -> List b

 81 | undmap f Nil = Nil

 82 | undmap f (ax :: axs) = f ax :: undmap f axs

 87 | dmapList : ((x : t) -> f x) -> (xs : List t) -> DList f xs

 88 | dmapList g Nil = Nil

 89 | dmapList g (x :: xs) = g x :: dmapList g xs

 95 |    : (0 f : a -> b)

 96 |   -> ((x : a) -> g (f x))

 97 |   -> (xs : List a)

 98 |   -> DList g (map f xs)

 99 | dmapList' f gg xs = pushToParams (dmapList gg xs)

110 |    : Monad f

111 |   => {0 t : Type}

112 |   -> {0 a, b : t -> Type}

113 |   -> {0 xs : List t}

115 |   -> ({0 x : t} -> a x -> f (b x))

116 |   -> DList a xs

117 |   -> f (DList b xs)

119 | dtraverse f Nil = pure Nil

120 | dtraverse f (ax :: axs) = do

121 |   bx <- f ax

122 |   bxs <- dtraverse f axs

124 |   pure (bx :: bxs)

131 |    : Monad m

132 |   => {0 a : Type}

133 |   -> {0 g : a -> Type}

135 |   -> ((x : a) -> m (g x))

136 |   -> (xs : List a)

137 |   -> m (DList g xs)

139 | dtraverseList f xs = dtraverse (\(Val x) => f x) (dmapList Val xs)

148 | dfoldr : ({0 x : t} -> el x -> acc -> acc) -> acc -> DList el ts -> acc

149 | dfoldr f acc Nil = acc

150 | dfoldr f acc (x :: xs) = f x $ dfoldr f acc xs

154 | dfoldl : ({0 x : t} -> acc -> el x -> acc) -> acc -> DList el ts -> acc

155 | dfoldl f acc Nil = acc

156 | dfoldl f acc (x :: xs) = dfoldl f (f acc x) xs

163 |    : ({0 x : t} -> f x -> (g x, h x))

164 |   -> (DList f xs)

165 |   -> (DList g xs, DList h xs)

166 | dunzipWith func Nil = (Nil, Nil)

167 | dunzipWith func (fx :: fxs) = let

168 |   (gx, hx) = func fx

169 |   (gxs, hxs) = dunzipWith func fxs

170 |   in (gx :: gxs, hx :: hxs)

175 |    : DList (\x => (f x, g x)) xs

176 |   -> (DList f xs, DList g xs)

177 | dunzip = dunzipWith id

182 |    : ({0 x : t} -> f x -> g x -> h x)

183 |   -> DList f xs

184 |   -> DList g xs

185 |   -> DList h xs

186 | dzipWith func Nil Nil = Nil

187 | dzipWith func (fx :: fxs) (gx :: gxs) = (func fx gx) :: dzipWith func fxs gxs

192 |    : DList f xs

193 |   -> DList g xs

194 |   -> DList (\x => (f x, g x)) xs

195 | dzip = dzipWith (,)

201 |    : {0 f : b -> Type}

202 |   -> (a -> (y ** f y))

203 |   -> List a

204 |   -> (ys ** DList f ys)

205 | unzipParamsWith g Nil = (Nil ** Nil)

206 | unzipParamsWith g (x :: xs) = let

207 |     (y ** fy) = g x

208 |     (ys ** fys) = unzipParamsWith g xs

209 |   in (y :: ys ** fy :: fys)

215 |    : {0 f : a -> Type}

216 |   -> (dpairs : List (x ** f x))

217 |   -> (xs ** DList f xs)

218 | unzipParams = unzipParamsWith id

223 |    : {0 f : b -> Type}

224 |   -> ((y : b) -> f y -> a)

225 |   -> (ys ** DList f ys)

226 |   -> List a

227 | zipParamsWith g (Nil ** Nil) = Nil

228 | zipParamsWith g (y :: ys ** fy :: fys) = let

229 |     x = g y fy

230 |     xs = zipParamsWith g (ys ** fys)

231 |   in (x :: xs)

235 | zipParams : {0 f : b -> Type} -> (ys ** DList f ys) -> List (y ** f y)

236 | zipParams dpairs = zipParamsWith (\y => \fy => (y ** fy)) dpairs

240 | unzipDSums : List (DSum f g) -> (Some (DList f), Some (DList g))

241 | unzipDSums Nil = (MkSome Nil, MkSome Nil)

242 | unzipDSums ((fx :=> gx) :: dsums) = let

243 |   (MkSome fxs, MkSome gxs) = unzipDSums dsums

244 |   in (MkSome (fx :: fxs), MkSome (gx :: gxs))

248 | zipToDSums : DList f xs -> DList g xs -> List (DSum f g)

249 | zipToDSums xs ys = undmap id (dzipWith (:=>) xs ys {h = const (DSum f g)})

254 |    : {0 f, g, h : t -> Type}

255 |   -> ({0 x : t} -> f x -> (g x, h x))

256 |   -> (dpairs : List (x : t ** (f x)))

257 |   -> (DList g (map DPair.fst dpairs), DList h (map DPair.fst dpairs))

258 | unzipDPairsWith func Nil = (Nil, Nil)

259 | unzipDPairsWith func ((x ** fx) :: dpairs) = let

260 |   (gx, hx) = func fx

261 |   (gxs, hxs) = unzipDPairsWith func dpairs

262 |   in (gx :: gxs, hx :: hxs)

268 |    : (dpairs : List (x : t ** (f x, g x)))

269 |   -> (DList f (map DPair.fst dpairs), DList g (map DPair.fst dpairs))

270 | unzipDPairs xs = unzipDPairsWith id xs

276 |    : {xs : List t}

277 |   -> {0 f, g, h : t -> Type}

278 |   -> ({0 x : t} -> f x -> g x -> h x)

279 |   -> DList f xs

280 |   -> DList g xs

281 |   -> List (x : t ** h x)

282 | zipToDPairsWith {xs} func fxs gxs = zipParams (xs ** dzipWith func fxs gxs)

288 |    : {xs : List t}

289 |   -> DList f xs

290 |   -> DList g xs

291 |   -> List (x : t ** (f x, g x))

292 | zipToDPairs = zipToDPairsWith (,)