-- To make use of someone else's code, we can ~import~ it.
import Test.QuickCheck
-- the module Test.QuickCheck provides us with tools for testing
-- whether a function we have designed is doing what it should.

{-
This code is superceded by later definitions, which explicitly represent the partiality of the transition function via a ~Maybe~ data type.

type DFA state symb = 
  ([state],[symb],state,[state],(state,symb) -> state)

notB :: DFA Int Char
notB = ([0,1],['a','b','c'],0,[0],deltaB)
  where
    deltaB (0,'b') = 1
    deltaB (0,_) = 0
    deltaB (1,_) = 1

evenFoddT :: DFA String Bool
evenFoddT = (["ee","eo","oe","oo"],[False,True],"ee",["eo"],deltaEO)
  where
    delta1 ("ee",False) = "oe"
    delta1 ("eo",False) = "oo"
    delta1 ("oe",False) = "ee"
    delta1 ("oo",False) = "eo"
    delta1 ("ee",True) = "eo"
    delta1 ("eo",True) = "ee"
    delta1 ("oe",True) = "oo"
    delta1 ("oo",True) = "oe"

a@(qs,sigma,q0,fs,delta) `recognizes` input =
  deltaStar (q0,input) `elem` fs
  where
    deltaStar (q,[]) = q
    deltaStar (q,(b:bs)) = deltaStar ((delta (q,b)),bs)

-}

type DFA state symb = 
  ([state],[symb],state,[state],(state,symb) -> Maybe state)

recognizes :: Eq q => DFA q s -> [s] -> Bool
a@(qs,sigma,q0,fs,delta) `recognizes` input =
  case deltaStar (q0,input) of
    Nothing -> False
    Just q -> q `elem` fs
  where
    deltaStar (q,[]) = Just q
    deltaStar (q,(b:bs)) =
      do
        q' <- delta (q,b)
        deltaStar (q',bs)

evenFoddT :: DFA (Bool,Bool) Bool
evenFoddT = (qEO,[False,True],(False,False),[(False,True)],deltaEO)
  where
    qEO = [(b,c) | b <- [False,True], c <- [False,True]]
    deltaEO ((b,c),False) = Just (not b, c)
    deltaEO ((b,c),True) = Just (b, not c)

test1 = []
test2 = [True]
test3 = [False,True]
test4 = [False,False,False,True,False]
test5 = [False,False,False,True,False,False,True]

prop_soundEO :: [Bool] -> Property
prop_soundEO s =
  acceptedEO s ==> (evenFalse s && oddTrue s)
  where
    acceptedEO = recognizes evenFoddT
    evenFalse = even . length . filter (not . id)
    oddTrue = odd . length . filter id

prop_completeEO :: [Bool] -> Property
prop_completeEO s =
  (evenFalse s && oddTrue s) ==> acceptedEO s
  where
    acceptedEO = recognizes evenFoddT
    evenFalse = even . length . filter (not . id)
    oddTrue = odd . length . filter id