Compare commits
10 commits
1e66888807
...
c344be1bea
Author | SHA1 | Date | |
---|---|---|---|
![]() |
c344be1bea | ||
![]() |
d781334419 | ||
![]() |
0fa510e31a | ||
![]() |
68bc86c496 | ||
![]() |
f044938d74 | ||
![]() |
aeb4266118 | ||
![]() |
599e553800 | ||
![]() |
8fa9f3698c | ||
![]() |
c6628aedd1 | ||
![]() |
0df55f349d |
9 changed files with 442 additions and 271 deletions
19
.gitignore
vendored
Normal file
19
.gitignore
vendored
Normal file
|
@ -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
|
77
Logic/Parse.hs
Normal file
77
Logic/Parse.hs
Normal file
|
@ -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
|
22
Logic/Statement.hs
Normal file
22
Logic/Statement.hs
Normal file
|
@ -0,0 +1,22 @@
|
||||||
|
module Logic.Statement where
|
||||||
|
|
||||||
|
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)
|
||||||
|
|
||||||
|
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)
|
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
|
291
Main.hs
291
Main.hs
|
@ -1,274 +1,23 @@
|
||||||
import Control.Applicative (Applicative, Alternative(..))
|
module Main where
|
||||||
import Data.Char (isAlphaNum)
|
|
||||||
import Data.Functor (Functor)
|
|
||||||
import Data.List (intercalate)
|
|
||||||
import Data.Maybe (fromJust)
|
|
||||||
import qualified Data.Set as S
|
|
||||||
|
|
||||||
newtype Parser symbol output = Parser
|
import Logic.Parse (eof, mkInput, ParseError(..))
|
||||||
{ runParser :: [symbol] -> Maybe (output, [symbol])
|
import Logic.Statement.Parse (stmt)
|
||||||
}
|
import Logic.Statement.Eval (bucket)
|
||||||
|
import Logic.Statement.Serialize (serializeLatexTruthTable)
|
||||||
|
|
||||||
instance Functor (Parser s) where
|
main :: IO ()
|
||||||
fmap :: (a -> b) -> Parser s a -> Parser s b
|
main = do
|
||||||
fmap f (Parser p) = Parser
|
line <- getLine
|
||||||
{ runParser = \xs -> do
|
case eof stmt $ mkInput line of
|
||||||
(result, xs') <- p xs
|
Left err -> fail err
|
||||||
return (f result, xs')
|
Right statement -> do
|
||||||
}
|
putStrLn $ show statement
|
||||||
|
putStrLn $ show $ bucket statement
|
||||||
instance Applicative (Parser s) where
|
putStr $ serializeLatexTruthTable statement
|
||||||
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
|
|
||||||
where
|
where
|
||||||
n = length token
|
fail err@(ParseError pos message) =
|
||||||
parse xs
|
putStrLn $
|
||||||
| token == take n xs = Just (token, drop n xs)
|
"parse error at position "
|
||||||
| otherwise = Nothing
|
<> show pos
|
||||||
|
<> ": "
|
||||||
parseWhile :: (Char -> Bool) -> Parser Char String
|
<> message
|
||||||
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 = 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)
|
|
||||||
|
|
||||||
serializeParts :: SerializeFormat -> Statement -> [String]
|
|
||||||
serializeParts = aux
|
|
||||||
where
|
|
||||||
aux Ascii = ascii
|
|
||||||
aux Latex = latex
|
|
||||||
|
|
||||||
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 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 ++ [")"]
|
|
||||||
|
|
||||||
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
|
|
||||||
where
|
|
||||||
open =
|
|
||||||
"\\begin{tabular}{" <>
|
|
||||||
replicate (length atomsList) 'c' <>
|
|
||||||
"|" <>
|
|
||||||
replicate (length serial) 'c' <>
|
|
||||||
"}\n"
|
|
||||||
|
|
||||||
close = "\\end{tabular}\n\n"
|
|
||||||
|
|
||||||
serial = serialize Latex s
|
|
||||||
|
|
||||||
atomsList :: [String]
|
|
||||||
atomsList = S.toAscList $ atoms s
|
|
||||||
|
|
||||||
header :: String
|
|
||||||
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 " & " (parts assignments) <>
|
|
||||||
" \\\\\n"
|
|
||||||
|
|
||||||
bools assignments = [if bool then "1" else "0" | (key, bool) <- assignments]
|
|
||||||
|
|
||||||
parts assignments =
|
|
||||||
(\xs -> [" " <> [x] <> " " | x <- xs]) $
|
|
||||||
fromJust $ serializeLatexTruthTableRow assignments s
|
|
||||||
|
|
7
Makefile
Normal file
7
Makefile
Normal file
|
@ -0,0 +1,7 @@
|
||||||
|
main: dirty clean
|
||||||
|
|
||||||
|
dirty:
|
||||||
|
ghc Main.hs -o logic
|
||||||
|
|
||||||
|
clean:
|
||||||
|
find | grep -E '\.(hi|o)' | xargs rm --
|
28
readme.md
Normal file
28
readme.md
Normal file
|
@ -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}
|
||||||
|
```
|
Loading…
Add table
Add a link
Reference in a new issue