-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Utils.SExpr
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Parsing of S-expressions (mainly used for parsing SMT-Lib get-value output)
-----------------------------------------------------------------------------

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

-- | ADT S-Expression format, suitable for representing get-model output of SMT-Lib
data SExpr = ECon    String
           | ENum    (Integer, Maybe Int)  -- Second argument is how wide the field was in bits, if known. Useful in FP parsing.
           | 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

-- | Extremely simple minded tokenizer, good for our use model.
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, [])         -- Strictly speaking, this is the unterminated string case; but let's ignore
                 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)

       -- characters that can stop the current token
       -- it is *crucial* that this list contains every character
       -- we can match in one of the previous cases!
       stopper :: String
stopper = " \t\n():|\""

-- | The balance of parens in this string. If 0, this means it's a legit line!
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

-- | Parse a string into an SExpr, potentially failing with an error message
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

        -- simplify numbers and root-obj values
        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   -- ignore the "casting"
        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   -- ignore the "casting"
        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)

        -- bit-vector value as CVC4 prints: (_ bv0 16) for instance
        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

        -- Deal with CVC4's approximate reals
        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

        -- NB. Note the lengths on the mantissa for the following two are 23/52; not 24/53!
        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)  -- kx^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)  -- kx
        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)  --  x^p
        getCoeff (                                        ECon "x"          ) = (Integer, Integer) -> Either String (Integer, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (    1,     1)  --  x
        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)  -- k
        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

-- | Parses the Z3 floating point formatted numbers like so: 1.321p5/1.2123e9 etc.
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

-- | Convert an (s, e, m) triple to a float value
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

-- | Convert an (s, e, m) triple to a float value
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

-- | Special constants of SMTLib2 and their internal translation. Mainly
-- rounding modes for now.
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)
                 ]

-- | Parse a function like value. These come in two flavors: Either in the form of
-- a store-expression or a lambda-expression. So we handle both here.
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         -- out-of luck. NB. This is where we would add support for other solvers!

-- | Parse a lambda expression, most likely z3 specific. There's some guess work
-- involved here regarding how z3 produces lambda-expressions; while we try to
-- be flexible, this is certainly not a full fledged parser. But hopefully it'll
-- cover everything z3 will throw at it.
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

                -- Catch cases like: x = a)
                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])

                -- Catch cases like: not x
                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])

                -- Catch (or x y z..)
                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

                -- Catch (and x y z..)
                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

                -- z3 sometimes puts together a bunch of booleans as final expression,
                -- see if we can catch that.
                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

                -- Otherwise, just treat it as an "unknown" arbitrary expression
                -- as the default. It could be something arbitrary of course, but it's
                -- too complicated to parse; and hopefully this is good enough.
                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 takes the condition of an ite, and returns precisely what match is done to the parameters
                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 a dictionary of assignments from the scrutinee
                        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

                        -- See if we can figure out what z3 is telling us; hopefully this
                        -- mapping covers everything we can see:
                        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) -- boolean negation, require it to be false
                        grok (ECon v :: String
v)                     = (String, SExpr) -> Maybe (String, SExpr)
forall a. a -> Maybe a
Just (String
v, SExpr
true)  -- boolean identity, require it to be true

                        -- Tough luck, we couldn't understand:
                        grok _ = Maybe (String, SExpr)
forall a. Maybe a
Nothing

-- | Parse a series of associations in the array notation, things that look like:
--
--     (store (store ((as const Array) 12) 3 5 9) 5 6 75)
--
-- This is (most likely) entirely Z3 specific. So, we might have to tweak it for other
-- solvers; though it isn't entirely clear how to do that as we do not know what solver
-- we're using here. The trick is to handle all of possible SExpr's we see.
-- We'll cross that bridge when we get to it.
--
-- NB. In case there's no "constraint" on the UI, Z3 produces the self-referential model:
--
--    (x (_ as-array x))
--
-- So, we specifically handle that here, by returning a Left of that name.
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

-- | Turn a sequence of left-right chain assignments (condition + free) into a single chain
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

        -- If we get into a case like this:
        --
        --     (store (store a 1 2) 1 3)
        --
        -- then we need to drop the 1->2 assignment!
        --
        -- The way we parse these, the first assignment wins.
        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)

        -- We don't want to derive Eq; as this is more careful on floats and such
        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
        -- Defensive programming: It's too long to list all pair up, so we use this function and
        -- GHC's pattern-match completion warning to catch cases we might've forgotten. If
        -- you ever get the error line above fire, because you must've disabled the pattern-match
        -- completion check warning! Shame on you.
        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) #-}