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

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Utils.Lib ( mlift2, mlift3, mlift4, mlift5, mlift6, mlift7, mlift8
                          , joinArgs, splitArgs
                          , stringToQFS, qfsToString
                          , isKString
                          , checkObservableName
                          , needsBars, barify, isEnclosedInBars
                          , noSurrounding, unQuote, unBar, nameSupply
                          , atProxy
                          ,   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 Data.Proxy

import Type.Reflection (typeRep)

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

-- | Add bars if needed
barify :: String -> String
barify :: String -> String
barify String
s | String -> Bool
needsBars String
s = Char
'|' Char -> String -> String
forall a. a -> [a] -> [a]
: String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|"
         | Bool
True        = String
s

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

-- | Converts a proxy to a readable result. This is useful when you want to write a polymorphic
-- proof, so that the name contains the instantiated version properly.
atProxy :: forall a. Typeable a => Proxy a -> String -> String
atProxy :: forall a. Typeable a => Proxy a -> String -> String
atProxy Proxy a
_ String
nm = String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" @" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
par (TypeRep a -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a))
 where par :: String -> String
par String
s | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
s = Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
             | Bool
True          = String
s

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