-- Companion source code to
--     Chris Okasaki
--     "The Role of Lazy Evaluation in Amortized Data Structures"
--     ICFP'96

-- FIFO queues

-- All operations take O(1) amortized time.

data Queue a = Queue Int [a] Int [a]
    -- Invariants: each queue has the form Queue lenf f lenr r
    --             where lenf = |f| /\ lenr = |r| /\ lenf >= lenr

empty :: Queue a
empty = Queue 0 [] 0 []

isEmpty :: Queue a -> Bool
isEmpty (Queue lenf f lenr r) = (lenf == 0)
    -- since lenf >= lenr, lenf == 0 implies lenr == 0

enqueue :: a -> Queue a -> Queue a
enqueue x (Queue lenf f lenr r) = makeq lenf f (lenr+1) (x:r)

dequeue :: Queue a -> (a, Queue a)
dequeue (Queue (lenf+1) (x:f) lenr r) = (x, makeq lenf f lenr r)

-- auxiliary pseudo-constructor: guarantees lenf >= lenr
makeq :: Int -> [a] -> Int -> [a] -> Queue a
makeq lenf f lenr r
    | lenr <= lenf   = Queue lenf f lenr r
    | lenr == lenf+1 = Queue (lenf+lenr) (f ++ reverse r) 0 []