
  0 | module BatchedQueue
  1 | 
  2 | import Data.List
  3 | 
  4 | import Queue
  5 | 
  6 | %default total
  7 | 
  8 | export
  9 | data BatchedQueue a = BQ (List a) (List a)
 10 | 
 11 | check : List a -> List a -> BatchedQueue a
 12 | check [] r = BQ (reverse r) []
 13 | check f  r = BQ f           r
 14 | 
 15 | export
 16 | partial
 17 | Queue BatchedQueue where
 18 |   empty = BQ [] []
 19 |   isEmpty (BQ f r) = isNil f
 20 | 
 21 |   snoc (BQ f r) x = check f (x :: r)
 22 | 
 23 |   head (BQ []       _) = idris_crash "empty queue"
 24 |   head (BQ (x :: f) r) = x
 25 | 
 26 |   tail (BQ []       _) = idris_crash "empty queue"
 27 |   tail (BQ (x :: f) r) = check f r
 28 |