> module WeberLogic.Actions (
> toNand, toNor, truthTree,
> and, or, implies, iff, nand, nor, isConsistent,
> truthTableStrs, truthTableValues)
> where
> import Prelude hiding (and, or)
> import Text.Printf
> import Data.List (union)
> import WeberLogic.Parser
> instance Show Letter where
> show exp =
> case exp of
> Name a -> [a]
> Variable a -> [a]
> instance Eq Letter where
> (==) exp1 exp2 =
> case (exp1, exp2) of
> (Name a, Name b) -> a == b
> (Variable a, Variable b) -> a == b
> (_, _) -> False
> instance Show LogicExp where
> show exp =
> case exp of
> Not a -> printf "~%s" (show a)
> Or a b -> printf "(%s+%s)" (show a) (show b)
> Xor a b -> printf "(%s⊕%s)" (show a) (show b)
> And a b -> printf "(%s&%s)" (show a) (show b)
> Implies a b -> printf "(%s->%s)" (show a) (show b)
> Iff a b -> printf "(%s<->%s)" (show a) (show b)
> Nand a b -> printf "(%s|%s)" (show a) (show b)
> Nor a b -> printf "(%s/%s)" (show a) (show b)
> Predicate a bs -> printf "%c%s" a $ concatMap (show) bs
> instance Eq LogicExp where
> (==) exp1 exp2 =
> case (exp1, exp2) of
> (Predicate a as, Predicate b bs) -> a == b && as == bs
> (Not a, Not b) -> a == b
> (Or a b, Or c d) -> a == c && b == d
> (Xor a b, Xor c d) -> a == c && b == d
> (And a b, And c d) -> a == c && b == d
> (Implies a b, Implies c d) -> a == c && b == d
> (Iff a b, Iff c d) -> a == c && b == d
> (Nand a b, Nand c d) -> a == c && b == d
> (Nor a b, Nor c d) -> a == c && b == d
> (_, _) -> False
> lmap :: (LogicExp -> LogicExp) -> LogicExp -> LogicExp
> lmap f exp =
> case exp of
> Not a -> f $ Not (lmap f a)
> Or a b -> f $ Or (lmap f a) (lmap f b)
> And a b -> f $ And (lmap f a) (lmap f b)
> Xor a b -> f $ Xor (lmap f a) (lmap f b)
> Implies a b -> f $ Implies (lmap f a) (lmap f b)
> Iff a b -> f $ Iff (lmap f a) (lmap f b)
> Nand a b -> f $ Nand (lmap f a) (lmap f b)
> Nor a b -> f $ Nor (lmap f a) (lmap f b)
> Predicate a bs -> f exp
> toNand :: LogicExp -> LogicExp
> toNand exp = lmap (toNand') exp
> where toNand' e = case e of
> Not a -> a `Nand` a
> Or a b -> (a `Nand` a) `Nand` (b `Nand` b)
> And a b -> (a `Nand` b) `Nand` (a `Nand` b)
> Nand a b -> a `Nand` b
> Nor a b -> ((a `Nand` a) `Nand` (b `Nand` b)) `Nand`
> ((a `Nand` a) `Nand` (b `Nand` b))
> Implies a b -> toNand $ Or (toNand $ Not a) b
> Iff a b -> toNand $ (a `Implies` b) `And` (b `Implies` a)
> _ -> e
> toNor :: LogicExp -> LogicExp
> toNor exp = lmap (toNor') exp
> where toNor' e = case e of
> Not a -> a `Nor` a
> Or a b -> (a `Nor` b) `Nor` (a `Nor` b)
> And a b -> (a `Nor` a) `Nor` (b `Nor` b)
> Nor a b -> a `Nor` b
> Nand a b -> ((a `Nor` a) `Nor` (b `Nor` b)) `Nor`
> ((a `Nor` a) `Nor` (b `Nor` b))
> Implies a b -> toNor $ Or (toNor $ Not a) b
> Iff a b -> toNor $ (a `Implies` b) `And` (b `Implies` a)
> _ -> e
> decompose :: [LogicExp] -> [[LogicExp]]
> decompose es = decompose' es []
> decompose' :: [LogicExp] -> [LogicExp] -> [[LogicExp]]
> decompose' exps as
> | null exps = [as]
> | otherwise = let (e:es) = exps
> in case e of
> Predicate _ _ -> decompose' es (e:as)
> Not(Predicate _ _) -> decompose' es (e:as)
> And x y -> decompose' (x:y:es) as
> Or x y -> (decompose' (x:es) as) ++ (decompose' (y:es) as)
> Implies x y -> (decompose' ((Not x):es) as) ++ (decompose' (y:es) as)
> Iff x y -> decompose' (Or (And x y) (And (Not x) (Not y)):es) as
> Not(And x y) -> (decompose' ((Not x):es) as) ++ (decompose' ((Not y):es) as)
> Not(Or x y) -> decompose' ((Not x):(Not y):es) as
> Not(Implies x y) -> decompose' ((And x (Not y)):es) as
> Not(Iff x y) -> decompose' (Or (And x y) (And (Not x) (Not y)):es) as
> isConsistent :: [LogicExp] -> Bool
> isConsistent es = isConsistent' es []
> isConsistent' :: [LogicExp] -> [LogicExp] -> Bool
> isConsistent' exps as
> | null exps = True
> | otherwise = let (e:es) = exps
> in case e of
> Predicate _ _ -> if elem (Not e) as then False else isConsistent' es (e:as)
> Not(Predicate x xs) -> if elem (Predicate x xs) as then False else isConsistent' es (e:as)
> And x y -> isConsistent' (x:y:es) as
> Or x y -> (isConsistent' (x:es) as) || (isConsistent' (y:es) as)
> Implies x y -> (isConsistent' ((Not x):es) as) || (isConsistent' (y:es) as)
> Iff x y -> isConsistent' (Or (And x y) (And (Not x) (Not y)):es) as
> Not(And x y) -> (isConsistent' ((Not x):es) as) || (isConsistent' ((Not y):es) as)
> Not(Or x y) -> isConsistent' ((Not x):(Not y):es) as
> Not(Implies x y) -> isConsistent' ((And x (Not y)):es) as
> Not(Iff x y) -> isConsistent' (Or (And x y) (And (Not x) (Not y)):es) as
> truthTree :: [LogicExp] -> IO()
> truthTree es = do
> printf "%s\n" $ show es
> truthTree' es [] 0
> truthTree' :: [LogicExp] -> [LogicExp] -> Int -> IO()
> truthTree' exps as indent = do
> if null exps
> then print "Open" indent
> else let (e:es) = exps
> in do
> print (show e) indent
> case e of
> Predicate x xs -> if elem (Not e) as
> then print "Closed" indent
> else truthTree' es (e:as) indent
>
> Not(Predicate x xs) -> if elem (Predicate x xs) as
> then print "Closed" indent
> else truthTree' es (e:as) indent
>
> Not(Not x) -> truthTree' (x:es) as indent
>
> And x y -> truthTree' (x:y:es) as indent
>
> Or x y -> do
> truthTree' (x:es) as (indent+1)
> truthTree' (y:es) as (indent+1)
>
> Implies x y -> let z = Or (Not x) (y)
> in truthTree' (z:es) as indent
>
> Iff x y -> let z = Or (And x y) (And (Not x) (Not y))
> in truthTree' (z:es) as indent
>
> Not(And x y) -> let z = Or (Not x) (Not y)
> in truthTree' (z:es) as indent
>
> Not(Or x y) -> let z = And (Not x) (Not y)
> in truthTree' (z:es) as indent
>
> Not(Implies x y) -> let z = Or (Not x) y
> in truthTree' (z:es) as indent
>
> Not(Iff x y) -> let z = Or (And x y) (And (Not x) (Not y))
> in truthTree' (z:es) as indent
>
> where print str indent = printf "%s%s\n" (replicate (indent*2) ' ') str
> evalutateBinary :: (Bool -> Bool -> Bool) -> LogicExp -> LogicExp ->
> [(LogicExp, Bool)] -> Bool
> evalutateBinary operator exp1 exp2 xs = exp1' `operator` exp2'
> where exp1' = evaluate exp1 xs;
> exp2' = evaluate exp2 xs
> evaluate :: LogicExp -> [(LogicExp, Bool)] -> Bool
> evaluate exp xs =
> case exp of
> Predicate a as -> if exp == c then v else evaluate exp xs'
> where ((c,v):xs') = xs
> Not a -> not $ evaluate a xs
> And a b -> evalutateBinary and a b xs
> Or a b -> evalutateBinary or a b xs
> Xor a b -> evalutateBinary xor a b xs
> Nand a b -> evalutateBinary nand a b xs
> Nor a b -> evalutateBinary nor a b xs
> Implies a b -> evalutateBinary implies a b xs
> Iff a b -> evalutateBinary iff a b xs
> and :: Bool -> Bool -> Bool
> and True True = True
> and _ _ = False
> or :: Bool -> Bool -> Bool
> or True _ = True
> or _ True = True
> or _ _ = False
> implies :: Bool -> Bool -> Bool
> implies True False = False
> implies _ _ = True
> iff :: Bool -> Bool -> Bool
> iff True True = True
> iff False False = True
> iff _ _ = False
> xor :: Bool -> Bool -> Bool
> xor False False = False
> xor True True = False
> xor _ _ = True
> nand :: Bool -> Bool -> Bool
> nand x y = not (x `and` y)
> nor :: Bool -> Bool -> Bool
> nor x y = not (x `or` y)
> truthTableStrs :: LogicExp -> [String]
> truthTableStrs exp =
> let (predicates, values, results) = truthTableValues exp
> header_lhs = concatMap (printf "%-5s " . show) predicates
> header_rhs = printf "| %-5s" $ show exp
> header = header_lhs ++ header_rhs
> rows_lhs = map (concatMap (printf "%-5s " . show)) values
> rows_rhs = map (printf "| %-5s" . show) results
> rows = zipWith (++) rows_lhs rows_rhs
> in header : rows
> truthTableValues :: LogicExp -> ([LogicExp], [[Bool]], [Bool])
> truthTableValues exp =
> let (_, _, preds) = getBasics exp
> pred_values = map (zip preds) (perm (length preds) [True, False])
> values = map (map (snd)) pred_values
> results = map (evaluate exp) pred_values
> in (preds, values, results)
> perm i xs | i > 0 = [ x:ys | x <- xs, ys <- perm (i1) xs]
> | otherwise = [[]]
>
> getBasics :: LogicExp -> ([Letter], [Letter], [LogicExp])
> getBasics exp =
> case exp of
> Predicate a bs -> foldl sumTuples ([], [], [exp]) $ map toTuple bs
> where toTuple p = case p of
> Name a -> ([p], [], [])
> Variable a -> ([], [p], [])
> Not a -> getBasics a
> Nor a b -> sumTuples (getBasics a) (getBasics b)
> Nand a b -> sumTuples (getBasics a) (getBasics b)
> And a b -> sumTuples (getBasics a) (getBasics b)
> Or a b -> sumTuples (getBasics a) (getBasics b)
> Xor a b -> sumTuples (getBasics a) (getBasics b)
> Iff a b -> sumTuples (getBasics a) (getBasics b)
> Implies a b -> sumTuples (getBasics a) (getBasics b)
> where sumTuples (xs1, xs2, xs3) (ys1, ys2, ys3) =
> ((xs1 `union` ys1), (xs2 `union` ys2), (xs3 `union` ys3))