{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
-- | This module implements a specialized s-expression parser
--
-- The parser in s-cargot is very general, but that also makes it a bit
-- inefficient.  This module implements a drop-in replacement parser for the one
-- in What4.Serialize.Parser using megaparsec.  It is completely specialized to
-- the types in this library.
module What4.Serialize.FastSExpr (
  parseSExpr
  ) where

import           Control.Applicative
import qualified Control.Monad.Fail as MF
import qualified Data.Parameterized.NatRepr as PN
import           Data.Parameterized.Some ( Some(..) )
import           Data.Ratio ( (%) )
import qualified Data.SCargot.Repr.WellFormed as SC
import qualified Data.Set as Set
import qualified Data.Text as T
import qualified LibBF as BF
import           Numeric.Natural ( Natural )
import qualified Text.Megaparsec as TM
import qualified Text.Megaparsec.Char as TMC
import qualified Text.Megaparsec.Char.Lexer as TMCL
import qualified What4.BaseTypes as WT
import qualified What4.Serialize.SETokens as WST

-- | Parse 'T.Text' into the well-formed s-expression type from s-cargot.
parseSExpr :: T.Text -> Either String (SC.WellFormedSExpr WST.Atom)
parseSExpr :: Text -> Either [Char] (WellFormedSExpr Atom)
parseSExpr Text
t =
  case Parsec What4ParseError Text (WellFormedSExpr Atom)
-> [Char]
-> Text
-> Either
     (ParseErrorBundle Text What4ParseError) (WellFormedSExpr Atom)
forall e s a.
Parsec e s a -> [Char] -> s -> Either (ParseErrorBundle s e) a
TM.runParser (Parser ()
ws Parser ()
-> Parsec What4ParseError Text (WellFormedSExpr Atom)
-> Parsec What4ParseError Text (WellFormedSExpr Atom)
forall a b.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity b
-> ParsecT What4ParseError Text Identity b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Parsec What4ParseError Text (WellFormedSExpr Atom)
parse) [Char]
"<input>" Text
t of
    Left ParseErrorBundle Text What4ParseError
errBundle -> [Char] -> Either [Char] (WellFormedSExpr Atom)
forall a b. a -> Either a b
Left (ParseErrorBundle Text What4ParseError -> [Char]
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> [Char]
TM.errorBundlePretty ParseErrorBundle Text What4ParseError
errBundle)
    Right WellFormedSExpr Atom
a -> WellFormedSExpr Atom -> Either [Char] (WellFormedSExpr Atom)
forall a b. b -> Either a b
Right WellFormedSExpr Atom
a

data What4ParseError = ErrorParsingHexFloat String
                     | InvalidExponentOrSignificandSize Natural Natural
  deriving (Int -> What4ParseError -> ShowS
[What4ParseError] -> ShowS
What4ParseError -> [Char]
(Int -> What4ParseError -> ShowS)
-> (What4ParseError -> [Char])
-> ([What4ParseError] -> ShowS)
-> Show What4ParseError
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> What4ParseError -> ShowS
showsPrec :: Int -> What4ParseError -> ShowS
$cshow :: What4ParseError -> [Char]
show :: What4ParseError -> [Char]
$cshowList :: [What4ParseError] -> ShowS
showList :: [What4ParseError] -> ShowS
Show, What4ParseError -> What4ParseError -> Bool
(What4ParseError -> What4ParseError -> Bool)
-> (What4ParseError -> What4ParseError -> Bool)
-> Eq What4ParseError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: What4ParseError -> What4ParseError -> Bool
== :: What4ParseError -> What4ParseError -> Bool
$c/= :: What4ParseError -> What4ParseError -> Bool
/= :: What4ParseError -> What4ParseError -> Bool
Eq, Eq What4ParseError
Eq What4ParseError =>
(What4ParseError -> What4ParseError -> Ordering)
-> (What4ParseError -> What4ParseError -> Bool)
-> (What4ParseError -> What4ParseError -> Bool)
-> (What4ParseError -> What4ParseError -> Bool)
-> (What4ParseError -> What4ParseError -> Bool)
-> (What4ParseError -> What4ParseError -> What4ParseError)
-> (What4ParseError -> What4ParseError -> What4ParseError)
-> Ord What4ParseError
What4ParseError -> What4ParseError -> Bool
What4ParseError -> What4ParseError -> Ordering
What4ParseError -> What4ParseError -> What4ParseError
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: What4ParseError -> What4ParseError -> Ordering
compare :: What4ParseError -> What4ParseError -> Ordering
$c< :: What4ParseError -> What4ParseError -> Bool
< :: What4ParseError -> What4ParseError -> Bool
$c<= :: What4ParseError -> What4ParseError -> Bool
<= :: What4ParseError -> What4ParseError -> Bool
$c> :: What4ParseError -> What4ParseError -> Bool
> :: What4ParseError -> What4ParseError -> Bool
$c>= :: What4ParseError -> What4ParseError -> Bool
>= :: What4ParseError -> What4ParseError -> Bool
$cmax :: What4ParseError -> What4ParseError -> What4ParseError
max :: What4ParseError -> What4ParseError -> What4ParseError
$cmin :: What4ParseError -> What4ParseError -> What4ParseError
min :: What4ParseError -> What4ParseError -> What4ParseError
Ord)

instance TM.ShowErrorComponent What4ParseError where
  showErrorComponent :: What4ParseError -> [Char]
showErrorComponent What4ParseError
e =
    case What4ParseError
e of
      ErrorParsingHexFloat [Char]
hf -> [Char]
"Error parsing hex float literal: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
hf
      InvalidExponentOrSignificandSize Natural
ex Natural
s ->
        [[Char]] -> [Char]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [ [Char]
"Invalid exponent or significand size: exponent size = "
               , Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
ex
               , [Char]
", significand size = "
               , Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
s
               ]

type Parser a = TM.Parsec What4ParseError T.Text a

parse :: Parser (SC.WellFormedSExpr WST.Atom)
parse :: Parsec What4ParseError Text (WellFormedSExpr Atom)
parse = Parsec What4ParseError Text (WellFormedSExpr Atom)
parseList Parsec What4ParseError Text (WellFormedSExpr Atom)
-> Parsec What4ParseError Text (WellFormedSExpr Atom)
-> Parsec What4ParseError Text (WellFormedSExpr Atom)
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (Atom -> WellFormedSExpr Atom
forall atom. atom -> WellFormedSExpr atom
SC.WFSAtom (Atom -> WellFormedSExpr Atom)
-> ParsecT What4ParseError Text Identity Atom
-> Parsec What4ParseError Text (WellFormedSExpr Atom)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a. Parser a -> Parser a
lexeme ParsecT What4ParseError Text Identity Atom
parseAtom)

parseList :: Parser (SC.WellFormedSExpr WST.Atom)
parseList :: Parsec What4ParseError Text (WellFormedSExpr Atom)
parseList = do
  Char
_ <- Parser Char -> Parser Char
forall a. Parser a -> Parser a
lexeme (Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
'(')
  [WellFormedSExpr Atom]
items <- Parsec What4ParseError Text (WellFormedSExpr Atom)
-> ParsecT What4ParseError Text Identity [WellFormedSExpr Atom]
forall (m :: Type -> Type) a. MonadPlus m => m a -> m [a]
TM.many Parsec What4ParseError Text (WellFormedSExpr Atom)
parse
  Char
_ <- Parser Char -> Parser Char
forall a. Parser a -> Parser a
lexeme (Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
')')
  WellFormedSExpr Atom
-> Parsec What4ParseError Text (WellFormedSExpr Atom)
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([WellFormedSExpr Atom] -> WellFormedSExpr Atom
forall atom. [WellFormedSExpr atom] -> WellFormedSExpr atom
SC.WFSList [WellFormedSExpr Atom]
items)

parseId :: Parser T.Text
parseId :: Parser Text
parseId = [Char] -> Text
T.pack ([Char] -> Text)
-> ParsecT What4ParseError Text Identity [Char] -> Parser Text
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((:) (Char -> ShowS)
-> Parser Char -> ParsecT What4ParseError Text Identity ShowS
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Char
first ParsecT What4ParseError Text Identity ShowS
-> ParsecT What4ParseError Text Identity [Char]
-> ParsecT What4ParseError Text Identity [Char]
forall a b.
ParsecT What4ParseError Text Identity (a -> b)
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Parser Char -> ParsecT What4ParseError Text Identity [Char]
forall (m :: Type -> Type) a. MonadPlus m => m a -> m [a]
TM.many Parser Char
rest)
  where
    w4symbol :: Char -> Bool
w4symbol Char
c =  Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'@'
               Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'+'
               Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'-'
               Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'='
               Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'<'
               Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'>'
               Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'
               Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.'
    first :: Parser Char
first = Parser Char
ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
TMC.letterChar Parser Char -> Parser Char -> Parser Char
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (Token Text -> Bool)
-> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
TM.satisfy Char -> Bool
Token Text -> Bool
w4symbol
    rest :: Parser Char
rest = Parser Char
ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
TMC.alphaNumChar Parser Char -> Parser Char -> Parser Char
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (Token Text -> Bool)
-> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
TM.satisfy Char -> Bool
Token Text -> Bool
w4symbol

parseNat :: Parser Natural
parseNat :: Parser Natural
parseNat = do
  Tokens Text
_ <- Tokens Text -> ParsecT What4ParseError Text Identity (Tokens Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
TMC.string Tokens Text
"#u"
  Parser Natural
forall e s (m :: Type -> Type) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
TMCL.decimal

parseInt :: Parser Integer
parseInt :: Parser Integer
parseInt = Parser Integer
forall e s (m :: Type -> Type) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
TMCL.decimal Parser Integer -> Parser Integer -> Parser Integer
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> Parser Integer -> Parser Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
'-' Parser Char -> Parser Integer -> Parser Integer
forall a b.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity b
-> ParsecT What4ParseError Text Identity b
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Integer
forall e s (m :: Type -> Type) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
TMCL.decimal))

