
  0 | module PhysicistsQueue
  1 | 
  2 | import Data.List
  3 | 
  4 | import Queue
  5 | 
  6 | %default total
  7 | 
  8 | export
  9 | data PhysicistsQueue a = PQ (List a) Int (Lazy (List a)) Int (List a)
 10 | 
 11 | checkw : List a -> Int -> List a -> Int -> List a -> PhysicistsQueue a
 12 | checkw [] lenf f lenr r = PQ f lenf f lenr r
 13 | checkw w  lenf f lenr r = PQ w lenf f lenr r
 14 | 
 15 | check : List a -> Int -> List a -> Int -> List a -> PhysicistsQueue a
 16 | check w lenf f lenr r =
 17 |   if lenr <= lenf then checkw w lenf f lenr r
 18 |   else checkw f (lenf + lenr) (f ++ reverse r) 0 []
 19 | 
 20 | export
 21 | partial
 22 | Queue PhysicistsQueue where
 23 |   empty = PQ [] 0 [] 0 []
 24 |   isEmpty (PQ w lenf f lenr r) = lenf == 0
 25 | 
 26 |   snoc (PQ w lenf f lenr r) x = check w lenf f (lenr + 1) (x :: r)
 27 | 
 28 |   head (PQ []       lenf f lenr r) = idris_crash "empty queue"
 29 |   head (PQ (x :: w) lenf f lenr r) = x
 30 | 
 31 |   tail (PQ []       lenf f lenr r) = idris_crash "empty queue"
 32 |   tail (PQ (x :: w) lenf f lenr r) = check w (lenf - 1) (tail {ok = nef} f) lenr r
 33 |    where nef = believe_me "f = x :: w ++ _"
 34 |