1----------------------------------------------------------------------------- 2-- | 3-- Module : Data.SBV.Utils.Lib 4-- Copyright : (c) Levent Erkok 5-- License : BSD3 6-- Maintainer: erkokl@gmail.com 7-- Stability : experimental 8-- 9-- Misc helpers 10----------------------------------------------------------------------------- 11 12{-# LANGUAGE RankNTypes #-} 13{-# LANGUAGE ScopedTypeVariables #-} 14 15{-# OPTIONS_GHC -Wall -Werror #-} 16 17module Data.SBV.Utils.Lib ( mlift2, mlift3, mlift4, mlift5, mlift6, mlift7, mlift8 18 , joinArgs, splitArgs 19 , stringToQFS, qfsToString 20 , isKString 21 ) 22 where 23 24import Data.Char (isSpace, chr, ord) 25import Data.Dynamic (fromDynamic, toDyn, Typeable) 26import Data.Maybe (fromJust, isJust, isNothing) 27 28import Numeric (readHex, showHex) 29 30-- | We have a nasty issue with the usual String/List confusion in Haskell. However, we can 31-- do a simple dynamic trick to determine where we are. The ice is thin here, but it seems to work. 32isKString :: forall a. Typeable a => a -> Bool 33isKString _ = isJust (fromDynamic (toDyn (undefined :: a)) :: Maybe String) 34 35-- | Monadic lift over 2-tuples 36mlift2 :: Monad m => (a' -> b' -> r) -> (a -> m a') -> (b -> m b') -> (a, b) -> m r 37mlift2 k f g (a, b) = f a >>= \a' -> g b >>= \b' -> return $ k a' b' 38 39-- | Monadic lift over 3-tuples 40mlift3 :: Monad m => (a' -> b' -> c' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (a, b, c) -> m r 41mlift3 k f g h (a, b, c) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> return $ k a' b' c' 42 43-- | Monadic lift over 4-tuples 44mlift4 :: 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 45mlift4 k f g h i (a, b, c, d) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> return $ k a' b' c' d' 46 47-- | Monadic lift over 5-tuples 48mlift5 :: 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 49mlift5 k f g h i j (a, b, c, d, e) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> j e >>= \e' -> return $ k a' b' c' d' e' 50 51-- | Monadic lift over 6-tuples 52mlift6 :: 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 53mlift6 k f g h i j l (a, b, c, d, e, y) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> j e >>= \e' -> l y >>= \y' -> return $ k a' b' c' d' e' y' 54 55-- | Monadic lift over 7-tuples 56mlift7 :: 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 57mlift7 k f g h i j l m (a, b, c, d, e, y, z) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> j e >>= \e' -> l y >>= \y' -> m z >>= \z' -> return $ k a' b' c' d' e' y' z' 58 59-- | Monadic lift over 8-tuples 60mlift8 :: 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 61mlift8 k f g h i j l m n (a, b, c, d, e, y, z, w) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> j e >>= \e' -> l y >>= \y' -> m z >>= \z' -> n w >>= \w' -> return $ k a' b' c' d' e' y' z' w' 62 63-- Command line argument parsing code courtesy of Neil Mitchell's cmdargs package: see 64-- <http://github.com/ndmitchell/cmdargs/blob/master/System/Console/CmdArgs/Explicit/SplitJoin.hs> 65 66-- | Given a sequence of arguments, join them together in a manner that could be used on 67-- the command line, giving preference to the Windows @cmd@ shell quoting conventions. 68-- 69-- For an alternative version, intended for actual running the result in a shell, see "System.Process.showCommandForUser" 70joinArgs :: [String] -> String 71joinArgs = unwords . map f 72 where f x = q ++ g x ++ q 73 where hasSpace = any isSpace x 74 q = ['\"' | hasSpace || null x] 75 g ('\\':'\"':xs) = '\\':'\\':'\\':'\"': g xs 76 g "\\" | hasSpace = "\\\\" 77 g ('\"':xs) = '\\':'\"': g xs 78 g (x':xs) = x' : g xs 79 g [] = [] 80 81data State = Init -- either I just started, or just emitted something 82 | Norm -- I'm seeing characters 83 | Quot -- I've seen a quote 84 85-- | Given a string, split into the available arguments. The inverse of 'joinArgs'. 86-- Courtesy of the cmdargs package. 87splitArgs :: String -> [String] 88splitArgs = join . f Init 89 where -- Nothing is start a new string 90 -- Just x is accumulate onto the existing string 91 join :: [Maybe Char] -> [String] 92 join [] = [] 93 join xs = map fromJust a : join (drop 1 b) 94 where (a,b) = break isNothing xs 95 96 f Init (x:xs) | isSpace x = f Init xs 97 f Init "\"\"" = [Nothing] 98 f Init "\"" = [Nothing] 99 f Init xs = f Norm xs 100 f m ('\"':'\"':'\"':xs) = Just '\"' : f m xs 101 f m ('\\':'\"':xs) = Just '\"' : f m xs 102 f m ('\\':'\\':'\"':xs) = Just '\\' : f m ('\"':xs) 103 f Norm ('\"':xs) = f Quot xs 104 f Quot ('\"':'\"':xs) = Just '\"' : f Norm xs 105 f Quot ('\"':xs) = f Norm xs 106 f Norm (x:xs) | isSpace x = Nothing : f Init xs 107 f m (x:xs) = Just x : f m xs 108 f _ [] = [] 109 110-- | Given an SMTLib string (i.e., one that works in the string theory), convert it to a Haskell equivalent 111qfsToString :: String -> String 112qfsToString = go 113 where go "" = "" 114 115 go ('\\':'u':'{':d4:d3:d2:d1:d0:'}' : rest) | [(v, "")] <- readHex [d4, d3, d2, d1, d0] = chr v : go rest 116 go ('\\':'u': d3:d2:d1:d0 : rest) | [(v, "")] <- readHex [ d3, d2, d1, d0] = chr v : go rest 117 go ('\\':'u':'{': d3:d2:d1:d0:'}' : rest) | [(v, "")] <- readHex [ d3, d2, d1, d0] = chr v : go rest 118 go ('\\':'u':'{': d2:d1:d0:'}' : rest) | [(v, "")] <- readHex [ d2, d1, d0] = chr v : go rest 119 go ('\\':'u':'{': d1:d0:'}' : rest) | [(v, "")] <- readHex [ d1, d0] = chr v : go rest 120 go ('\\':'u':'{': d0:'}' : rest) | [(v, "")] <- readHex [ d0] = chr v : go rest 121 122 -- Otherwise, just proceed; hopefully we covered everything above 123 go (c : rest) = c : go rest 124 125-- | Given a Haskell string, convert it to SMTLib. if ord is 0x00020 to 0x0007E, then we print it 126-- will completely be different! 127stringToQFS :: String -> String 128stringToQFS = concatMap cvt 129 where cvt c 130 | c == '"' = "\"\"" 131 | oc >= 0x20 && oc <= 0x7E = [c] 132 | True = "\\u{" ++ showHex oc "" ++ "}" 133 where oc = ord c 134