
  0 | module BootstrappedQueue
  1 | 
  2 | import Data.List
  3 | 
  4 | import Queue
  5 | 
  6 | %default total
  7 | 
  8 | export
  9 | data BootstrappedQueue a = E | Q Int (List a) (BootstrappedQueue (Lazy (List a))) Int (List a)
 10 | 
 11 | mutual
 12 |   checkF : Int -> List a -> BootstrappedQueue (Lazy (List a)) -> Int -> List a
 13 |         -> BootstrappedQueue a
 14 |   checkF lenfm [] E lenr r = E
 15 |   checkF lenfm [] m lenr r = Q lenfm (force $ head m) (tail m) lenr r
 16 |   checkF lenfm f  m lenr r = Q lenfm f m lenr r
 17 | 
 18 |   checkQ : Int -> List a -> BootstrappedQueue (Lazy (List a)) -> Int -> List a
 19 |         -> BootstrappedQueue a
 20 |   checkQ lenfm f m lenr r =
 21 |     if lenr <= lenfm then checkF lenfm f m lenr r
 22 |     else checkF (lenfm + lenr) f (snoc m (delay $ reverse r)) 0 []
 23 | 
 24 |   export
 25 |   Queue BootstrappedQueue where
 26 |     empty = E -- Incorrect in original: Q 0 [] E 0 []
 27 |     isEmpty E = True
 28 |     isEmpty _ = False
 29 | 
 30 |     snoc E x = Q 1 [x] E 0 [] -- Incorrect in original: q 1 [x] E 0 []
 31 |     snoc (Q lenfm f m lenr r) x = assert_total $ checkQ lenfm f m (lenr + 1) (x :: r)
 32 | 
 33 |     head E                            = idris_crash "empty queue"
 34 |     head (Q lenfm (x :: f') m lenr r) = x
 35 |     head (Q _     []        _ _    _) =
 36 |       assert_total $ idris_crash "head: Q with Nil front"
 37 | 
 38 |     tail E                            = idris_crash "empty queue"
 39 |     tail (Q lenfm (x :: f') m lenr r) = assert_total $ checkQ (lenfm - 1) f' m lenr r
 40 |     tail (Q _     []        _ _    _) =
 41 |       assert_total $ idris_crash "tail: Q with Nil front"
 42 |