megaparsec
This commit is contained in:
parent
b45e0a3717
commit
864880d58d
@ -21,8 +21,9 @@ description: Please see the README on GitHub at <https://github.com/gith
|
|||||||
|
|
||||||
dependencies:
|
dependencies:
|
||||||
- base >= 4.7 && < 5
|
- base >= 4.7 && < 5
|
||||||
- transformers
|
- mtl
|
||||||
|
- parser-combinators
|
||||||
|
- megaparsec
|
||||||
library:
|
library:
|
||||||
source-dirs: src
|
source-dirs: src
|
||||||
|
|
||||||
|
212
src/Lib.hs
212
src/Lib.hs
@ -1,146 +1,32 @@
|
|||||||
|
{-# LANGUAGE GADTs #-}
|
||||||
|
{-# LANGUAGE TypeFamilies #-}
|
||||||
|
{-# LANGUAGE DeriveFunctor #-}
|
||||||
{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
|
{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
|
||||||
{-# LANGUAGE TypeOperators #-}
|
{-# LANGUAGE TypeOperators #-}
|
||||||
|
{-# LANGUAGE LambdaCase #-}
|
||||||
module Lib where
|
module Lib where
|
||||||
|
|
||||||
import Data.Char
|
import Control.Monad
|
||||||
import Control.Monad
|
import Control.Monad.State
|
||||||
import Control.Applicative
|
import Data.Char
|
||||||
import Control.Monad.Trans.State
|
import Control.Monad.List
|
||||||
import Control.Monad.Trans.Class
|
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
|
||||||
|
|
||||||
|
type Parser = Parsec Void String
|
||||||
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
|
|
||||||
|
|
||||||
parens :: Parser a -> Parser a
|
parens :: Parser a -> Parser a
|
||||||
parens m = do
|
parens = between (string "(") (string ")")
|
||||||
reserved "("
|
reserved :: String -> Parser String
|
||||||
n <- token m
|
reserved a = do
|
||||||
reserved ")"
|
a' <- string a
|
||||||
return n
|
space
|
||||||
|
return a'
|
||||||
|
|
||||||
data Sentence = T
|
data Sentence = T
|
||||||
| F
|
| F
|
||||||
@ -154,45 +40,38 @@ data Sentence = T
|
|||||||
|
|
||||||
|
|
||||||
instance Show Sentence where
|
instance Show Sentence where
|
||||||
show T = "T"
|
show T = "T"
|
||||||
show F = "F"
|
show F = "F"
|
||||||
show (V c) = [c]
|
show (V c) = [c]
|
||||||
show (N s) = "~"++show s
|
show (N s) = "~"++show s
|
||||||
show (SOR a b) = "(" ++ show a ++ " v " ++ show b ++ ")"
|
show (SOR a b) = "(" ++ show a ++ " v " ++ show b ++ ")"
|
||||||
show (SAND a b) = "(" ++ show a ++ " ^ " ++ 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 ++ ")"
|
show (SIMP a b) = "(" ++ show a ++ " => " ++ show b ++ ")"
|
||||||
|
|
||||||
|
|
||||||
sentence :: Parser Sentence
|
sentence :: Parser Sentence
|
||||||
sentence = all <|> parens sentence
|
sentence = all <|> parens sentence
|
||||||
where
|
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
|
t = do
|
||||||
char 'T'
|
reserved "T"
|
||||||
return T
|
return T
|
||||||
f = do
|
f = do
|
||||||
char 'F'
|
reserved "F"
|
||||||
return F
|
return F
|
||||||
v = do
|
v = do
|
||||||
i <- oneOf ['a'..'z']
|
i <- oneOf ['a'..'z']
|
||||||
|
space
|
||||||
return $ V i
|
return $ V i
|
||||||
orOP = reserved "v" >> return SOR
|
bin name f = InfixL (f <$ (string name >> space))
|
||||||
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
|
|
||||||
neg = do
|
neg = do
|
||||||
char '~'
|
char '~'
|
||||||
s1 <- sentence
|
s1 <- sentence
|
||||||
return $ N s1
|
return $ N s1
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
tautology :: Sentence -> StateT [(Char,Bool)] [] Bool
|
tautology :: Sentence -> StateT [(Char,Bool)] [] Bool
|
||||||
tautology T = return True
|
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 (SAND a b) = liftM2 (&&) (tautology a) (tautology b)
|
||||||
tautology (SEQ 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)
|
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'
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user