-----------------------------------------------------------------------------
-- |
-- 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
                          , needsBars, isEnclosedInBars
                          , noSurrounding, unQuote, unBar, nameSupply
                          ,   curry2,   curry3,   curry4,   curry5,   curry6,   curry7,   curry8,   curry9,   curry10,   curry11,   curry12
                          , uncurry2, uncurry3, uncurry4, uncurry5, uncurry6, uncurry7, uncurry8, uncurry9, uncurry10, uncurry11, uncurry12
                          )
                          where

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

import Numeric (readHex, showHex)

import Data.SBV.SMT.SMTLibNames (isReserved)

-- | 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

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

-- Remove one pair of surrounding 'c's, if present
noSurrounding :: Char -> String -> String
noSurrounding :: Char -> String -> String
noSurrounding Char
c (Char
c':cs :: String
cs@(Char
_:String
_)) | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c' Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Char
forall a. HasCallStack => [a] -> a
last String
cs  = String -> String
forall a. HasCallStack => [a] -> [a]
init String
cs
noSurrounding Char
_ String
s                                        = String
s

-- Remove a pair of surrounding quotes
unQuote :: String -> String
unQuote :: String -> String
unQuote = Char -> String -> String
noSurrounding Char
'"'

-- Remove a pair of surrounding bars
unBar :: String -> String
unBar :: String -> String
unBar = Char -> String -> String
noSurrounding Char
'|'

-- Is this string surrounded by bars? NB. There shouldn't be any other bars or backslash anywhere
isEnclosedInBars :: String -> Bool
isEnclosedInBars :: String -> Bool
isEnclosedInBars String
nm =  String
"|" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
nm
                    Bool -> Bool -> Bool
