{-# 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
| AStr (Some W4.StringInfoRepr) Text
| AInt Integer
| ANat Natural
| AReal Rational
| AFloat (Some W4.FloatPrecisionRepr) BF.BigFloat
| ABV Int Integer
| ABool Bool
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)
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
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
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
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
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)
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
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
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
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
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")
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#"
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
'#'
[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
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)