-- Informatics 1 Functional Programming
-- Mock exam
--
-- Solutions

import Data.Char
import Data.List
import Data.Maybe
import Control.Monad
import Test.QuickCheck

-- Question 1
-- 1a.

isFaceCard :: Char -> Bool
isFaceCard x = x == 'A' || x == 'K' || x == 'Q' || x == 'J'

isCard :: Char -> Bool
isCard x = isFaceCard x || (isDigit x && x /= '1')

f :: String -> Bool
f xs = and [ isFaceCard x | x <- xs, isCard x ]

test1a =
    f "ABCDE"     == True   &&
    f "none here" == True   &&
    f "4 Aces"    == False  &&
    f "01234"     == False  &&
    f ""          == True   &&
    f "1 Ace"     == True   

-- 1b.

g :: String -> Bool
g [] = True
g (x:xs) | isCard x  = isFaceCard x && g xs
         | otherwise = g xs

test1b =
    g "ABCDE"     == True   &&
    g "none here" == True   &&
    g "4 Aces"    == False  &&
    g "01234"     == False  &&
    g ""          == True   &&
    g "1 Ace"     == True   


test1 = test1a && test1b

prop_1 :: String -> Bool
prop_1 xs = f xs == g xs


-- Question 2
-- 2a.

p :: [a] -> [a]
p xs = concat [ if even i then [x] else [x,x] | (x,i) <- zip xs [0..] ]

test2a =
    p "abcdefg" == "abbcddeffg"   &&
    p [1,2,3,4] == [1,2,2,3,4,4]  &&
    p ""        == ""


-- 2b.

q :: [a] -> [a]
q [] = []
q [x] = [x]
q (x:y:xs) = x : y : y : q xs

test2b =
    q "abcdefg" == "abbcddeffg"   &&
    q [1,2,3,4] == [1,2,2,3,4,4]  &&
    q ""        == ""

-- 2c.

r :: [a] -> [a]
r xs = foldr (++) [] (map s (zip xs [0..]))
  where
  s (x,i) = if even i then [x] else [x,x]

test2c =
    r "abcdefg" == "abbcddeffg"   &&
    r [1,2,3,4] == [1,2,2,3,4,4]  &&
    r ""        == ""

test2 = test2a && test2b && test2c

prop_2 :: [Int] -> Bool
prop_2 xs  =  p xs == q xs && q xs == r xs


-- Question 3

data  Proposition  =   Var String
		   |   F
		   |   T
		   |   Not Proposition
		   |   Proposition :|: Proposition
		   |   Proposition :&: Proposition
		   deriving (Eq, Ord, Show)

instance Arbitrary Proposition where
  arbitrary = sized expr
    where
      expr 0 =
        oneof [return F,
               return T,
               liftM Var (elements ["p", "q", "r", "s", "t"])]
      expr n | n > 0 =
        oneof [return F,
               return T,
               liftM Var (elements ["p", "q", "r", "s", "t"]),
               liftM Not (expr (n-1)),
               liftM2 (:&:) (expr (n `div` 2)) (expr (n `div` 2)),
               liftM2 (:|:) (expr (n `div` 2)) (expr (n `div` 2))]


-- 3a.

isNorm :: Proposition -> Bool
isNorm (Var x)           =  True
isNorm T                 =  True
isNorm F                 =  True
isNorm (Not (Var x))     =  True
isNorm (Not p)           =  False
isNorm (p :|: q)         =  isNorm p && isNorm q
isNorm (p :&: q)         =  isNorm p && isNorm q

ok3a =
  isNorm (Var "p" :&: Not (Var "q"))        ==  True   &&
  isNorm (Not (Var "p" :|: Var "q"))        ==  False  &&
  isNorm ((Not (Not (Var "p")) :|: Not T))  ==  False  &&
  isNorm (Not (Var "p" :&: Not (Var "q")))  ==  False

-- 3b.

norm :: Proposition -> Proposition
norm (Var x)          =  Var x
norm T                =  T
norm F                =  F
norm (Not (Var x))    =  Not (Var x)
norm (Not T)          =  F
norm (Not F)          =  T
norm (Not (Not p))    =  norm p
norm (Not (p :|: q))  =  norm (Not p) :&: norm (Not q)
norm (Not (p :&: q))  =  norm (Not p) :|: norm (Not q)
norm (p :|: q)        =  norm p :|: norm q
norm (p :&: q)        =  norm p :&: norm q

ok3b =
     norm (Var "p" :&: Not (Var "q"))
      ==  (Var "p" :&: Not (Var "q"))
  && norm (Not (Var "p" :|: Var "q"))
      ==  Not (Var "p") :&: Not (Var "q")
  && norm ((Not (Not (Var "p")) :|: Not T))
      ==  (Var "p" :|: F)  
  && norm (Not (Var "p" :&: Not (Var "q")))
      ==  Not (Var "p") :|: Var "q"

test3 = ok3a && ok3b

prop_3 :: Proposition -> Bool
prop_3 p  =  isNorm (norm p)


main =
  print test1 >>
  quickCheck prop_1 >>
  print test2 >>
  quickCheck prop_2 >>
  print test3 >>
  quickCheck prop_3