Mercurial > 12ws.info2
comparison exercises/src/Form.hs @ 19:6688bf4a5836
Rename Form-File to match module name
author | Markus Kaiser <markus.kaiser@in.tum.de> |
---|---|
date | Fri, 07 Dec 2012 01:34:16 +0100 |
parents | exercises/src/Exercise_8_Form.hs@a899535b1674 |
children | a316877ed3d9 |
comparison
equal
deleted
inserted
replaced
18:a899535b1674 | 19:6688bf4a5836 |
---|---|
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 -} |