module HOL.Parse
where
import qualified Data.ByteString.Lazy as ByteString
import qualified Data.Char as Char
import qualified Data.List as List
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as Text
import qualified Data.Text.Lazy.Encoding as Text.Encoding
import Text.Parsec ((<|>),Parsec)
import qualified Text.Parsec as Parsec
import Text.Parsec.Text.Lazy ()
import HOL.Name
spaceParser :: Parsec Text st ()
spaceParser :: Parsec Text st ()
spaceParser = [Char] -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
Parsec.oneOf [Char]
" \t" ParsecT Text st Identity Char
-> Parsec Text st () -> Parsec Text st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Parsec Text st ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
eolParser :: Parsec Text st ()
eolParser :: Parsec Text st ()
eolParser = Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'\n' ParsecT Text st Identity Char
-> Parsec Text st () -> Parsec Text st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Parsec Text st ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
lineParser :: Parsec Text st Char
lineParser :: Parsec Text st Char
lineParser = [Char] -> Parsec Text st Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
Parsec.noneOf [Char]
"\n"
class Parsable a where
parser :: Parsec Text st a
fromText :: Text -> Maybe a
fromText Text
t =
case Parsec Text () a -> [Char] -> Text -> Either ParseError a
forall s t a.
Stream s Identity t =>
Parsec s () a -> [Char] -> s -> Either ParseError a
Parsec.parse (Parsec Text () a
forall a st. Parsable a => Parsec Text st a
parser Parsec Text () a -> ParsecT Text () Identity () -> Parsec Text () a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
Parsec.eof) [Char]
"" Text
t of
Left ParseError
_ -> Maybe a
forall a. Maybe a
Nothing
Right a
a -> a -> Maybe a
forall a. a -> Maybe a
Just a
a
fromString :: String -> Maybe a
fromString = Text -> Maybe a
forall a. Parsable a => Text -> Maybe a
fromText (Text -> Maybe a) -> ([Char] -> Text) -> [Char] -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Text
Text.pack
fromStringUnsafe :: String -> a
fromStringUnsafe [Char]
s =
case [Char] -> Maybe a
forall a. Parsable a => [Char] -> Maybe a
fromString [Char]
s of
Just a
a -> a
a
Maybe a
Nothing -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"couldn't parse " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
s
fromTextFile :: FilePath -> IO a
fromTextFile [Char]
file = do
ByteString
bs <- [Char] -> IO ByteString
ByteString.readFile [Char]
file
let txt :: Text
txt = ByteString -> Text
Text.Encoding.decodeUtf8 ByteString
bs
case Parsec Text () a -> [Char] -> Text -> Either ParseError a
forall s t a.
Stream s Identity t =>
Parsec s () a -> [Char] -> s -> Either ParseError a
Parsec.parse (Parsec Text () a
forall a st. Parsable a => Parsec Text st a
parser Parsec Text () a -> ParsecT Text () Identity () -> Parsec Text () a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
Parsec.eof) [Char]
file Text
txt of
Left ParseError
e -> [Char] -> IO a
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO a) -> [Char] -> IO a
forall a b. (a -> b) -> a -> b
$ ParseError -> [Char]
forall a. Show a => a -> [Char]
show ParseError
e
Right a
a -> a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
data ParseInteger =
StartParseInteger
| ZeroParseInteger
| NegativeParseInteger
| NonZeroParseInteger Bool !Integer
| ErrorParseInteger
advanceParseInteger :: ParseInteger -> Char -> ParseInteger
advanceParseInteger :: ParseInteger -> Char -> ParseInteger
advanceParseInteger = ParseInteger -> Char -> ParseInteger
advance
where
advance :: ParseInteger -> Char -> ParseInteger
advance ParseInteger
StartParseInteger Char
'0' = ParseInteger
ZeroParseInteger
advance ParseInteger
StartParseInteger Char
'-' = ParseInteger
NegativeParseInteger
advance ParseInteger
StartParseInteger Char
d | Char -> Bool
Char.isDigit Char
d = Char -> ParseInteger
positive Char
d
advance ParseInteger
NegativeParseInteger Char
'0' = ParseInteger
ErrorParseInteger
advance ParseInteger
NegativeParseInteger Char
d | Char -> Bool
Char.isDigit Char
d = Char -> ParseInteger
negative Char
d
advance (NonZeroParseInteger Bool
s Integer
n) Char
d | Char -> Bool
Char.isDigit Char
d = Bool -> Integer -> Char -> ParseInteger
accumulate Bool
s Integer
n Char
d
advance ParseInteger
_ Char
_ = ParseInteger
ErrorParseInteger
positive :: Char -> ParseInteger
positive = Bool -> Integer -> ParseInteger
NonZeroParseInteger Bool
True (Integer -> ParseInteger)
-> (Char -> Integer) -> Char -> ParseInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Integer
charToInteger
negative :: Char -> ParseInteger
negative = Bool -> Integer -> ParseInteger
NonZeroParseInteger Bool
False (Integer -> ParseInteger)
-> (Char -> Integer) -> Char -> ParseInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Integer
charToInteger
accumulate :: Bool -> Integer -> Char -> ParseInteger
accumulate Bool
s Integer
n Char
d = Bool -> Integer -> ParseInteger
NonZeroParseInteger Bool
s (Integer
10 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Char -> Integer
charToInteger Char
d)
charToInteger :: Char -> Integer
charToInteger = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> (Char -> Int) -> Char -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
Char.digitToInt
endParseInteger :: ParseInteger -> Maybe Integer
endParseInteger :: ParseInteger -> Maybe Integer
endParseInteger ParseInteger
ZeroParseInteger = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
endParseInteger (NonZeroParseInteger Bool
s Integer
i) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (if Bool
s then Integer
i else (-Integer
i))
endParseInteger ParseInteger
_ = Maybe Integer
forall a. Maybe a
Nothing
type FoldlParseInteger a =
(ParseInteger -> Char -> ParseInteger) ->
ParseInteger -> a -> ParseInteger
parseInteger :: FoldlParseInteger a -> a -> Maybe Integer
parseInteger :: FoldlParseInteger a -> a -> Maybe Integer
parseInteger FoldlParseInteger a
f = ParseInteger -> Maybe Integer
endParseInteger (ParseInteger -> Maybe Integer)
-> (a -> ParseInteger) -> a -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FoldlParseInteger a
f ParseInteger -> Char -> ParseInteger
advanceParseInteger ParseInteger
StartParseInteger
instance Parsable Integer where
parser :: Parsec Text st Integer
parser = Parsec Text st Integer
forall st. Parsec Text st Integer
zero Parsec Text st Integer
-> Parsec Text st Integer -> Parsec Text st Integer
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parsec Text st Integer
forall st. Parsec Text st Integer
negative Parsec Text st Integer
-> Parsec Text st Integer -> Parsec Text st Integer
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parsec Text st Integer
forall st. Parsec Text st Integer
positive
where
zero :: ParsecT Text u Identity Integer
zero = do
Char
_ <- Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'0'
Integer -> ParsecT Text u Identity Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
0
negative :: ParsecT Text u Identity Integer
negative = do
Char
_ <- Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'-'
Integer
k <- ParsecT Text u Identity Integer
forall st. Parsec Text st Integer
positive
Integer -> ParsecT Text u Identity Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (-Integer
k)
positive :: ParsecT Text u Identity Integer
positive = do
Integer
h <- ParsecT Text u Identity Integer
forall st. Parsec Text st Integer
positiveDigit
[Integer]
t <- ParsecT Text u Identity Integer
-> ParsecT Text u Identity [Integer]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
Parsec.many ParsecT Text u Identity Integer
forall st. Parsec Text st Integer
digit
Integer -> ParsecT Text u Identity Integer
forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer -> Integer -> Integer) -> Integer -> [Integer] -> Integer
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\Integer
n Integer
d -> Integer
10 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d) Integer
h [Integer]
t)
digit :: ParsecT Text u Identity Integer
digit = ParsecT Text u Identity Integer
forall st. Parsec Text st Integer
zero ParsecT Text u Identity Integer
-> ParsecT Text u Identity Integer
-> ParsecT Text u Identity Integer
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT Text u Identity Integer
forall st. Parsec Text st Integer
positiveDigit
positiveDigit :: ParsecT Text u Identity Integer
positiveDigit = do
Char
d <- [Char] -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
Parsec.oneOf [Char]
"123456789"
Integer -> ParsecT Text u Identity Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Char -> Int
Char.digitToInt Char
d)
fromText :: Text -> Maybe Integer
fromText = FoldlParseInteger Text -> Text -> Maybe Integer
forall a. FoldlParseInteger a -> a -> Maybe Integer
parseInteger FoldlParseInteger Text
forall a. (a -> Char -> a) -> a -> Text -> a
Text.foldl'
fromString :: [Char] -> Maybe Integer
fromString = FoldlParseInteger [Char] -> [Char] -> Maybe Integer
forall a. FoldlParseInteger a -> a -> Maybe Integer
parseInteger FoldlParseInteger [Char]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl'
instance Parsable Name where
parser :: Parsec Text st Name
parser = do
Char
_ <- Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'"'
[[Char]]
cs <- ParsecT Text st Identity [[Char]]
forall u. ParsecT Text u Identity [[Char]]
components
Char
_ <- Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'"'
Name -> Parsec Text st Name
forall (m :: * -> *) a. Monad m => a -> m a
return (Namespace -> [Char] -> Name
Name ([[Char]] -> Namespace
Namespace ([[Char]] -> [[Char]]
forall a. [a] -> [a]
init [[Char]]
cs)) ([[Char]] -> [Char]
forall a. [a] -> a
last [[Char]]
cs))
where
components :: ParsecT Text u Identity [[Char]]
components = ParsecT Text u Identity [Char]
-> ParsecT Text u Identity Char -> ParsecT Text u Identity [[Char]]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
Parsec.sepBy1 ParsecT Text u Identity [Char]
forall u. ParsecT Text u Identity [Char]
component (Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'.')
component :: ParsecT Text u Identity [Char]
component = ParsecT Text u Identity Char -> ParsecT Text u Identity [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
Parsec.many ParsecT Text u Identity Char
forall u. ParsecT Text u Identity Char
char
char :: ParsecT Text u Identity Char
char = [Char] -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
Parsec.noneOf [Char]
escapable ParsecT Text u Identity Char
-> ParsecT Text u Identity Char -> ParsecT Text u Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT Text u Identity Char
forall u. ParsecT Text u Identity Char
escapedChar
escapedChar :: ParsecT Text u Identity Char
escapedChar = do
Char
_ <- Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'\\'
Char
c <- [Char] -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
Parsec.oneOf [Char]
escapable
Char -> ParsecT Text u Identity Char
forall (m :: * -> *) a. Monad m => a -> m a
return Char
c
escapable :: [Char]
escapable = [Char]
"\"\\."