
  0 | module HTTP.API.TList
  1 | 
  2 | import public Data.List.Quantifiers
  3 | 
  4 | %default total
  5 | 
  6 | ||| A list of erased (!) types.
  7 | |||
  8 | ||| This is represents the size of a heterogeneous list (it is just
  9 | ||| a natural number at runtime) and is used to split off a
 10 | ||| predefined prefix off a heterogeneous list.
 11 | public export
 12 | data TList : List Type -> Type where
 13 |   Nil  : TList []
 14 |   (::) : (0 t : Type) -> TList ts -> TList (t::ts)
 15 | 
 16 | ||| We can split a concatenation of heterogeneous lists by removing
 17 | ||| a fixed-sized prefix.
 18 | |||
 19 | ||| As a witness of the size of the prefix, a value of type `TList`
 20 | ||| is required.
 21 | public export
 22 | splitHList : TList ts -> HList (ts ++ rem) -> (HList ts, HList rem)
 23 | splitHList []        vs      = ([],vs)
 24 | splitHList (t :: ts) (v::vs) =
 25 |   let (xs,ys) := splitHList ts vs
 26 |    in (v::xs,ys)
 27 | 
 28 | ||| Concatenates two `TList`s.
 29 | public export
 30 | (++) : TList xs -> TList ys -> TList (xs++ys)
 31 | (++) (t::ts) tys = t :: (ts ++ tys)
 32 | (++) []      tys = tys
 33 |