{- |
module: $Header$
description: Parsing
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

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

-------------------------------------------------------------------------------
-- Parsing whitespace
-------------------------------------------------------------------------------

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"

-------------------------------------------------------------------------------
-- Parsable types
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Integers
-------------------------------------------------------------------------------

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'

-------------------------------------------------------------------------------
-- Names
-------------------------------------------------------------------------------

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]
"\"\\."