compiled
This commit is contained in:
parent
864880d58d
commit
98c0f85e6a
@ -3,4 +3,4 @@ module Main where
|
||||
import Lib
|
||||
|
||||
main :: IO ()
|
||||
main = go
|
||||
main = getLine >>= go
|
||||
|
@ -34,9 +34,13 @@ executables:
|
||||
ghc-options:
|
||||
- -threaded
|
||||
- -rtsopts
|
||||
- -static
|
||||
- -O2
|
||||
- -with-rtsopts=-N
|
||||
dependencies:
|
||||
- parser-sandbox
|
||||
cc-options: -static
|
||||
ld-options: -static -pthread
|
||||
|
||||
tests:
|
||||
parser-sandbox-test:
|
||||
|
BIN
parser-sandbox-exe
Executable file
BIN
parser-sandbox-exe
Executable file
Binary file not shown.
35
src/Lib.hs
35
src/Lib.hs
@ -17,6 +17,7 @@ import Text.Megaparsec
|
||||
import Text.Megaparsec.Char
|
||||
import Data.Void
|
||||
import Control.Monad.Combinators.Expr
|
||||
import Data.List
|
||||
|
||||
type Parser = Parsec Void String
|
||||
|
||||
@ -36,25 +37,12 @@ data Sentence = T
|
||||
| Sentence `SAND` Sentence
|
||||
| Sentence `SEQ` Sentence
|
||||
| Sentence `SIMP` Sentence
|
||||
deriving (Eq)
|
||||
|
||||
|
||||
instance Show Sentence where
|
||||
show T = "T"
|
||||
show F = "F"
|
||||
show (V c) = [c]
|
||||
show (N s) = "~"++show s
|
||||
show (SOR a b) = "(" ++ show a ++ " v " ++ show b ++ ")"
|
||||
show (SAND a b) = "(" ++ show a ++ " ^ " ++ show b ++ ")"
|
||||
show (SEQ a b) = "(" ++ show a ++ " == " ++ show b ++ ")"
|
||||
show (SIMP a b) = "(" ++ show a ++ " => " ++ show b ++ ")"
|
||||
|
||||
deriving (Eq, Show)
|
||||
|
||||
sentence :: Parser Sentence
|
||||
sentence = all <|> parens sentence
|
||||
where
|
||||
all = t <|> f <|> v <|> neg <|> try (parens $ makeExprParser sentence [[bin "v" SOR, bin "^" SAND]
|
||||
,[bin "==" SEQ, bin "=>" SIMP]])
|
||||
all = t <|> f <|> v <|> neg <|> or' <|> and' <|> eq' <|> imp'
|
||||
t = do
|
||||
reserved "T"
|
||||
return T
|
||||
@ -62,17 +50,25 @@ sentence = all <|> parens sentence
|
||||
reserved "F"
|
||||
return F
|
||||
v = do
|
||||
i <- oneOf ['a'..'z']
|
||||
i <- oneOf $ ['a'..'z'] \\ ['v']
|
||||
space
|
||||
return $ V i
|
||||
bin name f = InfixL (f <$ (string name >> space))
|
||||
bin a b = try $ parens $ do
|
||||
s1 <- sentence
|
||||
space
|
||||
string a
|
||||
space
|
||||
s2 <- sentence
|
||||
return $ b s1 s2
|
||||
or' = bin "v" SOR
|
||||
and' = bin "^" SAND
|
||||
eq' = bin "==" SEQ
|
||||
imp' = bin "=>" SIMP
|
||||
neg = do
|
||||
char '~'
|
||||
s1 <- sentence
|
||||
return $ N s1
|
||||
|
||||
|
||||
|
||||
tautology :: Sentence -> StateT [(Char,Bool)] [] Bool
|
||||
tautology T = return True
|
||||
tautology F = return False
|
||||
@ -90,6 +86,7 @@ tautology (SOR a b) = liftM2 (||) (tautology a) (tautology b)
|
||||
tautology (SAND a b) = liftM2 (&&) (tautology a) (tautology b)
|
||||
tautology (SEQ a b) = liftM2 (==) (tautology a) (tautology b)
|
||||
tautology (SIMP a b) = liftM2 (||) (not <$> tautology a) (tautology b)
|
||||
|
||||
checkTautology s = all ((==True) . fst ) $ runStateT (tautology s) []
|
||||
|
||||
go s = do
|
||||
|
Loading…
Reference in New Issue
Block a user