diff --git a/package.yaml b/package.yaml index fa5df27..b12a5f4 100644 --- a/package.yaml +++ b/package.yaml @@ -21,8 +21,9 @@ description: Please see the README on GitHub at = 4.7 && < 5 -- transformers - +- mtl +- parser-combinators +- megaparsec library: source-dirs: src diff --git a/src/Lib.hs b/src/Lib.hs index 52b8d6c..72cfbea 100644 --- a/src/Lib.hs +++ b/src/Lib.hs @@ -1,146 +1,32 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DeriveFunctor #-} {-# OPTIONS_GHC -fno-warn-unused-do-bind #-} {-# LANGUAGE TypeOperators #-} - +{-# LANGUAGE LambdaCase #-} module Lib where -import Data.Char -import Control.Monad -import Control.Applicative -import Control.Monad.Trans.State -import Control.Monad.Trans.Class +import Control.Monad +import Control.Monad.State +import Data.Char +import Control.Monad.List +import Control.Monad.Identity +import Control.Monad.Writer +import Debug.Trace +import Text.Megaparsec +import Text.Megaparsec.Char +import Data.Void +import Control.Monad.Combinators.Expr - -newtype Parser a = Parser { parse :: String -> [(a,String)]} - - - - - -runParser :: Parser a -> String -> a -runParser m s = - case parse m s of - [(res,[])] -> res - [(_,rs)] -> error "Parser did not consume entire stream" - _ -> error "Parser error" - - - -item :: Parser Char -item = Parser $ \s -> - case s of - [] -> [] - (c:cs) -> [(c,cs)] - - -bind :: Parser a -> (a -> Parser b) -> Parser b -bind p f = Parser $ \s -> - do - (a1,s1) <- parse p s - parse (f a1) s1 - -unit :: a -> Parser a -unit a = Parser (\s -> [(a,s)]) - - -instance Functor Parser where - fmap f (Parser cs) = Parser $ \s -> [(f a, b) | (a,b) <- cs s] - -instance Applicative Parser where - pure = return - (Parser cs1) <*> (Parser cs2) = Parser (\s -> [(f a, s2) | (f, s1) <- cs1 s, (a, s2) <- cs2 s1]) - -instance Monad Parser where - return = unit - (>>=) = bind - -instance MonadPlus Parser where - mzero = failure - mplus = combine - -instance Alternative Parser where - empty = mzero - (<|>) = option - -failure :: Parser a -failure = Parser $ \cs -> [] - -combine :: Parser a -> Parser a -> Parser a -combine p q = Parser $ \s -> parse p s <> parse q s - - -option :: Parser a -> Parser a -> Parser a -option p q = Parser $ \s -> - case parse p s of - [] -> parse q s - res -> res - -satisfy :: (Char -> Bool) -> Parser Char -satisfy p = - item >>= \c -> - if p c - then unit c - else (Parser (\cs -> [])) - - -oneOf :: [Char] -> Parser Char -oneOf s = satisfy (flip elem s) - -chainl :: Parser a -> Parser (a -> a -> a) -> a -> Parser a -chainl p op a = (p `chainl1` op) <|> return a - -chainl1 :: Parser a -> Parser (a -> a -> a) -> Parser a -chainl1 p op = do { a <- p; rest a} - where rest a = (do - f <- op - b <- p - rest (f a b)) <|> return a - - - - -char :: Char -> Parser Char -char c = satisfy (c ==) - -natural :: Parser Integer -natural = read <$> some (satisfy isDigit) - - -string :: String -> Parser String -string [] = return [] -string (c:cs) = do - char c - string cs - return (c:cs) - -token :: Parser a -> Parser a -token p = do - a <- p - spaces - return a - -reserved :: String -> Parser String -reserved s = token (string s) - -spaces :: Parser String -spaces = many $ oneOf " \n\r" - - -digit :: Parser Char -digit = satisfy isDigit - -number :: Parser Int -number = do - s <- string "-" <|> return [] - cs <- some digit - return $ read $ s ++ cs +type Parser = Parsec Void String parens :: Parser a -> Parser a -parens m = do - reserved "(" - n <- token m - reserved ")" - return n - +parens = between (string "(") (string ")") +reserved :: String -> Parser String +reserved a = do + a' <- string a + space + return a' data Sentence = T | F @@ -154,45 +40,38 @@ data Sentence = T 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 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 (SEQ a b) = "(" ++ show a ++ " == " ++ show b ++ ")" show (SIMP a b) = "(" ++ show a ++ " => " ++ show b ++ ")" + sentence :: Parser Sentence -sentence = all <|> parens sentence +sentence = all <|> parens sentence where - all = t <|> f <|> v <|> neg <|> or <|> and <|> eq <|> imp + all = t <|> f <|> v <|> neg <|> try (parens $ makeExprParser sentence [[bin "v" SOR, bin "^" SAND] + ,[bin "==" SEQ, bin "=>" SIMP]]) t = do - char 'T' + reserved "T" return T f = do - char 'F' + reserved "F" return F v = do i <- oneOf ['a'..'z'] + space return $ V i - orOP = reserved "v" >> return SOR - andOP = reserved "^" >> return SOR - eqOP = reserved "==" >> return SEQ - binary op = chainl1 (token $ parens sentence) op - or = binary orOP - and = binary andOP - eq = binary eqOP - imp = do - s1 <- token $ parens sentence - reserved "=>" - s2 <- token $ parens sentence - return $ SIMP s1 s2 + bin name f = InfixL (f <$ (string name >> space)) neg = do char '~' s1 <- sentence return $ N s1 + tautology :: Sentence -> StateT [(Char,Bool)] [] Bool tautology T = return True @@ -211,11 +90,16 @@ 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) [] +checkTautology s = all ((==True) . fst ) $ runStateT (tautology s) [] + +go s = do + let s' = parse sentence "" s + case s' of + Left x -> print x + Right x -> do + print x + print $ checkTautology x + + -go = do - s <- getLine - let s' = runParser sentence s - print s' - print $ checkTautology s'