parseReal :: Parser Rational
parseReal :: Parser Rational
parseReal = do
  Tokens Text
_ <- Tokens Text -> ParsecT What4ParseError Text Identity (Tokens Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
TMC.string Tokens Text
"#r"
  Integer
n <- Parser Integer
forall e s (m :: Type -> Type) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
TMCL.decimal
  Char
_ <- Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
'/'
  Integer
d <- Parser Integer
forall e s (m :: Type -> Type) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
TMCL.decimal
  Rational -> Parser Rational
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
d)

parseBV :: Parser (Int, Integer)
parseBV :: Parser (Int, Integer)
parseBV = do
  Char
_ <- Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
'#'
  Char
t <- Parser Char
ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type). MonadParsec e s m => m (Token s)
TM.anySingle
  case Char
t of
    Char
'b' -> Int -> Integer -> Parser (Int, Integer)
parseBin Int
0 Integer
0
    Char
'x' -> Parser (Int, Integer)
parseHex
    Char
_ -> [Char] -> Parser (Int, Integer)
forall a. [Char] -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
MF.fail ([Char]
"Invalid bitvector class: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> [Char]
forall a. Show a => a -> [Char]
show Char
t)
  where
    parseBin :: Int -> Integer -> Parser (Int, Integer)
    parseBin :: Int -> Integer -> Parser (Int, Integer)
