split Logic.Statement into files, simpler serialization
This commit is contained in:
hi
parent
0fa510e31a
commit
d781334419
5 changed files with 276 additions and 217 deletions
|
|
@ -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
|
||||
|
|
|
|||
47
Logic/Statement/Eval.hs
Normal file
47
Logic/Statement/Eval.hs
Normal file
|
|
@ -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
|
||||
49
Logic/Statement/Parse.hs
Normal file
49
Logic/Statement/Parse.hs
Normal file
|
|
@ -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
|
||||
173
Logic/Statement/Serialize.hs
Normal file
173
Logic/Statement/Serialize.hs
Normal file
|
|
@ -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
|
||||
9
Main.hs
9
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 $
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue