diff --git a/SBVTestSuite/GoldFiles/lambda81.gold b/SBVTestSuite/GoldFiles/lambda81.gold new file mode 100644 index 00000000..8fb03781 --- /dev/null +++ b/SBVTestSuite/GoldFiles/lambda81.gold @@ -0,0 +1,16 @@ +CAUGHT EXCEPTION + + +*** Data.SBV.Lambda: Detected free variables passed to a lambda. +*** +*** Free vars : l1_s0 +*** Definition: (lambda ((l2_s0 Int)) +*** (+ l1_s0 l2_s0)) +*** +*** 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. + +CallStack (from HasCallStack): + error, called at ./Data/SBV/Lambda.hs:135:13 in sbv-11.0.5-inplace:Data.SBV.Lambda \ No newline at end of file diff --git a/SBVTestSuite/TestSuite/Basics/Lambda.hs b/SBVTestSuite/TestSuite/Basics/Lambda.hs index 0ab4bdb0..eb919f27 100644 --- a/SBVTestSuite/TestSuite/Basics/Lambda.hs +++ b/SBVTestSuite/TestSuite/Basics/Lambda.hs @@ -27,7 +27,7 @@ module TestSuite.Basics.Lambda(tests) where import Prelude hiding((++), map, foldl, foldr, sum, length, zip, zipWith, all, any, concat, filter) import qualified Prelude as P -import Control.Monad (unless) +import Control.Monad (unless, void) import qualified Control.Exception as C import Data.SBV.Control @@ -231,6 +231,7 @@ tests = , goldenCapturedIO "lambda79" $ \f -> sbv2smt def_t1 >>= writeFile f , goldenCapturedIO "lambda80" $ \f -> sbv2smt def_t2 >>= writeFile f + , goldenCapturedIO "lambda81" $ errorOut freeVar1 ] P.++ qc1 "lambdaQC1" P.sum (foldr (+) (0::SInteger)) P.++ qc2 "lambdaQC2" (+) (smtFunction "sadd" ((+) :: SInteger -> SInteger -> SInteger)) @@ -362,6 +363,19 @@ eval2 cArg1 cArg2 (sFun, cFun) rf = do m <- runSMTWith z3{verbose=True, redirect getModel _ -> error $ "Unexpected output: " P.++ show cs +-- Tests that error out +errorOut :: (SMTConfig -> IO a) -> FilePath -> IO () +errorOut t rf = void (t z3{verbose=True, redirectVerbose=Just rf}) + `C.catch` \(e::C.SomeException) -> do appendFile rf "CAUGHT EXCEPTION\n\n" + appendFile rf (show e) + +-- Don't allow free variables in higher-order functions. Firstification can't handle these. +freeVar1 :: SMTConfig -> IO SatResult +freeVar1 cfg = satWith cfg $ do + zs <- free_ + xs <- free_ + constrain $ xs .== literal [1,2,3::Integer] + pure $ zs .== map (\x -> map (\y -> x+y) (literal [3,4,5])) xs {- HLint ignore module "Use map once" -} {- HLint ignore module "Use sum" -}