-- | 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]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Atom] -> ShowS
$cshowList :: [Atom] -> ShowS
show :: Atom -> [Char]
$cshow :: Atom -> [Char]
showsPrec :: Int -> Atom -> ShowS
$cshowsPrec :: Int -> Atom -> ShowS
Show, Atom -> Atom -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Atom -> Atom -> Bool
$c/= :: Atom -> Atom -> Bool
== :: Atom -> Atom -> Bool
$c== :: Atom -> Atom -> Bool
Eq, Eq 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
min :: Atom -> Atom -> Atom
$cmin :: Atom -> Atom -> Atom
max :: Atom -> Atom -> Atom
$cmax :: Atom -> Atom -> Atom
>= :: Atom -> Atom -> Bool
$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
compare :: Atom -> Atom -> Ordering
$ccompare :: Atom -> Atom -> Ordering
Ord)

type SExpr = SC.WellFormedSExpr Atom

string :: Some W4.StringInfoRepr -> Text -> SExpr
string :: Some StringInfoRepr -> Text -> SExpr
string Some StringInfoRepr
strInfo Text
str = forall t. t -> WellFormedSExpr t
SC.A 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 = forall t. t -> WellFormedSExpr t
SC.A 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 = forall t. t -> WellFormedSExpr t
SC.A forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Atom
AId

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

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

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

