# HG changeset patch # User Markus Kaiser # Date 1354840456 -3600 # Node ID 6688bf4a58367d3f6caf39d81e6d244a6c12e083 # Parent a899535b1674f2cfdb93ec94ed9c4dff9ba68e99 Rename Form-File to match module name diff -r a899535b1674 -r 6688bf4a5836 exercises/src/Exercise_8.hs --- a/exercises/src/Exercise_8.hs Fri Dec 07 01:26:31 2012 +0100 +++ b/exercises/src/Exercise_8.hs Fri Dec 07 01:34:16 2012 +0100 @@ -12,6 +12,7 @@ f1 :: Fraction f1 = Over 7 5 + norm :: Fraction -> Fraction norm = undefined @@ -24,7 +25,6 @@ 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"))))) diff -r a899535b1674 -r 6688bf4a5836 exercises/src/Exercise_8_Form.hs --- a/exercises/src/Exercise_8_Form.hs Fri Dec 07 01:26:31 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,114 +0,0 @@ -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 -} diff -r a899535b1674 -r 6688bf4a5836 exercises/src/Form.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/exercises/src/Form.hs Fri Dec 07 01:34:16 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 -}