    -- | Definition of the S-Expression tokens used to
    -- (de)serialize What4 expressions.

    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}

    module What4.Serialize.SETokens
        ( Atom(..)
        , string, ident, int, nat, bitvec, bool, real, float
        , string', ident'
        , printAtom
        , printSExpr
        , parseSExpr
        )
        where

    import qualified Data.Foldable as F
    import qualified Data.Parameterized.NatRepr as PN
    import qualified Data.SCargot as SC
    import qualified Data.SCargot.Comments as SC
    import qualified Data.SCargot.Repr as SC
    import qualified Data.SCargot.Repr.WellFormed as SC
    import           Data.Semigroup
    import qualified Data.Sequence as Seq
    import           Data.Text (Text)
    import qualified Data.Text as T
    import qualified LibBF as BF
    import           Numeric.Natural ( Natural )
    import qualified Text.Parsec as P
    import           Text.Parsec.Text ( Parser )
    import           Text.Printf ( printf )
    import           Data.Ratio

    import           Data.Parameterized.Some ( Some(..))
    import qualified What4.BaseTypes as W4

    import           Prelude

    data Atom =
      AId Text
      -- ^ An identifier.
      | AStr (Some W4.StringInfoRepr) Text
      -- ^ A prefix followed by a string literal
      -- (.e.g, AStr "u" "Hello World" is serialize as `#u"Hello World"`).
      | AInt Integer
      -- ^ Integer (i.e., unbounded) literal.
      | ANat Natural
      -- ^ Natural (i.e., unbounded) literal
      | AReal Rational
      -- ^ Real (i.e., unbounded) literal.
      | AFloat (Some W4.FloatPrecisionRepr) BF.BigFloat
      -- ^ A floating point literal (with precision)
      | ABV Int Integer
      -- ^ Bitvector, width and then value.
      | ABool Bool
      -- ^ Boolean literal.
      deriving (Int -> Atom -> ShowS
    [Atom] -> ShowS
    Atom -> [Char]
    (Int -> Atom -> ShowS)
    -> (Atom -> [Char]) -> ([Atom] -> ShowS) -> Show Atom
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Atom -> ShowS
    showsPrec :: Int -> Atom -> ShowS
    $cshow :: Atom -> [Char]
    show :: Atom -> [Char]
    $cshowList :: [Atom] -> ShowS
    showList :: [Atom] -> ShowS
    Show, Atom -> Atom -> Bool
    (Atom -> Atom -> Bool) -> (Atom -> Atom -> Bool) -> Eq Atom
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Atom -> Atom -> Bool
    == :: Atom -> Atom -> Bool
    $c/= :: Atom -> Atom -> Bool
    /= :: Atom -> Atom -> Bool
    Eq, Eq Atom
    Eq Atom =>
    (Atom -> Atom -> Ordering)
    -> (Atom -> Atom -> Bool)
    -> (Atom -> Atom -> Bool)
    -> (Atom -> Atom -> Bool)
    -> (Atom -> Atom -> Bool)
    -> (Atom -> Atom -> Atom)
    -> (Atom -> Atom -> Atom)
    -> Ord Atom
    Atom -> Atom -> Bool
    Atom -> Atom -> Ordering
    Atom -> Atom -> Atom
    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 :: Atom -> Atom -> Ordering
    compare :: Atom -> Atom -> Ordering
    $c< :: Atom -> Atom -> Bool
    < :: Atom -> Atom -> Bool
    $c<= :: Atom -> Atom -> Bool
    <= :: Atom -> Atom -> Bool
    $c> :: Atom -> Atom -> Bool
    > :: Atom -> Atom -> Bool
    $c>= :: Atom -> Atom -> Bool
    >= :: Atom -> Atom -> Bool
    $cmax :: Atom -> Atom -> Atom
    max :: Atom -> Atom -> Atom
    $cmin :: Atom -> Atom -> Atom
    min :: Atom -> Atom -> Atom
    Ord)

    type SExpr = SC.WellFormedSExpr Atom

    string :: Some W4.StringInfoRepr -> Text -> SExpr
    string :: Some StringInfoRepr -> Text -> SExpr
    string Some StringInfoRepr
    strInfo Text
    str = Atom -> SExpr
    forall t. t -> WellFormedSExpr t
    SC.A (Atom -> SExpr) -> Atom -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Some StringInfoRepr -> Text -> Atom
    AStr Some StringInfoRepr
    strInfo Text
    str

    string' :: Some W4.StringInfoRepr -> String -> SExpr
    string' :: Some StringInfoRepr -> [Char] -> SExpr
    string' Some StringInfoRepr
    strInfo [Char]
    str = Atom -> SExpr
    forall t. t -> WellFormedSExpr t
    SC.A (Atom -> SExpr) -> Atom -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Some StringInfoRepr -> Text -> Atom
    AStr Some StringInfoRepr
    strInfo ([Char] -> Text
    T.pack [Char]
    str)

    -- | Lift an unquoted identifier.
    ident :: Text -> SExpr
    ident :: Text -> SExpr
    ident = Atom -> SExpr
    forall t. t -> WellFormedSExpr t
    SC.A (Atom -> SExpr) -> (Text -> Atom) -> Text -> SExpr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Atom
    AId

    ident' :: String -> SExpr
    ident' :: [Char] -> SExpr
    ident' = Atom -> SExpr
    forall t. t -> WellFormedSExpr t
    SC.A (Atom -> SExpr) -> ([Char] -> Atom) -> [Char] -> SExpr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Atom
    AId (Text -> Atom) -> ([Char] -> Text) -> [Char] -> Atom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Text
    T.pack

    -- | Lift an integer.
    int :: Integer -> SExpr
    int :: Integer -> SExpr
    int = Atom -> SExpr
    forall t. t -> WellFormedSExpr t
    SC.A (Atom -> SExpr) -> (Integer -> Atom) -> Integer -> SExpr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Atom
    AInt

    -- | Lift a natural
    nat :: Natural -> SExpr
    nat :: Natural -> SExpr
    nat = Atom -> SExpr
    forall t. t -> WellFormedSExpr t
    SC.A (Atom -> SExpr) -> (Natural -> Atom) -> Natural -> SExpr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Natural -> Atom
    ANat

    -- | Lift a real
    real :: Rational -> SExpr
    real :: Rational -> SExpr
    real = Atom -> SExpr
    forall t. t -> WellFormedSExpr t
    SC.A (Atom -> SExpr) -> (Rational -> Atom) -> Rational -> SExpr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rational -> Atom
    AReal

    -- | Lift a float
    float :: W4.FloatPrecisionRepr fpp -> BF.BigFloat -> SExpr
    float :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> BigFloat -> SExpr
    float FloatPrecisionRepr fpp
    rep BigFloat
    bf = Atom -> SExpr
    forall t. t -> WellFormedSExpr t
    SC.A (Some FloatPrecisionRepr -> BigFloat -> Atom
    AFloat (FloatPrecisionRepr fpp -> Some FloatPrecisionRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some FloatPrecisionRepr fpp
    rep) BigFloat
    bf)

    -- | Lift a bitvector.
    bitvec :: Natural -> Integer -> SExpr
    bitvec :: Natural -> Integer -> SExpr
    bitvec Natural
    w Integer
    v = Atom -> SExpr
    forall t. t -> WellFormedSExpr t
    SC.A (Atom -> SExpr) -> Atom -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer -> Atom
    ABV (Natural -> Int
    forall a. Enum a => a -> Int
    fromEnum Natural
    w) Integer
    v

    -- | Lift a boolean.
    bool :: Bool -> SExpr
    bool :: Bool -> SExpr
    bool = Atom -> SExpr
    forall t. t -> WellFormedSExpr t
    SC.A (Atom -> SExpr) -> (Bool -> Atom) -> Bool -> SExpr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Atom
    ABool

    -- * Output of the S-Expression Formula language

    -- | Generates the the S-expression tokens represented by the sexpr
    -- argument, preceeded by a list of strings output as comments.
    printSExpr :: Seq.Seq String -> SExpr -> T.Text
    printSExpr :: Seq [Char] -> SExpr -> Text
    printSExpr Seq [Char]
    comments SExpr
    sexpr =
      let outputFmt :: SExprPrinter Atom (SExpr Atom)
    outputFmt = Int
    -> SExprPrinter Atom (SExpr Atom) -> SExprPrinter Atom (SExpr Atom)
    forall atom carrier.
    Int -> SExprPrinter atom carrier -> SExprPrinter atom carrier
    SC.setIndentAmount Int
    1 (SExprPrinter Atom (SExpr Atom) -> SExprPrinter Atom (SExpr Atom))
    -> SExprPrinter Atom (SExpr Atom) -> SExprPrinter Atom (SExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ (Atom -> Text) -> SExprPrinter Atom (SExpr Atom)
    forall atom. (atom -> Text) -> SExprPrinter atom (SExpr atom)
    SC.unconstrainedPrint Atom -> Text
    printAtom
      in Seq [Char] -> Text
    formatComment Seq [Char]
    comments Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> (SExprPrinter Atom (SExpr Atom) -> SExpr Atom -> Text
    forall atom carrier. SExprPrinter atom carrier -> carrier -> Text
    SC.encodeOne SExprPrinter Atom (SExpr Atom)
    outputFmt (SExpr Atom -> Text) -> SExpr Atom -> Text
    forall a b. (a -> b) -> a -> b
    $ SExpr -> SExpr Atom
    forall atom. WellFormedSExpr atom -> SExpr atom
    SC.fromWellFormed SExpr
    sexpr)

    formatComment :: Seq.Seq String -> T.Text
    formatComment :: Seq [Char] -> Text
    formatComment Seq [Char]
    c
      | Seq [Char] -> Bool
    forall a. Seq a -> Bool
    Seq.null Seq [Char]
    c = Text
    T.empty
      | Bool
    otherwise = [Char] -> Text
    T.pack ([Char] -> Text) -> [Char] -> Text
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ ShowS -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap ShowS
    forall {t} {t}. (PrintfArg t, PrintfType t) => t -> t
    formatLine (Seq [Char] -> [[Char]]
    forall a. Seq a -> [a]
    forall (t :: Type -> Type) a. Foldable t => t a -> [a]
    F.toList Seq [Char]
    c)
      where
        formatLine :: t -> t
    formatLine t
    l = [Char] -> t -> t
    forall r. PrintfType r => [Char] -> r
    printf [Char]
    ";; %s" t
    l

    printAtom :: Atom -> T.Text
    printAtom :: Atom -> Text
    printAtom Atom
    a =
      case Atom
    a of
        AId Text
    s -> Text
    s
        AStr Some StringInfoRepr
    si Text
    s -> (Some StringInfoRepr -> Text
    stringInfoToPrefix Some StringInfoRepr
    si)Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>Text
    "\""Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>Text
    sText -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>Text
    "\""
        AInt Integer
    i -> [Char] -> Text
    T.pack (Integer -> [Char]
    forall a. Show a => a -> [Char]
    show Integer
    i)
        ANat Natural
    n -> [Char] -> Text
    T.pack ([Char] -> Text) -> [Char] -> Text
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "#u"[Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++(Natural -> [Char]
    forall a. Show a => a -> [Char]
    show Natural
    n)
        AReal Rational
    r -> [Char] -> Text
    T.pack ([Char] -> Text) -> [Char] -> Text
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "#r"[Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++(Integer -> [Char]
    forall a. Show a => a -> [Char]
    show (Rational -> Integer
    forall a. Ratio a -> a
    numerator Rational
    r))[Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++[Char]
    "/"[Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++(Integer -> [Char]
    forall a. Show a => a -> [Char]
    show (Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    r))
        ABV Int
    w Integer
    val -> Int -> Integer -> Text
    formatBV Int
    w Integer
    val
        ABool Bool
    b -> if Bool
    b then Text
    "#true" else Text
    "#false"
        AFloat (Some FloatPrecisionRepr x
    rep) BigFloat
    bf -> FloatPrecisionRepr x -> BigFloat -> Text
    forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> BigFloat -> Text
    formatFloat FloatPrecisionRepr x
    rep BigFloat
    bf

    -- | Format a floating point value with no rounding in base 16
    formatFloat :: W4.FloatPrecisionRepr fpp -> BF.BigFloat -> T.Text
    formatFloat :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> BigFloat -> Text
    formatFloat (W4.FloatingPointPrecisionRepr NatRepr eb
    eb NatRepr sb
    sb) BigFloat
    bf =
      [Char] -> Text
    T.pack ([Char] -> [Char] -> [Char] -> ShowS
    forall r. PrintfType r => [Char] -> r
    printf [Char]
    "#f#%s#%s#%s" (NatRepr eb -> [Char]
    forall a. Show a => a -> [Char]
    show NatRepr eb
    eb) (NatRepr sb -> [Char]
    forall a. Show a => a -> [Char]
    show NatRepr sb
    sb) (Int -> ShowFmt -> BigFloat -> [Char]
    BF.bfToString Int
    16 (Maybe Word -> ShowFmt
    BF.showFree Maybe Word
    forall a. Maybe a
    Nothing) BigFloat
    bf))

    formatBV :: Int -> Integer -> T.Text
    formatBV :: Int -> Integer -> Text
    formatBV Int
    w Integer
    val = [Char] -> Text
    T.pack ([Char]
    prefix [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> Integer -> [Char]
    forall r. PrintfType r => [Char] -> r
    printf [Char]
    fmt Integer
    val)
      where
        ([Char]
    prefix, [Char]
    fmt)
          | Int
    w Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `rem` Int
    4 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = ([Char]
    "#x", [Char]
    "%0" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show (Int
    w Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `div` Int
    4) [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "x")
          | Bool
    otherwise = ([Char]
    "#b", [Char]
    "%0" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    w [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "b")

    -- * Input and parse of the S-Expression Formula language

    -- | This is only the base-level parsing of atoms.  The full language
    -- parsing is handled by the base here and the Parser definitions.

    parseId :: Parser Text
    parseId :: Parser Text
    parseId = [Char] -> Text
    T.pack ([Char] -> Text) -> ParsecT Text () Identity [Char] -> Parser Text
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((:) (Char -> ShowS)
    -> ParsecT Text () Identity Char -> ParsecT Text () Identity ShowS
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ParsecT Text () Identity Char
    forall {u}. ParsecT Text u Identity Char
    first ParsecT Text () Identity ShowS
    -> ParsecT Text () Identity [Char]
    -> ParsecT Text () Identity [Char]
    forall a b.
    ParsecT Text () Identity (a -> b)
    -> ParsecT Text () Identity a -> ParsecT Text () Identity b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ParsecT Text () Identity Char -> ParsecT Text () Identity [Char]
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m [a]
    P.many ParsecT Text () Identity Char
    forall {u}. ParsecT Text u Identity Char
    rest)
      where first :: ParsecT Text u Identity Char
    first = ParsecT Text u Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.letter ParsecT Text u Identity Char
    -> ParsecT Text u Identity Char -> ParsecT Text u Identity Char
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    P.<|> [Char] -> ParsecT Text u Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m Char
    P.oneOf [Char]
    "@+-=<>_."
            rest :: ParsecT Text u Identity Char
    rest = ParsecT Text u Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.letter ParsecT Text u Identity Char
    -> ParsecT Text u Identity Char -> ParsecT Text u Identity Char
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    P.<|> ParsecT Text u Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.digit ParsecT Text u Identity Char
    -> ParsecT Text u Identity Char -> ParsecT Text u Identity Char
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    P.<|> [Char] -> ParsecT Text u Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m Char
    P.oneOf [Char]
    "+-=<>_."

    stringInfoToPrefix :: Some W4.StringInfoRepr -> Text
    stringInfoToPrefix :: Some StringInfoRepr -> Text
    stringInfoToPrefix (Some StringInfoRepr x
    W4.Char16Repr) = Text
    "#char16"
    stringInfoToPrefix (Some StringInfoRepr x
    W4.Char8Repr) = Text
    "#char8"
    stringInfoToPrefix (Some StringInfoRepr x
    W4.UnicodeRepr) = Text
    ""

    parseStrInfo :: Parser (Some W4.StringInfoRepr)
    parseStrInfo :: Parser (Some StringInfoRepr)
    parseStrInfo =
      Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a
    P.try ([Char] -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m [Char]
    P.string [Char]
    "#char16" ParsecT Text () Identity [Char]
    -> Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
    forall a b.
    ParsecT Text () Identity a
    -> ParsecT Text () Identity b -> ParsecT 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 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
    W4.Char16Repr))
      Parser (Some StringInfoRepr)
    -> Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    P.<|> Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a
    P.try ([Char] -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m [Char]
    P.string [Char]
    "#char8" ParsecT Text () Identity [Char]
    -> Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
    forall a b.
    ParsecT Text () Identity a
    -> ParsecT Text () Identity b -> ParsecT 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 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
    W4.Char8Repr))
      Parser (Some StringInfoRepr)
    -> Parser (Some StringInfoRepr) -> Parser (Some StringInfoRepr)
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    P.<|> (Some StringInfoRepr -> Parser (Some StringInfoRepr)
    forall a. a -> ParsecT 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
    W4.UnicodeRepr))

    parseStr :: Parser (Some W4.StringInfoRepr, Text)
    parseStr :: Parser (Some StringInfoRepr, Text)
    parseStr = do
      Some StringInfoRepr
    prefix <- Parser (Some StringInfoRepr)
    parseStrInfo
      Char
    _ <- Char -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    P.char Char
    '"'
      [Char]
    str <- [[Char]] -> [Char]
    forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
    concat ([[Char]] -> [Char])
    -> ParsecT Text () Identity [[Char]]
    -> ParsecT Text () Identity [Char]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ParsecT Text () Identity [Char]
    -> ParsecT Text () Identity [[Char]]
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m [a]
    P.many ( do { Char
    _ <- Char -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    P.char Char
    '\\'; Char
    c <- ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.anyChar ; [Char] -> ParsecT Text () Identity [Char]
    forall a. a -> ParsecT Text () Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return [Char
    '\\',Char
    c]} ParsecT Text () Identity [Char]
    -> ParsecT Text () Identity [Char]
    -> ParsecT Text () Identity [Char]
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    P.<|> ParsecT Text () Identity Char -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m [a]
    P.many1 ([Char] -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m Char
    P.noneOf (Char
    '"'Char -> ShowS
    forall a. a -> [a] -> [a]
    :[Char]
    "\\")))
      Char
    _ <- Char -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    P.char Char
    '"'
      (Some StringInfoRepr, Text) -> Parser (Some StringInfoRepr, Text)
    forall a. a -> ParsecT Text () Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((Some StringInfoRepr, Text) -> Parser (Some StringInfoRepr, Text))
    -> (Some StringInfoRepr, Text)
    -> Parser (Some StringInfoRepr, Text)
    forall a b. (a -> b) -> a -> b
    $ (Some StringInfoRepr
    prefix, [Char] -> Text
    T.pack [Char]
    str)

    parseReal :: Parser Rational
    parseReal :: Parser Rational
    parseReal = do
      [Char]
    _ <- [Char] -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m [Char]
    P.string [Char]
    "#r"
      Integer
    n <- ([Char] -> Integer
    forall a. Read a => [Char] -> a
    read :: (String -> Integer)) ([Char] -> Integer)
    -> ParsecT Text () Identity [Char]
    -> ParsecT Text () Identity Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ParsecT Text () Identity Char -> ParsecT Text () Identity [Char]
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m [a]
    P.many ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.digit
      Char
    _ <- Char -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    P.char Char
    '/'
      Integer
    d <- ([Char] -> Integer
    forall a. Read a => [Char] -> a
    read :: (String -> Integer)) ([Char] -> Integer)
    -> ParsecT Text () Identity [Char]
    -> ParsecT Text () Identity Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ParsecT Text () Identity Char -> ParsecT Text () Identity [Char]
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m [a]
    P.many ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.digit
      Rational -> Parser Rational
    forall a. a -> ParsecT Text () Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Rational -> Parser Rational) -> Rational -> Parser Rational
    forall a b. (a -> b) -> a -> b
    $ Integer
    n Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    d

    parseInt :: Parser Integer
    parseInt :: ParsecT Text () Identity Integer
    parseInt = do
      ([Char] -> Integer
    forall a. Read a => [Char] -> a
    read ([Char] -> Integer)
    -> ParsecT Text () Identity [Char]
    -> ParsecT Text () Identity Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ParsecT Text () Identity Char -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m [a]
    P.many1 ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.digit)
      ParsecT Text () Identity Integer
    -> ParsecT Text () Identity Integer
    -> ParsecT Text () Identity Integer
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    P.<|> (Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *(-Integer
    1)) (Integer -> Integer) -> ([Char] -> Integer) -> [Char] -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Integer
    forall a. Read a => [Char] -> a
    read ([Char] -> Integer)
    -> ParsecT Text () Identity [Char]
    -> ParsecT Text () Identity Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Char -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    P.char Char
    '-' ParsecT Text () Identity Char
    -> ParsecT Text () Identity [Char]
    -> ParsecT Text () Identity [Char]
    forall a b.
    ParsecT Text () Identity a
    -> ParsecT Text () Identity b -> ParsecT Text () Identity b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> ParsecT Text () Identity Char -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m [a]
    P.many1 ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.digit)

    parseNat :: Parser Natural
    parseNat :: Parser Natural
    parseNat = do
      [Char]
    _ <- [Char] -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m [Char]
    P.string [Char]
    "#u"
      [Char]
    n <- ParsecT Text () Identity Char -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m [a]
    P.many1 ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.digit
      Natural -> Parser Natural
    forall a. a -> ParsecT Text () Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Natural -> Parser Natural) -> Natural -> Parser Natural
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Natural
    forall a. Read a => [Char] -> a
    read [Char]
    n

    parseBool :: Parser Bool
    parseBool :: Parser Bool
    parseBool = do
      (Parser Bool -> Parser Bool
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a
    P.try ([Char] -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m [Char]
    P.string [Char]
    "#false" ParsecT Text () Identity [Char] -> Parser Bool -> Parser Bool
    forall a b.
    ParsecT Text () Identity a
    -> ParsecT Text () Identity b -> ParsecT Text () Identity b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Bool -> Parser Bool
    forall a. a -> ParsecT Text () Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Bool
    False))
      Parser Bool -> Parser Bool -> Parser Bool
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    P.<|> ([Char] -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m [Char]
    P.string [Char]
    "#true" ParsecT Text () Identity [Char] -> Parser Bool -> Parser Bool
    forall a b.
    ParsecT Text () Identity a
    -> ParsecT Text () Identity b -> ParsecT Text () Identity b
    forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
    *> Bool -> Parser Bool
    forall a. a -> ParsecT Text () Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Bool
    True)

    parseBV :: Parser (Int, Integer)
    parseBV :: Parser (Int, Integer)
    parseBV = Char -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    P.char Char
    '#' ParsecT Text () Identity Char
    -> Parser (Int, Integer) -> Parser (Int, Integer)
    forall a b.
    ParsecT Text () Identity a
    -> ParsecT Text () Identity b -> ParsecT Text () Identity b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> ((Char -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    P.char Char
    'b' ParsecT Text () Identity Char
    -> Parser (Int, Integer) -> Parser (Int, Integer)
    forall a b.
    ParsecT Text () Identity a
    -> ParsecT Text () Identity b -> ParsecT Text () Identity b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Parser (Int, Integer)
    parseBin) Parser (Int, Integer)
    -> Parser (Int, Integer) -> Parser (Int, Integer)
    forall s u (m :: Type -> Type) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    P.<|> (Char -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    P.char Char
    'x' ParsecT Text () Identity Char
    -> Parser (Int, Integer) -> Parser (Int, Integer)
    forall a b.
    ParsecT Text () Identity a
    -> ParsecT Text () Identity b -> ParsecT Text () Identity b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Parser (Int, Integer)
    forall {u}. ParsecT Text u Identity (Int, Integer)
    parseHex))
      where parseBin :: Parser (Int, Integer)
    parseBin = [Char] -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m Char
    P.oneOf [Char]
    "10" ParsecT Text () Identity Char
    -> (Char -> Parser (Int, Integer)) -> Parser (Int, Integer)
    forall a b.
    ParsecT Text () Identity a
    -> (a -> ParsecT Text () Identity b) -> ParsecT Text () Identity b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \Char
    d -> (Int, Integer) -> Parser (Int, Integer)
    parseBin' (Int
    1, if Char
    d Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '1' then Integer
    1 else Integer
    0)

            parseBin' :: (Int, Integer) -> Parser (Int, Integer)
            parseBin' :: (Int, Integer) -> Parser (Int, Integer)
    parseBin' (Int
    bits, Integer
    x) = do
              ParsecT Text () Identity Char
    -> ParsecT Text () Identity (Maybe Char)
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m (Maybe a)
    P.optionMaybe ([Char] -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m Char
    P.oneOf [Char]
    "10") ParsecT Text () Identity (Maybe Char)
    -> (Maybe Char -> Parser (Int, Integer)) -> Parser (Int, Integer)
    forall a b.
    ParsecT Text () Identity a
    -> (a -> ParsecT Text () Identity b) -> ParsecT Text () Identity b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                Just Char
    d -> (Int, Integer) -> Parser (Int, Integer)
    parseBin' (Int
    bits Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1, Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    2 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + (if Char
    d Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '1' then Integer
    1 else Integer
    0))
                Maybe Char
    Nothing -> (Int, Integer) -> Parser (Int, Integer)
    forall a. a -> ParsecT Text () Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Int
    bits, Integer
    x)

            parseHex :: ParsecT Text u Identity (Int, Integer)
    parseHex = (\[Char]
    s -> ([Char] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [Char]
    s 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]
    s))) ([Char] -> (Int, Integer))
    -> ParsecT Text u Identity [Char]
    -> ParsecT Text u Identity (Int, Integer)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ParsecT Text u Identity Char -> ParsecT Text u Identity [Char]
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m [a]
    P.many1 ParsecT Text u Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.hexDigit

    parseFloat :: Parser (Some W4.FloatPrecisionRepr, BF.BigFloat)
    parseFloat :: Parser (Some FloatPrecisionRepr, BigFloat)
    parseFloat = do
      [Char]
    _ <- [Char] -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m [Char]
    P.string [Char]
    "#f#"
      -- We printed the nat reprs out in decimal
      Natural
    eb :: Natural
         <- [Char] -> Natural
    forall a. Read a => [Char] -> a
    read ([Char] -> Natural)
    -> ParsecT Text () Identity [Char] -> Parser Natural
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ParsecT Text () Identity Char -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m [a]
    P.many1 ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.digit
      Char
    _ <- Char -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    P.char Char
    '#'
      Natural
    sb :: Natural
         <- [Char] -> Natural
    forall a. Read a => [Char] -> a
    read ([Char] -> Natural)
    -> ParsecT Text () Identity [Char] -> Parser Natural
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ParsecT Text () Identity Char -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m [a]
    P.many1 ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.digit
      Char
    _ <- Char -> ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    P.char Char
    '#'

      -- The float value itself is printed out as a hex literal
      [Char]
    hexDigits <- ParsecT Text () Identity Char -> ParsecT Text () Identity [Char]
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m [a]
    P.many1 ParsecT Text () Identity Char
    forall s (m :: Type -> Type) u.
    Stream s m Char =>
    ParsecT s u m Char
    P.hexDigit

      Some NatRepr x
    ebRepr <- Some NatRepr -> ParsecT Text () Identity (Some NatRepr)
    forall a. a -> ParsecT 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 Text () Identity (Some NatRepr)
    forall a. a -> ParsecT 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)
    W4.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 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
    _ -> [Char] -> Parser (Some FloatPrecisionRepr, BigFloat)
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    [Char] -> ParsecT s u m a
    P.unexpected ([Char]
    "Error parsing hex float: 0x" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    hexDigits)
        (Maybe (LeqProof 2 x), Maybe (LeqProof 2 x))
    _ -> [Char] -> Parser (Some FloatPrecisionRepr, BigFloat)
    forall s (m :: Type -> Type) t u a.
    Stream s m t =>
    [Char] -> ParsecT s u m a
    P.unexpected ([Char]
    "Invalid exponent or significand size: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Natural, Natural) -> [Char]
    forall a. Show a => a -> [Char]
    show (Natural
    eb, Natural
    sb))

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

    parseSExpr :: T.Text -> Either String SExpr
    parseSExpr :: Text -> Either [Char] SExpr
    parseSExpr = SExprParser Atom SExpr -> Text -> Either [Char] SExpr
    forall atom carrier.
    SExprParser atom carrier -> Text -> Either [Char] carrier
    SC.decodeOne (SExprParser Atom SExpr -> Text -> Either [Char] SExpr)
    -> SExprParser Atom SExpr -> Text -> Either [Char] SExpr
    forall a b. (a -> b) -> a -> b
    $ SExprParser Atom (SExpr Atom) -> SExprParser Atom SExpr
    forall a b.
    SExprParser a (SExpr b) -> SExprParser a (WellFormedSExpr b)
    SC.asWellFormed (SExprParser Atom (SExpr Atom) -> SExprParser Atom SExpr)
    -> SExprParser Atom (SExpr Atom) -> SExprParser Atom SExpr
    forall a b. (a -> b) -> a -> b
    $ SExprParser Atom (SExpr Atom) -> SExprParser Atom (SExpr Atom)
    forall t a. SExprParser t a -> SExprParser t a
    SC.withLispComments (Parser Atom -> SExprParser Atom (SExpr Atom)
    forall atom. Parser atom -> SExprParser atom (SExpr atom)
    SC.mkParser Parser Atom
    parseAtom)