From d781334419349ad363209fa30afd63d4450a4fe3 Mon Sep 17 00:00:00 2001 From: hi Date: Fri, 8 Aug 2025 04:36:22 +0000 Subject: [PATCH] split Logic.Statement into files, simpler serialization --- Logic/Statement.hs | 215 ----------------------------------- Logic/Statement/Eval.hs | 47 ++++++++ Logic/Statement/Parse.hs | 49 ++++++++ Logic/Statement/Serialize.hs | 173 ++++++++++++++++++++++++++++ Main.hs | 9 +- 5 files changed, 276 insertions(+), 217 deletions(-) create mode 100644 Logic/Statement/Eval.hs create mode 100644 Logic/Statement/Parse.hs create mode 100644 Logic/Statement/Serialize.hs diff --git a/Logic/Statement.hs b/Logic/Statement.hs index 09b94ec..6902140 100644 --- a/Logic/Statement.hs +++ b/Logic/Statement.hs @@ -1,11 +1,5 @@ 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 @@ -17,47 +11,6 @@ data 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 @@ -67,171 +20,3 @@ atoms = toAscList . mkSet 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/Logic/Statement/Eval.hs b/Logic/Statement/Eval.hs new file mode 100644 index 0000000..83d716c --- /dev/null +++ b/Logic/Statement/Eval.hs @@ -0,0 +1,47 @@ +module Logic.Statement.Eval where + +import Logic.Statement (Statement(..), atoms) + +import Data.List (intercalate) +import Data.Either (fromRight) + +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] + +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 + +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) + +implies :: Bool -> Bool -> Bool +implies b1 b2 = not b1 || b2 diff --git a/Logic/Statement/Parse.hs b/Logic/Statement/Parse.hs new file mode 100644 index 0000000..d256a43 --- /dev/null +++ b/Logic/Statement/Parse.hs @@ -0,0 +1,49 @@ +module Logic.Statement.Parse where + +import Logic.Parse + ( Parser(..) + , Input(..) + , ParseError + , expected + , parseToken + , parseIf + ) +import Logic.Statement (Statement(..)) + +import Control.Applicative (Alternative((<|>), some)) +import Data.Char (isAlphaNum) + +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 diff --git a/Logic/Statement/Serialize.hs b/Logic/Statement/Serialize.hs new file mode 100644 index 0000000..fa76f5b --- /dev/null +++ b/Logic/Statement/Serialize.hs @@ -0,0 +1,173 @@ +module Logic.Statement.Serialize where + +import Logic.Statement (Statement(..), atoms) +import Logic.Statement.Eval (enumerate, eval, implies) + +import Data.List (intercalate) +import Data.Either (fromRight) + +data TokenString = TokenString + { tsCanEval :: CanEval + , tsLevel :: Int + , tsString :: String + } deriving (Show, Eq) + +data CanEval + = Filler + | CanEval + deriving (Show, Eq) + +data TokenValue = TokenValue + { tvLevel :: Int + , tvValue :: Value + } deriving (Show, Eq) + +data Value + = NoValue + | Value Bool + deriving (Show, Eq) + +data SerializeFormat + = Plain + | Latex +-- | PrefixPlain + deriving (Show, Eq) + +serialize :: SerializeFormat -> Statement -> String +serialize fmt s = concat $ map tsString $ serializeStrings fmt s + +serializeStrings :: SerializeFormat -> Statement -> [TokenString] +serializeStrings fmt = aux 0 + where + aux :: Int -> Statement -> [TokenString] + aux = + case fmt of + Plain -> serializeStringsPlain + Latex -> serializeStringsLatex + +-- Internal function +serializeStringsPlain :: Int -> Statement -> [TokenString] +serializeStringsPlain level = aux + where + f = serializeStringsPlain + level' = level + 1 + + aux (Atom key) = [TokenString CanEval level key] + aux (Not s) = [TokenString CanEval level "!"] ++ f level' s + aux (And s1 s2) = connective level "&" (f level' s1) (f level' s2) + aux (Or s1 s2) = connective level "|" (f level' s1) (f level' s2) + aux (Implies s1 s2) = connective level "->" (f level' s1) (f level' s2) + aux (Iff s1 s2) = connective level "<->" (f level' s1) (f level' s2) + +-- Internal function +serializeStringsLatex :: Int -> Statement -> [TokenString] +serializeStringsLatex level = aux + where + f = serializeStringsLatex + level' = level + 1 + + aux (Atom key) = [TokenString CanEval level key] + aux (Not s) = [TokenString CanEval level "\\neg "] ++ f level' s + aux (And s1 s2) = connective level "\\land " (f level' s1) (f level' s2) + aux (Or s1 s2) = connective level "\\lor " (f level' s1) (f level' s2) + aux (Implies s1 s2) = connective level "\\to " (f level' s1) (f level' s2) + aux (Iff s1 s2) = connective level "\\leftrightarrow " (f level' s1) (f level' s2) + +-- Internal function +connective :: Int -> String -> [TokenString] -> [TokenString] -> [TokenString] +connective level middle tokens1 tokens2 = + [TokenString Filler level "("] + ++ tokens1 + ++ [TokenString CanEval level middle] + ++ tokens2 + ++ [TokenString Filler level ")"] + +-- Using infix convention with brackets +serializeValues :: [(String, Bool)] -> Statement -> Either String [TokenValue] +serializeValues ass = fmap snd . aux 0 + where + aux :: Int -> Statement -> Either String (Bool, [TokenValue]) + aux level s@(Atom key) = do + bool <- eval ass s + return (bool, [TokenValue level $ Value bool]) + aux level (Not s) = do + (bool, tokens) <- aux (level + 1) s + return (not bool, [TokenValue level $ Value $ not bool] ++ tokens) + aux level (And s1 s2) = connective level (&&) s1 s2 + aux level (Or s1 s2) = connective level (||) s1 s2 + aux level (Implies s1 s2) = connective level implies s1 s2 + aux level (Iff s1 s2) = connective level (==) s1 s2 + + connective + :: Int + -> (Bool -> Bool -> Bool) + -> Statement + -> Statement + -> Either String (Bool, [TokenValue]) + connective level f s1 s2 = do + (bool1, tokens1) <- aux (level + 1) s1 + (bool2, tokens2) <- aux (level + 1) s2 + let bracket = [TokenValue level NoValue] + let bool = f bool1 bool2 + return (bool, bracket ++ tokens1 ++ [TokenValue level $ Value bool] ++ tokens2 ++ bracket) + +serializeLatexTruthTable :: Statement -> String +serializeLatexTruthTable s = open <> header <> "\\hline\n" <> body <> close + where + open :: String + open = "\\begin{tabular}{" <> replicate (length $ atoms s) 'c' <> "||" <> spec <> "}\n" + + close :: String + close = "\\end{tabular}\n" + + spec :: String + spec + | length serial == 0 = undefined + | length serial == 1 = "c" + | isMain (head serial) = "c|" <> replicate (length serial - 1) 'c' + | isMain (serial !! (length serial - 1)) = replicate (length serial - 1) 'c' <> "|c" + | otherwise = concat $ map (\token -> if isMain token then "|c|" else "c") serial + + isMain :: TokenString -> Bool + isMain (TokenString CanEval level string) = level == 0 + isMain _ = False + + serial :: [TokenString] + serial = serializeStrings Latex s + + header :: String + header = + intercalate " & " (map dollars $ atoms s) <> + " & " <> + intercalate " & " (map dollars $ map tsString serial) <> + " \\\\\n" + + dollars :: String -> String + dollars string = "$" <> string <> "$" + + body :: String + body = concat $ map line $ enumerate $ atoms s + + line :: [(String, Bool)] -> String + line ass = + intercalate " & " (bools ass) <> + " & " <> + intercalate " & " (cells ass) <> + "\\\\\n" + + bools :: [(String, Bool)] -> [String] + bools ass = [if bool then "1" else "0" | (key, bool) <- ass] + + cells :: [(String, Bool)] -> [String] + cells ass = map cell $ fromRight undefined $ serializeValues ass s + + cell :: TokenValue -> String + cell (TokenValue level value) = + case value of + NoValue -> "" + Value bool -> mkBold level $ if bool then "1" else "0" + + mkBold :: Int -> String -> String + mkBold level string + | level == 0 = "\\textbf " <> string + | otherwise = string diff --git a/Main.hs b/Main.hs index 1b4a479..20e5aeb 100644 --- a/Main.hs +++ b/Main.hs @@ -1,12 +1,17 @@ module Main where import Logic.Parse (eof, mkInput, ParseError(..)) -import Logic.Statement (stmt) +import Logic.Statement.Parse (stmt) +import Logic.Statement.Serialize (serializeLatexTruthTable) main :: IO () main = do line <- getLine - either fail print $ eof stmt $ mkInput line + case eof stmt $ mkInput line of + Left err -> fail err + Right statement -> do + putStrLn $ show statement + putStr $ serializeLatexTruthTable statement where fail err@(ParseError pos message) = putStrLn $