    {-# 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
      _ <- 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
    '(')
      items <- TM.many parse
      _ <- lexeme (TMC.char ')')
      return (SC.WFSList 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 -> 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"
      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 -> 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"
      n <- TMCL.decimal
      _ <- TMC.char '/'
      d <- TMCL.decimal
      return (n % d)

    parseBV :: Parser (Int, Integer)
    parseBV :: Parser (Int, Integer)
    parseBV = do
      _ <- 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
    '#'
      t <- TM.anySingle
      case 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
          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 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
          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
          return (length digits * 4, read ("0x" ++ digits))

    parseBool :: Parser Bool
    parseBool :: Parser Bool
    parseBool = do
      _ <- 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
    '#'
      TM.try (TMC.string "true" *> return True) <|> (TMC.string "false" *> return 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
      prefix <- Parser (Some StringInfoRepr)
    parseStrInfo
      _ <- TMC.char '"'
      str <- concat <$> TM.many (parseEscaped <|> TM.some (TM.noneOf ('"':"\\")))
      _ <- TMC.char '"'
      return (prefix, T.pack str)
      where
        parseEscaped :: ParsecT What4ParseError Text Identity [Char]
    parseEscaped = do
          _ <- 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
    '\\'
          c <- TM.anySingle
          return ['\\', c]

    parseFloat :: Parser (Some WT.FloatPrecisionRepr, BF.BigFloat)
    parseFloat :: Parser (Some FloatPrecisionRepr, BigFloat)
    parseFloat = do
      _ <- 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
      eb :: Natural
         <- TMCL.decimal
      _ <- TMC.char '#'
      sb :: Natural
         <- TMCL.decimal
      _ <- TMC.char '#'

      -- The float value itself is printed out as a hex literal
      hexDigits <- TM.some TMC.hexDigitChar

      Some ebRepr <- return (PN.mkNatRepr eb)
      Some sbRepr <- return (PN.mkNatRepr sb)
      case (PN.testLeq (PN.knownNat @2) ebRepr, PN.testLeq (PN.knownNat @2) 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