parseBin !Int
nBits !Integer
value= do
      Maybe Char
mb <- Parser Char -> ParsecT What4ParseError Text Identity (Maybe Char)
forall (f :: Type -> Type) a. Alternative f => f a -> f (Maybe a)
TM.optional Parser Char
ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
TMC.binDigitChar
      case Maybe Char
mb of
        Maybe Char
Nothing -> (Int, Integer) -> Parser (Int, Integer)
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int
nBits, Integer
value)
        Just Char
bitChar -> Int -> Integer -> Parser (Int, Integer)
parseBin (Int
nBits Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Integer
value Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ if Char
bitChar Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'1' then Integer
1 else Integer
0)
    parseHex :: Parser (Int, Integer)
    parseHex :: Parser (Int, Integer)
parseHex = do
      [Char]
digits <- Parser Char -> ParsecT What4ParseError Text Identity [Char]
forall (m :: Type -> Type) a. MonadPlus m => m a -> m [a]
TM.some Parser Char
ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
TMC.hexDigitChar
      (Int, Integer) -> Parser (Int, Integer)
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([Char] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Char]
digits Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
4, [Char] -> Integer
forall a. Read a => [Char] -> a
read ([Char]
"0x" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
digits))

parseBool :: Parser Bool
parseBool :: Parser Bool
parseBool = do
  Char
