# HG changeset patch
# User Markus Kaiser <markus.kaiser@in.tum.de>
# Date 1354839991 -3600
# Node ID a899535b1674f2cfdb93ec94ed9c4dff9ba68e99
# Parent  73170284e0092fe91f127904bd3081b947c71f85
week 8

diff -r 73170284e009 -r a899535b1674 blatt8.pdf
Binary file blatt8.pdf has changed
diff -r 73170284e009 -r a899535b1674 exercises/src/Exercise_8.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/exercises/src/Exercise_8.hs	Fri Dec 07 01:26:31 2012 +0100
@@ -0,0 +1,61 @@
+module Exercise_8 where
+import Form
+import Data.Ratio
+import Test.QuickCheck
+
+{---------------------------------------------------------------------}
+{- Aufgabe G8.1 -}
+
+f0 :: Fraction
+f0 = Over 1 2
+
+f1 :: Fraction
+f1 = Over 7 5
+
+norm :: Fraction -> Fraction
+norm = undefined 
+
+
+
+{---------------------------------------------------------------------}
+{- Aufgabe G8.2 -}
+-- siehe Exercise_8_Form.hs
+
+p0 :: Form
+p0 = (Var "a" :&: Var "b") :|: (Not (Var "a") :&: Not (Var "b"))
+
+
+p1 :: Form
+p1 = ((Not $ Not $ Var "a") :|: (Not ((Var "b") :->: (Not (Var "c")))))
+
+
+
+{---------------------------------------------------------------------}
+{- Aufgabe G8.3 -}
+
+v0 = [("pizza", 7), ("cola", 2), ("apfel", 1)]
+
+a0 :: Arith
+a0 = Add  (Add  (Mul  (Const 3) (IVar "pizza")) (IVar "cola")) (IVar "apfel")
+
+data Arith = Add Arith Arith | Mul Arith Arith | Const Integer | IVar String deriving Show
+
+
+evalArith :: [(String,Integer)] -> Arith -> Integer
+evalArith = undefined
+
+
+
+{---------------------------------------------------------------------}
+{- Aufgabe G8.4 -}
+
+mkTable :: Form -> [[String]]
+mkTable = undefined
+
+
+showTable :: Form -> String
+showTable = unlines . map unwords . mkTable
+
+
+printTable :: Form -> IO ()
+printTable = putStrLn . showTable
\ No newline at end of file
diff -r 73170284e009 -r a899535b1674 exercises/src/Exercise_8_Form.hs
--- /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 -}