--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/exercises/src/Exercise_8_Form.hs	Fri Dec 07 01:26:31 2012 +0100
@@ -0,0 +1,114 @@
+module Form where
+
+import Data.List (nub)
+import Control.Monad
+import Test.QuickCheck
+
+type Name = String
+data Form = F | T | Var Name | Not Form | Form :&: Form | Form :|: Form
+          deriving Eq
+
+instance Show Form where
+  show F = "F"
+  show T = "T"
+  show (Var x) = x
+  show (Not p) = par("~" ++ show p)
+  show (p :&: q) = par(show p ++ " & " ++ show q)
+  show (p :|: q) = par(show p ++ " | " ++ show q)
+  {- TODO -}
+
+par :: String -> String
+par s = "(" ++ s ++ ")"
+
+-- Wertebelegung
+type Valuation = [(Name,Bool)]
+
+eval :: Valuation -> Form -> Bool
+eval e F = False
+eval e T = True
+eval e (Var x) = the(lookup x e) where the(Just b) = b
+eval e (Not p) = not(eval e p)
+eval e (p :&: q) = eval e p && eval e q
+eval e (p :|: q) = eval e p || eval e q
+{- TODO -}
+
+vars :: Form -> [Name]
+vars F = []
+vars T = []
+vars (Var x) = [x]
+vars (Not p) = vars p
+vars (p :&: q) = nub (vars p ++ vars q)
+vars (p :|: q) = nub (vars p ++ vars q)
+{- TODO -}
+
+vals :: [Name] -> [Valuation]
+vals []	= [[]]
+vals (x:xs) = [ (x,False):e | e <- vals xs ] ++ [ (x,True ):e | e <- vals xs ]
+
+satisfiable :: Form -> Bool
+satisfiable p = or [eval e p | e <- vals(vars p)]
+
+tautology :: Form -> Bool
+tautology = not . satisfiable . Not
+
+prop_vals1 xs =
+  length(vals xs) == 2 ^ length xs
+
+prop_vals2 xs =
+  distinct (vals xs)
+
+distinct :: Eq a => [a] -> Bool
+distinct [] = True
+distinct (x:xs) = not(elem x xs) && distinct xs
+
+prop_vals1' xs =
+  length xs <= 10 ==>
+  length(vals xs) == 2 ^ length xs
+
+prop_vals2' xs =
+  length xs <= 10 ==> distinct (vals xs)
+
+isSimple :: Form -> Bool
+isSimple (Not p)    =  not (isOp p)
+  where
+  isOp (Not p)    =  True
+  isOp (p :&: q)  =  True
+  isOp (p :|: q)  =  True
+  isOp p          =  False
+isSimple (p :&: q)  =  isSimple p && isSimple q
+isSimple (p :|: q)  =  isSimple p && isSimple q
+isSimple p          =  True
+{- TODO -}
+
+simplify :: Form -> Form
+simplify (Not p)    =  pushNot (simplify p)
+  where
+  pushNot (Not p)    =  p
+  pushNot (p :&: q)  =  pushNot p :|: pushNot q
+  pushNot (p :|: q)  =  pushNot p :&: pushNot q
+  pushNot p          =  Not p
+simplify (p :&: q)  =  simplify p :&: simplify q
+simplify (p :|: q)  =  simplify p :|: simplify q
+simplify p          =  p
+{- TODO -}
+
+-- allow QuickCheck to generate arbitrary values of type Form
+instance Arbitrary Form where
+  arbitrary = sized prop
+    where
+    name = sized $ \size -> elements (map (:[]) $ take (size + 1) ['a'..'z'])
+    prop 0  =
+      oneof [return F,
+             return T,
+             liftM Var name]
+    prop n | n > 0 =
+      oneof [return F,
+             return T,
+             liftM Var name,
+             liftM Not (prop (n-1)),
+             liftM2 (:&:) (prop(n `div` 2)) (prop(n `div` 2)),
+             liftM2 (:|:) (prop(n `div` 2)) (prop(n `div` 2))]
+{- TODO -}
+
+prop_simplify p = isSimple(simplify p)
+{- TODO -}