Functional fun with logical expressions

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)

Leave a comment

Sign in to comment.

About mauke

user-pic I blog about Perl.