From 0df55f349d53ba99f5b945a4db2a0cc79896ac8a Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Thu, 31 Jul 2025 12:24:41 +0000
Subject: [PATCH 01/10] undo progress on making the cols align

---
 Main.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Main.hs b/Main.hs
index 2ff6318..3e10d75 100644
--- a/Main.hs
+++ b/Main.hs
@@ -270,5 +270,5 @@ truthtable s = open <> header <> "\\hline\n" <> body <> close
     bools assignments = [if bool then "1" else "0" | (key, bool) <- assignments]
 
     parts assignments =
-      (\xs -> [" " <> [x] <> " " | x <- xs]) $
+      (\xs -> [[x] | x <- xs]) $
       fromJust $ serializeLatexTruthTableRow assignments s

From c6628aedd153e118bd4b5e4d8f5b4e76d3aabd31 Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Thu, 31 Jul 2025 12:25:53 +0000
Subject: [PATCH 02/10] no spaces in latex truth table

---
 Main.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Main.hs b/Main.hs
index 3e10d75..9421ae3 100644
--- a/Main.hs
+++ b/Main.hs
@@ -270,5 +270,5 @@ truthtable s = open <> header <> "\\hline\n" <> body <> close
     bools assignments = [if bool then "1" else "0" | (key, bool) <- assignments]
 
     parts assignments =
-      (\xs -> [[x] | x <- xs]) $
+      (\xs -> [[x] | x <- filter (\i -> i /= ' ') xs]) $
       fromJust $ serializeLatexTruthTableRow assignments s

From 8fa9f3698c53252bc3c7b24747bb852fc4da0ecd Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Thu, 31 Jul 2025 12:32:46 +0000
Subject: [PATCH 03/10] oops: the last commit but properly

---
 Main.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Main.hs b/Main.hs
index 9421ae3..1d75a66 100644
--- a/Main.hs
+++ b/Main.hs
@@ -263,12 +263,12 @@ truthtable s = open <> header <> "\\hline\n" <> body <> close
 
     line assignments =
       intercalate " & " (bools assignments) <>
-      " & " <>
-      intercalate " & " (parts assignments) <>
-      " \\\\\n"
+      " &" <>
+      intercalate "&" (parts assignments) <>
+      "\\\\\n"
 
     bools assignments = [if bool then "1" else "0" | (key, bool) <- assignments]
 
     parts assignments =
-      (\xs -> [[x] | x <- filter (\i -> i /= ' ') xs]) $
+      (\xs -> [if x /= ' ' then [' ', x, ' '] else " " | x <- xs]) $
       fromJust $ serializeLatexTruthTableRow assignments s

From 599e55380041625761b8ecd88c44a64f10224f23 Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Fri, 1 Aug 2025 13:07:44 +0000
Subject: [PATCH 04/10] latex truth table: main column

---
 Main.hs | 110 +++++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 74 insertions(+), 36 deletions(-)

diff --git a/Main.hs b/Main.hs
index 1d75a66..2d20ada 100644
--- a/Main.hs
+++ b/Main.hs
@@ -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

From aeb42661187f5b10dec4b36a5ddb05a6cabc5179 Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Fri, 1 Aug 2025 14:07:58 +0000
Subject: [PATCH 05/10] typo: \cap \cup -> \land \lor

---
 Main.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Main.hs b/Main.hs
index 2d20ada..fc5a032 100644
--- a/Main.hs
+++ b/Main.hs
@@ -219,8 +219,8 @@ serializeCells = aux Main
 
     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 (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)
 

From f044938d7443e5851f8ea7959bbe5d16d74858ad Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Sat, 2 Aug 2025 09:21:25 +0000
Subject: [PATCH 06/10] latex truth table: fix table spec length

---
 Main.hs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Main.hs b/Main.hs
index fc5a032..6007106 100644
--- a/Main.hs
+++ b/Main.hs
@@ -281,7 +281,8 @@ truthtable s = open <> header <> "\\hline\n" <> body <> close
 
     close = "\\end{tabular}\n\n"
 
-    serial = serialize Latex s
+    serial :: [Cell]
+    serial = serializeCells Latex s
 
     atomsList :: [String]
     atomsList = S.toAscList $ atoms s
@@ -290,7 +291,7 @@ truthtable s = open <> header <> "\\hline\n" <> body <> close
     header =
       intercalate " & " (map dollars atomsList) <>
       " & " <>
