
  0 | module BankersQueue
  1 | 
  2 | import Queue
  3 | import OStream
  4 | 
  5 | %default total
  6 | 
  7 | export
  8 | data BankersQueue a = BQ Int (OStream a) Int (OStream a)
  9 | 
 10 | check : Int -> OStream a -> Int -> OStream a -> BankersQueue a
 11 | check lenf f lenr r =
 12 |   if lenr <= lenf then BQ lenf f lenr r
 13 |   else BQ (lenf+lenr) (OStream.append f (OStream.reverse r)) 0 []
 14 | 
 15 | export
 16 | partial
 17 | Queue BankersQueue where
 18 |   empty = BQ 0 [] 0 []
 19 |   isEmpty (BQ lenf f lenr r) = lenf == 0
 20 | 
 21 |   snoc (BQ lenf f lenr r) x = check lenf f (lenr + 1) (x :: r)
 22 | 
 23 |   head (BQ lenf []        lenr r) = idris_crash "empty queue"
 24 |   head (BQ lenf (x :: f') lenr r) = x
 25 | 
 26 |   tail (BQ lenf []        lenr r) = idris_crash "empty queue"
 27 |   tail (BQ lenf (x :: f') lenr r) = check (lenf - 1) f' lenr r
 28 |