module TestQueue where

import 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:
----------------------- -}
-- dequeue (enqueue emptyQueue x) = emptyQueue
prop_1 :: Int -> Bool
prop_1 x =  dequeue (enqueue emptyQueue x) == emptyQueue

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

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

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

-- isEmptyQueue emptyQueue    = True
-- isEmptyQueue (enqueue q x) = False
prop_5 :: Queue Int -> Int -> Bool 
prop_5 q x = (isEmptyQueue emptyQueue  == True) && 
             (isEmptyQueue (enqueue q x) == False)
{----------------------------------------------------------------------}


data Queue a = Q [a] [a]  -- Q ws rs Schreibende >> Leseende
               deriving Show
{---------------------------------------------------------------------
Invarianten: 
------------
(1) fuer alle (ws,rs): rs = [] -> ws = []
(2) (ws1,rs1) == (ws2,rs2) 
     -> rs1 ++ (reverse ws1) = rs2 ++ (reverse ws2)
----------------------------------------------------------------------}

inv_1 :: Queue Int -> Bool 
inv_1 (Q 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)




instance Eq a => Eq (Queue a)
 where 
   (Q ws1 rs1) == (Q ws2 rs2) = 
       rs1 ++ (reverse ws1) == rs2 ++ (reverse ws2)


-- 
emptyQueue :: Queue a
emptyQueue =  Q [] []

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

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

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

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


instance Arbitrary a => Arbitrary (Queue a) 
  where
     arbitrary = do rs <- arbitrary
                    ws <- arbitrary
                    return (Q rs ws)