latex truth table: main column

This commit is contained in:
hi 2025-08-01 13:07:44 +00:00
parent 8fa9f3698c
commit 599e553800

110
Main.hs
View file

@ -184,61 +184,99 @@ data SerializeFormat
| Latex
deriving (Show, Eq)
serializeParts :: SerializeFormat -> Statement -> [String]
serializeParts = aux
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 Ascii = ascii
aux Latex = latex
aux mkCell Ascii = ascii mkCell
aux mkCell Latex = latex mkCell
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)
ascii' = ascii NotMain
latex' = latex NotMain
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)
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)
connective token s1 s2 = ["("] ++ s1 ++ [token] ++ s2 ++ [")"]
latex mkCell (Atom key) = [mkCell key]
latex mkCell (Not s) = [mkCell "\\neg "] ++ latex' s
latex mkCell (And s1 s2) = connective (mkCell "\\cap ") (latex' s1) (latex' s2)
latex mkCell (Or s1 s2) = connective (mkCell "\\cup ") (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 $ serializeParts fmt s
serialize fmt s = concat $ map fromCell $ serializeCells fmt s
serializeLatexTruthTableRow :: [(String, Bool)] -> Statement -> Maybe String
serializeLatexTruthTableRow = latexRow
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 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
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 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
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' <>
"|" <>
replicate (length serial) 'c' <>
"||" <>
cellsSpec <>
"}\n"
close = "\\end{tabular}\n\n"
@ -252,7 +290,7 @@ truthtable s = open <> header <> "\\hline\n" <> body <> close
header =
intercalate " & " (map dollars atomsList) <>
" & " <>
intercalate " & " (map dollars $ serializeParts Latex s) <>
intercalate " & " (map dollars $ map fromCell $ serializeCells Latex s) <>
" \\\\\n"
dollars :: String -> String
@ -264,11 +302,11 @@ truthtable s = open <> header <> "\\hline\n" <> body <> close
line assignments =
intercalate " & " (bools assignments) <>
" &" <>
intercalate "&" (parts assignments) <>
intercalate "&" (cells assignments) <>
"\\\\\n"
bools assignments = [if bool then "1" else "0" | (key, bool) <- assignments]
parts assignments =
(\xs -> [if x /= ' ' then [' ', x, ' '] else " " | x <- xs]) $
cells assignments =
(\xs -> [if x /= " " then " " <> x <> " " else " " | x <- xs]) $
fromJust $ serializeLatexTruthTableRow assignments s