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

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

{-# OPTIONS_GHC -Wall -Werror #-}

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

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

import Numeric (readHex, showHex)

-- | We have a nasty issue with the usual String/List confusion in Haskell. However, we can
-- do a simple dynamic trick to determine where we are. The ice is thin here, but it seems to work.
isKString :: forall a. Typeable a => a -> Bool
isKString :: forall a. Typeable a => a -> Bool
isKString a
_ = forall a. Maybe a -> Bool
isJust (forall a. Typeable a => Dynamic -> Maybe a
fromDynamic (forall a. Typeable a => a -> Dynamic
toDyn (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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> d -> m d'
i d
d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \d'
d' -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> d -> m d'
i d
d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \d'
d' -> e -> m e'
j e
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \e'
e' -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> d -> m d'
i d
d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \d'
d' -> e -> m e'
j e
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \e'
e' -> f -> m f'
l f
y forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \f'
y' -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> d -> m d'
i d
d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \d'
d' -> e -> m e'
j e
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \e'
e' -> f -> m f'
l f
y forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \f'
y' -> g -> m g'
m g
z forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \g'
z' -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'
a' -> b -> m b'
g b
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b'
b' -> c -> m c'
h c
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'
c' -> d -> m d'
i d
d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \d'
d' -> e -> m e'
j e
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \e'
e' -> f -> m f'
l f
y forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \f'
y' -> g -> m g'
m g
z forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \g'
z' -> h -> m h'
n h
w forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \h'
w' -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map String -> String
f
    where f :: String -> String
f String
x = String
q forall a. [a] -> [a] -> [a]
++ String -> String
g String
x forall a. [a] -> [a] -> [a]
++ String
q
            where hasSpace :: Bool
hasSpace = 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
|| forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
x]
                  g :: String -> String
g (Char
'\\':Char
'\"':String
xs)            = Char
'\\'forall a. a -> [a] -> [a]
:Char
'\\'forall a. a -> [a] -> [a]
:Char
'\\'forall a. a -> [a] -> [a]
:Char
'\"'forall a. a -> [a] -> [a]
: String -> String
g String
xs
                  g String
"\\"           | Bool
hasSpace = String
"\\\\"
                  g (Char
'\"':String
xs)                 = Char
'\\'forall a. a -> [a] -> [a]
:Char
'\"'forall a. a -> [a] -> [a]
: String -> String
g String
xs
                  g (Char
x':String
xs)                   = Char
x' 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 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 = forall a b. (a -> b) -> [a] -> [b]
map forall a. HasCallStack => Maybe a -> a
fromJust [Maybe Char]
a forall a. a -> [a] -> [a]
: [Maybe Char] -> [String]
join (forall a. Int -> [a] -> [a]
drop Int
1 [Maybe Char]
b)
            where ([Maybe Char]
a,[Maybe Char]
b) = forall a. (a -> Bool) -> [a] -> ([a], [a])
break 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
"\"\""             = [forall a. Maybe a
Nothing]
          f State
Init String
"\""               = [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)   = forall a. a -> Maybe a
Just Char
'\"' forall a. a -> [a] -> [a]
: State -> String -> [Maybe Char]
f State
m String
xs
          f State
m (Char
'\\':Char
'\"':String
xs)        = forall a. a -> Maybe a
Just Char
'\"' forall a. a -> [a] -> [a]
: State -> String -> [Maybe Char]
f State
m String
xs
          f State
m (Char
'\\':Char
'\\':Char
'\"':String
xs)   = forall a. a -> Maybe a
Just Char
'\\' forall a. a -> [a] -> [a]
: State -> String -> [Maybe Char]
f State
m (Char
'\"'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)     = forall a. a -> Maybe a
Just 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 = forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
: State -> String -> [Maybe Char]
f State
Init String
xs
          f State
m (Char
x:String
xs)                = forall a. a -> Maybe a
Just Char
x 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
"")] <- forall a. (Eq a, Num a) => ReadS a
readHex [Char
d4, Char
d3, Char
d2, Char
d1, Char
d0] = Int -> Char
chr Int
v 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
"")] <- forall a. (Eq a, Num a) => ReadS a
readHex [    Char
d3, Char
d2, Char
d1, Char
d0] = Int -> Char
chr Int
v 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
"")] <- forall a. (Eq a, Num a) => ReadS a
readHex [    Char
d3, Char
d2, Char
d1, Char
d0] = Int -> Char
chr Int
v 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
"")] <- forall a. (Eq a, Num a) => ReadS a
readHex [        Char
d2, Char
d1, Char
d0] = Int -> Char
chr Int
v 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
"")] <- forall a. (Eq a, Num a) => ReadS a
readHex [            Char
d1, Char
d0] = Int -> Char
chr Int
v forall a. a -> [a] -> [a]
: String -> String
go String
rest
        go (Char
'\\':Char
'u':Char
'{':            Char
d0:Char
'}' : String
rest) | [(Int
v, String
"")] <- forall a. (Eq a, Num a) => ReadS a
readHex [                Char
d0] = Int -> Char
chr Int
v 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 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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
cvt
  where cvt :: Char -> String
cvt Char
c
         | Char
c forall a. Eq a => a -> a -> Bool
== Char
'"'                 = String
"\"\""
         | Int
oc forall a. Ord a => a -> a -> Bool
>= Int
0x20 Bool -> Bool -> Bool
&& Int
oc forall a. Ord a => a -> a -> Bool
<= Int
0x7E = [Char
c]
         | Bool
True                     = String
"\\u{" forall a. [a] -> [a] -> [a]
++ forall a. (Integral a, Show a) => a -> String -> String
showHex Int
oc String
"" forall a. [a] -> [a] -> [a]
++ String
"}"
         where oc :: Int
oc = Char -> Int
ord Char
c