Last active
February 26, 2017 19:07
-
-
Save anirudhpillai/4544e47e4e9b575898311296c180a558 to your computer and use it in GitHub Desktop.
A REPL which tells if a given propositional formula is satisfiable or not.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment