-----------------------------------------------------------------------------
-- |
-- 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, makeHaskellFunction
                            , unQuote, simplifyECon
                            , nameSupply
                            ) where

import Data.Bits   (setBit, testBit)
import Data.Char   (isDigit, ord, isSpace)
import Data.Either (partitionEithers)
import Data.List   (isPrefixOf, nubBy, intercalate)
import Data.Maybe  (fromMaybe, listToMaybe)
import Data.Word   (Word32, Word64)

import Control.Monad (foldM)

import Numeric    (readInt, readSigned, readDec, readHex, fromRat)

import Data.SBV.Core.AlgReals
import Data.SBV.Core.SizedFloats
import Data.SBV.Core.Data (nan, infinity, RoundingMode(..))

import Data.SBV.Utils.Lib (unBar, unQuote, nameSupply)

import Data.SBV.Utils.Numeric (fpIsEqualObjectH, 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
           | EFloatingPoint FP
           | 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
$cshowsPrec :: Int -> SExpr -> ShowS
showsPrec :: Int -> SExpr -> ShowS
$cshow :: SExpr -> String
show :: SExpr -> String
$cshowList :: [SExpr] -> ShowS
showList :: [SExpr] -> ShowS
Show

-- | Extremely simple minded tokenizer, good for our use model.
tokenize :: String -> [String]
tokenize :: String -> [String]
tokenize String
inp = String -> [String] -> [String]
go String
inp []
 where go :: String -> [String] -> [String]
go String
"" [String]
sofar = [String] -> [String]
forall a. [a] -> [a]
reverse [String]
sofar

       go (Char
c:String
cs) [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 (Char
'(':String
cs) [String]
sofar = String -> [String] -> [String]
go String
cs (String
"(" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
       go (Char
')':String
cs) [String]
sofar = String -> [String] -> [String]
go String
cs (String
")" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)

       go (Char
':':Char
':':String
cs) [String]
sofar = String -> [String] -> [String]
go String
cs (String
"::" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)

       go (Char
':':String
cs) [String]
sofar = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
stopper) String
cs of
                            (String
pre, String
rest) -> String -> [String] -> [String]
go String
rest ((Char
':'Char -> ShowS
forall a. a -> [a] -> [a]
:String
pre) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)

       go (Char
'|':String
r) [String]
sofar = let wrap :: ShowS
wrap String
s = Char
'|' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"
                          in case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'|') String
r of
                               (String
pre, Char
'|':String
rest) -> String -> [String] -> [String]
go String
rest (ShowS
wrap String
pre String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
                               (String
pre, String
rest)     -> String -> [String] -> [String]
go String
rest (ShowS
wrap String
pre String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)

       go (Char
';':String
r) [String]
sofar = String -> [String] -> [String]
go (Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
1 ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\n') String
r)) [String]
sofar

       go (Char
'"':String
r) [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 []             String
acc = (ShowS
forall a. [a] -> [a]
reverse String
acc, [])         -- Strictly speaking, this is the unterminated string case; but let's ignore
                 grabString (Char
'"' :Char
'"':String
cs)  String
acc = String -> String -> (String, String)
grabString String
cs (Char
'"' Char -> ShowS
forall a. a -> [a] -> [a]
:String
acc)
                 grabString (Char
'"':String
cs)       String
acc = (ShowS
forall a. [a] -> [a]
reverse String
acc, String
cs)
                 grabString (Char
c:String
cs)         String
acc = String -> String -> (String, String)
grabString String
cs (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:String
acc)

                 (String
str, String
rest) = String -> String -> (String, String)
grabString String
r []
                 finalStr :: String
finalStr    = Char
'"' Char -> ShowS
forall a. a -> [a] -> [a]
: String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\""

       go String
cs [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
                       (String
pre, 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 = String
" \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 Int
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 (String
"(" : [String]
rest) = Int -> [String] -> Int
go (Int
balanceInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [String]
rest
        go !Int
balance (String
")" : [String]
rest) = Int -> [String] -> Int
go (Int
balanceInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [String]
rest
        go !Int
balance (String
_   : [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 String
inp = do (sexp, extras) <- [String] -> Either String (SExpr, [String])
parse [String]
inpToks
                    if null extras
                       then case sexp of
                              EApp [ECon String
"error", ECon 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
$ String
"Solver returned an error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
er
                              SExpr
_                            -> SExpr -> Either String SExpr
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return SExpr
sexp

                       else die "Extra tokens after valid input"
  where inpToks :: [String]
inpToks = String -> [String]
tokenize String
inp

        die :: String -> Either String b
die 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
$  String
"SBV.Provers.SExpr: Failed to parse S-Expr: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
w
                     String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n*** Input : <" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
inp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"

        parse :: [String] -> Either String (SExpr, [String])
parse []         = String -> Either String (SExpr, [String])
forall {b}. String -> Either String b
die String
"ran out of tokens"
        parse (String
"(":[String]
toks) = do (f, r) <- [String] -> [SExpr] -> Either String ([SExpr], [String])
parseApp [String]
toks []
                              f' <- cvt (EApp f)
                              return (f', r)
        parse (String
")":[String]
_)    = String -> Either String (SExpr, [String])
forall {b}. String -> Either String b
die String
"extra tokens after close paren"
        parse [String
tok]      = do t <- String -> Either String SExpr
pTok String
tok
                              return (t, [])
        parse [String]
_          = String -> Either String (SExpr, [String])
forall {b}. String -> Either String b
die String
"ill-formed s-expr"

        parseApp :: [String] -> [SExpr] -> Either String ([SExpr], [String])
parseApp []         [SExpr]
_     = String -> Either String ([SExpr], [String])
forall {b}. String -> Either String b
die String
"failed to grab s-expr application"
        parseApp (String
")":[String]
toks) [SExpr]
sofar = ([SExpr], [String]) -> Either String ([SExpr], [String])
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return ([SExpr] -> [SExpr]
forall a. [a] -> [a]
reverse [SExpr]
sofar, [String]
toks)
        parseApp (String
"(":[String]
toks) [SExpr]
sofar = do (f, r) <- [String] -> Either String (SExpr, [String])
parse (String
"("String -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
toks)
                                       parseApp r (f : sofar)
        parseApp (String
tok:[String]
toks) [SExpr]
sofar = do t <- String -> Either String SExpr
pTok String
tok
                                       parseApp toks (t : sofar)

        pTok :: String -> Either String SExpr
pTok String
"false" = SExpr -> Either String SExpr
forall a. a -> Either String a
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
0, Maybe Int
forall a. Maybe a
Nothing)
        pTok String
"true"  = SExpr -> Either String SExpr
forall a. a -> Either String a
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
1, Maybe Int
forall a. Maybe a
Nothing)

        pTok (Char
'0':Char
'b':String
r)                                 = Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum (Int -> Maybe Int
forall a. a -> Maybe a
Just (String -> Int
forall a. [a] -> 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 Integer
2 (Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"01") (\Char
c -> Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') String
r
        pTok (Char
'b':Char
'v':String
r) | Bool -> Bool
not (String -> Bool
forall a. [a] -> 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
/= Char
'[') String
r)
        pTok (Char
'#':Char
'b':String
r)                                 = Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum (Int -> Maybe Int
forall a. a -> Maybe a
Just (String -> Int
forall a. [a] -> 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 Integer
2 (Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"01") (\Char
c -> Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') String
r
        pTok (Char
'#':Char
'x':String
r)                                 = Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int
4 Int -> Int -> Int
forall a. Num a => a -> a -> a
* String -> Int
forall a. [a] -> 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 String
n | String -> Bool
possiblyNum String
n = if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
intChar String
n then 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 -> ReadS Integer
forall a. Real a => ReadS a -> ReadS a
readSigned ReadS Integer
forall a. (Eq a, Num a) => ReadS a
readDec String
n else String -> Either String SExpr
forall {m :: * -> *}. Monad m => String -> m SExpr
getReal String
n
        pTok String
n                 = SExpr -> Either String SExpr
forall a. a -> Either String a
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)

        -- crude, but effective!
        possiblyNum :: String -> Bool
possiblyNum String
s = case String
s of
                          String
""        -> Bool
False
                          (Char
'-':Char
c:String
_) -> Char -> Bool
isDigit Char
c
                          (Char
c:String
_)     -> Char -> Bool
isDigit Char
c

        intChar :: Char -> Bool
intChar Char
c = Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'-' Bool -> Bool -> Bool
|| Char -> Bool
isDigit Char
c

        mkNum :: Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum Maybe Int
l [(Integer
n, String
"")] = SExpr -> Either String SExpr
forall a. a -> Either String a
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 Maybe Int
_ [(Integer, String)]
_         = String -> Either String SExpr
forall {b}. String -> Either String b
die String
"cannot read number"

        getReal :: String -> m SExpr
getReal String
n = SExpr -> m SExpr
forall a. a -> m a
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 -> 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. HasCallStack => [a] -> [a]
init String
n

        -- simplify numbers and root-obj values
        cvt :: SExpr -> Either String SExpr
cvt (EApp [ECon String
"to_int",  EReal AlgReal
a])                       = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"to_real", EReal AlgReal
a])                       = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"/", EReal AlgReal
a, EReal AlgReal
b])                    = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"/", EReal AlgReal
a, ENum  (Integer, Maybe Int)
b])                    = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"/", ENum  (Integer, Maybe Int)
a, EReal AlgReal
b])                    = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"/", ENum  (Integer, Maybe Int)
a, ENum  (Integer, Maybe Int)
b])                    = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"-", EReal AlgReal
a])                             = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"-", ENum (Integer, Maybe Int)
a])                              = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"_", ENum (Integer, Maybe Int)
a, ENum (Integer, Maybe Int)
_b])                     = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"root-obj", EApp (ECon String
"+":[SExpr]
trms), ENum (Integer, Maybe Int)
k]) = do 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SExpr -> Either String (Integer, Integer)
getCoeff [SExpr]
trms
                                                                        return $ EReal $ mkPolyReal (Right (fst k, ts))
        cvt (EApp [ECon String
"as", SExpr
n, EApp [ECon String
"_", ECon String
"FloatingPoint", ENum (Integer
11, Maybe Int
_), ENum (Integer
53, Maybe Int
_)]]) = SExpr -> Either String SExpr
getDouble SExpr
n
        cvt (EApp [ECon String
"as", SExpr
n, EApp [ECon String
"_", ECon String
"FloatingPoint", ENum ( Integer
8, Maybe Int
_), ENum (Integer
24, Maybe Int
_)]]) = SExpr -> Either String SExpr
getFloat  SExpr
n
        cvt (EApp [ECon String
"as", SExpr
n, ECon String
"Float64"])                                                    = SExpr -> Either String SExpr
getDouble SExpr
n
        cvt (EApp [ECon String
"as", SExpr
n, ECon String
"Float32"])                                                    = SExpr -> Either String SExpr
getFloat  SExpr
n

        -- Deal with CVC4's approximate reals
        cvt x :: SExpr
