diff --git a/CHANGES.md b/CHANGES.md index 7efd7d68..ce10eac5 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -5,13 +5,15 @@ * Generalize the signatures of the default project-embed implementations of the Queriable class. - * Generalize support for higher-order functions. These are still experimental, as SMTLib's higher-order - function support is nascent. (Version 3 of SMTLib will have proper support for such functions, which - is not released yet.) Currently, SBV can handle higher order versions of any, all, and filter, all - exported from Data.SBV.List module. These functions take as arguments lambda-functions, and SBV - translates them carefully for Z3 and CVC5 which has preliminary support. Proof-support in backend - solvers for higher-order functions is still quite weak, though KnuckleDragger makes things easier. - See Documentation.SBV.Examples.KnuckleDragger.Lists for several examples. + * Generalize support for polyorphic and higher-order functions. These are still experimental, as SMTLib's + higher-order function support is nascent. (Version 3 of SMTLib will have proper support for such functions, which + is not released yet.) Currently, SBV can handle polymorphic and higher-order usage of: 'reverse', 'any', 'all', 'filter', + 'map', 'foldl', 'foldr', 'zip', and 'zipWith'; all exported from the 'Data.SBV.List' module. These functions are supported + polymporphically, and (except reverse and zip) all take a function as an argument. SBV firstifies these + functions, and the resulting code is compatible with Z3 and CVC5. (Firstification might change in the + future, as SMTLib gains support for more higher-order features itself.) Proof-support in backend solvers + for higher-order functions is still quite weak, though KnuckleDragger makes things easier. See + Documentation.SBV.Examples.KnuckleDragger.Lists for several examples. * [BACKWARDS COMPATIBILITY] Removed rarely used functions mapi, foldli, foldri from Data.SBV.List. These can now be defined by the user as we have proper support for fold and map using lambdas. diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs index 90f13770..54e91df8 100644 --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -2510,7 +2510,7 @@ retrieveConstCode (UICodeC (v, _)) = Just v -- Plain constants instance HasKind a => SMTDefinable (SBV a) where sbv2smt a = do st <- mkNewState defaultSMTCfg (LambdaGen 0) - s <- lambdaStr st (kindOf a) a + s <- lambdaStr st True (kindOf a) a pure $ intercalate "\n" [ "; Automatically generated by SBV. Do not modify!" , "; Type: " ++ smtType (kindOf a) , show s @@ -3273,7 +3273,7 @@ lambdaArray :: forall a b. (SymVal a, HasKind b) => (SBV a -> SBV b) -> SArray a lambdaArray f = SBV . SVal k . Right $ cache g where k = KArray (kindOf (Proxy @a)) (kindOf (Proxy @b)) - g st = do def <- lambdaStr st (kindOf (Proxy @b)) f + g st = do def <- lambdaStr st True (kindOf (Proxy @b)) f newExpr st k (SBVApp (ArrayLambda def) []) -- | Turn a constant association-list and a default into a symbolic array. diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs index 5cfa2975..0dea3072 100644 --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -541,15 +541,15 @@ data SeqOp = SeqConcat -- ^ See StrConcat | SeqSuffixOf -- ^ See StrSuffixOf | SeqReplace -- ^ See StrReplace -- Polymorphic and higher order functions - | SBVReverse Kind -- ^ reverse k. Where k is either [a] or String. Reverses the argument, accordingly. - | SBVZip Kind Kind -- ^ zip k1 k2. Where we zip [k1] and [k2] to produce [(k1, k2)] + | SBVReverse Kind -- ^ reverse k. Where k is either [a] or String. Reverses the argument, accordingly. + | SBVZip Kind Kind -- ^ zip k1 k2. Where we zip [k1] and [k2] to produce [(k1, k2)] | SBVZipWith Kind Kind Kind SMTLambda -- ^ zipWith a b c fun. Where fun :: a -> b -> c, and zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] - | SBVMap Kind Kind SMTLambda -- ^ map a b fun. Where fun :: a -> b, and map :: (a -> b) -> [a] -> [b] - | SBVFoldl Kind Kind SMTLambda -- ^ foldl a b fun. Where fun :: b -> a -> b, and foldl :: (b -> a -> b) -> b -> [a] -> b - | SBVFoldr Kind Kind SMTLambda -- ^ foldr a b fun. Where fun :: a -> b -> b, and foldr :: (a -> b -> b) -> b -> [a] -> b - | SBVFilter Kind SMTLambda -- ^ filter a fun. Where fun :: a -> Bool, and filter :: (a -> Bool) -> [a] -> [a] - | SBVAll Kind SMTLambda -- ^ all a fun. Where fun :: a -> Bool, and all :: (a -> Bool) -> [a] -> Bool - | SBVAny Kind SMTLambda -- ^ any a fun. Where fun :: a -> Bool, and any :: (a -> Bool) -> [a] -> Bool + | SBVMap Kind Kind SMTLambda -- ^ map a b fun. Where fun :: a -> b, and map :: (a -> b) -> [a] -> [b] + | SBVFoldl Kind Kind SMTLambda -- ^ foldl a b fun. Where fun :: b -> a -> b, and foldl :: (b -> a -> b) -> b -> [a] -> b + | SBVFoldr Kind Kind SMTLambda -- ^ foldr a b fun. Where fun :: a -> b -> b, and foldr :: (a -> b -> b) -> b -> [a] -> b + | SBVFilter Kind SMTLambda -- ^ filter a fun. Where fun :: a -> Bool, and filter :: (a -> Bool) -> [a] -> [a] + | SBVAll Kind SMTLambda -- ^ all a fun. Where fun :: a -> Bool, and all :: (a -> Bool) -> [a] -> Bool + | SBVAny Kind SMTLambda -- ^ any a fun. Where fun :: a -> Bool, and any :: (a -> Bool) -> [a] -> Bool deriving (Eq, Ord, G.Data, NFData, Generic) -- | Show instance for SeqOp. Again, mapping is important. @@ -2284,6 +2284,7 @@ data SMTConfig = SMTConfig { , ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess. , redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied. , kdRibbonLength :: Int -- ^ Line length for KD proofs + , firstifyUniqueLen :: Int -- ^ Unique length used for firstified names. } -- | Ignore internal names and those the user told us to diff --git a/Data/SBV/Lambda.hs b/Data/SBV/Lambda.hs index 398a6b58..76779491 100644 --- a/Data/SBV/Lambda.hs +++ b/Data/SBV/Lambda.hs @@ -126,17 +126,35 @@ extractAllUniversals other = error $ unlines [ "" -- | Generic creator for anonymous lamdas. -lambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => (Defn -> b) -> State -> Kind -> a -> m b -lambdaGen trans inState fk f = inSubState inState $ \st -> trans <$> convert st fk (mkLambda st f) +lambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => Bool -> (Defn -> b) -> State -> Kind -> a -> m b +lambdaGen allowFreeVars trans inState fk f = inSubState inState $ \st -> handle <$> convert st fk (mkLambda st f) + where handle d@(Defn frees _ _ _) + | allowFreeVars || null frees + = trans d + | True + = error $ unlines [ "" + , "*** Data.SBV.Lambda: Detected free variables passed to a lambda." + , "***" + , "*** Free vars : " ++ unwords frees + , "*** Definition: " ++ sh d + , "***" + , "*** In certain contexts, SBV only allows closed-lambdas, i.e., those that do not have any free variables in." + , "***" + , "*** Please rewrite your program to pass the free variable as an explicit argument to the lambda if possible." + , "*** If this workaround isn't applicable, please report this as a use-case for further possible enhancements." + ] + + sh (Defn _frees Nothing _ops body) = body 0 + sh (Defn _frees (Just params) _ops body) = "(lambda " ++ extractAllUniversals params ++ "\n" ++ body 2 ++ ")" -- | Create an SMTLib lambda, in the given state. -lambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Kind -> a -> m SMTDef -lambda inState fk = lambdaGen mkLam inState fk +lambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Bool -> Kind -> a -> m SMTDef +lambda inState allowFreeVars fk = lambdaGen allowFreeVars mkLam inState fk where mkLam (Defn frees params ops body) = SMTLam fk frees ops (extractAllUniversals <$> params) body -- | Create an anonymous lambda, rendered as n SMTLib string. The kind passed is the kind of the final result. -lambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Kind -> a -> m SMTLambda -lambdaStr st k a = SMTLambda <$> lambdaGen mkLam st k a +lambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Bool -> Kind -> a -> m SMTLambda +lambdaStr st allowFreeVars k a = SMTLambda <$> lambdaGen allowFreeVars mkLam st k a where mkLam (Defn _frees Nothing _ops body) = body 0 mkLam (Defn _frees (Just params) _ops body) = "(lambda " ++ extractAllUniversals params ++ "\n" ++ body 2 ++ ")" @@ -336,7 +354,7 @@ toLambda level curProgInfo cfg expectedKind result@Result{resAsgns = SBVPgm asgn where mkAsgn (sv, e@(SBVApp (Label l) _)) = ((sv, converter e), Just l) mkAsgn (sv, e) = ((sv, converter e), Nothing) - converter = cvtExp curProgInfo (capabilities (solver cfg)) rm tableMap + converter = cvtExp cfg curProgInfo (capabilities (solver cfg)) rm tableMap out :: SV diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs index fb75ecda..35dbb4c6 100644 --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -414,7 +414,7 @@ map f l kb = kindOf (Proxy @b) klb = kindOf (Proxy @(SList b)) r st = do sva <- sbvToSV st l - lam <- lambdaStr st kb f + lam <- lambdaStr st False kb f let op = SeqOp (SBVMap ka kb lam) registerSpecialFunction st op newExpr st klb (SBVApp op [sva]) @@ -448,7 +448,7 @@ foldl f base l kb = kindOf (Proxy @b) r st = do svb <- sbvToSV st base svl <- sbvToSV st l - lam <- lambdaStr st kb f + lam <- lambdaStr st False kb f let op = SeqOp (SBVFoldl ka kb lam) registerSpecialFunction st op newExpr st kb (SBVApp op [svb, svl]) @@ -476,7 +476,7 @@ foldr f base l kb = kindOf (Proxy @b) r st = do svb <- sbvToSV st base svl <- sbvToSV st l - lam <- lambdaStr st kb f + lam <- lambdaStr st False kb f let op = SeqOp (SBVFoldr ka kb lam) registerSpecialFunction st op newExpr st kb (SBVApp op [svb, svl]) @@ -529,7 +529,7 @@ zipWith f xs ys r st = do svxs <- sbvToSV st xs svys <- sbvToSV st ys - lam <- lambdaStr st kb f + lam <- lambdaStr st False kb f let op = SeqOp (SBVZipWith ka kb kc lam) registerSpecialFunction st op newExpr st kr (SBVApp op [svxs, svys]) @@ -558,7 +558,7 @@ all f l | True = SBV $ SVal KBool $ Right $ cache r where r st = do sva <- sbvToSV st l - lam <- lambdaStr st KBool f + lam <- lambdaStr st False KBool f let op = SeqOp (SBVAll (kindOf (Proxy @a)) lam) registerSpecialFunction st op newExpr st KBool (SBVApp op [sva]) @@ -577,7 +577,7 @@ any f l | True = SBV $ SVal KBool $ Right $ cache r where r st = do sva <- sbvToSV st l - lam <- lambdaStr st KBool f + lam <- lambdaStr st False KBool f let op = SeqOp (SBVAny (kindOf (Proxy @a)) lam) registerSpecialFunction st op newExpr st KBool (SBVApp op [sva]) @@ -600,7 +600,7 @@ filter f l k = kindOf (Proxy @(SList a)) r st = do sva <- sbvToSV st l - lam <- lambdaStr st KBool f + lam <- lambdaStr st False KBool f let op = SeqOp (SBVFilter (kindOf (Proxy @a)) lam) registerSpecialFunction st op newExpr st k (SBVApp op [sva]) diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs index 1ed45828..3cea36aa 100644 --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -107,6 +107,7 @@ mkConfig s smtVersion startOpts = SMTConfig { verbose = Fals , ignoreExitCode = False , redirectVerbose = Nothing , kdRibbonLength = 40 + , firstifyUniqueLen = 6 } -- | If supported, this makes all output go to stdout, which works better with SBV diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs index d187ed06..9d1a034c 100644 --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -18,8 +18,11 @@ module Data.SBV.SMT.SMTLib2(cvt, cvtExp, cvtCV, cvtInc, declUserFuns, constructTables) where +import Crypto.Hash.SHA512 (hash) +import qualified Data.ByteString.Base16 as B +import qualified Data.ByteString.Char8 as BC + import Data.Bits (bit) -import Data.Char (isSpace) import Data.List (intercalate, partition, nub, elemIndex) import Data.Maybe (listToMaybe, catMaybes) @@ -44,18 +47,26 @@ import qualified Data.Generics.Uniplate.Data as G import qualified Data.Graph as DG --- | A globally (hopefully!) unique name for the operator --- TODO: Perhaps replace this with a simpler hash? -getFuncName :: Op -> String -getFuncName o = "|" ++ map clean (compress (show o)) ++ "|" - where clean c | isSpace c || c == '|' = '_' - | True = c - - compress (x:y:rest) - | all isSpace [x, y] = compress (y:rest) - | True = x : compress (y:rest) - compress (x:rest) = x : compress rest - compress "" = "" +-- | For higher-order functions, we firstify them. This requires a uniqu name creation. Here, +-- we create a firstified name based on the operation. The suffix appended will have at most uniqLen length. +firstify :: Int -> Op -> String +firstify uniqLen o = prefix o ++ "_" ++ take uniqLen (BC.unpack (B.encode (hash (BC.pack (show o))))) + where prefix (SeqOp SBVReverse {}) = "sbv.reverse" + prefix (SeqOp SBVZip {}) = "sbv.zip" + prefix (SeqOp SBVZipWith {}) = "sbv.zipWith" + prefix (SeqOp SBVMap {}) = "sbv.map" + prefix (SeqOp SBVFoldl {}) = "sbv.foldl" + prefix (SeqOp SBVFoldr {}) = "sbv.foldr" + prefix (SeqOp SBVFilter {}) = "sbv.filter" + prefix (SeqOp SBVAll {}) = "sbv.all" + prefix (SeqOp SBVAny {}) = "sbv.any" + prefix _ = error $ unlines [ "***" + , "*** Data.SBV.firstify: Didn't expect firstification to be called." + , "***" + , "*** Operator: " ++ show o + , "***" + , "*** Please report this as a bug." + ] -- | Translate a problem into an SMTLib2 script cvt :: SMTLibConverter ([String], [String]) @@ -255,8 +266,8 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs ++ map nonConstTable nonConstTables ++ [ "; --- uninterpreted constants ---" ] ++ concatMap (declUI curProgInfo) uis - ++ [ "; --- SBV Function definitions" | not (null specialFuncs) ] - ++ concat [declSBVFunc cfg op | op <- reverse specialFuncs] + ++ [ "; --- Firstified function definitions" | not (null specialFuncs) ] + ++ concat firstifiedFuncs ++ [ "; --- user defined functions ---"] ++ userDefs ++ [ "; --- assignments ---" ] @@ -266,7 +277,40 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs ++ [ "; --- formula ---" ] ++ finalAssert - userDefs = declUserFuns defs + + firstifiedFuncs + = case dup res of + Nothing -> map (snd . snd) res + Just (o, o', n) -> let curLen = firstifyUniqueLen cfg + in error $ unlines [ "" + , "*** Data.SBV: Insufficient unique length in firstification." + , "***" + , "*** Operator 1 : " ++ show o + , "*** Operator 2 : " ++ show o' + , "*** Mapped name: " ++ n + , "*** Unique len : " ++ show curLen + , "***" + , "*** Such collisions should be rare, but looks like you ran into one!" + , "*** Try running with an increased unique-length:" + , "***" + , "*** solver{firstifyUniqueLen = N}" + , "***" + , "*** where N is larger than " ++ show curLen + , "***" + , "*** For instance:" + , "***" + , "*** satWith z3{firstUniqueLen = " ++ show (curLen + 1) ++ "}" + , "***" + , "*** If that doesn't resolve the problem, or if you believe this is caused by some" + , "*** other problem, please report his as a bug." + ] + where res = [(op, declSBVFunc cfg op) | op <- reverse specialFuncs] + dup [] = Nothing + dup ((o, (n, _)): xs) = case [o' | (o', (n', _)) <- xs, n == n'] of + [] -> dup xs + (o' : _) -> Just (o, o', n) + + userDefs = declUserFuns defs exportedDefs | null userDefs = ["; No calls to 'smtFunction' found."] @@ -321,21 +365,45 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs _ -> Nothing -- Declare "known" SBV functions here -declSBVFunc :: SMTConfig -> Op -> [String] -declSBVFunc cfg op = case op of - SeqOp (SBVReverse KString) -> mkStringRev - SeqOp (SBVReverse (KList k)) -> mkSeqRev (KList k) - SeqOp (SBVZip k1 k2) -> mkZip k1 k2 Nothing - SeqOp (SBVZipWith k1 k2 k3 (SMTLambda f)) -> mkZip k1 k2 (Just (k3, f)) - SeqOp (SBVMap k1 k2 (SMTLambda f)) -> mkMap k1 k2 f - SeqOp (SBVFoldl k1 k2 (SMTLambda f)) -> mkFoldl k1 k2 f - SeqOp (SBVFoldr k1 k2 (SMTLambda f)) -> mkFoldr k1 k2 f - SeqOp (SBVFilter ek (SMTLambda f)) -> mkFilter ek f - SeqOp (SBVAll ek (SMTLambda f)) -> mkAnyAll True ek f - SeqOp (SBVAny ek (SMTLambda f)) -> mkAnyAll False ek f - _ -> error $ "Data.SBV.declSBVFunc: Unexpected internal function: " +declSBVFunc :: SMTConfig -> Op -> (String, [String]) +declSBVFunc cfg op = (nm, comment ++ body) + where nm = firstify (firstifyUniqueLen cfg) op + + comment = ["; Firstified function: " ++ htyp] + + body = case op of + SeqOp (SBVReverse KString) -> mkStringRev + SeqOp (SBVReverse (KList k)) -> mkSeqRev (KList k) + SeqOp (SBVZip k1 k2) -> mkZip k1 k2 Nothing + SeqOp (SBVZipWith k1 k2 k3 (SMTLambda f)) -> mkZip k1 k2 (Just (k3, f)) + SeqOp (SBVMap k1 k2 (SMTLambda f)) -> mkMap k1 k2 f + SeqOp (SBVFoldl k1 k2 (SMTLambda f)) -> mkFoldl k1 k2 f + SeqOp (SBVFoldr k1 k2 (SMTLambda f)) -> mkFoldr k1 k2 f + SeqOp (SBVFilter ek (SMTLambda f)) -> mkFilter ek f + SeqOp (SBVAll ek (SMTLambda f)) -> mkAnyAll True ek f + SeqOp (SBVAny ek (SMTLambda f)) -> mkAnyAll False ek f + _ -> error $ "Data.SBV.declSBVFunc: Unexpected internal function: " ++ show (op, nm) - where nm = getFuncName op + + shf :: String -> [Kind] -> Kind -> String + shf f args rt = f ++ " :: " ++ intercalate " -> " (map show (args ++ [rt])) + + shh :: String -> ([Kind], Kind) -> ([Kind], Kind) -> String + shh f (fargs, fret) (args, rt) = f ++ " :: (" ++ intercalate " -> " (map show (fargs ++ [fret])) ++ ") -> " + ++ intercalate " -> " (map show (args ++ [rt])) + + htyp = case op of + SeqOp (SBVReverse KString) -> shf "reverse" [KString] KString + SeqOp (SBVReverse k@KList{}) -> shf "reverse" [k] k + SeqOp (SBVZip a b) -> shf "zip" [KList a, KList b] (KList (KTuple [a, b])) + SeqOp (SBVZipWith a b c _) -> shh "zipWith" ([a, b], c) ([KList a, KList b], KList c) + SeqOp (SBVMap a b _) -> shh "map" ([a], b) ([KList a], KList b) + SeqOp (SBVFoldl a b _) -> shh "foldl" ([b, a], b) ([b, KList a], b) + SeqOp (SBVFoldr a b _) -> shh "foldr" ([a, b], b) ([b, KList a], b) + SeqOp (SBVFilter a _) -> shh "filter" ([a], KBool) ([KList a], KList a) + SeqOp (SBVAll a _) -> shh "all" ([a], KBool) ([KList a], KBool) + SeqOp (SBVAny a _) -> shh "any" ([a], KBool) ([KList a], KBool) + _ -> error $ "Data.SBV.declSBVFunc: Unexpected internal function: " ++ show (op, nm) -- in Z3, lambdas are applied with select. In CVC5, it's @. This might change with higher-order features being added to SMTLib in v3 par x = "(" ++ x ++ ")" @@ -614,8 +682,8 @@ cvtInc curProgInfo inps newKs (_, consts) tbls uis (SBVPgm asgnsSeq) cstrs cfg = declDef :: ProgInfo -> SMTConfig -> TableMap -> (SV, SBVExpr) -> [String] declDef curProgInfo cfg tableMap (s, expr) = case expr of - SBVApp (Label m) [e] -> defineFun cfg (s, cvtSV e) (Just m) - e -> defineFun cfg (s, cvtExp curProgInfo caps rm tableMap e) Nothing + SBVApp (Label m) [e] -> defineFun cfg (s, cvtSV e) (Just m) + e -> defineFun cfg (s, cvtExp cfg curProgInfo caps rm tableMap e) Nothing where caps = capabilities (solver cfg) rm = roundingMode cfg @@ -813,8 +881,8 @@ getTable m i | Just tn <- i `IM.lookup` m = tn | True = "table" ++ show i -- constant tables are always named this way -cvtExp :: ProgInfo -> SolverCapabilities -> RoundingMode -> TableMap -> SBVExpr -> String -cvtExp curProgInfo caps rm tableMap expr@(SBVApp _ arguments) = sh expr +cvtExp :: SMTConfig -> ProgInfo -> SolverCapabilities -> RoundingMode -> TableMap -> SBVExpr -> String +cvtExp cfg curProgInfo caps rm tableMap expr@(SBVApp _ arguments) = sh expr where hasPB = supportsPseudoBooleans caps hasInt2bv = supportsInt2bv caps hasDistinct = supportsDistinct caps @@ -944,6 +1012,8 @@ cvtExp curProgInfo caps rm tableMap expr@(SBVApp _ arguments) = sh expr ps = " (" ++ unwords (map smtType params) ++ ") " aResult = "(_ is (" ++ fld ++ ps ++ smtType res ++ "))" + firstifiedName = firstify (firstifyUniqueLen cfg) + sh (SBVApp Ite [a, b, c]) = "(ite " ++ cvtSV a ++ " " ++ cvtSV b ++ " " ++ cvtSV c ++ ")" sh (SBVApp (LkUp (t, aKnd, _, l) i e) []) @@ -1090,16 +1160,16 @@ cvtExp curProgInfo caps rm tableMap expr@(SBVApp _ arguments) = sh expr sh (SBVApp (RegExOp o@RegExNEq{}) []) = show o -- Reverse and higher order functions are special - sh (SBVApp o@(SeqOp SBVReverse{}) args) = "(" ++ getFuncName o ++ " " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp o@(SeqOp SBVZip{}) args) = "(" ++ getFuncName o ++ " " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp o@(SeqOp SBVZipWith{}) args) = "(" ++ getFuncName o ++ " " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp o@(SeqOp SBVReverse{}) args) = "(" ++ getFuncName o ++ " " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp o@(SeqOp SBVMap{}) args) = "(" ++ getFuncName o ++ " " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp o@(SeqOp SBVFoldl{}) args) = "(" ++ getFuncName o ++ " " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp o@(SeqOp SBVFoldr{}) args) = "(" ++ getFuncName o ++ " " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp o@(SeqOp SBVFilter{}) args) = "(" ++ getFuncName o ++ " " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp o@(SeqOp SBVAll{} ) args) = "(" ++ getFuncName o ++ " " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp o@(SeqOp SBVAny{} ) args) = "(" ++ getFuncName o ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp o@(SeqOp SBVReverse{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp o@(SeqOp SBVZip{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp o@(SeqOp SBVZipWith{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp o@(SeqOp SBVReverse{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp o@(SeqOp SBVMap{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp o@(SeqOp SBVFoldl{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp o@(SeqOp SBVFoldr{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp o@(SeqOp SBVFilter{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp o@(SeqOp SBVAll{} ) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp o@(SeqOp SBVAny{} ) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" sh (SBVApp (SeqOp op) args) = "(" ++ show op ++ " " ++ unwords (map cvtSV args) ++ ")" diff --git a/sbv.cabal b/sbv.cabal index ad93670b..05f1e302 100644 --- a/sbv.cabal +++ b/sbv.cabal @@ -87,12 +87,15 @@ Library default-language: Haskell2010 build-depends : QuickCheck , array - , async >= 2.2.5 + , async >= 2.2.5 + , bytestring + , base16-bytestring + , cryptohash-sha512 , containers , deepseq , directory , filepath - , libBF >= 0.6.8 + , libBF >= 0.6.8 , mtl , pretty , process