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])  
            -- (rs,ws) Leseende << Schreibende
{---------------------------------------------------------------------
Invarianten: 
------------
(1) fuer alle (rs,ws): rs = [] -> ws = []
(2) (rs1,ws1) == (rs2,ws2) 
     -> rs1 ++ (reverse ws1) 
        = rs2 ++ (reverse ws2)
----------------------------------------------------------------------}

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

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

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

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

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