|
18
|
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 -} |
