
  0 | module ImplicitQueue
  1 | 
  2 | import Queue
  3 | 
  4 | %default total
  5 | 
  6 | data Digit a = Zero | One a | Two a a
  7 | 
  8 | export
  9 | data ImplicitQueue a =
 10 |     Shallow (Digit a)
 11 |   | Deep (Digit a) (Lazy (ImplicitQueue (a, a))) (Digit a)
 12 | 
 13 | export
 14 | Queue ImplicitQueue where
 15 |   empty = Shallow Zero
 16 |   isEmpty (Shallow Zero) = True
 17 |   isEmpty x              = False
 18 | 
 19 |   snoc (Shallow Zero) y = Shallow (One y)
 20 |   snoc (Shallow (One x)) y = Deep (Two x y) empty Zero
 21 |   snoc (Deep f m Zero) y = Deep f m (One y)
 22 |   snoc (Deep f m (One x)) y = Deep f (snoc m (x, y)) Zero
 23 |   snoc (Shallow (Two _ _)) _ = assert_total $ idris_crash "snoc: Shallow Two"
 24 |   snoc (Deep _ _ (Two _ _)) _ = assert_total $ idris_crash "snoc: Deep last Two"
 25 | 
 26 |   head (Shallow Zero   ) = idris_crash "empty queue"
 27 |   head (Shallow (One x)) = x
 28 |   head (Deep (One x)   m r) = x
 29 |   head (Deep (Two x y) m r) = x
 30 |   head (Shallow (Two _ _)) = assert_total $ idris_crash "head: Shallow Two"
 31 |   head (Deep Zero _ _) = assert_total $ idris_crash "head: Deep head Zero"
 32 | 
 33 |   tail (Shallow Zero) = idris_crash "empty queue"
 34 |   tail (Shallow (One x)) = empty
 35 |   tail (Deep (Two x y) m r) = Deep (One y) m r
 36 |   tail (Deep (One x) m r) =
 37 |     if isEmpty m then Shallow r
 38 |     else let (y, z) = the (a, a) $ head m in Deep (Two y z) (tail m) r
 39 |   tail (Shallow (Two _ _)) = assert_total $ idris_crash "tail: Shallow Two"
 40 |   tail (Deep Zero _ _) = assert_total $ idris_crash "tail: Deep head Zero"
 41 |