{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Utils.SExpr (SExpr(..), parenDeficit, parseSExpr, parseSExprFunction) where
import Data.Bits (setBit, testBit)
import Data.Char (isDigit, ord, isSpace)
import Data.Either (partitionEithers)
import Data.List (isPrefixOf)
import Data.Maybe (fromMaybe, listToMaybe)
import Data.Word (Word32, Word64)
import Numeric (readInt, readDec, readHex, fromRat)
import Data.SBV.Core.AlgReals
import Data.SBV.Core.Data (nan, infinity, RoundingMode(..))
import Data.SBV.Utils.Numeric (fpIsEqualObjectH)
import Data.Numbers.CrackNum (wordToFloat, wordToDouble)
data SExpr = ECon String
| ENum (Integer, Maybe Int)
| EReal AlgReal
| EFloat Float
| EDouble Double
| EApp [SExpr]
deriving Int -> SExpr -> ShowS
[SExpr] -> ShowS
SExpr -> String
(Int -> SExpr -> ShowS)
-> (SExpr -> String) -> ([SExpr] -> ShowS) -> Show SExpr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SExpr] -> ShowS
$cshowList :: [SExpr] -> ShowS
show :: SExpr -> String
$cshow :: SExpr -> String
showsPrec :: Int -> SExpr -> ShowS
$cshowsPrec :: Int -> SExpr -> ShowS
Show
tokenize :: String -> [String]
tokenize :: String -> [String]
tokenize inp :: String
inp = String -> [String] -> [String]
go String
inp []
where go :: String -> [String] -> [String]
go "" sofar :: [String]
sofar = [String] -> [String]
forall a. [a] -> [a]
reverse [String]
sofar
go (c :: Char
c:cs :: String
cs) sofar :: [String]
sofar
| Char -> Bool
isSpace Char
c = String -> [String] -> [String]
go ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
cs) [String]
sofar
go ('(':cs :: String
cs) sofar :: [String]
sofar = String -> [String] -> [String]
go String
cs ("(" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
go (')':cs :: String
cs) sofar :: [String]
sofar = String -> [String] -> [String]
go String
cs (")" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
go (':':':':cs :: String
cs) sofar :: [String]
sofar = String -> [String] -> [String]
go String
cs ("::" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
go (':':cs :: String
cs) sofar :: [String]
sofar = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
stopper) String
cs of
(pre :: String
pre, rest :: String
rest) -> String -> [String] -> [String]
go String
rest ((':'Char -> ShowS
forall a. a -> [a] -> [a]
:String
pre) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
go ('|':r :: String
r) sofar :: [String]
sofar = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '|') String
r of
(pre :: String
pre, '|':rest :: String
rest) -> String -> [String] -> [String]
go String
rest (String
pre String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
(pre :: String
pre, rest :: String
rest) -> String -> [String] -> [String]
go String
rest (String
pre String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
go ('"':r :: String
r) sofar :: [String]
sofar = String -> [String] -> [String]
go String
rest (String
finalStr String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
where grabString :: String -> String -> (String, String)
grabString [] acc :: String
acc = (ShowS
forall a. [a] -> [a]
reverse String
acc, [])
grabString ('"' :'"':cs :: String
cs) acc :: String
acc = String -> String -> (String, String)
grabString String
cs ('"' Char -> ShowS
forall a. a -> [a] -> [a]
:String
acc)
grabString ('"':cs :: String
cs) acc :: String
acc = (ShowS
forall a. [a] -> [a]
reverse String
acc, String
cs)
grabString (c :: Char
c:cs :: String
cs) acc :: String
acc = String -> String -> (String, String)
grabString String
cs (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:String
acc)
(str :: String
str, rest :: String
rest) = String -> String -> (String, String)
grabString String
r []
finalStr :: String
finalStr = '"' Char -> ShowS
forall a. a -> [a] -> [a]
: String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\""
go cs :: String
cs sofar :: [String]
sofar = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` String
stopper) String
cs of
(pre :: String
pre, post :: String
post) -> String -> [String] -> [String]
go String
post (String
pre String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
stopper :: String
stopper = " \t\n():|\""
parenDeficit :: String -> Int
parenDeficit :: String -> Int
parenDeficit = Int -> [String] -> Int
go 0 ([String] -> Int) -> (String -> [String]) -> String -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
tokenize
where go :: Int -> [String] -> Int
go :: Int -> [String] -> Int
go !Int
balance [] = Int
balance
go !Int
balance ("(" : rest :: [String]
rest) = Int -> [String] -> Int
go (Int
balanceInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) [String]
rest
go !Int
balance (")" : rest :: [String]
rest) = Int -> [String] -> Int
go (Int
balanceInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [String]
rest
go !Int
balance (_ : rest :: [String]
rest) = Int -> [String] -> Int
go Int
balance [String]
rest
parseSExpr :: String -> Either String SExpr
parseSExpr :: String -> Either String SExpr
parseSExpr inp :: String
inp = do (sexp :: SExpr
sexp, extras :: [String]
extras) <- [String] -> Either String (SExpr, [String])
parse [String]
inpToks
if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
extras
then case SExpr
sexp of
EApp [ECon "error", ECon er :: String
er] -> String -> Either String SExpr
forall a b. a -> Either a b
Left (String -> Either String SExpr) -> String -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ "Solver returned an error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
er
_ -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SExpr
sexp
else String -> Either String SExpr
forall b. String -> Either String b
die "Extra tokens after valid input"
where inpToks :: [String]
inpToks = String -> [String]
tokenize String
inp
die :: String -> Either String b
die w :: String
w = String -> Either String b
forall a b. a -> Either a b
Left (String -> Either String b) -> String -> Either String b
forall a b. (a -> b) -> a -> b
$ "SBV.Provers.SExpr: Failed to parse S-Expr: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
w
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n*** Input : <" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
inp String -> ShowS
forall a. [a] -> [a] -> [a]
++ ">"
parse :: [String] -> Either String (SExpr, [String])
parse [] = String -> Either String (SExpr, [String])
forall b. String -> Either String b
die "ran out of tokens"
parse ("(":toks :: [String]
toks) = do (f :: [SExpr]
f, r :: [String]
r) <- [String] -> [SExpr] -> Either String ([SExpr], [String])
parseApp [String]
toks []
SExpr
f' <- SExpr -> Either String SExpr
cvt ([SExpr] -> SExpr
EApp [SExpr]
f)
(SExpr, [String]) -> Either String (SExpr, [String])
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr
f', [String]
r)
parse (")":_) = String -> Either String (SExpr, [String])
forall b. String -> Either String b
die "extra tokens after close paren"
parse [tok :: String
tok] = do SExpr
t <- String -> Either String SExpr
pTok String
tok
(SExpr, [String]) -> Either String (SExpr, [String])
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr
t, [])
parse _ = String -> Either String (SExpr, [String])
forall b. String -> Either String b
die "ill-formed s-expr"
parseApp :: [String] -> [SExpr] -> Either String ([SExpr], [String])
parseApp [] _ = String -> Either String ([SExpr], [String])
forall b. String -> Either String b
die "failed to grab s-expr application"
parseApp (")":toks :: [String]
toks) sofar :: [SExpr]
sofar = ([SExpr], [String]) -> Either String ([SExpr], [String])
forall (m :: * -> *) a. Monad m => a -> m a
return ([SExpr] -> [SExpr]
forall a. [a] -> [a]
reverse [SExpr]
sofar, [String]
toks)
parseApp ("(":toks :: [String]
toks) sofar :: [SExpr]
sofar = do (f :: SExpr
f, r :: [String]
r) <- [String] -> Either String (SExpr, [String])
parse ("("String -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
toks)
[String] -> [SExpr] -> Either String ([SExpr], [String])
parseApp [String]
r (SExpr
f SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [SExpr]
sofar)
parseApp (tok :: String
tok:toks :: [String]
toks) sofar :: [SExpr]
sofar = do SExpr
t <- String -> Either String SExpr
pTok String
tok
[String] -> [SExpr] -> Either String ([SExpr], [String])
parseApp [String]
toks (SExpr
t SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [SExpr]
sofar)
pTok :: String -> Either String SExpr
pTok "false" = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ (Integer, Maybe Int) -> SExpr
ENum (0, Maybe Int
forall a. Maybe a
Nothing)
pTok "true" = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ (Integer, Maybe Int) -> SExpr
ENum (1, Maybe Int
forall a. Maybe a
Nothing)
pTok ('0':'b':r :: String
r) = Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum (Int -> Maybe Int
forall a. a -> Maybe a
Just (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
r)) ([(Integer, String)] -> Either String SExpr)
-> [(Integer, String)] -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Integer -> (Char -> Bool) -> (Char -> Int) -> ReadS Integer
forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
readInt 2 (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "01") (\c :: Char
c -> Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord '0') String
r
pTok ('b':'v':r :: String
r) | Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
r) Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
r = Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum Maybe Int
forall a. Maybe a
Nothing ([(Integer, String)] -> Either String SExpr)
-> [(Integer, String)] -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ ReadS Integer
forall a. (Eq a, Num a) => ReadS a
readDec ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '[') String
r)
pTok ('#':'b':r :: String
r) = Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum (Int -> Maybe Int
forall a. a -> Maybe a
Just (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
r)) ([(Integer, String)] -> Either String SExpr)
-> [(Integer, String)] -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Integer -> (Char -> Bool) -> (Char -> Int) -> ReadS Integer
forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
readInt 2 (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "01") (\c :: Char
c -> Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord '0') String
r
pTok ('#':'x':r :: String
r) = Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum (Int -> Maybe Int
forall a. a -> Maybe a
Just (4 Int -> Int -> Int
forall a. Num a => a -> a -> a
* String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
r)) ([(Integer, String)] -> Either String SExpr)
-> [(Integer, String)] -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ ReadS Integer
forall a. (Eq a, Num a) => ReadS a
readHex String
r
pTok n :: String
n
| Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
n) Bool -> Bool -> Bool
&& Char -> Bool
isDigit (String -> Char
forall a. [a] -> a
head String
n)
= if '.' Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
n then String -> Either String SExpr
forall (m :: * -> *). Monad m => String -> m SExpr
getReal String
n
else Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum Maybe Int
forall a. Maybe a
Nothing ([(Integer, String)] -> Either String SExpr)
-> [(Integer, String)] -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ ReadS Integer
forall a. (Eq a, Num a) => ReadS a
readDec String
n
pTok n :: String
n = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ String -> SExpr
ECon (ShowS
constantMap String
n)
mkNum :: Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum l :: Maybe Int
l [(n :: Integer
n, "")] = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ (Integer, Maybe Int) -> SExpr
ENum (Integer
n, Maybe Int
l)
mkNum _ _ = String -> Either String SExpr
forall b. String -> Either String b
die "cannot read number"
getReal :: String -> m SExpr
getReal n :: String
n = SExpr -> m SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> m SExpr) -> SExpr -> m SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (AlgReal -> SExpr) -> AlgReal -> SExpr
forall a b. (a -> b) -> a -> b
$ Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal ((Bool, String)
-> Either (Bool, String) (Integer, [(Integer, Integer)])
forall a b. a -> Either a b
Left (Bool
exact, String
n'))
where exact :: Bool
exact = Bool -> Bool
not ("?" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` ShowS
forall a. [a] -> [a]
reverse String
n)
n' :: String
n' | Bool
exact = String
n
| Bool
True = ShowS
forall a. [a] -> [a]
init String
n
cvt :: SExpr -> Either String SExpr
cvt (EApp [ECon "to_int", EReal a :: AlgReal
a]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal AlgReal
a
cvt (EApp [ECon "to_real", EReal a :: AlgReal
a]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal AlgReal
a
cvt (EApp [ECon "/", EReal a :: AlgReal
a, EReal b :: AlgReal
b]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (AlgReal
a AlgReal -> AlgReal -> AlgReal
forall a. Fractional a => a -> a -> a
/ AlgReal
b)
cvt (EApp [ECon "/", EReal a :: AlgReal
a, ENum b :: (Integer, Maybe Int)
b]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (AlgReal
a AlgReal -> AlgReal -> AlgReal
forall a. Fractional a => a -> a -> a
/ Integer -> AlgReal
forall a. Num a => Integer -> a
fromInteger ((Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
b))
cvt (EApp [ECon "/", ENum a :: (Integer, Maybe Int)
a, EReal b :: AlgReal
b]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (Integer -> AlgReal
forall a. Num a => Integer -> a
fromInteger ((Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
a) AlgReal -> AlgReal -> AlgReal
forall a. Fractional a => a -> a -> a
/ AlgReal
b )
cvt (EApp [ECon "/", ENum a :: (Integer, Maybe Int)
a, ENum b :: (Integer, Maybe Int)
b]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (Integer -> AlgReal
forall a. Num a => Integer -> a
fromInteger ((Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
a) AlgReal -> AlgReal -> AlgReal
forall a. Fractional a => a -> a -> a
/ Integer -> AlgReal
forall a. Num a => Integer -> a
fromInteger ((Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
b))
cvt (EApp [ECon "-", EReal a :: AlgReal
a]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (-AlgReal
a)
cvt (EApp [ECon "-", ENum a :: (Integer, Maybe Int)
a]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ (Integer, Maybe Int) -> SExpr
ENum (-((Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
a), (Integer, Maybe Int) -> Maybe Int
forall a b. (a, b) -> b
snd (Integer, Maybe Int)
a)
cvt (EApp [ECon "_", ENum a :: (Integer, Maybe Int)
a, ENum _b :: (Integer, Maybe Int)
_b]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ (Integer, Maybe Int) -> SExpr
ENum (Integer, Maybe Int)
a
cvt (EApp [ECon "root-obj", EApp (ECon "+":trms :: [SExpr]
trms), ENum k :: (Integer, Maybe Int)
k]) = do [(Integer, Integer)]
ts <- (SExpr -> Either String (Integer, Integer))
-> [SExpr] -> Either String [(Integer, Integer)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Either String (Integer, Integer)
getCoeff [SExpr]
trms
SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (AlgReal -> SExpr) -> AlgReal -> SExpr
forall a b. (a -> b) -> a -> b
$ Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal ((Integer, [(Integer, Integer)])
-> Either (Bool, String) (Integer, [(Integer, Integer)])
forall a b. b -> Either a b
Right ((Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
k, [(Integer, Integer)]
ts))
cvt (EApp [ECon "as", n :: SExpr
n, EApp [ECon "_", ECon "FloatingPoint", ENum (11, _), ENum (53, _)]]) = SExpr -> Either String SExpr
getDouble SExpr
n
cvt (EApp [ECon "as", n :: SExpr
n, EApp [ECon "_", ECon "FloatingPoint", ENum ( 8, _), ENum (24, _)]]) = SExpr -> Either String SExpr
getFloat SExpr
n
cvt (EApp [ECon "as", n :: SExpr
n, ECon "Float64"]) = SExpr -> Either String SExpr
getDouble SExpr
n
cvt (EApp [ECon "as", n :: SExpr
n, ECon "Float32"]) = SExpr -> Either String SExpr
getFloat SExpr
n
cvt x :: SExpr
x@(EApp [ECon "witness", EApp [EApp [ECon v :: String
v, ECon "Real"]]
, EApp [ECon "or", EApp [ECon "=", ECon v' :: String
v', val :: SExpr
val], _]]) | String
v String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
v' = do
SExpr
approx <- SExpr -> Either String SExpr
cvt SExpr
val
case SExpr
approx of
ENum (s :: Integer
s, _) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (AlgReal -> SExpr) -> AlgReal -> SExpr
forall a b. (a -> b) -> a -> b
$ Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal ((Bool, String)
-> Either (Bool, String) (Integer, [(Integer, Integer)])
forall a b. a -> Either a b
Left (Bool
False, Integer -> String
forall a. Show a => a -> String
show Integer
s))
EReal aval :: AlgReal
aval -> case AlgReal
aval of
AlgRational _ r :: Rational
r -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (AlgReal -> SExpr) -> AlgReal -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> Rational -> AlgReal
AlgRational Bool
False Rational
r
_ -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal AlgReal
aval
_ -> String -> Either String SExpr
forall b. String -> Either String b
die (String -> Either String SExpr) -> String -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ "Cannot parse a CVC4 approximate value from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
x
cvt (EApp [ECon "fp", ENum (s :: Integer
s, Just 1), ENum ( e :: Integer
e, Just 8), ENum (m :: Integer
m, Just 23)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat (Float -> SExpr) -> Float -> SExpr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer -> Float
getTripleFloat Integer
s Integer
e Integer
m
cvt (EApp [ECon "fp", ENum (s :: Integer
s, Just 1), ENum ( e :: Integer
e, Just 11), ENum (m :: Integer
m, Just 52)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble (Double -> SExpr) -> Double -> SExpr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer -> Double
getTripleDouble Integer
s Integer
e Integer
m
cvt (EApp [ECon "_", ECon "NaN", ENum ( 8, _), ENum (24, _)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat Float
forall a. Floating a => a
nan
cvt (EApp [ECon "_", ECon "NaN", ENum (11, _), ENum (53, _)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble Double
forall a. Floating a => a
nan
cvt (EApp [ECon "_", ECon "+oo", ENum ( 8, _), ENum (24, _)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat Float
forall a. Floating a => a
infinity
cvt (EApp [ECon "_", ECon "+oo", ENum (11, _), ENum (53, _)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble Double
forall a. Floating a => a
infinity
cvt (EApp [ECon "_", ECon "-oo", ENum ( 8, _), ENum (24, _)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat (-Float
forall a. Floating a => a
infinity)
cvt (EApp [ECon "_", ECon "-oo", ENum (11, _), ENum (53, _)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble (-Double
forall a. Floating a => a
infinity)
cvt (EApp [ECon "_", ECon "+zero", ENum ( 8, _), ENum (24, _)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat 0
cvt (EApp [ECon "_", ECon "+zero", ENum (11, _), ENum (53, _)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble 0
cvt (EApp [ECon "_", ECon "-zero", ENum ( 8, _), ENum (24, _)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat (-0)
cvt (EApp [ECon "_", ECon "-zero", ENum (11, _), ENum (53, _)]) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble (-0)
cvt x :: SExpr
x = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return SExpr
x
getCoeff :: SExpr -> Either String (Integer, Integer)
getCoeff (EApp [ECon "*", ENum k :: (Integer, Maybe Int)
k, EApp [ECon "^", ECon "x", ENum p :: (Integer, Maybe Int)
p]]) = (Integer, Integer) -> Either String (Integer, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
k, (Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
p)
getCoeff (EApp [ECon "*", ENum k :: (Integer, Maybe Int)
k, ECon "x" ] ) = (Integer, Integer) -> Either String (Integer, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
k, 1)
getCoeff ( EApp [ECon "^", ECon "x", ENum p :: (Integer, Maybe Int)
p] ) = (Integer, Integer) -> Either String (Integer, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return ( 1, (Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
p)
getCoeff ( ECon "x" ) = (Integer, Integer) -> Either String (Integer, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return ( 1, 1)
getCoeff ( ENum k :: (Integer, Maybe Int)
k ) = (Integer, Integer) -> Either String (Integer, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
k, 0)
getCoeff x :: SExpr
x = String -> Either String (Integer, Integer)
forall b. String -> Either String b
die (String -> Either String (Integer, Integer))
-> String -> Either String (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ "Cannot parse a root-obj,\nProcessing term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
x
getDouble :: SExpr -> Either String SExpr
getDouble (ECon s :: String
s) = case (String
s, String -> Maybe Double
forall a. (Read a, RealFloat a) => String -> Maybe a
rdFP ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '+') String
s)) of
("plusInfinity", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble Double
forall a. Floating a => a
infinity
("minusInfinity", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble (-Double
forall a. Floating a => a
infinity)
("oo", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble Double
forall a. Floating a => a
infinity
("-oo", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble (-Double
forall a. Floating a => a
infinity)
("zero", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble 0
("-zero", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble (-0)
("NaN", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble Double
forall a. Floating a => a
nan
(_, Just v :: Double
v) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble Double
v
_ -> String -> Either String SExpr
forall b. String -> Either String b
die (String -> Either String SExpr) -> String -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ "Cannot parse a double value from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
getDouble (EApp [_, s :: SExpr
s, _, _]) = SExpr -> Either String SExpr
getDouble SExpr
s
getDouble (EReal r :: AlgReal
r) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble (Double -> SExpr) -> Double -> SExpr
forall a b. (a -> b) -> a -> b
$ Rational -> Double
forall a. RealFloat a => Rational -> a
fromRat (Rational -> Double) -> Rational -> Double
forall a b. (a -> b) -> a -> b
$ AlgReal -> Rational
forall a. Real a => a -> Rational
toRational AlgReal
r
getDouble x :: SExpr
x = String -> Either String SExpr
forall b. String -> Either String b
die (String -> Either String SExpr) -> String -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ "Cannot parse a double value from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
x
getFloat :: SExpr -> Either String SExpr
getFloat (ECon s :: String
s) = case (String
s, String -> Maybe Float
forall a. (Read a, RealFloat a) => String -> Maybe a
rdFP ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '+') String
s)) of
("plusInfinity", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat Float
forall a. Floating a => a
infinity
("minusInfinity", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat (-Float
forall a. Floating a => a
infinity)
("oo", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat Float
forall a. Floating a => a
infinity
("-oo", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat (-Float
forall a. Floating a => a
infinity)
("zero", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat 0
("-zero", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat (-0)
("NaN", _ ) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat Float
forall a. Floating a => a
nan
(_, Just v :: Float
v) -> SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat Float
v
_ -> String -> Either String SExpr
forall b. String -> Either String b
die (String -> Either String SExpr) -> String -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ "Cannot parse a float value from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
getFloat (EReal r :: AlgReal
r) = SExpr -> Either String SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat (Float -> SExpr) -> Float -> SExpr
forall a b. (a -> b) -> a -> b
$ Rational -> Float
forall a. RealFloat a => Rational -> a
fromRat (Rational -> Float) -> Rational -> Float
forall a b. (a -> b) -> a -> b
$ AlgReal -> Rational
forall a. Real a => a -> Rational
toRational AlgReal
r
getFloat (EApp [_, s :: SExpr
s, _, _]) = SExpr -> Either String SExpr
getFloat SExpr
s
getFloat x :: SExpr
x = String -> Either String SExpr
forall b. String -> Either String b
die (String -> Either String SExpr) -> String -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ "Cannot parse a float value from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
x
rdFP :: (Read a, RealFloat a) => String -> Maybe a
rdFP :: String -> Maybe a
rdFP s :: String
s = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "pe") String
s of
(m :: String
m, 'p':e :: String
e) -> String -> Maybe a
forall a. Read a => String -> Maybe a
rd String
m Maybe a -> (a -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \m' :: a
m' -> String -> Maybe a
forall a. Read a => String -> Maybe a
rd String
e Maybe a -> (a -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \e' :: a
e' -> a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a
m' a -> a -> a
forall a. Num a => a -> a -> a
* ( 2 a -> a -> a
forall a. Floating a => a -> a -> a
** a
e')
(m :: String
m, 'e':e :: String
e) -> String -> Maybe a
forall a. Read a => String -> Maybe a
rd String
m Maybe a -> (a -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \m' :: a
m' -> String -> Maybe a
forall a. Read a => String -> Maybe a
rd String
e Maybe a -> (a -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \e' :: a
e' -> a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a
m' a -> a -> a
forall a. Num a => a -> a -> a
* (10 a -> a -> a
forall a. Floating a => a -> a -> a
** a
e')
(m :: String
m, "") -> String -> Maybe a
forall a. Read a => String -> Maybe a
rd String
m
_ -> Maybe a
forall a. Maybe a
Nothing
where rd :: String -> Maybe a
rd v :: String
v = case ReadS a
forall a. Read a => ReadS a
reads String
v of
[(n :: a
n, "")] -> a -> Maybe a
forall a. a -> Maybe a
Just a
n
_ -> Maybe a
forall a. Maybe a
Nothing
getTripleFloat :: Integer -> Integer -> Integer -> Float
getTripleFloat :: Integer -> Integer -> Integer -> Float
getTripleFloat s :: Integer
s e :: Integer
e m :: Integer
m = Word32 -> Float
wordToFloat Word32
w32
where sign :: [Bool]
sign = [Integer
s Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 1]
expt :: [Bool]
expt = [Integer
e Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [ 7, 6 .. 0]]
mantissa :: [Bool]
mantissa = [Integer
m Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [22, 21 .. 0]]
positions :: [Int]
positions = [Int
i | (i :: Int
i, b :: Bool
b) <- [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [31, 30 .. 0] ([Bool]
sign [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
expt [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
mantissa), Bool
b]
w32 :: Word32
w32 = (Int -> Word32 -> Word32) -> Word32 -> [Int] -> Word32
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Word32 -> Int -> Word32) -> Int -> Word32 -> Word32
forall a b c. (a -> b -> c) -> b -> a -> c
flip Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
setBit) (0::Word32) [Int]
positions
getTripleDouble :: Integer -> Integer -> Integer -> Double
getTripleDouble :: Integer -> Integer -> Integer -> Double
getTripleDouble s :: Integer
s e :: Integer
e m :: Integer
m = Word64 -> Double
wordToDouble Word64
w64
where sign :: [Bool]
sign = [Integer
s Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 1]
expt :: [Bool]
expt = [Integer
e Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [10, 9 .. 0]]
mantissa :: [Bool]
mantissa = [Integer
m Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [51, 50 .. 0]]
positions :: [Int]
positions = [Int
i | (i :: Int
i, b :: Bool
b) <- [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [63, 62 .. 0] ([Bool]
sign [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
expt [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
mantissa), Bool
b]
w64 :: Word64
w64 = (Int -> Word64 -> Word64) -> Word64 -> [Int] -> Word64
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Word64 -> Int -> Word64) -> Int -> Word64 -> Word64
forall a b c. (a -> b -> c) -> b -> a -> c
flip Word64 -> Int -> Word64
forall a. Bits a => a -> Int -> a
setBit) (0::Word64) [Int]
positions
constantMap :: String -> String
constantMap :: ShowS
constantMap n :: String
n = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
n ([String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe [String
to | (from :: [String]
from, to :: String
to) <- [([String], String)]
special, String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
from])
where special :: [([String], String)]
special = [ (["RNE", "roundNearestTiesToEven"], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundNearestTiesToEven)
, (["RNA", "roundNearestTiesToAway"], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundNearestTiesToAway)
, (["RTP", "roundTowardPositive"], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundTowardPositive)
, (["RTN", "roundTowardNegative"], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundTowardNegative)
, (["RTZ", "roundTowardZero"], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundTowardZero)
]
parseSExprFunction :: SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
parseSExprFunction :: SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
parseSExprFunction e :: SExpr
e
| Just r :: ([([SExpr], SExpr)], SExpr)
r <- SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseLambdaExpression SExpr
e = Either String ([([SExpr], SExpr)], SExpr)
-> Maybe (Either String ([([SExpr], SExpr)], SExpr))
forall a. a -> Maybe a
Just (([([SExpr], SExpr)], SExpr)
-> Either String ([([SExpr], SExpr)], SExpr)
forall a b. b -> Either a b
Right ([([SExpr], SExpr)], SExpr)
r)
| Just r :: Either String ([([SExpr], SExpr)], SExpr)
r <- SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
parseStoreAssociations SExpr
e = Either String ([([SExpr], SExpr)], SExpr)
-> Maybe (Either String ([([SExpr], SExpr)], SExpr))
forall a. a -> Maybe a
Just Either String ([([SExpr], SExpr)], SExpr)
r
| Bool
True = Maybe (Either String ([([SExpr], SExpr)], SExpr))
forall a. Maybe a
Nothing
parseLambdaExpression :: SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseLambdaExpression :: SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseLambdaExpression funExpr :: SExpr
funExpr = case SExpr
funExpr of
EApp [ECon "lambda", EApp params :: [SExpr]
params, body :: SExpr
body] -> (SExpr -> Maybe String) -> [SExpr] -> Maybe [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Maybe String
getParam [SExpr]
params Maybe [String]
-> ([String] -> Maybe [Either ([SExpr], SExpr) SExpr])
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([String] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr])
-> SExpr -> [String] -> Maybe [Either ([SExpr], SExpr) SExpr]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [String] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
lambda SExpr
body Maybe [Either ([SExpr], SExpr) SExpr]
-> ([Either ([SExpr], SExpr) SExpr]
-> Maybe ([([SExpr], SExpr)], SExpr))
-> Maybe ([([SExpr], SExpr)], SExpr)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Either ([SExpr], SExpr) SExpr]
-> Maybe ([([SExpr], SExpr)], SExpr)
chainAssigns
_ -> Maybe ([([SExpr], SExpr)], SExpr)
forall a. Maybe a
Nothing
where getParam :: SExpr -> Maybe String
getParam (EApp [ECon v :: String
v, _]) = String -> Maybe String
forall a. a -> Maybe a
Just String
v
getParam _ = Maybe String
forall a. Maybe a
Nothing
lambda :: [String] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
lambda :: [String] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
lambda params :: [String]
params body :: SExpr
body = [Either ([SExpr], SExpr) SExpr] -> [Either ([SExpr], SExpr) SExpr]
forall a. [a] -> [a]
reverse ([Either ([SExpr], SExpr) SExpr]
-> [Either ([SExpr], SExpr) SExpr])
-> Maybe [Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go [] SExpr
body
where true :: SExpr
true = (Integer, Maybe Int) -> SExpr
ENum (1, Maybe Int
forall a. Maybe a
Nothing)
false :: SExpr
false = (Integer, Maybe Int) -> SExpr
ENum (0, Maybe Int
forall a. Maybe a
Nothing)
go :: [Either ([SExpr], SExpr) SExpr] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go :: [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go sofar :: [Either ([SExpr], SExpr) SExpr]
sofar (EApp [ECon "ite", selector :: SExpr
selector, thenBranch :: SExpr
thenBranch, elseBranch :: SExpr
elseBranch])
= do [SExpr]
s <- SExpr -> Maybe [SExpr]
select SExpr
selector
[Either ([SExpr], SExpr) SExpr]
tB <- [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go [] SExpr
thenBranch
case [SExpr]
-> [Either ([SExpr], SExpr) SExpr] -> Maybe ([SExpr], SExpr)
cond [SExpr]
s [Either ([SExpr], SExpr) SExpr]
tB of
Just sv :: ([SExpr], SExpr)
sv -> [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go (([SExpr], SExpr) -> Either ([SExpr], SExpr) SExpr
forall a b. a -> Either a b
Left ([SExpr], SExpr)
sv Either ([SExpr], SExpr) SExpr
-> [Either ([SExpr], SExpr) SExpr]
-> [Either ([SExpr], SExpr) SExpr]
forall a. a -> [a] -> [a]
: [Either ([SExpr], SExpr) SExpr]
sofar) SExpr
elseBranch
_ -> Maybe [Either ([SExpr], SExpr) SExpr]
forall a. Maybe a
Nothing
go sofar :: [Either ([SExpr], SExpr) SExpr]
sofar inner :: SExpr
inner@(EApp [ECon "=", _, _])
= [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go [Either ([SExpr], SExpr) SExpr]
sofar ([SExpr] -> SExpr
EApp [String -> SExpr
ECon "ite", SExpr
inner, SExpr
true, SExpr
false])
go sofar :: [Either ([SExpr], SExpr) SExpr]
sofar (EApp [ECon "not", inner :: SExpr
inner])
= [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go [Either ([SExpr], SExpr) SExpr]
sofar ([SExpr] -> SExpr
EApp [String -> SExpr
ECon "ite", SExpr
inner, SExpr
false, SExpr
true])
go sofar :: [Either ([SExpr], SExpr) SExpr]
sofar (EApp (ECon "or" : elts :: [SExpr]
elts))
= let xform :: [SExpr] -> SExpr
xform [] = SExpr
false
xform [x :: SExpr
x] = SExpr
x
xform (x :: SExpr
x:xs :: [SExpr]
xs) = [SExpr] -> SExpr
EApp [String -> SExpr
ECon "ite", SExpr
x, SExpr
true, [SExpr] -> SExpr
xform [SExpr]
xs]
in [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go [Either ([SExpr], SExpr) SExpr]
sofar (SExpr -> Maybe [Either ([SExpr], SExpr) SExpr])
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
xform [SExpr]
elts
go sofar :: [Either ([SExpr], SExpr) SExpr]
sofar (EApp (ECon "and" : elts :: [SExpr]
elts))
= let xform :: [SExpr] -> SExpr
xform [] = SExpr
true
xform [x :: SExpr
x] = SExpr
x
xform (x :: SExpr
x:xs :: [SExpr]
xs) = [SExpr] -> SExpr
EApp [String -> SExpr
ECon "ite", SExpr
x, [SExpr] -> SExpr
xform [SExpr]
xs, SExpr
false]
in [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go [Either ([SExpr], SExpr) SExpr]
sofar (SExpr -> Maybe [Either ([SExpr], SExpr) SExpr])
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
xform [SExpr]
elts
go sofar :: [Either ([SExpr], SExpr) SExpr]
sofar e :: SExpr
e
| Just s :: [SExpr]
s <- SExpr -> Maybe [SExpr]
select SExpr
e
= [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go (([SExpr], SExpr) -> Either ([SExpr], SExpr) SExpr
forall a b. a -> Either a b
Left ([SExpr]
s, SExpr
true) Either ([SExpr], SExpr) SExpr
-> [Either ([SExpr], SExpr) SExpr]
-> [Either ([SExpr], SExpr) SExpr]
forall a. a -> [a] -> [a]
: [Either ([SExpr], SExpr) SExpr]
sofar) SExpr
false
go sofar :: [Either ([SExpr], SExpr) SExpr]
sofar e :: SExpr
e = [Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall a. a -> Maybe a
Just ([Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr])
-> [Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall a b. (a -> b) -> a -> b
$ SExpr -> Either ([SExpr], SExpr) SExpr
forall a b. b -> Either a b
Right SExpr
e Either ([SExpr], SExpr) SExpr
-> [Either ([SExpr], SExpr) SExpr]
-> [Either ([SExpr], SExpr) SExpr]
forall a. a -> [a] -> [a]
: [Either ([SExpr], SExpr) SExpr]
sofar
cond :: [SExpr] -> [Either ([SExpr], SExpr) SExpr] -> Maybe ([SExpr], SExpr)
cond :: [SExpr]
-> [Either ([SExpr], SExpr) SExpr] -> Maybe ([SExpr], SExpr)
cond s :: [SExpr]
s [Right v :: SExpr
v] = ([SExpr], SExpr) -> Maybe ([SExpr], SExpr)
forall a. a -> Maybe a
Just ([SExpr]
s, SExpr
v)
cond _ _ = Maybe ([SExpr], SExpr)
forall a. Maybe a
Nothing
select :: SExpr -> Maybe [SExpr]
select :: SExpr -> Maybe [SExpr]
select e :: SExpr
e
| Just dict :: [(String, SExpr)]
dict <- SExpr -> [(String, SExpr)] -> Maybe [(String, SExpr)]
build SExpr
e [] = (String -> Maybe SExpr) -> [String] -> Maybe [SExpr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> [(String, SExpr)] -> Maybe SExpr
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, SExpr)]
dict) [String]
params
| Bool
True = Maybe [SExpr]
forall a. Maybe a
Nothing
where
build :: SExpr -> [(String, SExpr)] -> Maybe [(String, SExpr)]
build :: SExpr -> [(String, SExpr)] -> Maybe [(String, SExpr)]
build (EApp (ECon "and" : rest :: [SExpr]
rest)) sofar :: [(String, SExpr)]
sofar = let next :: SExpr -> Maybe [(String, SExpr)] -> Maybe [(String, SExpr)]
next _ Nothing = Maybe [(String, SExpr)]
forall a. Maybe a
Nothing
next c :: SExpr
c (Just x :: [(String, SExpr)]
x) = SExpr -> [(String, SExpr)] -> Maybe [(String, SExpr)]
build SExpr
c [(String, SExpr)]
x
in (SExpr -> Maybe [(String, SExpr)] -> Maybe [(String, SExpr)])
-> Maybe [(String, SExpr)] -> [SExpr] -> Maybe [(String, SExpr)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SExpr -> Maybe [(String, SExpr)] -> Maybe [(String, SExpr)]
next ([(String, SExpr)] -> Maybe [(String, SExpr)]
forall a. a -> Maybe a
Just [(String, SExpr)]
sofar) [SExpr]
rest
build expr :: SExpr
expr sofar :: [(String, SExpr)]
sofar | Just (v :: String
v, r :: SExpr
r) <- SExpr -> Maybe (String, SExpr)
grok SExpr
expr, String
v String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
params = [(String, SExpr)] -> Maybe [(String, SExpr)]
forall a. a -> Maybe a
Just ([(String, SExpr)] -> Maybe [(String, SExpr)])
-> [(String, SExpr)] -> Maybe [(String, SExpr)]
forall a b. (a -> b) -> a -> b
$ (String
v, SExpr
r) (String, SExpr) -> [(String, SExpr)] -> [(String, SExpr)]
forall a. a -> [a] -> [a]
: [(String, SExpr)]
sofar
| Bool
True = Maybe [(String, SExpr)]
forall a. Maybe a
Nothing
grok :: SExpr -> Maybe (String, SExpr)
grok (EApp [ECon "=", ECon v :: String
v, r :: SExpr
r]) = (String, SExpr) -> Maybe (String, SExpr)
forall a. a -> Maybe a
Just (String
v, SExpr
r)
grok (EApp [ECon "=", r :: SExpr
r, ECon v :: String
v]) = (String, SExpr) -> Maybe (String, SExpr)
forall a. a -> Maybe a
Just (String
v, SExpr
r)
grok (EApp [ECon "not", ECon v :: String
v]) = (String, SExpr) -> Maybe (String, SExpr)
forall a. a -> Maybe a
Just (String
v, SExpr
false)
grok (ECon v :: String
v) = (String, SExpr) -> Maybe (String, SExpr)
forall a. a -> Maybe a
Just (String
v, SExpr
true)
grok _ = Maybe (String, SExpr)
forall a. Maybe a
Nothing
parseStoreAssociations :: SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
parseStoreAssociations :: SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
parseStoreAssociations (EApp [ECon "_", ECon "as-array", ECon nm :: String
nm]) = Either String ([([SExpr], SExpr)], SExpr)
-> Maybe (Either String ([([SExpr], SExpr)], SExpr))
forall a. a -> Maybe a
Just (Either String ([([SExpr], SExpr)], SExpr)
-> Maybe (Either String ([([SExpr], SExpr)], SExpr)))
-> Either String ([([SExpr], SExpr)], SExpr)
-> Maybe (Either String ([([SExpr], SExpr)], SExpr))
forall a b. (a -> b) -> a -> b
$ String -> Either String ([([SExpr], SExpr)], SExpr)
forall a b. a -> Either a b
Left String
nm
parseStoreAssociations e :: SExpr
e = ([([SExpr], SExpr)], SExpr)
-> Either String ([([SExpr], SExpr)], SExpr)
forall a b. b -> Either a b
Right (([([SExpr], SExpr)], SExpr)
-> Either String ([([SExpr], SExpr)], SExpr))
-> Maybe ([([SExpr], SExpr)], SExpr)
-> Maybe (Either String ([([SExpr], SExpr)], SExpr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Either ([SExpr], SExpr) SExpr]
-> Maybe ([([SExpr], SExpr)], SExpr)
chainAssigns ([Either ([SExpr], SExpr) SExpr]
-> Maybe ([([SExpr], SExpr)], SExpr))
-> Maybe [Either ([SExpr], SExpr) SExpr]
-> Maybe ([([SExpr], SExpr)], SExpr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
vals SExpr
e)
where vals :: SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
vals :: SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
vals (EApp [EApp [ECon "as", ECon "const", ECon "Array"], defVal :: SExpr
defVal]) = [Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [SExpr -> Either ([SExpr], SExpr) SExpr
forall a b. b -> Either a b
Right SExpr
defVal]
vals (EApp [EApp [ECon "as", ECon "const", EApp (ECon "Array" : _)], defVal :: SExpr
defVal]) = [Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return [SExpr -> Either ([SExpr], SExpr) SExpr
forall a b. b -> Either a b
Right SExpr
defVal]
vals (EApp (ECon "store" : prev :: SExpr
prev : argsVal :: [SExpr]
argsVal)) | [SExpr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
argsVal Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2 = do [Either ([SExpr], SExpr) SExpr]
rest <- SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
vals SExpr
prev
[Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr])
-> [Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall a b. (a -> b) -> a -> b
$ ([SExpr], SExpr) -> Either ([SExpr], SExpr) SExpr
forall a b. a -> Either a b
Left ([SExpr] -> [SExpr]
forall a. [a] -> [a]
init [SExpr]
argsVal, [SExpr] -> SExpr
forall a. [a] -> a
last [SExpr]
argsVal) Either ([SExpr], SExpr) SExpr
-> [Either ([SExpr], SExpr) SExpr]
-> [Either ([SExpr], SExpr) SExpr]
forall a. a -> [a] -> [a]
: [Either ([SExpr], SExpr) SExpr]
rest
vals _ = Maybe [Either ([SExpr], SExpr) SExpr]
forall a. Maybe a
Nothing
chainAssigns :: [Either ([SExpr], SExpr) SExpr] -> Maybe ([([SExpr], SExpr)], SExpr)
chainAssigns :: [Either ([SExpr], SExpr) SExpr]
-> Maybe ([([SExpr], SExpr)], SExpr)
chainAssigns chain :: [Either ([SExpr], SExpr) SExpr]
chain = ([([SExpr], SExpr)], [SExpr]) -> Maybe ([([SExpr], SExpr)], SExpr)
forall b.
([([SExpr], SExpr)], [b]) -> Maybe ([([SExpr], SExpr)], b)
regroup (([([SExpr], SExpr)], [SExpr])
-> Maybe ([([SExpr], SExpr)], SExpr))
-> ([([SExpr], SExpr)], [SExpr])
-> Maybe ([([SExpr], SExpr)], SExpr)
forall a b. (a -> b) -> a -> b
$ [Either ([SExpr], SExpr) SExpr] -> ([([SExpr], SExpr)], [SExpr])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either ([SExpr], SExpr) SExpr]
chain
where regroup :: ([([SExpr], SExpr)], [b]) -> Maybe ([([SExpr], SExpr)], b)
regroup (vs :: [([SExpr], SExpr)]
vs, [d :: b
d]) = ([([SExpr], SExpr)], b) -> Maybe ([([SExpr], SExpr)], b)
forall a. a -> Maybe a
Just ([([SExpr], SExpr)] -> [([SExpr], SExpr)]
checkDup [([SExpr], SExpr)]
vs, b
d)
regroup _ = Maybe ([([SExpr], SExpr)], b)
forall a. Maybe a
Nothing
checkDup :: [([SExpr], SExpr)] -> [([SExpr], SExpr)]
checkDup :: [([SExpr], SExpr)] -> [([SExpr], SExpr)]
checkDup [] = []
checkDup (a :: ([SExpr], SExpr)
a@(key :: [SExpr]
key, _):as :: [([SExpr], SExpr)]
as) = ([SExpr], SExpr)
a ([SExpr], SExpr) -> [([SExpr], SExpr)] -> [([SExpr], SExpr)]
forall a. a -> [a] -> [a]
: [([SExpr], SExpr)] -> [([SExpr], SExpr)]
checkDup [([SExpr], SExpr)
r | r :: ([SExpr], SExpr)
r@(key' :: [SExpr]
key', _) <- [([SExpr], SExpr)]
as, Bool -> Bool
not ([SExpr]
key [SExpr] -> [SExpr] -> Bool
`sameKey` [SExpr]
key')]
sameKey :: [SExpr] -> [SExpr] -> Bool
sameKey :: [SExpr] -> [SExpr] -> Bool
sameKey as :: [SExpr]
as bs :: [SExpr]
bs
| [SExpr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SExpr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
bs = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (SExpr -> SExpr -> Bool) -> [SExpr] -> [SExpr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SExpr -> SExpr -> Bool
same [SExpr]
as [SExpr]
bs
| Bool
True = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "Data.SBV: Differing length of key received in chainAssigns: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([SExpr], [SExpr]) -> String
forall a. Show a => a -> String
show ([SExpr]
as, [SExpr]
bs)
same :: SExpr -> SExpr -> Bool
same :: SExpr -> SExpr -> Bool
same x :: SExpr
x y :: SExpr
y = case (SExpr
x, SExpr
y) of
(ECon a :: String
a, ECon b :: String
b) -> String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
b
(ENum (i :: Integer
i, _), ENum (j :: Integer
j, _)) -> Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j
(EReal a :: AlgReal
a, EReal b :: AlgReal
b) -> AlgReal -> AlgReal -> Bool
algRealStructuralEqual AlgReal
a AlgReal
b
(EFloat f1 :: Float
f1, EFloat f2 :: Float
f2) -> Float -> Float -> Bool
forall a. RealFloat a => a -> a -> Bool
fpIsEqualObjectH Float
f1 Float
f2
(EDouble d1 :: Double
d1, EDouble d2 :: Double
d2) -> Double -> Double -> Bool
forall a. RealFloat a => a -> a -> Bool
fpIsEqualObjectH Double
d1 Double
d2
(EApp as :: [SExpr]
as, EApp bs :: [SExpr]
bs) -> [SExpr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SExpr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
bs Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((SExpr -> SExpr -> Bool) -> [SExpr] -> [SExpr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SExpr -> SExpr -> Bool
same [SExpr]
as [SExpr]
bs)
(e1 :: SExpr
e1, e2 :: SExpr
e2) -> if SExpr -> Int
eRank SExpr
e1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== SExpr -> Int
eRank SExpr
e2
then String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "Data.SBV: You've found a bug in SBV! Please report: SExpr(same): " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (SExpr, SExpr) -> String
forall a. Show a => a -> String
show (SExpr
e1, SExpr
e2)
else Bool
False
eRank :: SExpr -> Int
eRank :: SExpr -> Int
eRank ECon{} = 0
eRank ENum{} = 1
eRank EReal{} = 2
eRank EFloat{} = 3
eRank EDouble{} = 4
eRank EApp{} = 5
{-# ANN chainAssigns ("HLint: ignore Redundant if" :: String) #-}