module Queue where

{--------------------------------------------------------------------- 
Interface:
----------
emptyQueue   :: Queue a
enqueue      :: Queue a -> a -> Queue a
dequeue      :: Queue a -> Queue a
firstQueue   :: Queue a -> a
isEmptyQueue :: Queue a -> Bool

Gleichungsspezifikation:
------------------------
dequeue (enqueue emptyQueue x) = emptyQueue
isEmptyQueue q = False -> dequeue (enqueue q x) = enqueue (dequeue q) x

firstQueue (enqueue emptyQueue x) = x
isEmptyQueue q = False -> firstQueue (enqueue q x) = firstQueue q

isEmptyQueue emptyQueue    = True
isEmptyQueue (enqueue q x) = False
----------------------------------------------------------------------}


type Queue a = ([a],[a])  -- (ws,rs) Schreibende >> Leseende

{---------------------------------------------------------------------
Invarianten: 
------------
(1) fuer alle (ws,rs): rs = [] -> ws = []
(2) (ws1,rs1) == (ws2,rs2) 
        -> rs1 ++ (reverse ws1) = rs2 ++ (reverse ws2)
----------------------------------------------------------------------}

emptyQueue :: Queue a
emptyQueue =  ([],[])

enqueue                   :: Queue a -> a -> Queue a
enqueue (ws,[])         x =  (ws,[x])  -- hier gilt: ws = [] 
enqueue (ws,rs@(r:rs')) x =  (x:ws,rs)

dequeue              :: Queue a -> Queue a
dequeue (ws, x:r:rs) =  (ws, r:rs)
dequeue (ws, [x])    =  ([], reverse ws) 

firstQueue            :: Queue a -> a
firstQueue (ws, r:rs) =  r

isEmptyQueue          :: Queue a -> Bool
isEmptyQueue (ws, rs) =  null rs  -- dann gilt auch ws = []