&& String
"|" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` String
nm
                    Bool -> Bool -> Bool
&& String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
nm Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2
                    Bool -> Bool -> Bool
&& Bool -> Bool
not ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String
"|\\" :: String)) (Int -> String -> String
forall a. Int -> [a] -> [a]
drop Int
1 (String -> String
forall a. HasCallStack => [a] -> [a]
init String
nm)))

-- Does this name need bar in SMTLib2?
needsBars :: String -> Bool
needsBars :: String -> Bool
needsBars String
""        = String -> Bool
forall a. HasCallStack => String -> a
error String
"Impossible happened: needsBars received an empty name!"
needsBars nm :: String
nm@(Char
h:String
tl) = Bool -> Bool
not (String -> Bool
isEnclosedInBars String
nm Bool -> Bool -> Bool
|| (Char -> Bool
isAscii Char
h Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
validChar String
tl))
 where  validChar :: Char -> Bool
validChar Char
x = Char -> Bool
isAscii Char
x Bool -> Bool -> Bool
&& (Char -> Bool
isAlphaNum Char
x Bool -> Bool -> Bool
|| Char
x Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String
"_" :: String))

-- An infinite supply of names, starting with a given set
nameSupply :: [String] -> [String]
nameSupply :: [String] -> [String]
nameSupply [String]
preSupply = [String]
preSupply [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
mkUnique [String]
extras
  where extras :: [String]
extras =  [String
"x", String
"y", String
"z"]                           -- x y z
               [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[Char
c] | Char
c <- [Char
'a' .. Char
'w']]                 -- a b c ... w
               [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [Char
'x' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i | Int
i <- [(Int
1::Int) ..]]       -- x1 x2 x3 ...

        -- make sure extras are different than preSupply. Note that extras
        -- themselves are unique, so we only have to check the preSupply
        mkUnique :: String -> String
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 = String -> String
mkUnique (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'"
                   | Bool
True               = String
x

-- Different arities of curry/uncurry
curry2 :: ((a, b) -> z) -> a -> b -> z
curry2 :: forall a b z. ((a, b) -> z) -> a -> b -> z
curry2 (a, b) -> z
fn a
a b
b = (a, b) -> z
fn (a
a, b
b)

curry3 :: ((a, b, c) -> z) -> a -> b -> c -> z
curry3 :: forall a b c z. ((a, b, c) -> z) -> a -> b -> c -> z
curry3 (a, b, c) -> z
fn a
a b
b c
c = (a, b, c) -> z
fn (a
a, b
b, c
c)

curry4 :: ((a, b, c, d) -> z) -> a -> b -> c -> d -> z
curry4 :: forall a b c d z. ((a, b, c, d) -> z) -> a -> b -> c -> d -> z
curry4 (a, b, c, d) -> z
fn a
a b
b c
c d
d = (a, b, c, d) -> z
fn (a
a, b
b, c
c, d
d)

curry5 :: ((a, b, c, d, e) -> z) -> a -> b -> c -> d -> e -> z
curry5 :: forall a b c d e z.
((a, b, c, d, e) -> z) -> a -> b -> c -> d -> e -> z
curry5 (a, b, c, d, e) -> z
fn a
a b
b c
c d
d e
e = (a, b, c, d, e) -> z
fn (a
a, b
b, c
c, d
d, e
e)

curry6 :: ((a, b, c, d, e, f) -> z) -> a -> b -> c -> d -> e -> f -> z
curry6 :: forall a b c d e f z.
((a, b, c, d, e, f) -> z) -> a -> b -> c -> d -> e -> f -> z
curry6 (a, b, c, d, e, f) -> z
fn a
a b
b c
c d
d e
e f
f = (a, b, c, d, e, f) -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f)

curry7 :: ((a, b, c, d, e, f, g) -> z) -> a -> b -> c -> d -> e -> f -> g -> z
curry7 :: forall a b c d e f g z.
((a, b, c, d, e, f, g) -> z)
-> a -> b -> c -> d -> e -> f -> g -> z
curry7 (a, b, c, d, e, f, g) -> z
fn a
a b
b c
c d
d e
e f
f g
g = (a, b, c, d, e, f, g) -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g)

curry8 :: ((a, b, c, d, e, f, g, h) -> z) -> a -> b -> c -> d -> e -> f -> g -> h -> z
curry8 :: forall a b c d e f g h z.
((a, b, c, d, e, f, g, h) -> z)
-> a -> b -> c -> d -> e -> f -> g -> h -> z
curry8 (a, b, c, d, e, f, g, h) -> z
fn a
a b
b c
c d
d e
e f
f g
g h
h = (a, b, c, d, e, f, g, h) -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h)

curry9 :: ((a, b, c, d, e, f, g, h, i) -> z) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> z
curry9 :: forall a b c d e f g h i z.
((a, b, c, d, e, f, g, h, i) -> z)
-> a -> b -> c -> d -> e -> f -> g -> h -> i -> z
curry9 (a, b, c, d, e, f, g, h, i) -> z
fn a
a b
b c
c d
d e
e f
f g
g h
h i
i = (a, b, c, d, e, f, g, h, i) -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h, i
i)

curry10 :: ((a, b, c, d, e, f, g, h, i, j) -> z) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> z
curry10 :: forall a b c d e f g h i j z.
((a, b, c, d, e, f, g, h, i, j) -> z)
-> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> z
curry10 (a, b, c, d, e, f, g, h, i, j) -> z
fn a
a b
b c
c d
d e
e f
f g
g h
h i
i j
j = (a, b, c, d, e, f, g, h, i, j) -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h, i
i, j
j)

curry11 :: ((a, b, c, d, e, f, g, h, i, j, k) -> z) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> z
curry11 :: forall a b c d e f g h i j k z.
((a, b, c, d, e, f, g, h, i, j, k) -> z)
-> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> z
curry11 (a, b, c, d, e, f, g, h, i, j, k) -> z
fn a
a b
b c
c d
d e
e f
f g
g h
h i
i j
j k
k = (a, b, c, d, e, f, g, h, i, j, k) -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h, i
i, j
j, k
k)

curry12 :: ((a, b, c, d, e, f, g, h, i, j, k, l) -> z) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> z
curry12 :: forall a b c d e f g h i j k l z.
((a, b, c, d, e, f, g, h, i, j, k, l) -> z)
-> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> z
curry12 (a, b, c, d, e, f, g, h, i, j, k, l) -> z
fn a
a b
b c
c d
d e
e f
f g
g h
h i
i j
j k
k l
l = (a, b, c, d, e, f, g, h, i, j, k, l) -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h, i
i, j
j, k
k, l
l)

uncurry2 :: (a -> b -> z) -> (a, b) -> z
uncurry2 :: forall a b z. (a -> b -> z) -> (a, b) -> z
uncurry2 a -> b -> z
fn (a
a, b
b) = a -> b -> z
fn a
a b
b

uncurry3 :: (a -> b -> c -> z) -> (a, b, c) -> z
uncurry3 :: forall a b c z. (a -> b -> c -> z) -> (a, b, c) -> z
uncurry3 a -> b -> c -> z
fn (a
a, b
b, c
c) = a -> b -> c -> z
fn a
a b
b c
c

uncurry4 :: (a -> b -> c -> d -> z) -> (a, b, c, d) -> z
uncurry4 :: forall a b c d z. (a -> b -> c -> d -> z) -> (a, b, c, d) -> z
uncurry4 a -> b -> c -> d -> z
fn (a
a, b
b, c
c, d
d) = a -> b -> c -> d -> z
fn a
a b
b c
c d
d

uncurry5 :: (a -> b -> c -> d -> e -> z) -> (a, b, c, d, e) -> z
uncurry5 :: forall a b c d e z.
(a -> b -> c -> d -> e -> z) -> (a, b, c, d, e) -> z
uncurry5 a -> b -> c -> d -> e -> z
fn (a
a, b
b, c
c, d
d, e
e) = a -> b -> c -> d -> e -> z
fn a
a b
b c
c d
d e
e

uncurry6 :: (a -> b -> c -> d -> e -> f -> z) -> (a, b, c, d, e, f) -> z
uncurry6 :: forall a b c d e f z.
(a -> b -> c -> d -> e -> f -> z) -> (a, b, c, d, e, f) -> z
uncurry6 a -> b -> c -> d -> e -> f -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f) = a -> b -> c -> d -> e -> f -> z
fn a
a b
b c
c d
d e
e f
f

uncurry7 :: (a -> b -> c -> d -> e -> f -> g -> z) -> (a, b, c, d, e, f, g) -> z
uncurry7 :: forall a b c d e f g z.
(a -> b -> c -> d -> e -> f -> g -> z)
-> (a, b, c, d, e, f, g) -> z
uncurry7 a -> b -> c -> d -> e -> f -> g -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g) = a -> b -> c -> d -> e -> f -> g -> z
fn a
a b
b c
c d
d e
e f
f g
g

uncurry8 :: (a -> b -> c -> d -> e -> f -> g -> h -> z) -> (a, b, c, d, e, f, g, h) -> z
uncurry8 :: forall a b c d e f g h z.
(a -> b -> c -> d -> e -> f -> g -> h -> z)
-> (a, b, c, d, e, f, g, h) -> z
uncurry8 a -> b -> c -> d -> e -> f -> g -> h -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h) = a -> b -> c -> d -> e -> f -> g -> h -> z
fn a
a b
b c
c d
d e
e f
f g
g h
h

uncurry9 :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> z) -> (a, b, c, d, e, f, g, h, i) -> z
uncurry9 :: forall a b c d e f g h i z.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> z)
-> (a, b, c, d, e, f, g, h, i) -> z
uncurry9 a -> b -> c -> d -> e -> f -> g -> h -> i -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h, i
i) = a -> b -> c -> d -> e -> f -> g -> h -> i -> z
fn a
a b
b c
c d
d e
e f
f g
g h
h i
i

uncurry10 :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> z) -> (a, b, c, d, e, f, g, h, i, j) -> z
uncurry10 :: forall a b c d e f g h i j z.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> z)
-> (a, b, c, d, e, f, g, h, i, j) -> z
uncurry10 a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h, i
i, j
j) = a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> z
fn a
a b
b c
c d
d e
e f
f g
g h
h i
i j
j

uncurry11 :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> z) -> (a, b, c, d, e, f, g, h, i, j, k) -> z
uncurry11 :: forall a b c d e f g h i j k z.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> z)
-> (a, b, c, d, e, f, g, h, i, j, k) -> z
uncurry11 a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h, i
i, j
j, k
k) = a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> z
fn a
a b
b c
c d
d e
e f
f g
g h
h i
i j
j k
k

uncurry12 :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> z) -> (a, b, c, d, e, f, g, h, i, j, k, l) -> z
uncurry12 :: forall a b c d e f g h i j k l z.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> z)
-> (a, b, c, d, e, f, g, h, i, j, k, l) -> z
uncurry12 a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> z
fn (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h, i
i, j
j, k
k, l
l) = a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> z
fn a
a b
b c
c d
d e
e f
f g
g h
h i
i j
j k
k l
l