
  0 | module Data.Queue1
  1 | 
  2 | import Data.List
  3 | import Data.List1
  4 | import Data.SnocList
  5 | 
  6 | %default total
  7 | 
  8 | -------------
  9 | --- Queue ---
 10 | -------------
 11 | 
 12 | -- add from right, remove from left
 13 | export
 14 | record Queue1 a where
 15 |   constructor MkQueue
 16 |   right : SnocList a
 17 |   left  : List1 a
 18 | 
 19 | export
 20 | singleton : a -> Queue1 a
 21 | singleton = MkQueue [<] . singleton
 22 | 
 23 | export
 24 | add : a -> Queue1 a -> Queue1 a
 25 | add x = { right $= (:< x) }
 26 | 
 27 | -- Constructs a `Queue1` which has all elements in the left part of the queue reverted
 28 | %inline
 29 | pureLeftsFromSnoc : SnocList a -> Maybe $ Queue1 a
 30 | pureLeftsFromSnoc = map (MkQueue [<]) . fromList . cast
 31 | 
 32 | export
 33 | remove : Queue1 a -> (a, Lazy (Maybe $ Queue1 a))
 34 | remove $ MkQueue r (head ::: l) = (head,) $ delay $ case l of
 35 |   []      => pureLeftsFromSnoc r
 36 |   (x::xs) => Just $ MkQueue r (x:::xs)
 37 | 
 38 | export
 39 | Functor Queue1 where
 40 |   map f = { left $= map f, right $= map f }
 41 | 
 42 | export
 43 | filter : (a -> Bool) -> Queue1 a -> Maybe $ Queue1 a
 44 | filter f $ MkQueue r l = do
 45 |   let filteredR = filter f r
 46 |   let Just filteredL = fromList $ filter f $ toList l
 47 |     | Nothing => pureLeftsFromSnoc filteredR
 48 |   Just $ MkQueue filteredR filteredL
 49 | 
 50 | ||| Returns a `List1` with newly added elements on the right and older elements in the left
 51 | export
 52 | toList1 : Queue1 a -> List1 a
 53 | toList1 $ MkQueue r l = l `appendl` cast r
 54 |