x@(EApp [ECon String
"witness", EApp [EApp [ECon String
v, ECon String
"Real"]]
                                   , EApp [ECon String
"or", EApp [ECon String
"=", ECon String
v', SExpr
val], SExpr
_]]) | String
v String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
v'   = do
                                                approx <- SExpr -> Either String SExpr
cvt SExpr
val
                                                case approx of
                                                  ENum (Integer
s, Maybe Int
_) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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 AlgReal
aval  -> case AlgReal
aval of
                                                                   AlgRational Bool
_ Rational
r -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
                                                                   AlgReal
_               -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
                                                  SExpr
_           -> 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
$ String
"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

        -- Deal with CVC5's algebraic reals. This is very crude!
        cvt x :: SExpr
x@(EApp (ECon String
"_" : ECon String
"real_algebraic_number" : [SExpr]
rest)) =
            let isComma :: SExpr -> Bool
isComma (ECon String
",") = Bool
True
                isComma SExpr
_          = Bool
False

                get :: SExpr -> Either String Rational
get (ENum    (Integer
n, Maybe Int
_))               = Rational -> Either String Rational
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rational -> Either String Rational)
-> Rational -> Either String Rational
forall a b. (a -> b) -> a -> b
$ Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
                get (EReal   (AlgRational Bool
True Rational
r)) = Rational -> Either String Rational
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return Rational
r
                get (EFloat  Float
f)                    = Rational -> Either String Rational
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rational -> Either String Rational)
-> Rational -> Either String Rational
forall a b. (a -> b) -> a -> b
$ Float -> Rational
forall a. Real a => a -> Rational
toRational Float
f
                get (EDouble Double
d)                    = Rational -> Either String Rational
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rational -> Either String Rational)
-> Rational -> Either String Rational
forall a b. (a -> b) -> a -> b
$ Double -> Rational
forall a. Real a => a -> Rational
toRational Double
d
                get SExpr
t                              = String -> Either String Rational
forall {b}. String -> Either String b
die (String -> Either String Rational)
-> String -> Either String Rational
forall a b. (a -> b) -> a -> b
$ String
"Cannot get a CVC5 real-algebraic bound from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
t

            in case Int -> [SExpr] -> [SExpr]
forall a. Int -> [a] -> [a]
drop Int
1 ((SExpr -> Bool) -> [SExpr] -> [SExpr]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool) -> (SExpr -> Bool) -> SExpr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SExpr -> Bool
isComma) [SExpr]
rest) of
                [EApp [SExpr
n1, SExpr
n2], SExpr
_] -> do low  <- SExpr -> Either String Rational
get SExpr
n1
                                         high <- get n2
                                         return $ EReal $ AlgInterval (OpenPoint low) (OpenPoint high)
                [SExpr]
