-- | 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)