_ <- Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
'#'
  Parser Bool -> Parser Bool
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try (Tokens Text -> ParsecT What4ParseError Text Identity (Tokens Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
TMC.string Tokens Text
"true" ParsecT What4ParseError Text Identity (Tokens Text)
-> Parser Bool -> Parser Bool
forall a b.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity b
-> ParsecT What4ParseError Text Identity b
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Bool -> Parser Bool
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
True) Parser Bool -> Parser Bool -> Parser Bool
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (Tokens Text -> ParsecT What4ParseError Text Identity (Tokens Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
TMC.string Tokens Text
"false" ParsecT What4ParseError Text Identity (Tokens Text)
-> Parser Bool -> Parser Bool
forall a b.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity b
-> ParsecT What4ParseError Text Identity b
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Bool -> Parser Bool
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
False)

parseStrInfo :: Parser (Some WT.StringInfoRepr)
parseStrInfo :: Parser (Some StringInfoRepr)
parseStrInfo = Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try (Tokens Text -> ParsecT What4ParseError Text Identity (Tokens Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
TMC.string Tokens Text
"#char16" ParsecT What4ParseError Text Identity (Tokens Text)
-> Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
forall a b.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity b
-> ParsecT What4ParseError Text Identity b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Some StringInfoRepr -> Parser (Some StringInfoRepr)
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (StringInfoRepr 'Char16 -> Some StringInfoRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some StringInfoRepr 'Char16
WT.Char16Repr))
           Parser (Some StringInfoRepr)
-> Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try (Tokens Text -> ParsecT What4ParseError Text Identity (Tokens Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
TMC.string Tokens Text
"#char8" ParsecT What4ParseError Text Identity (Tokens Text)
-> Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
forall a b.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity b
-> ParsecT What4ParseError Text Identity b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Some StringInfoRepr -> Parser (Some StringInfoRepr)
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (StringInfoRepr 'Char8 -> Some StringInfoRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some StringInfoRepr 'Char8
WT.Char8Repr))
           Parser (Some StringInfoRepr)
-> Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Some StringInfoRepr -> Parser (Some StringInfoRepr)
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (StringInfoRepr 'Unicode -> Some StringInfoRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some StringInfoRepr 'Unicode
WT.UnicodeRepr)

parseStr :: Parser (Some WT.StringInfoRepr, T.Text)
parseStr :: Parser (Some StringInfoRepr, Text)
parseStr = do
  Some StringInfoRepr
prefix <- Parser (Some StringInfoRepr)
parseStrInfo
  Char
_ <- Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
'"'
  [Char]
str <- [[Char]] -> [Char]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat ([[Char]] -> [Char])
-> ParsecT What4ParseError Text Identity [[Char]]
-> ParsecT What4ParseError Text Identity [Char]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT What4ParseError Text Identity [Char]
-> ParsecT What4ParseError Text Identity [[Char]]
forall (m :: Type -> Type) a. MonadPlus m => m a -> m [a]
TM.many (ParsecT What4ParseError Text Identity [Char]
parseEscaped ParsecT What4ParseError Text Identity [Char]
-> ParsecT What4ParseError Text Identity [Char]
-> ParsecT What4ParseError Text Identity [Char]
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser Char -> ParsecT What4ParseError Text Identity [Char]
forall (m :: Type -> Type) a. MonadPlus m => m a -> m [a]
TM.some ([Token Text] -> ParsecT What4ParseError Text Identity (Token Text)
forall (f :: Type -> Type) e s (m :: Type -> Type).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
TM.noneOf (Char
'"'Char -> ShowS
forall a. a -> [a] -> [a]
:[Char]
"\\")))
  Char
_ <- Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
'"'
  (Some StringInfoRepr, Text) -> Parser (Some StringInfoRepr, Text)
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some StringInfoRepr
prefix, [Char] -> Text
T.pack [Char]
str)
  where
    parseEscaped :: ParsecT What4ParseError Text Identity [Char]
parseEscaped = do
      Char
_ <- Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
'\\'
      Char
c <- Parser Char
ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type). MonadParsec e s m => m (Token s)
TM.anySingle
      [Char] -> ParsecT What4ParseError Text Identity [Char]
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [Char
'\\', Char
c]

parseFloat :: Parser (Some WT.FloatPrecisionRepr, BF.BigFloat)
parseFloat :: Parser (Some FloatPrecisionRepr, BigFloat)
parseFloat = do
  Tokens Text
_ <- Tokens Text -> ParsecT What4ParseError Text Identity (Tokens Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
TMC.string Tokens Text
"#f#"
  -- We printed the nat reprs out in decimal
  Natural
eb :: Natural
     <- Parser Natural
forall e s (m :: Type -> Type) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
TMCL.decimal
  Char
_ <- Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
'#'
  Natural
sb :: Natural
     <- Parser Natural
forall e s (m :: Type -> Type) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
TMCL.decimal
  Char
_ <- Token Text -> ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
TMC.char Char
Token Text
'#'

  -- The float value itself is printed out as a hex literal
  [Char]
hexDigits <- Parser Char -> ParsecT What4ParseError Text Identity [Char]
forall (m :: Type -> Type) a. MonadPlus m => m a -> m [a]
TM.some Parser Char
ParsecT What4ParseError Text Identity (Token Text)
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
TMC.hexDigitChar

  Some NatRepr x
ebRepr <- Some NatRepr
-> ParsecT What4ParseError Text Identity (Some NatRepr)
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Natural -> Some NatRepr
PN.mkNatRepr Natural
eb)
  Some NatRepr x
sbRepr <- Some NatRepr
-> ParsecT What4ParseError Text Identity (Some NatRepr)
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Natural -> Some NatRepr
PN.mkNatRepr Natural
sb)
  case (NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
PN.testLeq (forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat @2) NatRepr x
ebRepr, NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
PN.testLeq (forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat @2) NatRepr x
sbRepr) of
    (Just LeqProof 2 x
PN.LeqProof, Just LeqProof 2 x
PN.LeqProof) -> do
      let rep :: FloatPrecisionRepr ('FloatingPointPrecision x x)
rep = NatRepr x
-> NatRepr x -> FloatPrecisionRepr ('FloatingPointPrecision x x)
forall (eb :: Natural) (sb :: Natural).
(2 <= eb, 2 <= sb) =>
NatRepr eb
-> NatRepr sb -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
WT.FloatingPointPrecisionRepr NatRepr x
ebRepr NatRepr x
sbRepr

      -- We know our format: it is determined by the exponent bits (eb) and the
      -- significand bits (sb) parsed above
      let fmt :: BFOpts
fmt = Word -> BFOpts
BF.precBits (Natural -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
sb) BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> Int -> BFOpts
BF.expBits (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
eb)
      let (BigFloat
bf, Status
status) = Int -> BFOpts -> [Char] -> (BigFloat, Status)
BF.bfFromString Int
16 BFOpts
fmt [Char]
hexDigits
      case Status
status of
        Status
BF.Ok -> (Some FloatPrecisionRepr, BigFloat)
-> Parser (Some FloatPrecisionRepr, BigFloat)
forall a. a -> ParsecT What4ParseError Text Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (FloatPrecisionRepr ('FloatingPointPrecision x x)
-> Some FloatPrecisionRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some FloatPrecisionRepr ('FloatingPointPrecision x x)
rep, BigFloat
bf)
        Status
_ -> Set (ErrorFancy What4ParseError)
-> Parser (Some FloatPrecisionRepr, BigFloat)
forall e s (m :: Type -> Type) a.
MonadParsec e s m =>
Set (ErrorFancy e) -> m a
TM.fancyFailure (ErrorFancy What4ParseError -> Set (ErrorFancy What4ParseError)
forall a. a -> Set a
Set.singleton (What4ParseError -> ErrorFancy What4ParseError
forall e. e -> ErrorFancy e
TM.ErrorCustom ([Char] -> What4ParseError
ErrorParsingHexFloat [Char]
hexDigits)))
    (Maybe (LeqProof 2 x), Maybe (LeqProof 2 x))
_ -> Set (ErrorFancy What4ParseError)
-> Parser (Some FloatPrecisionRepr, BigFloat)
forall e s (m :: Type -> Type) a.
MonadParsec e s m =>
Set (ErrorFancy e) -> m a
TM.fancyFailure (ErrorFancy What4ParseError -> Set (ErrorFancy What4ParseError)
forall a. a -> Set a
Set.singleton (What4ParseError -> ErrorFancy What4ParseError
forall e. e -> ErrorFancy e
TM.ErrorCustom (Natural -> Natural -> What4ParseError
InvalidExponentOrSignificandSize Natural
eb Natural
sb)))


parseAtom :: Parser WST.Atom
parseAtom :: ParsecT What4ParseError Text Identity Atom
parseAtom = ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try ((Int -> Integer -> Atom) -> (Int, Integer) -> Atom
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Integer -> Atom
WST.ABV ((Int, Integer) -> Atom)
-> Parser (Int, Integer)
-> ParsecT What4ParseError Text Identity Atom
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Int, Integer)
parseBV)
        ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try (Bool -> Atom
WST.ABool (Bool -> Atom)
-> Parser Bool -> ParsecT What4ParseError Text Identity Atom
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Bool
parseBool)
        ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try (Integer -> Atom
WST.AInt (Integer -> Atom)
-> Parser Integer -> ParsecT What4ParseError Text Identity Atom
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
parseInt)
        ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try (Text -> Atom
WST.AId (Text -> Atom)
-> Parser Text -> ParsecT What4ParseError Text Identity Atom
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
parseId)
        ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try (Natural -> Atom
WST.ANat (Natural -> Atom)
-> Parser Natural -> ParsecT What4ParseError Text Identity Atom
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Natural
parseNat)
        ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try (Rational -> Atom
WST.AReal (Rational -> Atom)
-> Parser Rational -> ParsecT What4ParseError Text Identity Atom
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Rational
parseReal)
        ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try ((Some StringInfoRepr -> Text -> Atom)
-> (Some StringInfoRepr, Text) -> Atom
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Some StringInfoRepr -> Text -> Atom
WST.AStr ((Some StringInfoRepr, Text) -> Atom)
-> Parser (Some StringInfoRepr, Text)
-> ParsecT What4ParseError Text Identity Atom
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Some StringInfoRepr, Text)
parseStr)
        ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a.
ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> ParsecT What4ParseError Text Identity Atom
-> ParsecT What4ParseError Text Identity Atom
forall a. Parser a -> Parser a
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
TM.try ((Some FloatPrecisionRepr -> BigFloat -> Atom)
-> (Some FloatPrecisionRepr, BigFloat) -> Atom
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Some FloatPrecisionRepr -> BigFloat -> Atom
WST.AFloat ((Some FloatPrecisionRepr, BigFloat) -> Atom)
-> Parser (Some FloatPrecisionRepr, BigFloat)
-> ParsecT What4ParseError Text Identity Atom
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Some FloatPrecisionRepr, BigFloat)
parseFloat)

ws :: Parser ()
ws :: Parser ()
ws = Parser () -> Parser () -> Parser () -> Parser ()
forall e s (m :: Type -> Type).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
TMCL.space Parser ()
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
m ()
TMC.space1 (Tokens Text -> Parser ()
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> m ()
TMCL.skipLineComment ([Char] -> Text
T.pack [Char]
";")) Parser ()
forall a. ParsecT What4ParseError Text Identity a
forall (f :: Type -> Type) a. Alternative f => f a
empty

lexeme :: Parser a -> Parser a
lexeme :: forall a. Parser a -> Parser a
lexeme = Parser ()
-> ParsecT What4ParseError Text Identity a
-> ParsecT What4ParseError Text Identity a
forall e s (m :: Type -> Type) a.
MonadParsec e s m =>
m () -> m a -> m a
TMCL.lexeme Parser ()
ws