_                  -> 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
$ String
"Cannot parse a CVC5 real-algebraic number 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 String
"fp",    ENum (Integer
s, Just Int
1), ENum ( Integer
e, Just Int
8),  ENum (Integer
m, Just Int
23)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"fp",    ENum (Integer
s, Just Int
1), ENum ( Integer
e, Just Int
11), ENum (Integer
m, Just Int
52)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"fp",    ENum (Integer
s, Just Int
1), ENum ( Integer
e, Just Int
eb), ENum (Integer
m, Just Int
sb)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> (Integer, Int) -> (Integer, Int) -> FP
fpFromRawRep (Integer
s Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) (Integer
e, Int
eb) (Integer
m, Int
sbInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

        cvt (EApp [ECon String
"_",     ECon String
"NaN",       ENum ( Integer
8, Maybe Int
_),       ENum (Integer
24,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"_",     ECon String
"NaN",       ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"_",     ECon String
"NaN",       ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Int -> Int -> FP
fpNaN (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt (EApp [ECon String
"_",     ECon String
"+oo",       ENum ( Integer
8, Maybe Int
_),       ENum (Integer
24,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"_",     ECon String
"+oo",       ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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 String
"_",     ECon String
"+oo",       ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpInf Bool
False (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt (EApp [ECon String
"_",     ECon String
"-oo",       ENum ( Integer
8, Maybe Int
_),       ENum (Integer
24,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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
$ -Float
forall a. Floating a => a
infinity
        cvt (EApp [ECon String
"_",     ECon String
"-oo",       ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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
$ -Double
forall a. Floating a => a
infinity
        cvt (EApp [ECon String
"_",     ECon String
"-oo",       ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpInf Bool
True (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt (EApp [ECon String
"_",     ECon String
"+zero",     ENum ( Integer
8, Maybe Int
_),       ENum (Integer
24,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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
0
        cvt (EApp [ECon String
"_",     ECon String
"+zero",     ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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
0
        cvt (EApp [ECon String
"_",     ECon String
"+zero",     ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpZero Bool
False (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt (EApp [ECon String
"_",     ECon String
"-zero",     ENum ( Integer
8, Maybe Int
_),       ENum (Integer
24,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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
$ -Float
0
        cvt (EApp [ECon String
"_",     ECon String
"-zero",     ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
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
$ -Double
0
        cvt (EApp [ECon String
"_",     ECon String
"-zero",     ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = SExpr -> Either String SExpr
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpZero Bool
True (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt SExpr
x                                                                                        = SExpr -> Either String SExpr
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return SExpr
x

        getCoeff :: SExpr -> Either String (Integer, Integer)
getCoeff (EApp [ECon String
"*", ENum (Integer, Maybe Int)
k, EApp [ECon String
"^", ECon String
"x", ENum (Integer, Maybe Int)
p]]) = (Integer, Integer) -> Either String (Integer, Integer)
forall a. a -> Either String a
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 String
"*", ENum (Integer, Maybe Int)
k,                 ECon String
"x"        ] ) = (Integer, Integer) -> Either String (Integer, Integer)
forall a. a -> Either String a
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
1)  -- kx
        getCoeff (                        EApp [ECon String
"^", ECon String
"x", ENum (Integer, Maybe Int)
p] ) = (Integer, Integer) -> Either String (Integer, Integer)
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (    Integer
1, (Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
p)  --  x^p
        getCoeff (                                        ECon String
"x"          ) = (Integer, Integer) -> Either String (Integer, Integer)
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (    Integer
1,     Integer
1)  --  x
        getCoeff (                ENum (Integer, Maybe Int)
k                                    ) = (Integer, Integer) -> Either String (Integer, Integer)
forall a. a -> Either String a
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
0)  -- k
        getCoeff 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
$ String
"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 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
== Char
'+') String
s)) of
                                (String
"plusInfinity",  Maybe Double
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
                                (String
"minusInfinity", Maybe Double
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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)
                                (String
"oo",            Maybe Double
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
                                (String
"-oo",           Maybe Double
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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)
                                (String
"zero",          Maybe Double
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
0
                                (String
"-zero",         Maybe Double
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
0)
                                (String
"NaN",           Maybe Double
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
                                (String
_,               Just Double
v) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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, Maybe Double)
_               -> 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
$ String
"Cannot parse a double value from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
        getDouble (EApp [SExpr
_, SExpr
s, SExpr
_, SExpr
_]) = SExpr -> Either String SExpr
getDouble SExpr
s
        getDouble (EReal AlgReal
r) = SExpr -> Either String SExpr
forall a. a -> Either String a
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 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
$ String
"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 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
== Char
'+') String
s)) of
                                (String
"plusInfinity",  Maybe Float
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
                                (String
"minusInfinity", Maybe Float
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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)
                                (String
"oo",            Maybe Float
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
                                (String
"-oo",           Maybe Float
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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)
                                (String
"zero",          Maybe Float
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
0
                                (String
"-zero",         Maybe Float
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
0)
                                (String
"NaN",           Maybe Float
_     ) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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
                                (String
_,               Just Float
v) -> SExpr -> Either String SExpr
forall a. a -> Either String a
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, Maybe Float)
_               -> 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
$ String
"Cannot parse a float value from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
        getFloat (EReal AlgReal
r)  = SExpr -> Either String SExpr
forall a. a -> Either String a
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 [SExpr
_, SExpr
s, SExpr
_, SExpr
_]) = SExpr -> Either String SExpr
getFloat SExpr
s
        getFloat 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
$ String
"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 :: forall a. (Read a, RealFloat a) => String -> Maybe a
rdFP String
s = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"pe") String
s of
           (String
m, Char
'p':String
e) -> String -> Maybe a
forall {a}. Read a => String -> Maybe a
rd String
m Maybe a -> (a -> Maybe a) -> Maybe a
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
m' -> String -> Maybe a
forall {a}. Read a => String -> Maybe a
rd String
e Maybe a -> (a -> Maybe a) -> Maybe a
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
e' -> a -> Maybe a
forall a. 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
* ( a
2 a -> a -> a
forall a. Floating a => a -> a -> a
** a
e')
           (String
m, Char
'e':String
e) -> String -> Maybe a
forall {a}. Read a => String -> Maybe a
rd String
m Maybe a -> (a -> Maybe a) -> Maybe a
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
m' -> String -> Maybe a
forall {a}. Read a => String -> Maybe a
rd String
e Maybe a -> (a -> Maybe a) -> Maybe a
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
e' -> a -> Maybe a
forall a. 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
* (a
10 a -> a -> a
forall a. Floating a => a -> a -> a
** a
e')
           (String
m, String
"")    -> String -> Maybe a
forall {a}. Read a => String -> Maybe a
rd String
m
           (String, String)
_          -> Maybe a
forall a. Maybe a
Nothing
 where rd :: String -> Maybe a
rd String
v = case ReadS a
forall a. Read a => ReadS a
reads String
v of
                [(a
n, String
"")] -> a -> Maybe a
forall a. a -> Maybe a
Just a
n
                [(a, String)]
_         -> 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 Integer
s Integer
e Integer
m = Word32 -> Float
wordToFloat Word32
w32
  where sign :: [Bool]
sign      = [Integer
s Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1]
        expt :: [Bool]
expt      = [Integer
e Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [ Int
7,  Int
6 .. Int
0]]
        mantissa :: [Bool]
mantissa  = [Integer
m Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [Int
22, Int
21 .. Int
0]]
        positions :: [Int]
positions = [Int
i | (Int
i, Bool
b) <- [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
31, Int
30 .. Int
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 a b. (a -> b -> b) -> b -> [a] -> b
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) (Word32
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 Integer
s Integer
e Integer
m = Word64 -> Double
wordToDouble Word64
w64
  where sign :: [Bool]
sign      = [Integer
s Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1]
        expt :: [Bool]
expt      = [Integer
e Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [Int
10,  Int
9 .. Int
0]]
        mantissa :: [Bool]
mantissa  = [Integer
m Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [Int
51, Int
50 .. Int
0]]
        positions :: [Int]
positions = [Int
i | (Int
i, Bool
b) <- [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
63, Int
62 .. Int
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 a b. (a -> b -> b) -> b -> [a] -> b
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) (Word64
0::Word64) [Int]
positions

-- | Special constants of SMTLib2 and their internal translation. Mainly
-- rounding modes for now.
constantMap :: String -> String
constantMap :: ShowS
constantMap 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 | ([String]
from, String
to) <- [([String], String)]
special, String
n String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
from])
 where special :: [([String], String)]
special = [ ([String
"RNE", String
"roundNearestTiesToEven"], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundNearestTiesToEven)
                 , ([String
"RNA", String
"roundNearestTiesToAway"], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundNearestTiesToAway)
                 , ([String
"RTP", String
"roundTowardPositive"],    RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundTowardPositive)
                 , ([String
"RTN", String
"roundTowardNegative"],    RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundTowardNegative)
                 , ([String
"RTZ", String
"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 SExpr
e
  | Just ([([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 ([([SExpr], SExpr)], SExpr)
r <- SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseSetLambda         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 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 set-lambda expression, which is literally a lambda function, that might look like this:
--        (lambda ((x!1 String))
--          (or (not (or (= x!1 "o") (= x!1 "l") (= x!1 "e") (= x!1 "h")))
--              (= x!1 "o")
--              (= x!1 "l")
--              (= x!1 "e")
--              (= x!1 "h")))
--   For this, we do a little bit of an interpretative dance to see if we can "construct" the necesary expression.
--
--   In parsed form:
--      EApp [ECon "lambda",EApp [EApp [ECon "x!1",ECon "String"]],EApp [ECon "not",EApp [ECon "or",EApp [ECon "=",ECon "x!1",ECon "\"e\""],EApp [ECon "=",ECon "x!1",ECon "\"l\""]]]]
--
--   This is by no means comprehensive, and is quite crude, but hopefully covers the cases we see in practice.
parseSetLambda :: SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseSetLambda :: SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseSetLambda SExpr
funExpr = case SExpr
funExpr of
                               EApp [l :: SExpr
l@(ECon String
"lambda"), bv :: SExpr
bv@(EApp [EApp [ECon String
_, SExpr
_]]), SExpr
body] -> (SExpr -> SExpr) -> SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
go (\SExpr
bd -> [SExpr] -> SExpr
EApp [SExpr
l, SExpr
bv, SExpr
bd]) SExpr
body
                               SExpr
_                                                            -> Maybe ([([SExpr], SExpr)], SExpr)
forall a. Maybe a
Nothing
  where go :: (SExpr -> SExpr) -> SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
go SExpr -> SExpr
mkLambda = SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
build
         where build :: SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
build (EApp [ECon String
"not",  SExpr
rest      ]) =         ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
neg (([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr))
-> Maybe ([([SExpr], SExpr)], SExpr)
-> Maybe ([([SExpr], SExpr)], SExpr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<      SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
build SExpr
rest
               build (EApp (ECon String
"or"  : rest :: [SExpr]
rest@(SExpr
_:[SExpr]
_))) = (([([SExpr], SExpr)], SExpr)
 -> ([([SExpr], SExpr)], SExpr)
 -> Maybe ([([SExpr], SExpr)], SExpr))
-> [([([SExpr], SExpr)], SExpr)]
-> Maybe ([([SExpr], SExpr)], SExpr)
forall {m :: * -> *} {a}. Monad m => (a -> a -> m a) -> [a] -> m a
foldM1 ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
disj ([([([SExpr], SExpr)], SExpr)]
 -> Maybe ([([SExpr], SExpr)], SExpr))
-> Maybe [([([SExpr], SExpr)], SExpr)]
-> Maybe ([([SExpr], SExpr)], SExpr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (SExpr -> Maybe ([([SExpr], SExpr)], SExpr))
-> [SExpr] -> Maybe [([([SExpr], SExpr)], SExpr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
build [SExpr]
rest
               build (EApp (ECon String
"and" : rest :: [SExpr]
rest@(SExpr
_:[SExpr]
_))) = (([([SExpr], SExpr)], SExpr)
 -> ([([SExpr], SExpr)], SExpr)
 -> Maybe ([([SExpr], SExpr)], SExpr))
-> [([([SExpr], SExpr)], SExpr)]
-> Maybe ([([SExpr], SExpr)], SExpr)
forall {m :: * -> *} {a}. Monad m => (a -> a -> m a) -> [a] -> m a
foldM1 ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
conj ([([([SExpr], SExpr)], SExpr)]
 -> Maybe ([([SExpr], SExpr)], SExpr))
-> Maybe [([([SExpr], SExpr)], SExpr)]
-> Maybe ([([SExpr], SExpr)], SExpr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (SExpr -> Maybe ([([SExpr], SExpr)], SExpr))
-> [SExpr] -> Maybe [([([SExpr], SExpr)], SExpr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
build [SExpr]
rest
               build SExpr
other                            = SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseLambdaExpression (SExpr -> SExpr
mkLambda SExpr
other)

        -- We're guaranteed by above construction that foldM1 will never take an empty list (due to rest@(_:_) pattern match.)
        foldM1 :: (a -> a -> m a) -> [a] -> m a
foldM1 a -> a -> m a
_ []     = String -> m a
forall a. HasCallStack => String -> a
error String
"Data.SBV.parseSetLambda: Impossible happened; empty arg to foldM1"
        foldM1 a -> a -> m a
f (a
x:[a]
xs) = (a -> a -> m a) -> a -> [a] -> m a
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM a -> a -> m a
f a
x [a]
xs

        checkBool :: SExpr -> Bool
checkBool (ENum (Integer
1, Maybe Int
Nothing)) = Bool
True
        checkBool (ENum (Integer
0, Maybe Int
Nothing)) = Bool
True
        checkBool SExpr
_                   = Bool
False

        negBool :: SExpr -> SExpr
negBool (ENum (Integer
1, Maybe Int
Nothing)) = (Integer, Maybe Int) -> SExpr
ENum (Integer
0, Maybe Int
forall a. Maybe a
Nothing)
        negBool SExpr
_                   = (Integer, Maybe Int) -> SExpr
ENum (Integer
1, Maybe Int
forall a. Maybe a
Nothing)

        orBool :: SExpr -> SExpr -> SExpr
orBool t :: SExpr
t@(ENum (Integer
1, Maybe Int
Nothing)) SExpr
_                      = SExpr
t
        orBool SExpr
_                     t :: SExpr
t@(ENum (Integer
1, Maybe Int
Nothing))  = SExpr
t
        orBool SExpr
_ SExpr
_                                          = (Integer, Maybe Int) -> SExpr
ENum (Integer
0, Maybe Int
forall a. Maybe a
Nothing)

        andBool :: SExpr -> SExpr -> SExpr
andBool f :: SExpr
f@(ENum (Integer
0, Maybe Int
Nothing)) SExpr
_                     = SExpr
f
        andBool SExpr
_                     f :: SExpr
f@(ENum (Integer
0, Maybe Int
Nothing)) = SExpr
f
        andBool SExpr
_ SExpr
_                                         = (Integer, Maybe Int) -> SExpr
ENum (Integer
1, Maybe Int
forall a. Maybe a
Nothing)

        neg :: ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
        neg :: ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
neg ([([SExpr], SExpr)]
rows, SExpr
dflt)
         | (SExpr -> Bool) -> [SExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SExpr -> Bool
checkBool (SExpr
dflt SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: (([SExpr], SExpr) -> SExpr) -> [([SExpr], SExpr)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map ([SExpr], SExpr) -> SExpr
forall a b. (a, b) -> b
snd [([SExpr], SExpr)]
rows) = ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
forall a. a -> Maybe a
Just ([([SExpr]
e, SExpr -> SExpr
negBool SExpr
r) | ([SExpr]
e, SExpr
r) <- [([SExpr], SExpr)]
rows], SExpr -> SExpr
negBool SExpr
dflt)
         | Bool
True                                = Maybe ([([SExpr], SExpr)], SExpr)
forall a. Maybe a
Nothing

        disj, conj :: ([([SExpr], SExpr)], SExpr) -> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
        disj :: ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
disj = (SExpr -> SExpr -> SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> Maybe ([([SExpr], SExpr)], SExpr)
bin SExpr -> SExpr -> SExpr
orBool
        conj :: ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
conj = (SExpr -> SExpr -> SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> Maybe ([([SExpr], SExpr)], SExpr)
bin SExpr -> SExpr -> SExpr
andBool

        bin :: (SExpr -> SExpr -> SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> Maybe ([([SExpr], SExpr)], SExpr)
bin SExpr -> SExpr -> SExpr
f rd1 :: ([([SExpr], SExpr)], SExpr)
rd1@([([SExpr], SExpr)]
rows1, SExpr
dflt1) rd2 :: ([([SExpr], SExpr)], SExpr)
rd2@([([SExpr], SExpr)]
rows2, SExpr
dflt2)
          | (SExpr -> Bool) -> [SExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SExpr -> Bool
checkBool (SExpr
dflt1 SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: SExpr
dflt2 SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: (([SExpr], SExpr) -> SExpr) -> [([SExpr], SExpr)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map ([SExpr], SExpr) -> SExpr
forall a b. (a, b) -> b
snd [([SExpr], SExpr)]
rows1 [SExpr] -> [SExpr] -> [SExpr]
forall a. [a] -> [a] -> [a]
++ (([SExpr], SExpr) -> SExpr) -> [([SExpr], SExpr)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map ([SExpr], SExpr) -> SExpr
forall a b. (a, b) -> b
snd [([SExpr], SExpr)]
rows2) = ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
forall a. a -> Maybe a
Just ((SExpr -> SExpr -> SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr)
forall {t} {t}.
(Show t, Show t) =>
(t -> t -> SExpr)
-> ([([SExpr], t)], t)
-> ([([SExpr], t)], t)
-> ([([SExpr], SExpr)], SExpr)
combine SExpr -> SExpr -> SExpr
f ([([SExpr], SExpr)], SExpr)
rd1 ([([SExpr], SExpr)], SExpr)
rd2)
          | Bool
True                                                           = Maybe ([([SExpr], SExpr)], SExpr)
forall a. Maybe a
Nothing

        -- Since we don't have equality over SExprs (can of worms!), we use "show" equality here. The ice is thin, but it works!
        combine :: (t -> t -> SExpr)
-> ([([SExpr], t)], t)
-> ([([SExpr], t)], t)
-> ([([SExpr], SExpr)], SExpr)
combine t -> t -> SExpr
f ([([SExpr], t)]
rows1, t
dflt1) ([([SExpr], t)]
rows2, t
dflt2) = ([([SExpr], SExpr)]
rows, t -> t -> SExpr
f t
dflt1 t
dflt2)
          where rows :: [([SExpr], SExpr)]
rows = ([SExpr] -> ([SExpr], SExpr)) -> [[SExpr]] -> [([SExpr], SExpr)]
forall a b. (a -> b) -> [a] -> [b]
map [SExpr] -> ([SExpr], SExpr)
calc ([[SExpr]] -> [([SExpr], SExpr)])
-> [[SExpr]] -> [([SExpr], SExpr)]
forall a b. (a -> b) -> a -> b
$ ([SExpr] -> [SExpr] -> Bool) -> [[SExpr]] -> [[SExpr]]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (\[SExpr]
x [SExpr]
y -> [SExpr] -> String
forall a. Show a => a -> String
show [SExpr]
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== [SExpr] -> String
forall a. Show a => a -> String
show [SExpr]
y) ((([SExpr], t) -> [SExpr]) -> [([SExpr], t)] -> [[SExpr]]
forall a b. (a -> b) -> [a] -> [b]
map ([SExpr], t) -> [SExpr]
forall a b. (a, b) -> a
fst [([SExpr], t)]
rows1 [[SExpr]] -> [[SExpr]] -> [[SExpr]]
forall a. [a] -> [a] -> [a]
++ (([SExpr], t) -> [SExpr]) -> [([SExpr], t)] -> [[SExpr]]
forall a b. (a -> b) -> [a] -> [b]
map ([SExpr], t) -> [SExpr]
forall a b. (a, b) -> a
fst [([SExpr], t)]
rows2)

                calc :: [SExpr] -> ([SExpr], SExpr)
                calc :: [SExpr] -> ([SExpr], SExpr)
calc [SExpr]
args = ([SExpr]
args, t -> t -> SExpr
f ([([SExpr], t)] -> t -> [SExpr] -> t
forall {a} {a} {p}.
(Show a, Show a, Show p) =>
[(a, p)] -> p -> a -> p
find [([SExpr], t)]
rows1 t
dflt1 [SExpr]
args) ([([SExpr], t)] -> t -> [SExpr] -> t
forall {a} {a} {p}.
(Show a, Show a, Show p) =>
[(a, p)] -> p -> a -> p
find [([SExpr], t)]
rows2 t
dflt2 [SExpr]
args))

                find :: [(a, p)] -> p -> a -> p
find [(a, p)]
rs p
d a
a = case [p
r | (a
v, p
r) <- [(a, p)]
rs, a -> String
forall a. Show a => a -> String
show a
v String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== a -> String
forall a. Show a => a -> String
show a
a] of
                               []  -> p
d
                               [p
x] -> p
x
                               [p]
x   -> String -> p
forall a. HasCallStack => String -> a
error (String -> p) -> String -> p
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Data.SBV.parseSetLambda: Impossible happened while combining rows."
                                                      , String
"   First row  :"   String -> ShowS
forall a. [a] -> [a] -> [a]
++ [([SExpr], t)] -> String
forall a. Show a => a -> String
show [([SExpr], t)]
rows1
                                                      , String
"   First dflt :"  String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
dflt1
                                                      , String
"   Second row :"  String -> ShowS
forall a. [a] -> [a] -> [a]
++ [([SExpr], t)] -> String
forall a. Show a => a -> String
show [([SExpr], t)]
rows2
                                                      , String
"   Second dflt:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
dflt2
                                                      , String
"   Looking for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a
                                                      , String
"Multiple matches found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [p] -> String
forall a. Show a => a -> String
show [p]
x
                                                      ]

-- | 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 SExpr
funExpr = case SExpr -> SExpr
squashLambdas SExpr
funExpr of
                                  EApp [ECon String
"lambda", EApp [SExpr]
params, SExpr
body] -> (SExpr -> Maybe (String, Bool))
-> [SExpr] -> Maybe [(String, Bool)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SExpr -> Maybe (String, Bool)
getParam [SExpr]
params Maybe [(String, Bool)]
-> ([(String, Bool)] -> Maybe [Either ([SExpr], SExpr) SExpr])
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([(String, Bool)]
 -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr])
-> SExpr
-> [(String, Bool)]
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [(String, Bool)] -> 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 a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Either ([SExpr], SExpr) SExpr]
-> Maybe ([([SExpr], SExpr)], SExpr)
chainAssigns
                                  SExpr
_                                       -> Maybe ([([SExpr], SExpr)], SExpr)
forall a. Maybe a
Nothing
  where -- convert (lambda p1 (lambda p2 body)) to (lambda (p1 ++ p2) body)
        squashLambdas :: SExpr -> SExpr
squashLambdas (EApp  [ECon String
"lambda", EApp [SExpr]
p1
                                           , EApp [ECon String
"lambda", EApp [SExpr]
p2, SExpr
body]])
                            = SExpr -> SExpr
squashLambdas (SExpr -> SExpr) -> SExpr -> SExpr
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"lambda", [SExpr] -> SExpr
EApp ([SExpr]
p1 [SExpr] -> [SExpr] -> [SExpr]
forall a. [a] -> [a] -> [a]
++ [SExpr]
p2), SExpr
body]
        squashLambdas SExpr
other = SExpr
other

        getParam :: SExpr -> Maybe (String, Bool)
getParam (EApp [ECon String
v, ECon String
ty]) = (String, Bool) -> Maybe (String, Bool)
forall a. a -> Maybe a
Just (String
v, String
ty String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"Bool")
        getParam (EApp [ECon String
v, SExpr
_      ]) = (String, Bool) -> Maybe (String, Bool)
forall a. a -> Maybe a
Just (String
v, Bool
False)
        getParam SExpr
_                        = Maybe (String, Bool)
forall a. Maybe a
Nothing

        lambda :: [(String, Bool)]  -- Bool is True if this is a boolean variable. Otherwise we don't keep track of the type
               -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
        lambda :: [(String, Bool)] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
lambda [(String, Bool)]
params 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 (Integer
1, Maybe Int
forall a. Maybe a
Nothing)
                false :: SExpr
false = (Integer, Maybe Int) -> SExpr
ENum (Integer
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 [Either ([SExpr], SExpr) SExpr]
sofar (EApp [ECon String
"ite", SExpr
selector, SExpr
thenBranch, SExpr
elseBranch])
                  = do s  <- SExpr -> Maybe [SExpr]
select SExpr
selector
                       tB <- go [] thenBranch
                       case cond s tB of
                          Just ([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 ([SExpr], SExpr)
_       -> Maybe [Either ([SExpr], SExpr) SExpr]
forall a. Maybe a
Nothing

                -- Catch cases like: x = a)
                go [Either ([SExpr], SExpr) SExpr]
sofar inner :: SExpr
inner@(EApp [ECon String
"=", SExpr
_, SExpr
_])
                  = [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go [Either ([SExpr], SExpr) SExpr]
sofar ([SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"ite", SExpr
inner, SExpr
true, SExpr
false])

                -- Catch cases like: not x
                go [Either ([SExpr], SExpr) SExpr]
sofar (EApp [ECon String
"not", SExpr
inner])
                  = [Either ([SExpr], SExpr) SExpr]
-> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
go [Either ([SExpr], SExpr) SExpr]
sofar ([SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"ite", SExpr
inner, SExpr
false, SExpr
true])

                -- Catch (or x y z..)
                go [Either ([SExpr], SExpr) SExpr]
sofar (EApp (ECon String
"or" : [SExpr]
elts))
                  = let xform :: [SExpr] -> SExpr
xform []     = SExpr
false
                        xform [SExpr
x]    = SExpr
x
                        xform (SExpr
x:[SExpr]
xs) = [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"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 [Either ([SExpr], SExpr) SExpr]
sofar (EApp (ECon String
"and" : [SExpr]
elts))
                  = let xform :: [SExpr] -> SExpr
xform []     = SExpr
true
                        xform [SExpr
x]    = SExpr
x
                        xform (SExpr
x:[SExpr]
xs) = [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"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 [Either ([SExpr], SExpr) SExpr]
sofar SExpr
e
                 | Just [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 [Either ([SExpr], SExpr) SExpr]
sofar 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 [SExpr]
s [Right SExpr
v] = ([SExpr], SExpr) -> Maybe ([SExpr], SExpr)
forall a. a -> Maybe a
Just ([SExpr]
s, SExpr
v)
                cond [SExpr]
_ [Either ([SExpr], SExpr) SExpr]
_         = 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 SExpr
e
                   | Just [(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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (String -> [(String, SExpr)] -> Maybe SExpr
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, SExpr)]
dict) [String]
paramNames
                   | Bool
True                    = Maybe [SExpr]
forall a. Maybe a
Nothing
                  where paramNames :: [String]
paramNames = ((String, Bool) -> String) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Bool) -> String
forall a b. (a, b) -> a
fst [(String, Bool)]
params

                        -- 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 String
"and" : [SExpr]
rest)) [(String, SExpr)]
sofar = let next :: SExpr -> Maybe [(String, SExpr)] -> Maybe [(String, SExpr)]
next SExpr
_ Maybe [(String, SExpr)]
Nothing  = Maybe [(String, SExpr)]
forall a. Maybe a
Nothing
                                                                     next SExpr
c (Just [(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 a b. (a -> b -> b) -> b -> [a] -> b
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 SExpr
expr [(String, SExpr)]
sofar | Just (String
v, SExpr
r) <- SExpr -> Maybe (String, SExpr)
grok SExpr
expr, String
v String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
paramNames = [(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 String
"=", ECon String
v, SExpr
r]) = (String, SExpr) -> Maybe (String, SExpr)
forall a. a -> Maybe a
Just (String
v, SExpr
r)
                        grok (EApp [ECon String
"=", SExpr
r, ECon String
v]) = (String, SExpr) -> Maybe (String, SExpr)
forall a. a -> Maybe a
Just (String
v, SExpr
r)
                        grok (EApp [ECon String
"not", ECon 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 String
v)                     = case String
v String -> [(String, Bool)] -> Maybe Bool
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, Bool)]
params of
                                                               Just Bool
True -> (String, SExpr) -> Maybe (String, SExpr)
forall a. a -> Maybe a
Just (String
v, SExpr
true)  -- boolean identity, require it to be true
                                                               Maybe Bool
_         -> Maybe (String, SExpr)
forall a. Maybe a
Nothing

                        -- Tough luck, we couldn't understand:
                        grok SExpr
_ = 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 String
"_", ECon String
"as-array", ECon 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 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 String
"as", ECon String
"const", ECon String
"Array"],            SExpr
defVal]) = [Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall a. a -> Maybe a
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 String
"as", ECon String
"const", EApp (ECon String
"Array" : [SExpr]
_)], SExpr
defVal]) = [Either ([SExpr], SExpr) SExpr]
-> Maybe [Either ([SExpr], SExpr) SExpr]
forall a. a -> Maybe a
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 String
"store" : SExpr
prev : [SExpr]
argsVal)) | [SExpr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
argsVal Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2             = do rest <- SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
vals SExpr
prev
                                                                                             return $ Left (init argsVal, last argsVal) : rest
          vals SExpr
_                                                                        = Maybe [Either ([SExpr], SExpr) SExpr]
forall a. Maybe a
Nothing

-- | Turn a sequence of left-right chain assignments (condition + free) into a single chain
-- NB. We make sure the results here are unique, i.e., there's only one assignment to each unique entry
chainAssigns :: [Either ([SExpr], SExpr) SExpr] -> Maybe ([([SExpr], SExpr)], SExpr)
chainAssigns :: [Either ([SExpr], SExpr) SExpr]
-> Maybe ([([SExpr], SExpr)], SExpr)
chainAssigns [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 ([([SExpr], SExpr)]
vs, [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 ([([SExpr], SExpr)], [b])
_         = 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.
        -- NB. I'm not sure if solvers actually would return duplicate assignments, but just being safe here. (i.e.,
        -- this duplication may actually never happen in practice.)
        checkDup :: [([SExpr], SExpr)] -> [([SExpr], SExpr)]
        checkDup :: [([SExpr], SExpr)] -> [([SExpr], SExpr)]
checkDup []              = []
        checkDup (a :: ([SExpr], SExpr)
a@([SExpr]
key, SExpr
_):[([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@([SExpr]
key', SExpr
_) <- [([SExpr], SExpr)]
as, Bool -> Bool
not ([SExpr]
key [SExpr] -> [SExpr] -> Bool
`sameKey` [SExpr]
key')]

        sameKey :: [SExpr] -> [SExpr] -> Bool
        sameKey :: [SExpr] -> [SExpr] -> Bool
sameKey [SExpr]
as [SExpr]
bs
          | [SExpr] -> Int
forall a. [a] -> 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 a. [a] -> 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
$ String
"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 SExpr
x SExpr
y = case (SExpr
x, SExpr
y) of
                     (ECon String
a,            ECon String
b)            -> String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
b
                     (ENum (Integer
i, Maybe Int
_),       ENum (Integer
j, Maybe Int
_))       -> Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j
                     (EReal AlgReal
a,           EReal AlgReal
b)           -> AlgReal -> AlgReal -> Bool
algRealStructuralEqual AlgReal
a AlgReal
b
                     (EFloat  Float
f1,        EFloat  Float
f2)        -> Float -> Float -> Bool
forall a. RealFloat a => a -> a -> Bool
fpIsEqualObjectH Float
f1 Float
f2
                     (EDouble Double
d1,        EDouble Double
d2)        -> Double -> Double -> Bool
forall a. RealFloat a => a -> a -> Bool
fpIsEqualObjectH Double
d1 Double
d2
                     (EFloatingPoint FP
a1, EFloatingPoint FP
a2) -> FP -> FP -> Bool
forall a. RealFloat a => a -> a -> Bool
fpIsEqualObjectH FP
a1 FP
a2
                     (EApp [SExpr]
as,           EApp [SExpr]
bs)           -> [SExpr] -> Int
forall a. [a] -> 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 a. [a] -> 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)
                     (SExpr
e1,                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
$ String
"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{}           = Int
0
        eRank ENum{}           = Int
1
        eRank EReal{}          = Int
2
        eRank EFloat{}         = Int
3
        eRank EFloatingPoint{} = Int
4
        eRank EDouble{}        = Int
5
        eRank EApp{}           = Int
6

-- Turn
--  "((F (lambda ((x!1 Int)) (+ 3 (* 2 x!1)))))"
---  into
--  "F x = 3 + 2 * x"
-- if we can. We try but don't push too hard! This is only used for display purposes.
--
-- This isn't very fool-proof; can be confused if there are binding constructs etc.
-- Also, the generated text isn't necessarily fully Haskell acceptable.
-- But it seems to do an OK job for most common use cases.
makeHaskellFunction :: String -> String -> Bool -> Maybe [String] -> Maybe String
makeHaskellFunction :: String -> String -> Bool -> Maybe [String] -> Maybe String
makeHaskellFunction String
resp String
nm Bool
isCurried Maybe [String]
mbArgs
   = case String -> Either String SExpr
parseSExpr String
resp of
       Right (EApp [EApp [ECon String
o, SExpr
e]]) | String
o String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm -> do (args, bd) <- SExpr -> Maybe ([String], String)
lambda SExpr
e
                                                       let params | Bool
isCurried = [String] -> String
unwords [String]
args
                                                                  | Bool
True      = Char
'(' Char -> ShowS
forall a. a -> [a] -> [a]
: String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
args String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
                                                       return $ unBar nm ++ " " ++ params ++ " = " ++ bd
       Either String SExpr
_                                         -> Maybe String
forall a. Maybe a
Nothing

  where -- infinite supply of names; starting with the ones we're given
        preSupply :: [String]
preSupply = [String] -> Maybe [String] -> [String]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [String]
mbArgs

        lambda :: SExpr -> Maybe ([String], String)
        lambda :: SExpr -> Maybe ([String], String)
lambda (EApp [ECon String
"lambda", EApp [SExpr]
args, SExpr
bd]) = do as <- (SExpr -> Maybe String) -> [SExpr] -> Maybe [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SExpr -> Maybe String
getArg [SExpr]
args
                                                          let env = [String] -> [String] -> [(String, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
as ([String] -> [String]
nameSupply [String]
preSupply)
                                                          pure (map snd env, hprint env bd)
        lambda SExpr
_                                     = Maybe ([String], String)
forall a. Maybe a
Nothing

        getArg :: SExpr -> Maybe String
getArg (EApp [ECon String
argName, SExpr
_]) = String -> Maybe String
forall a. a -> Maybe a
Just String
argName
        getArg SExpr
_                        = Maybe String
forall a. Maybe a
Nothing

-- | z3 prints uninterpreted values like this: T!val!4 or T_val_4. Turn that into T_4
simplifyECon :: String -> String
simplifyECon :: ShowS
simplifyECon String
"" = String
""
simplifyECon (Char
'!':Char
'v':Char
'a':Char
'l':Char
'!':String
rest) = Char
'_' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
simplifyECon String
rest
simplifyECon (Char
'_':Char
'v':Char
'a':Char
'l':Char
'_':String
rest) = Char
'_' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
simplifyECon String
rest
simplifyECon (Char
c:String
cs) = Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
simplifyECon String
cs

-- Print as a Haskell expression, with minimal parens.
-- This isn't fool-proof; but it does an OK job
hprint :: [(String, String)] -> SExpr -> String
hprint :: [(String, String)] -> SExpr -> String
hprint [(String, String)]
env = Int -> SExpr -> String
forall {a}. (Ord a, Num a) => a -> SExpr -> String
go (Int
0 :: Int)
  where go :: a -> SExpr -> String
go a
p SExpr
e = case SExpr
e of
                   ECon String
n | Just String
a <- String
n String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, String)]
env -> String
a
                          | Bool
True                     -> ShowS
simplifyECon String
n
                   ENum (Integer
i, Maybe Int
_)       -> Integer -> String
forall a. Show a => a -> String
cnst Integer
i
                   EReal  AlgReal
a          -> AlgReal -> String
forall a. Show a => a -> String
cnst AlgReal
a
                   EFloat Float
f          -> Float -> String
forall a. Show a => a -> String
cnst Float
f
                   EFloatingPoint FP
f  -> FP -> String
forall a. Show a => a -> String
cnst FP
f
                   EDouble Double
f         -> Double -> String
forall a. Show a => a -> String
cnst Double
f

                   -- Handle lets
                   EApp [ECon String
"let", EApp [SExpr]
binders, SExpr
rhs] ->
                       let getBind :: SExpr -> String
getBind (EApp [ECon String
nm, SExpr
def]) = ShowS
simplifyECon String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++  a -> SExpr -> String
go a
0 SExpr
def
                           getBind SExpr
bnd                   = a -> SExpr -> String
go a
0 SExpr
bnd

                           binds :: String
binds = Char
'{' Char -> ShowS
forall a. a -> [a] -> [a]
: String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"; " ((SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
getBind [SExpr]
binders) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
                       in Bool -> ShowS
parenIf (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
1) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"let " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
binds String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> SExpr -> String
go a
0 SExpr
rhs

                   -- few simps
                   EApp [ECon String
"not", EApp [ECon String
">=", SExpr
a, SExpr
b]] -> a -> SExpr -> String
go a
p (SExpr -> String) -> SExpr -> String
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"<",  SExpr
a, SExpr
b]
                   EApp [ECon String
"not", EApp [ECon String
"<=", SExpr
a, SExpr
b]] -> a -> SExpr -> String
go a
p (SExpr -> String) -> SExpr -> String
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
">",  SExpr
a, SExpr
b]
                   EApp [ECon String
"not", EApp [ECon String
"<",  SExpr
a, SExpr
b]] -> a -> SExpr -> String
go a
p (SExpr -> String) -> SExpr -> String
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
">=", SExpr
a, SExpr
b]
                   EApp [ECon String
"not", EApp [ECon String
">",  SExpr
a, SExpr
b]] -> a -> SExpr -> String
go a
p (SExpr -> String) -> SExpr -> String
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"<=", SExpr
a, SExpr
b]

                   -- Handle x + -y that z3 is fond of producing
                   EApp [ECon String
a, SExpr
x, EApp [ECon String
m, ENum (-1, Maybe Int
_), SExpr
y]] | String -> Bool
isPlus String
a Bool -> Bool -> Bool
&& String -> Bool
isTimes String
m -> a -> SExpr -> String
go a
p (SExpr -> String) -> SExpr -> String
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"-", SExpr
x, SExpr
y]

                   -- Handle x + -NUM that z3 is also fond of producing
                   EApp [ECon String
a, SExpr
x, ENum (Integer
i, Maybe Int
mw)] | String -> Bool
isPlus String
a Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 -> a -> SExpr -> String
go a
p (SExpr -> String) -> SExpr -> String
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"-", SExpr
x, (Integer, Maybe Int) -> SExpr
ENum (-Integer
i, Maybe Int
mw)]

                   -- Handle -1 * x
                   EApp [ECon String
o, ENum (-1, Maybe Int
_), SExpr
b] | String -> Bool
isTimes String
o -> Bool -> ShowS
parenIf (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
8) (ShowS
neg (a -> SExpr -> String
go a
8 SExpr
b))

                   -- Move additive constants to the right, multiplicative constants to the left
                   EApp [ECon String
o, SExpr
x, SExpr
y] | String -> Bool
isPlus  String
o Bool -> Bool -> Bool
&& SExpr -> Bool
isConst SExpr
x Bool -> Bool -> Bool
&& Bool -> Bool
not (SExpr -> Bool
isConst SExpr
y) -> a -> SExpr -> String
go a
p (SExpr -> String) -> SExpr -> String
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
o, SExpr
y, SExpr
x]
                   EApp [ECon String
o, SExpr
x, SExpr
y] | String -> Bool
isTimes String
o Bool -> Bool -> Bool
&& SExpr -> Bool
isConst SExpr
y Bool -> Bool -> Bool
&& Bool -> Bool
not (SExpr -> Bool
isConst SExpr
x) -> a -> SExpr -> String
go a
p (SExpr -> String) -> SExpr -> String
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
o, SExpr
y, SExpr
x]

                   -- Simp arithmetic
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isPlus  String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
6 (String -> Maybe String
forall a. a -> Maybe a
Just String
"+")  [SExpr]
xs
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isMinus String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
6 (String -> Maybe String
forall a. a -> Maybe a
Just String
"-")  [SExpr]
xs
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isTimes String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
7 (String -> Maybe String
forall a. a -> Maybe a
Just String
"*")  [SExpr]
xs
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isDiv   String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
7 (String -> Maybe String
forall a. a -> Maybe a
Just String
"/")  [SExpr]
xs

                   -- Booleans
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isLT    String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
4 (String -> Maybe String
forall a. a -> Maybe a
Just String
"<")  [SExpr]
xs
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isLTE   String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
4 (String -> Maybe String
forall a. a -> Maybe a
Just String
"<=") [SExpr]
xs
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isGT    String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
4 (String -> Maybe String
forall a. a -> Maybe a
Just String
">")  [SExpr]
xs
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isGTE   String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
4 (String -> Maybe String
forall a. a -> Maybe a
Just String
">=") [SExpr]
xs
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isAND   String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
3 (String -> Maybe String
forall a. a -> Maybe a
Just String
"&&") [SExpr]
xs
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isOR    String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
2 (String -> Maybe String
forall a. a -> Maybe a
Just String
"||") [SExpr]
xs
                   EApp (ECon String
o : [SExpr]
xs) | String -> Bool
isEQ    String
o -> a -> Maybe String -> [SExpr] -> String
recurse a
4 (String -> Maybe String
forall a. a -> Maybe a
Just String
"==") [SExpr]
xs

                   -- Otherwise, just do prefix
                   EApp [SExpr]
xs                        -> a -> Maybe String -> [SExpr] -> String
recurse a
9 Maybe String
forall a. Maybe a
Nothing [SExpr]
xs

           where recurse :: a -> Maybe String -> [SExpr] -> String
recurse a
p' (Just String
op) [SExpr]
xs = Bool -> ShowS
parenIf (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
p') ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate (Char
' ' Char -> ShowS
forall a. a -> [a] -> [a]
: String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ") ((SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
parenNeg ShowS -> (SExpr -> String) -> SExpr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SExpr -> String
go a
p') [SExpr]
xs)
                 recurse a
p' Maybe String
Nothing   [SExpr]
xs = Bool -> ShowS
parenIf (a
p a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
p') ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords                       ((SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
parenNeg ShowS -> (SExpr -> String) -> SExpr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SExpr -> String
go a
p') [SExpr]
xs)

        isConst :: SExpr -> Bool
isConst ECon          {} = Bool
False
        isConst ENum          {} = Bool
True
        isConst EReal         {} = Bool
True
        isConst EFloat        {} = Bool
True
        isConst EFloatingPoint{} = Bool
True
        isConst EDouble       {} = Bool
True
        isConst EApp          {} = Bool
False

        parenNeg :: ShowS
parenNeg x :: String
x@(Char
'-':String
_) = ShowS
paren String
x
        parenNeg String
x         = String
x

        neg :: ShowS
neg (Char
'-':String
x) = String
x
        neg String
x       = Char
'-' Char -> ShowS
forall a. a -> [a] -> [a]
: Bool -> ShowS
parenIf ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
x) String
x

        cnst :: a -> String
cnst a
x = case a -> String
forall a. Show a => a -> String
show a
x of
                  sx :: String
sx@(Char
'-' : String
_) -> ShowS
paren String
sx
                  String
sx           -> String
sx

        paren :: ShowS
paren r :: String
r@(Char
'(':String
_) = String
r
        paren String
r         = Char
'(' Char -> ShowS
forall a. a -> [a] -> [a]
: String
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

        parenIf :: Bool -> ShowS
parenIf Bool
False String
r = String
r
        parenIf Bool
True  String
r = ShowS
paren String
r

        isPlus :: String -> Bool
isPlus  = (String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"+",  String
"bvadd"])
        isTimes :: String -> Bool
isTimes = (String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"*",  String
"bvmul"])
        isMinus :: String -> Bool
isMinus = (String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"-",  String
"bvsub"])
        isDiv :: String -> Bool
isDiv   = (String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"/",  String
"bvdiv"])
        isLT :: String -> Bool
isLT    = (String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"<",  String
"bvult", String
"bvslt", String
"fp.lt" ])
        isLTE :: String -> Bool
isLTE   = (String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"<=", String
"bvule", String
"bvsle", String
"fp.leq"])
        isGT :: String -> Bool
isGT    = (String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
">",  String
"bvugt", String
"bvsgt", String
"fp.gt" ])
        isGTE :: String -> Bool
isGTE   = (String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
">=", String
"bvuge", String
"bvsge", String
"fp.gte"])
        isEQ :: String -> Bool
isEQ    = (String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"=",  String
"fp.eq"])
        isAND :: String -> Bool
isAND   = (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"and")
        isOR :: String -> Bool
isOR    = (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"or")

{- HLint ignore chainAssigns "Redundant if" -}