    -----------------------------------------------------------------------------
    -- |
    -- 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, 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 :: forall a. Typeable a => 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 :: forall (m :: * -> *) a' b' r a b.
    Monad m =>
    (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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \b'
    b' -> r -> m r
    forall a. a -> m a
    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 :: forall (m :: * -> *) a' b' c' r a b c.
    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
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \c'
    c' -> r -> m r
    forall a. a -> m a
    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 :: forall (m :: * -> *) a' b' c' d' r a b c d.
    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
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \d'
    d' -> r -> m r
    forall a. a -> m a
    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 :: forall (m :: * -> *) a' b' c' d' e' r a b c d e.
    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
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \e'
    e' -> r -> m r
    forall a. a -> m a
    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 :: forall (m :: * -> *) a' b' c' d' e' f' r a b c d e f.
    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
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \f'
    y' -> r -> m r
    forall a. a -> m a
    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 :: forall (m :: * -> *) a' b' c' d' e' f' g' r a b c d e f g.
    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
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \g'
    z' -> r -> m r
    forall a. a -> m a
    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 :: forall (m :: * -> *) a' b' c' d' e' f' g' h' r a b c d e f g h.
    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
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \h'
    w' -> r -> m r
    forall a. a -> m a
    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 a. [a] -> 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 an SMTLib 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
    'u':Char
    '{':Char
    d4:Char
    d3:Char
    d2:Char
    d1:Char
    d0:Char
    '}' : String
    rest) | [(Int
    v, String
    "")] <- ReadS Int
    forall a. (Eq a, Num a) => ReadS a
    readHex [Char
    d4, Char
    d3, Char
    d2, Char
    d1, Char
    d0] = Int -> Char
    chr Int
    v Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    go String
    rest
            go (Char
    '\\':Char
    'u':       Char
    d3:Char
    d2:Char
    d1:Char
    d0     : String
    rest) | [(Int
    v, String
    "")] <- ReadS Int
    forall a. (Eq a, Num a) => ReadS a
    readHex [    Char
    d3, Char
    d2, Char
    d1, Char
    d0] = Int -> Char
    chr Int
    v Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    go String
    rest
            go (Char
    '\\':Char
    'u':Char
    '{':   Char
    d3:Char
    d2:Char
    d1:Char
    d0:Char
    '}' : String
    rest) | [(Int
    v, String
    "")] <- ReadS Int
    forall a. (Eq a, Num a) => ReadS a
    readHex [    Char
    d3, Char
    d2, Char
    d1, Char
    d0] = Int -> Char
    chr Int
    v Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    go String
    rest
            go (Char
    '\\':Char
    'u':Char
    '{':      Char
    d2:Char
    d1:Char
    d0:Char
    '}' : String
    rest) | [(Int
    v, String
    "")] <- ReadS Int
    forall a. (Eq a, Num a) => ReadS a
    readHex [        Char
    d2, Char
    d1, Char
    d0] = Int -> Char
    chr Int
    v Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    go String
    rest
            go (Char
    '\\':Char
    'u':Char
    '{':         Char
    d1:Char
    d0:Char
    '}' : String
    rest) | [(Int
    v, String
    "")] <- ReadS Int
    forall a. (Eq a, Num a) => ReadS a
    readHex [            Char
    d1, Char
    d0] = Int -> Char
    chr Int
    v Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    go String
    rest
            go (Char
    '\\':Char
    'u':Char
    '{':            Char
    d0:Char
    '}' : String
    rest) | [(Int
    v, String
    "")] <- ReadS Int
    forall a. (Eq a, Num a) => ReadS a
    readHex [                Char
    d0] = Int -> Char
    chr Int
    v Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    go String
    rest

            -- Otherwise, just proceed; hopefully we covered everything above
            go (Char
    c : String
    rest) = Char
    c Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    go String
    rest

    -- | Given a Haskell string, convert it to SMTLib. if ord is 0x00020 to 0x0007E, then we print it as is
    -- to cover the printable ASCII range.
    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 cvt :: Char -> String
    cvt Char
    c
             | Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '"'                 = String
    "\"\""
             | Int
    oc Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0x20 Bool -> Bool -> Bool
    && Int
    oc Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0x7E = [Char
    c]
             | Bool
    True                     = String
    "\\u{" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String -> String
    forall a. Integral a => a -> String -> String
    showHex Int
    oc String
    "" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "}"
             where oc :: Int
    oc = Char -> Int
    ord Char
    c