
  0 | module Data.TCQueue
  1 | 
  2 | %default total
  3 | 
  4 | public export
  5 | data Tree : (f : Type -> Type) -> (a, b : Type) -> Type where
  6 |   Leaf : (a -> f b) -> Tree f a b
  7 |   Node : {0 x : _} -> Tree f a x -> Tree f x b -> Tree f a b
  8 | 
  9 | public export
 10 | data TCQueue : (f : Type -> Type) -> (a, b : Type) -> Type where
 11 |   Empty  : TCQueue f a a
 12 |   Filled : Tree f a b -> TCQueue f a b
 13 | 
 14 | public export %inline
 15 | empty : TCQueue f a a
 16 | empty = Empty
 17 | 
 18 | public export %inline
 19 | singleton : (a -> f b) -> TCQueue f a b
 20 | singleton = Filled . Leaf
 21 | 
 22 | public export
 23 | cons : (a -> f x) -> TCQueue f x b -> TCQueue f a b
 24 | cons g Empty      = singleton g
 25 | cons g (Filled y) = Filled (Node (Leaf g) y)
 26 | 
 27 | public export
 28 | snoc : TCQueue f a x -> (x -> f b) -> TCQueue f a b
 29 | snoc Empty g      = singleton g
 30 | snoc (Filled y) g = Filled (Node y (Leaf g))
 31 | 
 32 | public export
 33 | (++) : TCQueue f a x -> TCQueue f x b -> TCQueue f a b
 34 | Empty    ++ w        = w
 35 | v        ++ Empty    = v
 36 | Filled v ++ Filled w = Filled (Node v w)
 37 | 
 38 | export infixr 5 :|
 39 | 
 40 | ||| Left-edge deconstruction
 41 | public export
 42 | data ViewL : (f : Type -> Type) ->  (a,b : Type) -> Type where
 43 |   EmptyV : ViewL f a a
 44 |   (:|)   : {0 x : _} -> (a -> f x) -> (TCQueue f x b) -> ViewL f a b
 45 | 
 46 | public export
 47 | uncons : TCQueue f a b -> ViewL f a b
 48 | uncons Empty               = EmptyV
 49 | uncons (Filled $ Leaf g)   = g :| Empty
 50 | uncons (Filled $ Node v w) = go v w
 51 | 
 52 |   where
 53 |     go : Tree f a x -> Tree f x b -> ViewL f a b
 54 |     go (Leaf g) w   = g :| Filled w
 55 |     go (Node y z) w = go y (Node z w)
 56 |