
  0 | module CatList
  1 | 
  2 | import CatenableList
  3 | import Queue
  4 | 
  5 | %default total
  6 | 
  7 | export
  8 | partial
  9 | data CatList : (Type -> Type) -> Type -> Type where
 10 |   E : CatList q a
 11 |   C : {q : Type -> Type} -> a -> q (Lazy (CatList q a)) -> CatList q a
 12 | 
 13 | partial
 14 | link : Queue q => CatList q a -> Lazy (CatList q a) -> CatList q a
 15 | link c s = case c of
 16 |   (C x xs) => C x (snoc xs s)
 17 |   E => idris_crash "link: to E"
 18 | 
 19 | partial
 20 | linkAll : {q : Type -> Type} -> Queue q => CatList q a -> q (Lazy (CatList q a)) -> CatList q a
 21 | linkAll t q' =
 22 |   if isEmpty q'
 23 |    then t
 24 |    else link t (linkAll (force $ Queue.head q') (assert_smaller q' $ tail q'))
 25 | 
 26 | export
 27 | partial
 28 | {q : Type -> Type} -> Queue q => CatenableList (CatList q) where
 29 |   empty = E
 30 |   isEmpty E = True
 31 |   isEmpty _ = False
 32 | 
 33 |   xs ++ E  = xs
 34 |   E  ++ ys = ys
 35 |   xs ++ ys = link xs ys
 36 | 
 37 |   cons x xs = (C x empty) ++ xs
 38 |   snoc xs x = xs ++ (C x empty)
 39 | 
 40 |   head E = idris_crash "empty list"
 41 |   head (C x _) = x
 42 | 
 43 |   tail E = idris_crash "empty list"
 44 |   tail (C x xs) =
 45 |     if isEmpty xs then E else linkAll (force $ Queue.head xs) (tail xs)
 46 |