module TestQueue where

import Test.QuickCheck

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

{-
Gleichungsspezifikation:
----------------------- -}
prop_1 :: Int -> Bool
prop_1 x =  dequeue (enqueue emptyQueue x) === emptyQueue

prop_2 :: Queue Int -> Int ->  Property 
prop_2 q x = isEmptyQueue q == False ==> 
               dequeue (enqueue q x) === enqueue (dequeue q) x

prop_3 :: Int -> Bool
prop_3 x = firstQueue (enqueue emptyQueue x) == x

prop_4 :: Queue Int -> Int -> Property 
prop_4 q x = isEmptyQueue q == False ==> 
               firstQueue (enqueue q x) == firstQueue q

prop_5 :: Queue Int -> Int -> Bool 
prop_5 q x = (isEmptyQueue emptyQueue) && 
             (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)
----------------------------------------------------------------------}

infix 2 === 
(rs1,ws1) === (rs2,ws2) = 
       rs1 ++ (reverse ws1) == rs2 ++ (reverse ws2)

inv_1 :: Queue Int -> Bool 
inv_1 (rs,ws) = not( null rs) || null ws

prop_6 :: Queue Int -> Property
prop_6 q = (inv_1 q && not (isEmptyQueue q)) ==> inv_1 (dequeue q)

prop_7 :: Queue Int -> Int -> Property
prop_7 q x = inv_1 q  ==> inv_1 (enqueue q x)

-- Testkontrolle
prop_8 :: Queue Int -> Property
prop_8 q@(rs,ws) 
         =  inv_1 q ==> 
            classify (null rs) "empty" $
            classify (length (rs++ws) == 1) "unit" $
            True

prop_9 :: Queue Int -> Property
prop_9 q@(rs,ws) 
         =  inv_1 q ==> 
            collect (length (rs++ws)) $
            True


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 = []