    -----------------------------------------------------------------------------
    -- |
    -- 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) 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.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 = 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 (String
    pre String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)
                                (String
    pre, String
    rest)     -> String -> [String] -> [String]
    go String
    rest (String
    pre String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [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 (SExpr
    sexp, [String]
    extras) <- [String] -> Either String (SExpr, [String])
    parse [String]
    inpToks
                        if [String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    extras
                           then case SExpr
    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 String -> Either String SExpr
    forall {b}. String -> Either String b
    die String
    "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 ([SExpr]
    f, [String]
    r) <- [String] -> [SExpr] -> Either String ([SExpr], [String])
    parseApp [String]
    toks []
                                  SExpr
    f' <- SExpr -> Either String SExpr
    cvt ([SExpr] -> SExpr
    EApp [SExpr]
    f)
                                  (SExpr, [String]) -> Either String (SExpr, [String])
    forall a. a -> Either String a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr
    f', [String]
    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 SExpr
    t <- String -> Either String SExpr
    pTok String
    tok
                                  (SExpr, [String]) -> Either String (SExpr, [String])
    forall a. a -> Either String a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr
    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 (SExpr
    f, [String]
    r) <- [String] -> Either String (SExpr, [String])
    parse (String
    "("String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :[String]
    toks)
                                           [String] -> [SExpr] -> Either String ([SExpr], [String])
    parseApp [String]
    r (SExpr
    f SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : [SExpr]
    sofar)
            parseApp (String
    tok:[String]
    toks) [SExpr]
    sofar = do SExpr
    t <- String -> Either String SExpr
    pTok String
    tok
                                           [String] -> [SExpr] -> Either String ([SExpr], [String])
    parseApp [String]
    toks (SExpr
    t SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : [SExpr]
    sofar)

            pTok :: String -> Either String SExpr
    pTok 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 [(Integer, Integer)]
    ts <- (SExpr -> Either String (Integer, Integer))
    -> [SExpr] -> Either String [(Integer, Integer)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM SExpr -> Either String (Integer, Integer)
    getCoeff [SExpr]
    trms
                                                                            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 ((Integer, [(Integer, Integer)])
    -> Either (Bool, String) (Integer, [(Integer, Integer)])
    forall a b. b -> Either a b
    Right ((Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    k, [(Integer, Integer)]
    ts))
            cvt (EApp [ECon 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
                                                    SExpr
    approx <- SExpr -> Either String SExpr
    cvt SExpr
    val
                                                    case SExpr
    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 Rational
    low  <- SExpr -> Either String Rational
    get SExpr
    n1
                                             Rational
    high <- SExpr -> Either String Rational
    get SExpr
    n2
                                             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
    $ RealPoint Rational -> RealPoint Rational -> AlgReal
    AlgInterval (Rational -> RealPoint Rational
    forall a. a -> RealPoint a
    OpenPoint Rational
    low) (Rational -> RealPoint Rational
    forall a. a -> RealPoint a
    OpenPoint Rational
    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
    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 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 [SExpr]
    s  <- SExpr -> Maybe [SExpr]
    select SExpr
    selector
                           [Either ([SExpr], SExpr) SExpr]
    tB <- [Either ([SExpr], SExpr) SExpr]
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    go [] SExpr
    thenBranch
                           case [SExpr]
    -> [Either ([SExpr], SExpr) SExpr] -> Maybe ([SExpr], SExpr)
    cond [SExpr]
    s [Either ([SExpr], SExpr) SExpr]
    tB of
                              Just ([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 [Either ([SExpr], SExpr) SExpr]
    rest <- SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    vals SExpr
    prev
                                                                                                 [Either ([SExpr], SExpr) SExpr]
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Either ([SExpr], SExpr) SExpr]
     -> Maybe [Either ([SExpr], SExpr) SExpr])
    -> [Either ([SExpr], SExpr) SExpr]
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall a b. (a -> b) -> a -> b
    $ ([SExpr], SExpr) -> Either ([SExpr], SExpr) SExpr
    forall a b. a -> Either a b
    Left ([SExpr] -> [SExpr]
    forall a. HasCallStack => [a] -> [a]
    init [SExpr]
    argsVal, [SExpr] -> SExpr
    forall a. HasCallStack => [a] -> a
    last [SExpr]
    argsVal) Either ([SExpr], SExpr) SExpr
    -> [Either ([SExpr], SExpr) SExpr]
    -> [Either ([SExpr], SExpr) SExpr]
    forall a. a -> [a] -> [a]
    : [Either ([SExpr], SExpr) SExpr]
    rest
              vals 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
    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.
            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
                         (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 -> Maybe [String] -> Maybe String
    makeHaskellFunction :: String -> String -> Maybe [String] -> Maybe String
    makeHaskellFunction String
    resp String
    nm 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 ([String]
    args, String
    bd) <- SExpr -> Maybe ([String], String)
    lambda SExpr
    e
                                                           String -> Maybe String
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> Maybe String) -> String -> Maybe String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords (String
    nm String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    args) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    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

            extras :: [String]
    extras =  [String
    "x", String
    "y", String
    "z"]
                   [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[Char
    c] | Char
    c <- [Char
    'a' .. Char
    'z'], Char
    c Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    < Char
    'x']
                   [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [Char
    'x' Char -> ShowS
    forall a. a -> [a] -> [a]
    : Int -> String
    forall a. Show a => a -> String
    show Int
    i | Int
    i <- [(Int
    1::Int) ..]]

            mkUnique :: ShowS
    mkUnique String
    x | String
    x String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    preSupply = ShowS
    mkUnique ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ String
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "'"
                       | Bool
    True               = String
    x

            supply :: [String]
    supply = [String]
    preSupply [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ShowS -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ShowS
    mkUnique [String]
    extras

            lambda :: SExpr -> Maybe ([String], String)
            lambda :: SExpr -> Maybe ([String], String)
    lambda (EApp [ECon String
    "lambda", EApp [SExpr]
    args, SExpr
    bd]) = do [String]
    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)]
    env = [String] -> [String] -> [(String, String)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [String]
    as [String]
    supply
                                                              ([String], String) -> Maybe ([String], String)
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (((String, String) -> String) -> [(String, String)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, String) -> String
    forall a b. (a, b) -> b
    snd [(String, String)]
    env, [(String, String)] -> SExpr -> String
    body [(String, String)]
    env SExpr
    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

            body :: [(String, String)] -> SExpr -> String
    body [(String, String)]
    env = SExpr -> String
    go
              where go :: SExpr -> String
                    go :: SExpr -> String
    go (ECon String
    n) | Just String
    a <- String -> [(String, String)] -> Maybe String
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    n [(String, String)]
    env = String
    a
                                | Bool
    True                   = String
    n

                    go (ENum (Integer
    i, Maybe Int
    _))      = Integer -> String
    forall a. Show a => a -> String
    show Integer
    i
                    go (EReal  AlgReal
    a)         = AlgReal -> String
    forall a. Show a => a -> String
    show AlgReal
    a
                    go (EFloat Float
    f)         = Float -> String
    forall a. Show a => a -> String
    show Float
    f
                    go (EFloatingPoint FP
    f) = FP -> String
    forall a. Show a => a -> String
    show FP
    f
                    go (EDouble Double
    f)        = Double -> String
    forall a. Show a => a -> String
    show Double
    f
                    go (EApp [SExpr]
    xs)          = [String] -> String
    app ((SExpr -> String) -> [SExpr] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (ShowS
    wrap ShowS -> (SExpr -> String) -> SExpr -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SExpr -> String
    go) [SExpr]
    xs)

                    parens :: ShowS
    parens String
    x = Char
    '(' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

                    wrap :: ShowS
    wrap String
    x | String
    "-" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    x = ShowS
    parens String
    x
                           | (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Char -> Bool
    isSpace String
    x      = ShowS
    parens String
    x
                           | Bool
    True               = String
    x

                    mkBin :: String -> String -> ShowS
    mkBin String
    o String
    a String
    b = ShowS
    wrap String
    a String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    wrap String
    b

                    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"])
                    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"])

                    -- Make an application, with some simplifications
                    app :: [String] -> String
                    app :: [String] -> String
    app (String
    o : [String]
    xs) | String -> Bool
    isPlus String
    o = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    " + " [String]
    xs

                    -- multiplication of arbitrary elements, with proviso for multiplication by -1
                    app [String
    m, String
    "(-1)", String
    x] | String -> Bool
    isTimes String
    m = Char
    '-' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    x
                    app (String
    m  : [String]
    xs)      | String -> Bool
    isTimes String
    m = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    " * " [String]
    xs

                    -- binary arith ops
                    app [String
    "-",  String
    a, String
    b] = String -> String -> ShowS
    mkBin String
    "-"  String
    a String
    b
                    app [String
    "/",  String
    a, String
    b] = String -> String -> ShowS
    mkBin String
    "/"  String
    a String
    b

                    app [String
    o, String
    a, String
    b] | String -> Bool
    isLT  String
    o = String -> String -> ShowS
    mkBin String
    "<"  String
    a String
    b
                    app [String
    o, String
    a, String
    b] | String -> Bool
    isLTE String
    o = String -> String -> ShowS
    mkBin String
    "<=" String
    a String
    b
                    app [String
    o, String
    a, String
    b] | String -> Bool
    isGT  String
    o = String -> String -> ShowS
    mkBin String
    ">"  String
    a String
    b
                    app [String
    o, String
    a, String
    b] | String -> Bool
    isGTE String
    o = String -> String -> ShowS
    mkBin String
    ">=" String
    a String
    b

                    -- give up, and just do prefix!
                    app [String]
    xs = [String] -> String
    unwords [String]
    xs

    {- HLint ignore chainAssigns "Redundant if" -}