> 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 (i-1) xs]
>           | otherwise = [[]]
 
> --                       ([Names],  [Variables], [Predicates])
> 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))