From 1e66888807048ef02a10dfe3bac4f763f970c238 Mon Sep 17 00:00:00 2001 From: hi Date: Thu, 31 Jul 2025 12:22:12 +0000 Subject: [PATCH] latex truth table: hard part --- Main.hs | 56 ++++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 46 insertions(+), 10 deletions(-) diff --git a/Main.hs b/Main.hs index 859b8c2..2ff6318 100644 --- a/Main.hs +++ b/Main.hs @@ -184,27 +184,52 @@ data SerializeFormat | Latex deriving (Show, Eq) -serialize :: SerializeFormat -> Statement -> String -serialize = aux +serializeParts :: SerializeFormat -> Statement -> [String] +serializeParts = aux where aux Ascii = ascii aux Latex = latex - ascii (Atom string) = string - ascii (Not s) = "!" <> ascii s + ascii (Atom key) = [key] + ascii (Not s) = ["!"] ++ ascii s ascii (And s1 s2) = connective "&" (ascii s1) (ascii s2) ascii (Or s1 s2) = connective "|" (ascii s1) (ascii s2) ascii (Implies s1 s2) = connective "->" (ascii s1) (ascii s2) ascii (Iff s1 s2) = connective "<->" (ascii s1) (ascii s2) - latex (Atom string) = string - latex (Not s) = "\\neg " <> latex s + latex (Atom key) = [key] + latex (Not s) = ["\\neg "] ++ latex s latex (And s1 s2) = connective "\\cap " (latex s1) (latex s2) latex (Or s1 s2) = connective "\\cup " (latex s1) (latex s2) latex (Implies s1 s2) = connective "\\to " (latex s1) (latex s2) latex (Iff s1 s2) = connective "\\leftrightarrow " (latex s1) (latex s2) - connective token s1 s2 = "(" <> s1 <> token <> s2 <> ")" + connective token s1 s2 = ["("] ++ s1 ++ [token] ++ s2 ++ [")"] + +serialize :: SerializeFormat -> Statement -> String +serialize fmt s = concat $ serializeParts fmt s + +serializeLatexTruthTableRow :: [(String, Bool)] -> Statement -> Maybe String +serializeLatexTruthTableRow = latexRow + where + latexRow ass (Atom key) = toInt <$> eval ass (Atom key) + latexRow ass (Not s) = (toInt <$> not <$> eval ass s) <> latexRow ass s + latexRow ass (And s1 s2) = latexRowBinaryConnective (&&) ass s1 s2 + latexRow ass (Or s1 s2) = latexRowBinaryConnective (||) ass s1 s2 + latexRow ass (Implies s1 s2) = latexRowBinaryConnective implies ass s1 s2 + latexRow ass (Iff s1 s2) = latexRowBinaryConnective (==) ass s1 s2 + + latexRowBinaryConnective op ass s1 s2 = + (\subrow1 subrow2 subeval1 subeval2 -> " " <> subrow1 <> (toInt $ op subeval1 subeval2) <> subrow2 <> " ") <$> + latexRow ass s1 <*> latexRow ass s2 <*> + eval ass s1 <*> eval ass s2 + + toInt :: Bool -> String + toInt False = "0" + toInt True = "1" + + implies :: Bool -> Bool -> Bool + implies b1 b2 = not b1 || b2 truthtable :: Statement -> String truthtable s = open <> header <> "\\hline\n" <> body <> close @@ -224,15 +249,26 @@ truthtable s = open <> header <> "\\hline\n" <> body <> close atomsList = S.toAscList $ atoms s header :: String - header = intercalate "&" atomsList <> " \\\\\n" + header = + intercalate " & " (map dollars atomsList) <> + " & " <> + intercalate " & " (map dollars $ serializeParts Latex s) <> + " \\\\\n" + dollars :: String -> String + dollars string = "$" <> string <> "$" + + body :: String body = concat $ map line $ enumerate atomsList line assignments = - intercalate "&" (bools assignments) <> + intercalate " & " (bools assignments) <> + " & " <> intercalate " & " (parts assignments) <> " \\\\\n" bools assignments = [if bool then "1" else "0" | (key, bool) <- assignments] - parts assignments = [""] + parts assignments = + (\xs -> [" " <> [x] <> " " | x <- xs]) $ + fromJust $ serializeLatexTruthTableRow assignments s