mauke

Here's a quickly thrown-together version of "Fun with logical expressions", written in Haskell:

{-# LANGUAGE LambdaCase #-}

module Main (main) where
import Control.Applicative (Applicative (..), (<$>))
import Control.Arrow       (first)
import Data.Ix             (inRange)
import Control.Monad       (guard, mplus, msum)
import Data.Maybe          (fromMaybe, isJust, listToMaybe)

data RawExpr
    = VarR Char
    | N RawExpr
    | D RawExpr RawExpr
    | C RawExpr RawExpr
    | I RawExpr RawExpr
    | E RawExpr RawExpr
    deriving (Eq, Ord, Read, Show)

newtype Parser a = Parser{ unParser :: String -> (a, String) }

instance Functor Parser where
    fmap f (Parser p) = Parser (first f . p)

instance Applicative Parser where
    pure x = Parser (\s -> (x, s))
    Parser f <*> Parser x = Parser (\s ->
        let (f', s')  = f s
            (x', s'') = x s'
        in (f' x', s''))

instance Monad Parser where
    return = pure
    Parser x >>= f = Parser (\s ->
        let (x', s') = x s
        in unParser (f x') s')

anyChar :: Parser Char
anyChar = Parser (\(c : cs) -> (c, cs))

parseRaw :: String -> RawExpr
parseRaw s = case unParser expr s of
    (x, "")   -> x
    (_, rest) -> error ("parseRaw: trailing garbage: " ++ show rest)
    where
    expr = anyChar >>= \case
        c | inRange ('a', 'z') c -> pure (VarR c)
        'N' -> N <$> expr
        'D' -> D <$> expr <*> expr
        'C' -> C <$> expr <*> expr
        'I' -> I <$> expr <*> expr
        'E' -> E <$> expr <*> expr

data ModExpr
    = VarM Char
    | T
    | F
    | Not ModExpr
    | Or [ModExpr]
    deriving (Eq, Ord, Read, Show)

desugar :: RawExpr -> ModExpr
desugar = \case
    VarR v -> VarM v
    N x    -> not (desugar x)
    D x y  -> or  (desugar x) (desugar y)
    C x y  -> and (desugar x) (desugar y)
    I x y  -> or (not (desugar x)) (desugar y)
    E x y  -> or (and x' y') (and (not x') (not y'))
        where
        x' = desugar x
        y' = desugar y
    where
    not     = Not
    or  x y = Or [x, y]
    and x y = not (or (not x) (not y))

render :: ModExpr -> String
render e = go e "" where
    go = \case
        VarM c -> (c :)
        T      -> ('1' :)
        F      -> ('0' :)
        Not x  -> ('~' :) . go x
        Or xs  -> ('V' :) . foldr (.) id (map go xs) . (';' :)

type Rule = ModExpr -> Maybe ModExpr

mkRule :: (Maybe ModExpr -> Maybe ModExpr) -> Rule
mkRule t = rule
    where
    rule e = t (Just e) `mplus` rec
        where
        rec = case e of
            Not x -> Not <$> rule x
            Or xs -> do
                let ys = map rule xs
                guard (any isJust ys)
                return (Or (zipWith fromMaybe xs ys))
            _ -> Nothing

not_not, not_true, not_false :: Rule
not_not = mkRule $ \e -> do
    Not (Not x) <- e
    pure x
not_true = mkRule $ \e -> do
    Not T <- e
    pure F
not_false = mkRule $ \e -> do
    Not F <- e
    pure T

or_true, or_false :: Rule
or_true = mkRule $ \e -> do
    Or xs <- e
    guard (T `elem` xs)
    pure T
or_false = mkRule $ \e -> do
    Or xs <- e
    let ys = filter (F /=) xs
    guard (length ys < length xs)
    pure $ Or ys

first3 :: (a -> r) -> (a, b, c) -> (r, b, c)
first3 f (x, y, z) = (f x, y, z)

second3 :: (b -> r) -> (a, b, c) -> (a, r, c)
second3 f (x, y, z) = (x, f y, z)

selectSplit :: [a] -> [([a], a, [a])]
selectSplit []       = []
selectSplit (x : xs) = ([], x, xs) : map (first3 (x :)) (selectSplit xs)

extract :: (a -> Maybe b) -> [a] -> Maybe ([a], b, [a])
extract f xs = msum (map (evert . second3 f) (selectSplit xs))
    where
    evert (x, Just y, z) = Just (x, y, z)
    evert _              = Nothing

or_none, or_one, or_assoc :: Rule
or_none = mkRule $ \e -> do
    Or [] <- e
    pure F
or_one = mkRule $ \e -> do
    Or [x] <- e
    pure x
or_assoc = mkRule $ \e -> do
    Or xs <- e
    (pre, ys, post) <- extractOr xs
    pure $ Or (pre ++ ys ++ post)
    where
    extractOr = extract (\case Or xs -> Just xs; _ -> Nothing)

isSubExpr :: ModExpr -> ModExpr -> Bool
isSubExpr e1 e2 =
    e1 == e2 || case e2 of
        Not x -> e1 `isSubExpr` x
        Or xs -> any (e1 `isSubExpr`) xs
        _ -> False

substitute :: ModExpr -> ModExpr -> ModExpr -> ModExpr
substitute x y = go
    where
    go = \case
        e | e == x -> y
        Not e      -> Not (go e)
        Or es      -> Or (map go es)
        e          -> e

or_spec :: Rule
or_spec = mkRule $ \e -> do
    Or xs <- e
    listToMaybe $ do
        (pre, x_orig, post) <- selectSplit xs
        (Not x, r) <- [(x_orig, T), (Not x_orig, F)]
        guard $ any (x `isSubExpr`) (pre ++ post)
        let z = Or (map (substitute x r) pre ++ [x_orig] ++ map (substitute x r) post)
        pure z

rules :: [Rule]
rules =
    [
        not_not, not_true, not_false,
        or_true, or_false,
        or_none, or_one, or_assoc,
        or_spec
    ]

simplify1 :: ModExpr -> Maybe ModExpr
simplify1 e = msum (map ($ e) rules)

simplify :: ModExpr -> (ModExpr, [String])
simplify e = case simplify1 e of
    Nothing -> (e, [])
    Just e' -> (render e' :) <$> simplify e'

process :: String -> String
process s = unlines $
    ("ORIG: " ++ s) :
    ("MOD: " ++ render e) :
    foldr (\x z -> ("...> " ++ x) : z) [v, ""] ts
    where
    e = desugar (parseRaw s)
    (r, ts) = simplify e
    v | r == T    = "Tautology"
      | otherwise = "Not a tautology"

main :: IO ()
main = interact (unlines . map process . lines)