diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..1d0658a --- /dev/null +++ b/.gitignore @@ -0,0 +1,19 @@ +# binaries +* + +# compilation intermediate files +*.hi +*.ho + +# vim generates these +*.swp +*.swo + +# include directories +!*/ + +# include files with an extension +!*.* + +# special cases +!Makefile diff --git a/Logic/Parse.hs b/Logic/Parse.hs new file mode 100644 index 0000000..4956bee --- /dev/null +++ b/Logic/Parse.hs @@ -0,0 +1,77 @@ +module Logic.Parse where + +import Control.Applicative (Applicative, Alternative(..)) +import Data.Functor (Functor) + +newtype Parser output = Parser + { runParser :: Input -> Either ParseError (output, Input) + } + +data Input = Input + { inputPos :: Int + , inputSeq :: [Char] + } deriving (Eq, Show) + +mkInput :: [Char] -> Input +mkInput = Input 0 + +data ParseError = + ParseError Int String + deriving (Show) + +expected :: String -> Input -> ParseError +expected thing input = ParseError (inputPos input) $ + "expected " <> thing <> ", found " <> show (take 20 $ inputSeq input) + +eof :: Parser a -> Input -> Either ParseError a +eof p input = do + (result, rest) <- runParser p input + case inputSeq rest of + [] -> Right result + _ -> Left $ expected "end of input" rest + +instance Functor Parser where + fmap :: (a -> b) -> Parser a -> Parser b + fmap f (Parser p) = Parser $ \input -> do + (result, rest) <- p input + return (f result, rest) + +instance Applicative Parser where + pure :: a -> Parser a + pure result = Parser $ \input -> Right (result, input) + + (Parser p1) <*> (Parser p2) = + Parser $ \input -> do + (f, rest) <- p1 input + (result, rest') <- p2 rest + return (f result, rest') + +instance Alternative Parser where + empty :: Parser a + empty = Parser $ const empty + + (Parser p1) <|> (Parser p2) = + Parser $ \input -> p1 input <|> p2 input + +instance Alternative (Either ParseError) where + empty :: Either ParseError a + empty = Left $ ParseError 0 "this parser always fails" + + (Right x) <|> _ = Right x + (Left _) <|> e = e + +parseToken :: String -> Parser String +parseToken token = Parser parse + where + n = length token + parse input@(Input pos xs) + | token == take n xs = Right $ (token,) $ Input (pos + n) (drop n xs) + | otherwise = Left $ expected (show token) input + +parseIf :: String -> (Char -> Bool) -> Parser Char +parseIf description check = Parser $ \input -> + case inputSeq input of + [] -> Left $ ParseError (inputPos input) "unexpected end of input" + (char:chars) + | check char -> Right $ (char,) $ Input (inputPos input + 1) chars + | otherwise -> Left $ expected description input diff --git a/Logic/Statement.hs b/Logic/Statement.hs new file mode 100644 index 0000000..09b94ec --- /dev/null +++ b/Logic/Statement.hs @@ -0,0 +1,237 @@ +module Logic.Statement where + +import Logic.Parse + +import Control.Applicative (Alternative((<|>), some)) +import Data.Char (isAlphaNum) +import Data.List (intercalate) +import Data.Either (fromRight) +import Data.Set (singleton, union, toAscList) + +data Statement + = Atom String + | Not Statement + | And Statement Statement + | Or Statement Statement + | Implies Statement Statement + | Iff Statement Statement + deriving (Show, Eq) + +stmtAtom :: Parser Statement +stmtAtom = Atom <$> parse + where + parse = some $ parseIf "statement variable" $ \char -> isAlphaNum char || char == '_' + +stmtNot :: Parser Statement +stmtNot = Not <$> (parseToken "!" *> stmt) + +stmtBinary :: Parser Statement +stmtBinary = parseToken "(" *> body <* parseToken ")" + where + body = (\s1 f s2 -> f s1 s2) <$> stmt <*> parseConnective <*> stmt + + parseConnective = + fmap (const And) (parseToken "&") + <|> fmap (const Or) (parseToken "|") + <|> fmap (const Implies) (parseToken "->") + <|> fmap (const Iff) (parseToken "<->") + <|> fail + + fail = Parser $ \input -> Left $ expected "connective" input + +stmt :: Parser Statement +stmt = Parser $ \input -> + let + parser = + case inputSeq input of + [] -> fail + ('!':_) -> stmtNot + ('(':_) -> stmtBinary + _ -> stmtAtom <|> fail + in runParser parser input + where + fail = Parser $ \input -> Left $ expected "statement" input + +p :: Statement +p = fromRight undefined $ eof stmt $ mkInput "((a->b)<->!c)" + +q :: Statement +q = fromRight undefined $ eof stmt $ mkInput "(!a<->((!(p->q)&x)|y))" + +atoms :: Statement -> [String] +atoms = toAscList . mkSet + where + mkSet (Atom key) = singleton key + mkSet (Not s) = mkSet s + mkSet (And s1 s2) = union (mkSet s1) (mkSet s2) + mkSet (Or s1 s2) = union (mkSet s1) (mkSet s2) + mkSet (Implies s1 s2) = union (mkSet s1) (mkSet s2) + mkSet (Iff s1 s2) = union (mkSet s1) (mkSet s2) + +eval :: [(String, Bool)] -> Statement -> Either String Bool +eval assignments = aux + where + aux (Atom key) = maybe (Left key) Right $ lookup key assignments + aux (Not s) = not <$> aux s + aux (And s1 s2) = (&&) <$> aux s1 <*> aux s2 + aux (Or s1 s2) = (||) <$> aux s1 <*> aux s2 + aux (Implies s1 s2) = not <$> ((&&) <$> aux s1 <*> (not <$> aux s2)) + aux (Iff s1 s2) = (==) <$> aux s1 <*> aux s2 + +data Bucket + = Tautology + | Contradiction + | Contingent + deriving (Eq, Show) + +bucket :: Statement -> Bucket +bucket s + | and values = Tautology + | all not values = Contradiction + | otherwise = Contingent + where + values = [fromRight undefined $ eval assignments s | assignments <- enumerate $ atoms s] + +enumerate :: [a] -> [[(a, Bool)]] +enumerate keys = map reverse $ aux start + where + aux assignments = (assignments:) $ + case next assignments of + Nothing -> [] + Just (assignments') -> aux assignments' + + start = map (, False) keys + + next [] = Nothing + next ((key, False):rest) = Just $ (key, True):rest + next ((key, True):rest) = ((key, False):) <$> (next rest) + +data SerializeFormat + = Ascii + | Latex + deriving (Show, Eq) + +data Cell + = Main String + | NotMain String + deriving (Show, Eq) + +fromCell :: Cell -> String +fromCell (Main x) = x +fromCell (NotMain x) = x + +fromCellLatex :: Cell -> String +fromCellLatex (Main x) = "\\textbf " <> x +fromCellLatex (NotMain x) = x + +isMain :: Cell -> Bool +isMain (Main _) = True +isMain _ = False + +serializeCells :: SerializeFormat -> Statement -> [Cell] +serializeCells = aux Main + where + aux mkCell Ascii = ascii mkCell + aux mkCell Latex = latex mkCell + + ascii' = ascii NotMain + latex' = latex NotMain + + ascii mkCell (Atom key) = [mkCell key] + ascii mkCell (Not s) = [mkCell "!"] ++ ascii' s + ascii mkCell (And s1 s2) = connective (mkCell "&") (ascii' s1) (ascii' s2) + ascii mkCell (Or s1 s2) = connective (mkCell "|") (ascii' s1) (ascii' s2) + ascii mkCell (Implies s1 s2) = connective (mkCell "->") (ascii' s1) (ascii' s2) + ascii mkCell (Iff s1 s2) = connective (mkCell "<->") (ascii' s1) (ascii' s2) + + latex mkCell (Atom key) = [mkCell key] + latex mkCell (Not s) = [mkCell "\\neg "] ++ latex' s + latex mkCell (And s1 s2) = connective (mkCell "\\land ") (latex' s1) (latex' s2) + latex mkCell (Or s1 s2) = connective (mkCell "\\lor ") (latex' s1) (latex' s2) + latex mkCell (Implies s1 s2) = connective (mkCell "\\to ") (latex' s1) (latex' s2) + latex mkCell (Iff s1 s2) = connective (mkCell "\\leftrightarrow ") (latex' s1) (latex' s2) + + connective middle s1 s2 = [NotMain "("] ++ s1 ++ [middle] ++ s2 ++ [NotMain ")"] + +serialize :: SerializeFormat -> Statement -> String +serialize fmt s = concat $ map fromCell $ serializeCells fmt s + +latexTruthTableMainColumnIndex :: Statement -> Int +latexTruthTableMainColumnIndex s = + fst $ head $ filter (\(i, cell) -> isMain cell) $ zip [0..] $ serializeCells Latex s + +serializeLatexTruthTableRow :: [(String, Bool)] -> Statement -> Either String [String] +serializeLatexTruthTableRow ass s = map fromCellLatex <$> latexRow Main ass s + where + latexRow mkCell ass (Atom key) = list <$> mkCell <$> toInt <$> eval ass (Atom key) + latexRow mkCell ass (Not s) = (list <$> mkCell <$> toInt <$> not <$> eval ass s) <> latexRow NotMain ass s + latexRow mkCell ass (And s1 s2) = latexRowBinaryConnective (&&) mkCell ass s1 s2 + latexRow mkCell ass (Or s1 s2) = latexRowBinaryConnective (||) mkCell ass s1 s2 + latexRow mkCell ass (Implies s1 s2) = latexRowBinaryConnective implies mkCell ass s1 s2 + latexRow mkCell ass (Iff s1 s2) = latexRowBinaryConnective (==) mkCell ass s1 s2 + + latexRowBinaryConnective op mkCell ass s1 s2 = + ( + \subrow1 subrow2 result -> + [NotMain " "] ++ subrow1 ++ [mkCell $ toInt result] ++ subrow2 ++ [NotMain " "] + ) <$> + latexRow NotMain ass s1 <*> latexRow NotMain ass s2 <*> + (op <$> eval ass s1 <*> eval ass s2) + + toInt :: Bool -> String + toInt False = "0" + toInt True = "1" + + list :: a -> [a] + list x = [x] + + implies :: Bool -> Bool -> Bool + implies b1 b2 = not b1 || b2 + +truthtable :: Statement -> String +truthtable s = open <> header <> "\\hline\n" <> body <> close + where + mainIndex = latexTruthTableMainColumnIndex s + + cellsSpec + | mainIndex == 0 && length serial <= 1 = "c" + | mainIndex == 0 = "c|" <> replicate (length serial - 1) 'c' + | mainIndex == length serial - 1 = replicate (length serial - 1) 'c' <> "|c" + | otherwise = replicate mainIndex 'c' <> "|c|" <> replicate (length serial - mainIndex - 1) 'c' + + open = + "\\begin{tabular}{" <> + replicate (length $ atoms s) 'c' <> + "||" <> + cellsSpec <> + "}\n" + + close = "\\end{tabular}\n\n" + + serial :: [Cell] + serial = serializeCells Latex s + + header :: String + header = + intercalate " & " (map dollars $ atoms s) <> + " & " <> + intercalate " & " (map dollars $ map fromCell serial) <> + " \\\\\n" + + dollars :: String -> String + dollars string = "$" <> string <> "$" + + body :: String + body = concat $ map line $ enumerate $ atoms s + + line assignments = + intercalate " & " (bools assignments) <> + " &" <> + intercalate "&" (cells assignments) <> + "\\\\\n" + + bools assignments = [if bool then "1" else "0" | (key, bool) <- assignments] + + cells assignments = + (\xs -> [if x /= " " then " " <> x <> " " else " " | x <- xs]) $ + fromRight undefined $ serializeLatexTruthTableRow assignments s diff --git a/Main.hs b/Main.hs index f82b840..1b4a479 100644 --- a/Main.hs +++ b/Main.hs @@ -1,313 +1,16 @@ -import Control.Applicative (Applicative, Alternative(..)) -import Data.Char (isAlphaNum) -import Data.Functor (Functor) -import Data.List (intercalate) -import Data.Maybe (fromJust) -import qualified Data.Set as S +module Main where -newtype Parser symbol output = Parser - { runParser :: [symbol] -> Maybe (output, [symbol]) - } +import Logic.Parse (eof, mkInput, ParseError(..)) +import Logic.Statement (stmt) -instance Functor (Parser s) where - fmap :: (a -> b) -> Parser s a -> Parser s b - fmap f (Parser p) = Parser - { runParser = \xs -> do - (result, xs') <- p xs - return (f result, xs') - } - -instance Applicative (Parser s) where - pure :: a -> Parser s a - pure result = Parser $ \xs -> Just (result, xs) - - (Parser p1) <*> (Parser p2) = - Parser $ \xs -> do - (f, xs') <- p1 xs - (result, xs'') <- p2 xs' - return (f result, xs'') - -instance Alternative (Parser s) where - empty :: Parser s a - empty = Parser $ const Nothing - - (Parser p1) <|> (Parser p2) = - Parser $ \xs -> p1 xs <|> p2 xs - -data Statement - = Atom String - | Not Statement - | And Statement Statement - | Or Statement Statement - | Implies Statement Statement - | Iff Statement Statement - deriving (Show, Eq) - -parseToken :: String -> Parser Char String -parseToken token = Parser parse +main :: IO () +main = do + line <- getLine + either fail print $ eof stmt $ mkInput line where - n = length token - parse xs - | token == take n xs = Just (token, drop n xs) - | otherwise = Nothing - -parseWhile :: (Char -> Bool) -> Parser Char String -parseWhile check = Parser parse - where - parse [] = Nothing - parse (token:rest) - | check token = - case parse rest of - Nothing -> Just ([token], rest) - Just (tokens, rest') -> Just (token:tokens, rest') - | otherwise = Nothing - -parseBrackets :: Parser Char a -> Parser Char a -parseBrackets p = parseToken "(" *> p <* parseToken ")" - -parseInfix :: String -> Parser Char a -> Parser Char a -> Parser Char (a, a) -parseInfix token p1 p2 = (,) <$> (p1 <* parseToken token) <*> p2 - -parseConnective :: String -> Parser Char a -> Parser Char a -> Parser Char (a, a) -parseConnective token p1 p2 = parseBrackets $ parseInfix token p1 p2 - -stmtAtom :: Parser Char Statement -stmtAtom = Atom <$> parse - where - parse = parseWhile $ \char -> isAlphaNum char || char == '_' - -stmtNot :: Parser Char Statement -stmtNot = Not <$> (parseToken "!" *> stmt) - -stmtAnd :: Parser Char Statement -stmtAnd = uncurry And <$> parseConnective "&" stmt stmt - -stmtOr :: Parser Char Statement -stmtOr = uncurry Or <$> parseConnective "|" stmt stmt - -stmtImplies :: Parser Char Statement -stmtImplies = uncurry Implies <$> parseConnective "->" stmt stmt - -stmtIff :: Parser Char Statement -stmtIff = uncurry Iff <$> parseConnective "<->" stmt stmt - -stmt :: Parser Char Statement -stmt = stmtAtom <|> stmtNot <|> stmtAnd <|> stmtOr <|> stmtImplies <|> stmtIff - -{- -ghci> runParser stmt "(!a<->((!(p->q)&x)|y))" -Just (Iff (Not (Atom "a")) (Or (And (Not (Implies (Atom "p") (Atom "q"))) (Atom "x")) (Atom "y")),"") --} - -p :: Statement -p = fromJust $ fst <$> runParser stmt "((a->b)<->!c)" - -q :: Statement -q = fromJust $ fst <$> runParser stmt "(!a<->((!(p->q)&x)|y))" - -atoms :: Statement -> S.Set String -atoms (Atom key) = S.singleton key -atoms (Not s) = atoms s -atoms (And s1 s2) = S.union (atoms s1) (atoms s2) -atoms (Or s1 s2) = S.union (atoms s1) (atoms s2) -atoms (Implies s1 s2) = S.union (atoms s1) (atoms s2) -atoms (Iff s1 s2) = S.union (atoms s1) (atoms s2) - -eval :: [(String, Bool)] -> Statement -> Maybe Bool -eval assignments = aux - where - aux (Atom key) = lookup key assignments - aux (Not s) = not <$> aux s - aux (And s1 s2) = (&&) <$> aux s1 <*> aux s2 - aux (Or s1 s2) = (||) <$> aux s1 <*> aux s2 - aux (Implies s1 s2) = not <$> ((&&) <$> aux s1 <*> (not <$> aux s2)) - aux (Iff s1 s2) = (==) <$> aux s1 <*> aux s2 - -data Bucket - = Tautology - | Contradiction - | Contingent - deriving (Eq, Show) - -bucket :: Statement -> Bucket -bucket s - | and values = Tautology - | all not values = Contradiction - | otherwise = Contingent - where - atomsList = S.toList $ atoms s - values = [fromJust $ eval assignments s | assignments <- enumerate $ atomsList] - -enumerate :: [a] -> [[(a, Bool)]] -enumerate keys = map reverse $ aux start - where - aux assignments = (assignments:) $ - case next assignments of - Nothing -> [] - Just (assignments') -> aux assignments' - - start = [(key, False) | key <- keys] - - next [] = Nothing - next ((k, False):rest) = Just $ (k, True):rest - next ((k, True):rest) = ((k, False):) <$> (next rest) - -{- - ghci> bucket $ fromJust $ fst <$> runParser stmt "(p<->p)" -Tautology -ghci> bucket p -Contingent -ghci> bucket q -Contingent -ghci> bucket $ fromJust $ fst <$> runParser stmt "(p<->!p)" -Contradiction -ghci> bucket $ fromJust $ fst <$> runParser stmt "(p|!p)" -Tautology -ghci> bucket $ fromJust $ fst <$> runParser stmt "(p->p)" -Tautology -ghci> bucket $ fromJust $ fst <$> runParser stmt "(p&!p)" -Contradiction -ghci> bucket $ fromJust $ fst <$> runParser stmt "(!(p->q)&!p)" -Contradiction -ghci> bucket $ fromJust $ fst <$> runParser stmt "(p|(p->q))" -Tautology -ghci> bucket $ fromJust $ fst <$> runParser stmt "((p->q)->(!p->r))" -Contingent -ghci> bucket $ fromJust $ fst <$> runParser stmt "(!(a&b)<->(!a|!b))" -Tautology -ghci> bucket $ fromJust $ fst <$> runParser stmt "(!(a|b)<->(!a&!b))" -Tautology --} - -data SerializeFormat - = Ascii - | Latex - deriving (Show, Eq) - -data Cell - = Main String - | NotMain String - deriving (Show, Eq) - -fromCell :: Cell -> String -fromCell (Main x) = x -fromCell (NotMain x) = x - -fromCellLatex :: Cell -> String -fromCellLatex (Main x) = "\\textbf " <> x -fromCellLatex (NotMain x) = x - -isMain :: Cell -> Bool -isMain (Main _) = True -isMain _ = False - -serializeCells :: SerializeFormat -> Statement -> [Cell] -serializeCells = aux Main - where - aux mkCell Ascii = ascii mkCell - aux mkCell Latex = latex mkCell - - ascii' = ascii NotMain - latex' = latex NotMain - - ascii mkCell (Atom key) = [mkCell key] - ascii mkCell (Not s) = [mkCell "!"] ++ ascii' s - ascii mkCell (And s1 s2) = connective (mkCell "&") (ascii' s1) (ascii' s2) - ascii mkCell (Or s1 s2) = connective (mkCell "|") (ascii' s1) (ascii' s2) - ascii mkCell (Implies s1 s2) = connective (mkCell "->") (ascii' s1) (ascii' s2) - ascii mkCell (Iff s1 s2) = connective (mkCell "<->") (ascii' s1) (ascii' s2) - - latex mkCell (Atom key) = [mkCell key] - latex mkCell (Not s) = [mkCell "\\neg "] ++ latex' s - latex mkCell (And s1 s2) = connective (mkCell "\\land ") (latex' s1) (latex' s2) - latex mkCell (Or s1 s2) = connective (mkCell "\\lor ") (latex' s1) (latex' s2) - latex mkCell (Implies s1 s2) = connective (mkCell "\\to ") (latex' s1) (latex' s2) - latex mkCell (Iff s1 s2) = connective (mkCell "\\leftrightarrow ") (latex' s1) (latex' s2) - - connective middle s1 s2 = [NotMain "("] ++ s1 ++ [middle] ++ s2 ++ [NotMain ")"] - -serialize :: SerializeFormat -> Statement -> String -serialize fmt s = concat $ map fromCell $ serializeCells fmt s - -latexTruthTableMainColumnIndex :: Statement -> Int -latexTruthTableMainColumnIndex s = - fst $ head $ filter (\(i, cell) -> isMain cell) $ zip [0..] $ serializeCells Latex s - -serializeLatexTruthTableRow :: [(String, Bool)] -> Statement -> Maybe [String] -serializeLatexTruthTableRow ass s = map fromCellLatex <$> latexRow Main ass s - where - latexRow mkCell ass (Atom key) = list <$> mkCell <$> toInt <$> eval ass (Atom key) - latexRow mkCell ass (Not s) = (list <$> mkCell <$> toInt <$> not <$> eval ass s) <> latexRow NotMain ass s - latexRow mkCell ass (And s1 s2) = latexRowBinaryConnective (&&) mkCell ass s1 s2 - latexRow mkCell ass (Or s1 s2) = latexRowBinaryConnective (||) mkCell ass s1 s2 - latexRow mkCell ass (Implies s1 s2) = latexRowBinaryConnective implies mkCell ass s1 s2 - latexRow mkCell ass (Iff s1 s2) = latexRowBinaryConnective (==) mkCell ass s1 s2 - - latexRowBinaryConnective op mkCell ass s1 s2 = - ( - \subrow1 subrow2 result -> - [NotMain " "] ++ subrow1 ++ [mkCell $ toInt result] ++ subrow2 ++ [NotMain " "] - ) <$> - latexRow NotMain ass s1 <*> latexRow NotMain ass s2 <*> - (op <$> eval ass s1 <*> eval ass s2) - - toInt :: Bool -> String - toInt False = "0" - toInt True = "1" - - list :: a -> [a] - list x = [x] - - implies :: Bool -> Bool -> Bool - implies b1 b2 = not b1 || b2 - -truthtable :: Statement -> String -truthtable s = open <> header <> "\\hline\n" <> body <> close - where - mainIndex = latexTruthTableMainColumnIndex s - - cellsSpec - | mainIndex == 0 && length serial <= 1 = "c" - | mainIndex == 0 = "c|" <> replicate (length serial - 1) 'c' - | mainIndex == length serial - 1 = replicate (length serial - 1) 'c' <> "|c" - | otherwise = replicate mainIndex 'c' <> "|c|" <> replicate (length serial - mainIndex - 1) 'c' - - open = - "\\begin{tabular}{" <> - replicate (length atomsList) 'c' <> - "||" <> - cellsSpec <> - "}\n" - - close = "\\end{tabular}\n\n" - - serial :: [Cell] - serial = serializeCells Latex s - - atomsList :: [String] - atomsList = S.toAscList $ atoms s - - header :: String - header = - intercalate " & " (map dollars atomsList) <> - " & " <> - intercalate " & " (map dollars $ map fromCell serial) <> - " \\\\\n" - - dollars :: String -> String - dollars string = "$" <> string <> "$" - - body :: String - body = concat $ map line $ enumerate atomsList - - line assignments = - intercalate " & " (bools assignments) <> - " &" <> - intercalate "&" (cells assignments) <> - "\\\\\n" - - bools assignments = [if bool then "1" else "0" | (key, bool) <- assignments] - - cells assignments = - (\xs -> [if x /= " " then " " <> x <> " " else " " | x <- xs]) $ - fromJust $ serializeLatexTruthTableRow assignments s + fail err@(ParseError pos message) = + putStrLn $ + "parse error at position " + <> show pos + <> ": " + <> message diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..47f8988 --- /dev/null +++ b/Makefile @@ -0,0 +1,7 @@ +main: dirty clean + +dirty: + ghc Main.hs -o logic + +clean: + find | grep -E '\.(hi|o)' | xargs rm --