A REPL which tells if a given propositional formula is satisfiable or not.

Tableau

import Text.ParserCombinators.Parsec hiding (spaces)
import System.Environment
import System.IO


-- Data types

data Formula = Proposition Char
             | Negation Formula
             | Binary Connective Formula Formula
             deriving (Eq, Show)

data Connective = Connective Char deriving (Show, Eq)

data Tableau = Node Formula Tableau Tableau | Empty


-- Parsing Functions

isProposition :: Parser Formula
isProposition = do
    x <- letter
    eof
    return $ Proposition x

checkProposition :: Parser Formula
checkProposition = do
    x <- letter
    return $ Proposition x

parseExpr2 :: Parser Formula
parseExpr2 = checkNegation <|> isBinary <|> checkProposition

isNegation :: Parser Formula
isNegation = do
    char '-'
    x <- parseExpr
    eof
    return $ Negation x

checkNegation :: Parser Formula
checkNegation = do
    char '-'
    x <- parseExpr2
    return $ Negation x

isBinary :: Parser Formula
isBinary = do
    char '('
    f1 <- parseExpr2
    conn <- oneOf "^>v"
    f2 <- parseExpr2
    char ')'
    return $ Binary (Connective conn) (f1) (f2)

parseExpr :: Parser Formula
parseExpr = isNegation
     <|> isBinary
     <|> isProposition

readExpr :: String ->  Maybe Formula
readExpr input = case parse parseExpr "lisp" input of
    Left err -> Nothing
    Right val -> Just val


-- Tableau solving functions

addAlpha :: Formula -> Tableau -> Tableau
addAlpha x Empty = (Node x Empty Empty)
addAlpha x (Node rt Empty Empty) = Node rt (Node x Empty Empty) Empty
addAlpha x (Node rt l Empty) = Node rt (addAlpha x l) Empty
addAlpha x (Node rt l r) = Node rt (addAlpha x l) (addAlpha x r)

addBeta :: Formula -> Formula -> Tableau -> Tableau
addBeta x y (Node rt Empty Empty) = Node rt (Node x Empty Empty) (Node y Empty Empty)
addBeta x y (Node rt l Empty) = Node rt (addBeta x y l) Empty
addBeta x y (Node rt l r) = Node rt (addBeta x y l) (addBeta x y r)

complete :: Tableau -> Tableau
complete Empty = Empty
complete val@(Node (Proposition x) p q) =
    Node (Proposition x) (complete p) (complete q)
complete val@(Node (Negation (Proposition x)) p q)  =
    Node (Negation (Proposition x)) (complete p) (complete q)
complete val@(Node (Binary (Connective '^') p q) _ _) = Node rt (complete l) (complete r)
  where
    (Node rt l r) = addAlpha q (addAlpha p val)
complete val@(Node (Binary (Connective 'v') p q) _ _) = Node rt (complete l) (complete r)
  where
    (Node rt l r) = addBeta p q val
complete val@(Node (Binary (Connective '>') p q) _ _) = Node rt (complete l) (complete r)
  where
    (Node rt l r) = addBeta (Negation p) q val
complete val@(Node (Negation (Negation (Proposition c))) _ _) = Node rt (complete l) (complete r)
  where
    (Node rt l r) = addAlpha (Proposition c) val
complete val@(Node (Negation (Negation f)) a b) = Node rt (complete l) (complete r)
  where
    (Node rt l r) = addAlpha f val
complete val@(Node (Negation (Binary (Connective 'v') p q)) a b) = Node rt (complete l) (complete r)
  where
    (Node rt l r) = addAlpha (Negation q) $ addAlpha (Negation p) val
complete val@(Node (Negation (Binary (Connective '^') p q)) a b) = Node rt (complete l) (complete r)
  where
    (Node rt l r) = addBeta (Negation p) (Negation q) val
complete val@(Node (Negation (Binary (Connective '>') p q)) a b) = Node rt (complete l) (complete r)
  where
    (Node rt l r) = addAlpha (Negation q) $ addAlpha p val

isBranchClosed :: [Formula] -> Bool
isBranchClosed [] = False
isBranchClosed (x:xs) = case x of
    (Proposition a) -> if elem (Negation (Proposition a)) xs then True else isBranchClosed xs
    (Negation (Proposition a)) -> if elem (Proposition a) xs then True else isBranchClosed xs
    _ -> isBranchClosed xs

isClosed :: [Formula] -> Tableau -> Bool
isClosed xs Empty = isBranchClosed xs
isClosed xs (Node x Empty Empty) = isBranchClosed (x:xs)
isClosed xs (Node x left Empty) = isClosed (x:xs) left
isClosed xs (Node x left right) = (isClosed (x:xs) left) && (isClosed (x:xs) right)

isSatisfiable :: Formula -> Bool
isSatisfiable x =
    not . isClosed [] . complete $ (Node x Empty Empty)


-- Creating the REPL

flushStr :: String -> IO ()
flushStr str = putStr str >> hFlush stdout

readPrompt :: String -> IO String
readPrompt prompt = flushStr prompt >> getLine

evalString :: String -> IO String
evalString x = case readExpr x of
    Nothing -> return "Invalid Formula"
    (Just val) -> if isSatisfiable val
                    then return "Satisfiable"
                    else return "Not Satisfiable"

evalAndPrint :: String -> IO ()
evalAndPrint expr = evalString expr >>= putStrLn

until_ :: Monad m => (a -> Bool) -> m a -> (a -> m ()) -> m ()
until_ pred prompt action = do
    result <- prompt
    if pred result
        then return ()
        else action result >> until_ pred prompt action

runRepl :: IO ()
runRepl = until_ (=="quit") (readPrompt "Formula>>> ") evalAndPrint


-- | Main
main :: IO ()
main = runRepl

-- main = do
--     args <- getArgs
--     putStrLn $ readExpr $ args !! 0