-- | Lift a real
real :: Rational -> SExpr
real :: Rational -> SExpr
real = forall t. t -> WellFormedSExpr t
SC.A 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 = forall t. t -> WellFormedSExpr t
SC.A (Some FloatPrecisionRepr -> BigFloat -> Atom
AFloat (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 = forall t. t -> WellFormedSExpr t
SC.A forall a b. (a -> b) -> a -> b
$ Int -> Integer -> Atom
ABV (forall a. Enum a => a -> Int
fromEnum Natural
w) Integer
v

-- | Lift a boolean.
bool :: Bool -> SExpr
bool :: Bool -> SExpr
bool = forall t. t -> WellFormedSExpr t
SC.A 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 = forall atom carrier.
Int -> SExprPrinter atom carrier -> SExprPrinter atom carrier
SC.setIndentAmount Int
1 forall a b. (a -> b) -> a -> b
$ forall atom. (atom -> Text) -> SExprPrinter atom (SExpr atom)
SC.unconstrainedPrint Atom -> Text
printAtom
  in Seq [Char] -> Text
formatComment Seq [Char]
comments forall a. Semigroup a => a -> a -> a
<> (forall atom carrier. SExprPrinter atom carrier -> carrier -> Text
SC.encodeOne SExprPrinter Atom (SExpr Atom)
outputFmt forall a b. (a -> b) -> a -> b
$ forall atom. WellFormedSExpr atom -> SExpr atom
SC.fromWellFormed SExpr
sexpr)


formatComment :: Seq.Seq String -> T.Text
formatComment :: Seq [Char] -> Text
formatComment Seq [Char]
c
  | forall a. Seq a -> Bool
Seq.null Seq [Char]
c = Text
T.empty
  | Bool
otherwise = [Char] -> Text
T.pack forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {t} {t}. (PrintfArg t, PrintfType t) => t -> t
formatLine (forall (t :: Type -> Type) a. Foldable t => t a -> [a]
F.toList Seq [Char]
c)
  where
    formatLine :: t -> t
formatLine t
l = 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)forall a. Semigroup a => a -> a -> a
<>Text
"\""forall a. Semigroup a => a -> a -> a
<>Text
sforall a. Semigroup a => a -> a -> a
<>Text
"\""
    AInt Integer
i -> [Char] -> Text
T.pack (forall a. Show a => a -> [Char]
show Integer
i)
    ANat Natural
n -> [Char] -> Text
T.pack forall a b. (a -> b) -> a -> b
$ [Char]
"#u"forall a. [a] -> [a] -> [a]
++(forall a. Show a => a -> [Char]
show Natural
n)
    AReal Rational
r -> [Char] -> Text
T.pack forall a b. (a -> b) -> a -> b
$ [Char]
"#r"forall a. [a] -> [a] -> [a]
++(forall a. Show a => a -> [Char]
show (forall a. Ratio a -> a
numerator Rational
r))forall a. [a] -> [a] -> [a]
++[Char]
"/"forall a. [a] -> [a] -> [a]
++(forall a. Show a => a -> [Char]
show (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 -> 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 (forall r. PrintfType r => [Char] -> r
printf [Char]
"#f#%s#%s#%s" (forall a. Show a => a -> [Char]
show NatRepr eb
eb) (forall a. Show a => a -> [Char]
show NatRepr sb
sb) (Int -> ShowFmt -> BigFloat -> [Char]
BF.bfToString Int
16 (Maybe Word -> ShowFmt
BF.showFree 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 forall a. [a] -> [a] -> [a]
++ forall r. PrintfType r => [Char] -> r
printf [Char]
fmt Integer
val)
  where
    ([Char]
prefix, [Char]
fmt)
      | Int
w forall a. Integral a => a -> a -> a
`rem` Int
4 forall a. Eq a => a -> a -> Bool
== Int
0 = ([Char]
"#x", [Char]
"%0" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Int
w forall a. Integral a => a -> a -> a
`div` Int
4) forall a. [a] -> [a] -> [a]
++ [Char]
"x")
      | Bool
otherwise = ([Char]
"#b", [Char]
"%0" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
w 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 forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((:) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {u}. ParsecT Text u Identity Char
first forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m [a]
P.many forall {u}. ParsecT Text u Identity Char
rest)
  where first :: ParsecT Text u Identity Char
first = forall s (m :: Type -> Type) u.
Stream s m Char =>
ParsecT s u m Char
P.letter forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> 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 = forall s (m :: Type -> Type) u.
Stream s m Char =>
ParsecT s u m Char
P.letter forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> forall s (m :: Type -> Type) u.
Stream s m Char =>
ParsecT s u m Char
P.digit forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> 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 =
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (forall s (m :: Type -> Type) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
P.string [Char]
"#char16" forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some StringInfoRepr 'Char16
W4.Char16Repr))
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (forall s (m :: Type -> Type) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
P.string [Char]
"#char8" forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some StringInfoRepr 'Char8
W4.Char8Repr))
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> (forall (m :: Type -> Type) a. Monad m => a -> m a
return (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
_ <- forall s (m :: Type -> Type) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'"'
  [Char]
str <- forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m [a]
P.many ( do { Char
_ <- forall s (m :: Type -> Type) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'\\'; Char
c <- forall s (m :: Type -> Type) u.
Stream s m Char =>
ParsecT s u m Char
P.anyChar ; forall (m :: Type -> Type) a. Monad m => a -> m a
return [Char
'\\',Char
c]} forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> forall s (m :: Type -> Type) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
P.many1 (forall s (m :: Type -> Type) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
P.noneOf (Char
'"'forall a. a -> [a] -> [a]
:[Char]
"\\")))
  Char
_ <- forall s (m :: Type -> Type) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'"'
  forall (m :: Type -> Type) a. Monad m => a -> m a
return 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]
_ <- forall s (m :: Type -> Type) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
P.string [Char]
"#r"
  Integer
n <- (forall a. Read a => [Char] -> a
read :: (String -> Integer)) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m [a]
P.many forall s (m :: Type -> Type) u.
Stream s m Char =>
ParsecT s u m Char
P.digit
  Char
_ <- forall s (m :: Type -> Type) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'/'
  Integer
d <- (forall a. Read a => [Char] -> a
read :: (String -> Integer)) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m [a]
P.many forall s (m :: Type -> Type) u.
Stream s m Char =>
ParsecT s u m Char
P.digit
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer
n forall a. Integral a => a -> a -> Ratio a
% Integer
d

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

parseBool :: Parser Bool
parseBool :: Parser Bool
parseBool = do 
  (forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (forall s (m :: Type -> Type) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
P.string [Char]
"#false" forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
False))
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> (forall s (m :: Type -> Type) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
P.string [Char]
"#true" forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
True)
  
parseBV :: Parser (Int, Integer)
parseBV :: Parser (Int, Integer)
parseBV = forall s (m :: Type -> Type) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'#' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> ((forall s (m :: Type -> Type) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'b' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Parser (Int, Integer)
parseBin) forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> (forall s (m :: Type -> Type) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'x' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall {u}. ParsecT Text u Identity (Int, Integer)
parseHex))
  where parseBin :: Parser (Int, Integer)
parseBin = forall s (m :: Type -> Type) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
P.oneOf [Char]
"10" 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 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
          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 (forall s (m :: Type -> Type) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
P.oneOf [Char]
"10") 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 forall a. Num a => a -> a -> a
+ Int
1, Integer
x forall a. Num a => a -> a -> a
* Integer
2 forall a. Num a => a -> a -> a
+ (if Char
d forall a. Eq a => a -> a -> Bool
== Char
'1' then Integer
1 else Integer
0))
            Maybe Char
Nothing -> 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 -> (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Char]
s forall a. Num a => a -> a -> a
* Int
4, forall a. Read a => [Char] -> a
read ([Char]
"0x" forall a. [a] -> [a] -> [a]
++ [Char]
s))) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: Type -> Type) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
P.many1 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]
_ <- 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
     <- forall a. Read a => [Char] -> a
read forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: Type -> Type) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
P.many1 forall s (m :: Type -> Type) u.
Stream s m Char =>
ParsecT s u m Char
P.digit
  Char
_ <- forall s (m :: Type -> Type) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'#'
  Natural
sb :: Natural
     <- forall a. Read a => [Char] -> a
read forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: Type -> Type) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
P.many1 forall s (m :: Type -> Type) u.
Stream s m Char =>
ParsecT s u m Char
P.digit
  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 <- forall s (m :: Type -> Type) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
P.many1 forall s (m :: Type -> Type) u.
Stream s m Char =>
ParsecT s u m Char
P.hexDigit

  Some NatRepr x
ebRepr <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (Natural -> Some NatRepr
PN.mkNatRepr Natural
eb)
  Some NatRepr x
sbRepr <- forall (m :: Type -> Type) a. Monad m => a -> m a
return (Natural -> Some NatRepr
PN.mkNatRepr Natural
sb)
  case (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, 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 = 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 (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
sb) forall a. Semigroup a => a -> a -> a
<> Int -> BFOpts
BF.expBits (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 -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some FloatPrecisionRepr ('FloatingPointPrecision x x)
rep, BigFloat
bf)
        Status
_ -> 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" forall a. [a] -> [a] -> [a]
++ [Char]
hexDigits)
    (Maybe (LeqProof 2 x), Maybe (LeqProof 2 x))
_ -> 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: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Natural
eb, Natural
sb))


parseAtom :: Parser Atom
parseAtom :: Parser Atom
parseAtom
  =     forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (Natural -> Atom
ANat  forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Natural
parseNat)
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Some FloatPrecisionRepr -> BigFloat -> Atom
AFloat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Some FloatPrecisionRepr, BigFloat)
parseFloat)
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (Rational -> Atom
AReal forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Rational
parseReal)
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (Integer -> Atom
AInt  forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text () Identity Integer
parseInt)
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (Text -> Atom
AId   forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
parseId)
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Some StringInfoRepr -> Text -> Atom
AStr  forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Some StringInfoRepr, Text)
parseStr)
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (Bool -> Atom
ABool forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Bool
parseBool)
  forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
P.<|> forall s u (m :: Type -> Type) a.
ParsecT s u m a -> ParsecT s u m a
P.try (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Integer -> Atom
ABV 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 = forall atom carrier.
SExprParser atom carrier -> Text -> Either [Char] carrier
SC.decodeOne forall a b. (a -> b) -> a -> b
$ forall a b.
SExprParser a (SExpr b) -> SExprParser a (WellFormedSExpr b)
SC.asWellFormed forall a b. (a -> b) -> a -> b
$ forall t a. SExprParser t a -> SExprParser t a
SC.withLispComments (forall atom. Parser atom -> SExprParser atom (SExpr atom)
SC.mkParser Parser Atom
parseAtom)