-      intercalate " & " (map dollars $ map fromCell $ serializeCells Latex s) <>
+      intercalate " & " (map dollars $ map fromCell serial) <>
       " \\\\\n"
 
     dollars :: String -> String

From 68bc86c496ce357e1663cec6b80d60b1cf608ca6 Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Sat, 2 Aug 2025 09:25:48 +0000
Subject: [PATCH 07/10] latex truth table: fix counting

---
 Main.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Main.hs b/Main.hs
index 6007106..f82b840 100644
--- a/Main.hs
+++ b/Main.hs
@@ -139,7 +139,7 @@ bucket s
     values = [fromJust $ eval assignments s | assignments <- enumerate $ atomsList]
 
 enumerate :: [a] -> [[(a, Bool)]]
-enumerate keys = aux start
+enumerate keys = map reverse $ aux start
   where
     aux assignments = (assignments:) $
       case next assignments of

From 0fa510e31a9928cca76d3e7fc169dc442ce831a3 Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Thu, 7 Aug 2025 09:23:50 +0000
Subject: [PATCH 08/10] separate into files, parser error messages

---
 .gitignore         |  19 +++
 Logic/Parse.hs     |  77 +++++++++++
 Logic/Statement.hs | 237 +++++++++++++++++++++++++++++++++
 Main.hs            | 323 ++-------------------------------------------
 Makefile           |   7 +
 5 files changed, 353 insertions(+), 310 deletions(-)
 create mode 100644 .gitignore
 create mode 100644 Logic/Parse.hs
 create mode 100644 Logic/Statement.hs
 create mode 100644 Makefile

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 --

From d781334419349ad363209fa30afd63d4450a4fe3 Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Fri, 8 Aug 2025 04:36:22 +0000
Subject: [PATCH 09/10] 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 $

From c344be1bea166a8fb76aa8bc32e57053e2e4cf5a Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Fri, 8 Aug 2025 04:39:55 +0000
Subject: [PATCH 10/10] readme

---
 Main.hs   |  2 ++
 readme.md | 28 ++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 readme.md

diff --git a/Main.hs b/Main.hs
index 20e5aeb..f3effef 100644
--- a/Main.hs
+++ b/Main.hs
@@ -2,6 +2,7 @@ module Main where
 
 import Logic.Parse (eof, mkInput, ParseError(..))
 import Logic.Statement.Parse (stmt)
+import Logic.Statement.Eval (bucket)
 import Logic.Statement.Serialize (serializeLatexTruthTable)
 
 main :: IO ()
@@ -11,6 +12,7 @@ main = do
     Left err -> fail err
     Right statement -> do
       putStrLn $ show statement
+      putStrLn $ show $ bucket statement
       putStr $ serializeLatexTruthTable statement
   where
     fail err@(ParseError pos message) =
diff --git a/readme.md b/readme.md
new file mode 100644
index 0000000..d841c09
--- /dev/null
+++ b/readme.md
@@ -0,0 +1,28 @@
+Statement logic !!!
+
+# Compile it
+
+```sh
+make
+```
+
+# Usage
+
+```sh
+echo '((p->q)<->(!q->!p))' | ./logic
+```
+
+## Output
+
+```
+Iff (Implies (Atom "p") (Atom "q")) (Implies (Not (Atom "q")) (Not (Atom "p")))
+Tautology
+\begin{tabular}{cc||cccccc|c|cccccccc}
+$p$ & $q$ & $($ & $($ & $p$ & $\to $ & $q$ & $)$ & $\leftrightarrow $ & $($ & $\neg $ & $q$ & $\to $ & $\neg $ & $p$ & $)$ & $)$ \\
+\hline
+0 & 0 &  &  & 0 & 1 & 0 &  & \textbf 1 &  & 1 & 0 & 1 & 1 & 0 &  & \\
+0 & 1 &  &  & 1 & 0 & 0 &  & \textbf 1 &  & 1 & 0 & 0 & 0 & 1 &  & \\
+1 & 0 &  &  & 0 & 1 & 1 &  & \textbf 1 &  & 0 & 1 & 1 & 1 & 0 &  & \\
+1 & 1 &  &  & 1 & 1 & 1 &  & \textbf 1 &  & 0 & 1 & 1 & 0 & 1 &  & \\
+\end{tabular}
+```