-----------------------------------------------------------------------------
-- |
-- 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
                          , checkObservableName
                          )
                          where

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

import Numeric (readHex, showHex)

import Data.SBV.SMT.SMTLibNames (smtLibReservedNames)

-- | 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 [Char] -> Bool
forall a. Maybe a -> Bool
isJust (Dynamic -> Maybe [Char]
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 :: [[Char]] -> [Char]
joinArgs = [[Char]] -> [Char]
unwords ([[Char]] -> [Char])
-> ([[Char]] -> [[Char]]) -> [[Char]] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> [Char]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> [Char]
f
    where f :: [Char] -> [Char]
f [Char]
x = [Char]
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
g [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
q
            where hasSpace :: Bool
hasSpace = (Char -> Bool) -> [Char] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace [Char]
x
                  q :: [Char]
q = [Char
'\"' | Bool
hasSpace Bool -> Bool -> Bool
|| [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
x]
                  g :: [Char] -> [Char]
g (Char
'\\':Char
'\"':[Char]
xs)            = Char
'\\'Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:Char
'\\'Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:Char
'\\'Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:Char
'\"'Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
g [Char]
xs
                  g [Char]
"\\"           | Bool
hasSpace = [Char]
"\\\\"
                  g (Char
'\"':[Char]
xs)                 = Char
'\\'Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:Char
'\"'Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
g [Char]
xs
                  g (Char
x':[Char]
xs)                   = Char
x' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
g [Char]
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 :: [Char] -> [[Char]]
splitArgs = [Maybe Char] -> [[Char]]
join ([Maybe Char] -> [[Char]])
-> ([Char] -> [Maybe Char]) -> [Char] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State -> [Char] -> [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] -> [[Char]]
join [] = []
          join [Maybe Char]
xs = (Maybe Char -> Char) -> [Maybe Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Maybe Char -> Char
forall a. HasCallStack => Maybe a -> a
fromJust [Maybe Char]
a [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [Maybe Char] -> [[Char]]
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 -> [Char] -> [Maybe Char]
f State
Init (Char
x:[Char]
xs) | Char -> Bool
isSpace Char
x = State -> [Char] -> [Maybe Char]
f State
Init [Char]
xs
          f State
Init [Char]
"\"\""             = [Maybe Char
forall a. Maybe a
Nothing]
          f State
Init [Char]
"\""               = [Maybe Char
forall a. Maybe a
Nothing]
          f State
Init [Char]
xs                 = State -> [Char] -> [Maybe Char]
f State
Norm [Char]
xs
          f State
m (Char
'\"':Char
'\"':Char
'\"':[Char]
xs)   = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\"' Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> [Char] -> [Maybe Char]
f State
m [Char]
xs
          f State
m (Char
'\\':Char
'\"':[Char]
xs)        = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\"' Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> [Char] -> [Maybe Char]
f State
m [Char]
xs
          f State
m (Char
'\\':Char
'\\':Char
'\"':[Char]
xs)   = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\\' Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> [Char] -> [Maybe Char]
f State
m (Char
'\"'Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:[Char]
xs)
          f State
Norm (Char
'\"':[Char]
xs)          = State -> [Char] -> [Maybe Char]
f State
Quot [Char]
xs
          f State
Quot (Char
'\"':Char
'\"':[Char]
xs)     = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\"' Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> [Char] -> [Maybe Char]
f State
Norm [Char]
xs
          f State
Quot (Char
'\"':[Char]
xs)          = State -> [Char] -> [Maybe Char]
f State
Norm [Char]
xs
          f State
Norm (Char
x:[Char]
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 -> [Char] -> [Maybe Char]
f State
Init [Char]
xs
          f State
m (Char
x:[Char]
xs)                = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
x Maybe Char -> [Maybe Char] -> [Maybe Char]
forall a. a -> [a] -> [a]
: State -> [Char] -> [Maybe Char]
f State
m [Char]
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 :: [Char] -> [Char]
qfsToString = [Char] -> [Char]
go
  where go :: [Char] -> [Char]
go [Char]
"" = [Char]
""

        go (Char
'\\':Char
'u':Char
'{':Char
d4:Char
d3:Char
d2:Char
d1:Char
d0:Char
'}' : [Char]
rest) | [(Int
v, [Char]
"")] <- 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 -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
go [Char]
rest
        go (Char
'\\':Char
'u':       Char
d3:Char
d2:Char
d1:Char
d0     : [Char]
rest) | [(Int
v, [Char]
"")] <- 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 -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
go [Char]
rest
        go (Char
'\\':Char
'u':Char
'{':   Char
d3:Char
d2:Char
d1:Char
d0:Char
'}' : [Char]
rest) | [(Int
v, [Char]
"")] <- 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 -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
go [Char]
rest
        go (Char
'\\':Char
'u':Char
'{':      Char
d2:Char
d1:Char
d0:Char
'}' : [Char]
rest) | [(Int
v, [Char]
"")] <- ReadS Int
forall a. (Eq a, Num a) => ReadS a
readHex [        Char
d2, Char
d1, Char
d0] = Int -> Char
chr Int
v Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
go [Char]
rest
        go (Char
'\\':Char
'u':Char
'{':         Char
d1:Char
d0:Char
'}' : [Char]
rest) | [(Int
v, [Char]
"")] <- ReadS Int
forall a. (Eq a, Num a) => ReadS a
readHex [            Char
d1, Char
d0] = Int -> Char
chr Int
v Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
go [Char]
rest
        go (Char
'\\':Char
'u':Char
'{':            Char
d0:Char
'}' : [Char]
rest) | [(Int
v, [Char]
"")] <- ReadS Int
forall a. (Eq a, Num a) => ReadS a
readHex [                Char
d0] = Int -> Char
chr Int
v Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
go [Char]
rest

        -- Otherwise, just proceed; hopefully we covered everything above
        go (Char
c : [Char]
rest) = Char
c Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
go [Char]
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 :: [Char] -> [Char]
stringToQFS = (Char -> [Char]) -> [Char] -> [Char]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> [Char]
cvt
  where cvt :: Char -> [Char]
cvt Char
c
         | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'"'                 = [Char]
"\"\""
         | 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                     = [Char]
"\\u{" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char] -> [Char]
forall a. Integral a => a -> [Char] -> [Char]
showHex Int
oc [Char]
"" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"}"
         where oc :: Int
oc = Char -> Int
ord Char
c

-- | Check if an observable name is good.
checkObservableName :: String -> Maybe String
checkObservableName :: [Char] -> Maybe [Char]
checkObservableName [Char]
lbl
  | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
lbl
  = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"SBV.observe: Bad empty name!"
  | (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower [Char]
lbl [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]]
smtLibReservedNames
  = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"SBV.observe: The name chosen is reserved, please change it!: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
lbl
  | [Char]
"s" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
lbl Bool -> Bool -> Bool
&& (Char -> Bool) -> [Char] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit (Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
drop Int
1 [Char]
lbl)
  = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"SBV.observe: Names of the form sXXX are internal to SBV, please use a different name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
lbl
  | Bool
True
  = Maybe [Char]
forall a. Maybe a
Nothing