-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Utils.Lib
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Misc helpers
-----------------------------------------------------------------------------

{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Utils.Lib ( mlift2, mlift3, mlift4, mlift5, mlift6, mlift7, mlift8
                          , joinArgs, splitArgs
                          , stringToQFS, qfsToString
                          , isKString
                          )
                          where

import Data.Char    (isSpace, chr, ord)
import Data.Dynamic (fromDynamic, toDyn, Typeable)
import Data.Maybe   (fromJust, isJust, isNothing)

import Numeric (readHex, readOct, showHex)

-- | We have a nasty issue with the usual String/List confusion in Haskell. However, we can
-- do a simple dynamic trick to determine where we are. The ice is thin here, but it seems to work.
isKString :: forall a. Typeable a => a -> Bool
isKString :: a -> Bool
isKString a
_ = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Dynamic -> Maybe String
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic (a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn (a
forall a. HasCallStack => a
undefined :: a)) :: Maybe String)

-- | Monadic lift over 2-tuples
mlift2 :: Monad m => (a' -> b' -> r) -> (a -> m a') -> (b -> m b') -> (a, b) -> m r
mlift2 :: (a' -> b' -> r) -> (a -> m a') -> (b -> m b') -> (a, b) -> m r
mlift2 a' -> b' -> r
k a -> m a'
f b -> m b'
g (a
a, b
b) = a -> m a'
f a
a m a' -> (a' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b m b' -> (b' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> r -> m r
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> m r) -> r -> m r
forall a b. (a -> b) -> a -> b
$ a' -> b' -> r
k a'
a' b'
b'

