Mercurial > 12ws.info2

comparison exercises/src/Exercise_8_Form.hs @ 18:a899535b1674

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
week 8
author Markus Kaiser <markus.kaiser@in.tum.de>
date Fri, 07 Dec 2012 01:26:31 +0100
parents
children
comparison
equal deleted inserted replaced
17:73170284e009 18:a899535b1674
1 module Form where
2
3 import Data.List (nub)
4 import Control.Monad
5 import Test.QuickCheck
6
7 type Name = String
8 data Form = F | T | Var Name | Not Form | Form :&: Form | Form :|: Form
9 deriving Eq
10
11 instance Show Form where
12 show F = "F"
13 show T = "T"
14 show (Var x) = x
15 show (Not p) = par("~" ++ show p)
16 show (p :&: q) = par(show p ++ " & " ++ show q)
17 show (p :|: q) = par(show p ++ " | " ++ show q)
18 {- TODO -}
19
20 par :: String -> String
21 par s = "(" ++ s ++ ")"
22
23 -- Wertebelegung
24 type Valuation = [(Name,Bool)]
25
26 eval :: Valuation -> Form -> Bool
27 eval e F = False
28 eval e T = True
29 eval e (Var x) = the(lookup x e) where the(Just b) = b
30 eval e (Not p) = not(eval e p)
31 eval e (p :&: q) = eval e p && eval e q
32 eval e (p :|: q) = eval e p || eval e q
33 {- TODO -}
34
35 vars :: Form -> [Name]
36 vars F = []
37 vars T = []
38 vars (Var x) = [x]
39 vars (Not p) = vars p
40 vars (p :&: q) = nub (vars p ++ vars q)
41 vars (p :|: q) = nub (vars p ++ vars q)
42 {- TODO -}
43
44 vals :: [Name] -> [Valuation]
45 vals [] = [[]]
46 vals (x:xs) = [ (x,False):e | e <- vals xs ] ++ [ (x,True ):e | e <- vals xs ]
47
48 satisfiable :: Form -> Bool
49 satisfiable p = or [eval e p | e <- vals(vars p)]
50
51 tautology :: Form -> Bool
52 tautology = not . satisfiable . Not
53
54 prop_vals1 xs =
55 length(vals xs) == 2 ^ length xs
56
57 prop_vals2 xs =
58 distinct (vals xs)
59
60 distinct :: Eq a => [a] -> Bool
61 distinct [] = True
62 distinct (x:xs) = not(elem x xs) && distinct xs
63
64 prop_vals1' xs =
65 length xs <= 10 ==>
66 length(vals xs) == 2 ^ length xs
67
68 prop_vals2' xs =
69 length xs <= 10 ==> distinct (vals xs)
70
71 isSimple :: Form -> Bool
72 isSimple (Not p) = not (isOp p)
73 where
74 isOp (Not p) = True
75 isOp (p :&: q) = True
76 isOp (p :|: q) = True
77 isOp p = False
78 isSimple (p :&: q) = isSimple p && isSimple q
79 isSimple (p :|: q) = isSimple p && isSimple q
80 isSimple p = True
81 {- TODO -}
82
83 simplify :: Form -> Form
84 simplify (Not p) = pushNot (simplify p)
85 where
86 pushNot (Not p) = p
87 pushNot (p :&: q) = pushNot p :|: pushNot q
88 pushNot (p :|: q) = pushNot p :&: pushNot q
89 pushNot p = Not p
90 simplify (p :&: q) = simplify p :&: simplify q
91 simplify (p :|: q) = simplify p :|: simplify q
92 simplify p = p
93 {- TODO -}
94
95 -- allow QuickCheck to generate arbitrary values of type Form
96 instance Arbitrary Form where
97 arbitrary = sized prop
98 where
99 name = sized $ \size -> elements (map (:[]) $ take (size + 1) ['a'..'z'])
100 prop 0 =
101 oneof [return F,
102 return T,
103 liftM Var name]
104 prop n | n > 0 =
105 oneof [return F,
106 return T,
107 liftM Var name,
108 liftM Not (prop (n-1)),
109 liftM2 (:&:) (prop(n `div` 2)) (prop(n `div` 2)),
110 liftM2 (:|:) (prop(n `div` 2)) (prop(n `div` 2))]
111 {- TODO -}
112
113 prop_simplify p = isSimple(simplify p)
114 {- TODO -}