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

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

inv_1 :: Queue Int -> Bool 
inv_1 (ws,rs) = 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)



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