-- | Monadic lift over 3-tuples
mlift3 :: Monad m => (a' -> b' -> c' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (a, b, c) -> m r
mlift3 :: (a' -> b' -> c' -> r)
-> (a -> m a') -> (b -> m b') -> (c -> m c') -> (a, b, c) -> m r
mlift3 a' -> b' -> c' -> r
k a -> m a'
f b -> m b'
g c -> m c'
h (a
a, b
b, c
c) = a -> m a'
f a
a m a' -> (a' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b m b' -> (b' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c m c' -> (c' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> r -> m r
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> m r) -> r -> m r
forall a b. (a -> b) -> a -> b
$ a' -> b' -> c' -> r
k a'
a' b'
b' c'
c'

-- | Monadic lift over 4-tuples
mlift4 :: Monad m => (a' -> b' -> c' -> d' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (a, b, c, d) -> m r
mlift4 :: (a' -> b' -> c' -> d' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (a, b, c, d)
-> m r
mlift4 a' -> b' -> c' -> d' -> r
k a -> m a'
f b -> m b'
g c -> m c'
h d -> m d'
i (a
a, b
b, c
c, d
d) = a -> m a'
f a
a m a' -> (a' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b m b' -> (b' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c m c' -> (c' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> d -> m d'
i d
d m d' -> (d' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \d'
d' -> r -> m r
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> m r) -> r -> m r
forall a b. (a -> b) -> a -> b
$ a' -> b' -> c' -> d' -> r
k a'
a' b'
b' c'
c' d'
d'

-- | Monadic lift over 5-tuples
mlift5 :: Monad m => (a' -> b' -> c' -> d' -> e' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (e -> m e') -> (a, b, c, d, e) -> m r
mlift5 :: (a' -> b' -> c' -> d' -> e' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (a, b, c, d, e)
-> m r
mlift5 a' -> b' -> c' -> d' -> e' -> r
k a -> m a'
f b -> m b'
g c -> m c'
h d -> m d'
i e -> m e'
j (a
a, b
b, c
c, d
d, e
e) = a -> m a'
f a
a m a' -> (a' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b m b' -> (b' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c m c' -> (c' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> d -> m d'
i d
d m d' -> (d' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \d'
d' -> e -> m e'
j e
e m e' -> (e' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \e'
e' -> r -> m r
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> m r) -> r -> m r
forall a b. (a -> b) -> a -> b
$ a' -> b' -> c' -> d' -> e' -> r
k a'
a' b'
b' c'
c' d'
d' e'
e'

-- | Monadic lift over 6-tuples
mlift6 :: Monad m => (a' -> b' -> c' -> d' -> e' -> f' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (e -> m e') -> (f -> m f') -> (a, b, c, d, e, f) -> m r
mlift6 :: (a' -> b' -> c' -> d' -> e' -> f' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (f -> m f')
-> (a, b, c, d, e, f)
-> m r
mlift6 a' -> b' -> c' -> d' -> e' -> f' -> r
k a -> m a'
f b -> m b'
g c -> m c'
h d -> m d'
i e -> m e'
j f -> m f'
l (a
a, b
b, c
c, d
d, e
e, f
y) = a -> m a'
f a
a m a' -> (a' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b m b' -> (b' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c m c' -> (c' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> d -> m d'
i d
d m d' -> (d' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \d'
d' -> e -> m e'
j e
e m e' -> (e' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \e'
e' -> f -> m f'
l f
y m f' -> (f' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \f'
y' -> r -> m r
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> m r) -> r -> m r
forall a b. (a -> b) -> a -> b
$ a' -> b' -> c' -> d' -> e' -> f' -> r
k a'
a' b'
b' c'
c' d'
d' e'
e' f'
y'

-- | Monadic lift over 7-tuples
mlift7 :: Monad m => (a' -> b' -> c' -> d' -> e' -> f' -> g' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (e -> m e') -> (f -> m f') -> (g -> m g') -> (a, b, c, d, e, f, g) -> m r
mlift7 :: (a' -> b' -> c' -> d' -> e' -> f' -> g' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (f -> m f')
-> (g -> m g')
-> (a, b, c, d, e, f, g)
-> m r
mlift7 a' -> b' -> c' -> d' -> e' -> f' -> g' -> r
k a -> m a'
f b -> m b'
g c -> m c'
h d -> m d'
i e -> m e'
j f -> m f'
l g -> m g'
m (a
a, b
b, c
c, d
d, e
e, f
y, g
z) = a -> m a'
f a
a m a' -> (a' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b m b' -> (b' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c m c' -> (c' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> d -> m d'
i d
d m d' -> (d' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \d'
d' -> e -> m e'
j e
e m e' -> (e' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \e'
e' -> f -> m f'
l f
y m f' -> (f' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \f'
y' -> g -> m g'
m g
z m g' -> (g' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \g'
z' -> r -> m r
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> m r) -> r -> m r
forall a b. (a -> b) -> a -> b
$ a' -> b' -> c' -> d' -> e' -> f' -> g' -> r
k a'
a' b'
b' c'
c' d'
d' e'
e' f'
y' g'
z'

-- | Monadic lift over 8-tuples
mlift8 :: Monad m => (a' -> b' -> c' -> d' -> e' -> f' -> g' -> h' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (e -> m e') -> (f -> m f') -> (g -> m g') -> (h -> m h') -> (a, b, c, d, e, f, g, h) -> m r
mlift8 :: (a' -> b' -> c' -> d' -> e' -> f' -> g' -> h' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (f -> m f')
-> (g -> m g')
-> (h -> m h')
-> (a, b, c, d, e, f, g, h)
-> m r
mlift8 a' -> b' -> c' -> d' -> e' -> f' -> g' -> h' -> r
k a -> m a'
f b -> m b'
g c -> m c'
h d -> m d'
i e -> m e'
j f -> m f'
l g -> m g'
m h -> m h'
n (a
a, b
b, c
c, d
d, e
e, f
y, g
z, h
w) = a -> m a'
f a
a m a' -> (a' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b m b' -> (b' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c m c' -> (c' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> d -> m d'
i d
d m d' -> (d' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \d'
d' -> e -> m e'
j e
e m e' -> (e' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \e'
e' -> f -> m f'
l f
y m f' -> (f' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \f'
y' -> g -> m g'
m g
z m g' -> (g' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \g'
z' -> h -> m h'
n h
w m h' -> (h' -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \h'
w' -> r -> m r
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> m r) -> r -> m r
forall a b. (a -> b) -> a -> b
$ a' -> b' -> c' -> d' -> e' -> f' -> g' -> h' -> r
k a'
a' b'
b' c'
c' d'
d' e'
e' f'
y' g'
z' h'
w'

-- Command line argument parsing code courtesy of Neil Mitchell's cmdargs package: see
-- <http://github.com/ndmitchell/cmdargs/blob/master/System/Console/CmdArgs/Explicit/SplitJoin.hs>

-- | Given a sequence of arguments, join them together in a manner that could be used on
--   the command line, giving preference to the Windows @cmd@ shell quoting conventions.
--
--   For an alternative version, intended for actual running the result in a shell, see "System.Process.showCommandForUser"
joinArgs :: [String] -> String
joinArgs :: [String] -> String
joinArgs = [String] -> String
unwords ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
f
    where f :: String -> String
f String
x = String
q String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
g String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
q
            where hasSpace :: Bool
hasSpace = (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
x
                  q :: String
q = [Char
'\"' | Bool
hasSpace Bool -> Bool -> Bool
|| String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
x]
                  g :: String -> String
g (Char
'\\':Char
'\"':String
xs)            = Char
'\\'Char -> String -> String
forall a. a -> [a] -> [a]
:Char
'\\'Char -> String -> String
forall a. a -> [a] -> [a]
:Char
'\\'Char -> String -> String
forall a. a -> [a] -> [a]
:Char
'\"'Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
g String
xs
                  g String
"\\"           | Bool
hasSpace = String
"\\\\"
                  g (Char
'\"':String
xs)                 = Char
'\\'Char -> String -> String
forall a. a -> [a] -> [a]
:Char
'\"'Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
g String
xs
                  g (Char
x':String
xs)                   = Char
x' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
g String
xs
                  g []                        = []

data State = Init -- either I just started, or just emitted something
           | Norm -- I'm seeing characters
           | Quot -- I've seen a quote

-- | Given a string, split into the available arguments. The inverse of 'joinArgs'.
-- Courtesy of the cmdargs package.
splitArgs :: String -> [String]
splitArgs :: String -> [String]
splitArgs = [Maybe Char] -> [String]
join ([Maybe Char] -> [String])
-> (String -> [Maybe Char]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State -> String -> [Maybe Char]
f State
Init
    where -- Nothing is start a new string
          -- Just x is accumulate onto the existing string
          join :: [Maybe Char] -> [String]
          join :: [Maybe Char] -> [String]
join [] = []
          join [Maybe Char]
xs = (Maybe Char -> Char) -> [Maybe Char] -> String
forall a b. (a -> b) -> [a] -> [b]
map Maybe Char -> Char
forall a. HasCallStack => Maybe a -> a
fromJust [Maybe Char]
a String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [Maybe Char] -> [String]
join (Int -> [Maybe Char] -> [Maybe Char]
forall a. Int -> [a] -> [a]
drop Int
1 [Maybe Char]
b)
            where ([Maybe Char]
a,[Maybe Char]
b) = (Maybe Char -> Bool)
-> [Maybe Char] -> ([Maybe Char], [Maybe Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Maybe Char -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe Char]
xs

          f :: State -> String -> [Maybe Char]
f State
Init (Char
x:String
xs) | Char -> Bool
isSpace Char
x = State -> String -> [Maybe Char]
f State
Init String
xs
          f State
Init String
"\"\""             = [Maybe Char
forall a. Maybe a
Nothing]
          f State
Init String
"\""               = [Maybe Char
forall a. Maybe a
Nothing]
          f State
Init String
xs                 = State -> String -> [Maybe Char]
f State
Norm String
xs
          f State
m (Char
'\"':Char
'\"':Char
'\"':String
xs)   = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\"' Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> String -> [Maybe Char]
f State
m String
xs
          f State
m (Char
'\\':Char
'\"':String
xs)        = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\"' Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> String -> [Maybe Char]
f State
m String
xs
          f State
m (Char
'\\':Char
'\\':Char
'\"':String
xs)   = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\\' Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> String -> [Maybe Char]
f State
m (Char
'\"'Char -> String -> String
forall a. a -> [a] -> [a]
:String
xs)
          f State
Norm (Char
'\"':String
xs)          = State -> String -> [Maybe Char]
f State
Quot String
xs
          f State
Quot (Char
'\"':Char
'\"':String
xs)     = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\"' Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> String -> [Maybe Char]
f State
Norm String
xs
          f State
Quot (Char
'\"':String
xs)          = State -> String -> [Maybe Char]
f State
Norm String
xs
          f State
Norm (Char
x:String
xs) | Char -> Bool
isSpace Char
x = Maybe Char
forall a. Maybe a
Nothing Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> String -> [Maybe Char]
f State
Init String
xs
          f State
m (Char
x:String
xs)                = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
x Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> String -> [Maybe Char]
f State
m String
xs
          f State
_ []                    = []

-- | Given a QF_S string (i.e., one that works in the string theory), convert it to a Haskell equivalent
qfsToString :: String -> String
qfsToString :: String -> String
qfsToString = String -> String
go
  where go :: String -> String
go String
""                                                          = String
""
        go (Char
'\\':Char
'n'       : String
rest)                                     = Int -> Char
chr Int
10 Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
go String
rest
        go (Char
'\\':Char
'\\'       : String
rest)                                    = Char
'\\'   Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
go String
rest
        go (Char
'\\':Char
'v'       : String
rest)                                     = Int -> Char
chr Int
11 Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
go String
rest
        go (Char
'\\':Char
'f'       : String
rest)                                     = Int -> Char
chr Int
12 Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
go String
rest
        go (Char
'\\':Char
'r'       : String
rest)                                     = Int -> Char
chr Int
13 Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
go String
rest
        go (Char
'\\':Char
'x':Char
c1:Char
c2 : String
rest) | [(Int
v, String
"")] <- ReadS Int
forall a. (Eq a, Num a) => ReadS a
readHex [Char
c1, Char
c2]     = Int -> Char
chr  Int
v Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
go String
rest
        go (Char
'\\':Char
c1:Char
c2:Char
c3  : String
rest) | [(Int
v, String
"")] <- ReadS Int
forall a. (Eq a, Num a) => ReadS a
readOct [Char
c1, Char
c2, Char
c3] = Int -> Char
chr  Int
v Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
go String
rest
        go (Char
c              : String
rest)                                     = Char
c      Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
go String
rest

-- | Given a Haskell, convert it to one that's understood by the QF_S logic
-- TODO: This function will require mods with the new String logic; as escapes
-- will completely be different!
stringToQFS :: String -> String
stringToQFS :: String -> String
stringToQFS = (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
cvt
  where -- strings are almost just show, but escapes are different. Sigh
        cvt :: Char -> String
cvt Char
c
         | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
o Bool -> Bool -> Bool
&& Int
o Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
32
         = [String]
escapeTable [String] -> Int -> String
forall a. [a] -> Int -> a
!! Int
o
         | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\\'
         = String
"\\\\"
         | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'"'
         = String
"\"\""
         | Int
o Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
128 Bool -> Bool -> Bool
&& Int
o Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
256
         = String
"\\x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
forall a. (Integral a, Show a) => a -> String -> String
showHex (Char -> Int
ord Char
c) String
""
         | Int
o Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
256
         = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: stringToQFS: Haskell character: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not representable in QF_S"
         | Bool
True
         = [Char
c]
         where o :: Int
o = Char -> Int
ord Char
c

        -- | First 32 values are coded in a custom way by Z3:
        escapeTable :: [String]
        escapeTable :: [String]
escapeTable = [ String
"\\x00", String
"\\x01", String
"\\x02", String
"\\x03", String
"\\x04", String
"\\x05", String
"\\x06", String
"\\x07", String
"\\x08", String
"\\x09", String
"\\n",   String
"\\v",   String
"\\f",   String
"\\r",   String
"\\x0E", String
"\\x0F"
                      , String
"\\x10", String
"\\x11", String
"\\x12", String
"\\x13", String
"\\x14", String
"\\x15", String
"\\x16", String
"\\x17", String
"\\x18", String
"\\x19", String
"\\x1A", String
"\\x1B", String
"\\x1C", String
"\\x1D", String
"\\x1E", String
"\\x1F"
                      ]