----------------------------------------------------------------------------- -- | -- Module : TestSuite.Basics.Lambda -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- Test lambda generation ----------------------------------------------------------------------------- {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wall -Werror #-} module TestSuite.Basics.Lambda(tests) where import Prelude hiding((++), map, foldl, foldr, sum, length, zip, zipWith, all, any, concat, filter, head) import qualified Prelude as P import qualified Data.List as P (partition) import Control.Monad (unless, void) import qualified Control.Exception as C import Data.SBV.Control import Data.SBV.Internals hiding(free_) import Documentation.SBV.Examples.Misc.Definitions import Data.SBV.List import Data.SBV.Tuple hiding (fst, snd) import Data.Proxy import Utils.SBVTestFramework data P mkSymbolic [''P] drinker :: Predicate drinker = pure $ quantifiedBool $ \(Exists x) (Forall y) -> d x .=> d y where d :: SP -> SBool d = uninterpret "D" -- Test suite tests :: TestTree tests = testGroup "Basics.Lambda" $ [ goldenCapturedIO "lambda01" $ record $ \st -> show <$> lambdaStr st TopLevel (kindOf (Proxy @SInteger)) (2 :: SInteger) , goldenCapturedIO "lambda02" $ record $ \st -> show <$> lambdaStr st TopLevel (kindOf (Proxy @SInteger)) (\x -> x+1 :: SInteger) , goldenCapturedIO "lambda03" $ record $ \st -> show <$> lambdaStr st TopLevel (kindOf (Proxy @SInteger)) (\x y -> x+y*2 :: SInteger) , goldenCapturedIO "lambda04" $ eval1 [1 .. 3 :: Integer] (mapl (const sFalse), P.map (const False)) , goldenCapturedIO "lambda05" $ eval1 [1 .. 5 :: Integer] (mapl (+1) . mapl (+2), P.map (+1) . P.map (+2)) , goldenCapturedIO "lambda06" $ eval1 [1 .. 5 :: Integer] ( mapl (\x -> P.sum [x .^ literal i | i <- [1..10 :: Integer]]) , P.map (\x -> P.sum [x ^ i | i <- [1..10 :: Integer]]) ) , goldenCapturedIO "lambda07" $ eval1 ([[1..5], [1..10], [1..20]] :: [[Integer]]) ( sum . map sum , P.sum . P.map P.sum ) , goldenCapturedIO "lambda08" $ eval1 [1 .. 5 :: Int64] (mapl (+1), P.map (+1)) , goldenCapturedIO "lambda09" $ eval1 [1 .. 5 :: Int8] (mapl (+1), P.map (+1)) , goldenCapturedIO "lambda10" $ eval1 [1 .. 5 :: Integer] (mapl (+1), P.map (+1)) , goldenCapturedIO "lambda11" $ eval1 [1 .. 5 :: Word8] (mapl (+1), P.map (+1)) , goldenCapturedIO "lambda12" $ eval1 [1 .. 3 :: Integer] (map singleton, P.map (: [])) , goldenCapturedIO "lambda13" $ eval1 [(x, y) | x <- [1..3], y <- [4..6 :: Integer]] (map (\t -> t^._1 + t^._2), P.map (uncurry (+))) , goldenCapturedIO "lambda14" $ eval1 [1 .. 5 :: Integer] (zipWithL (+) [sEnum|10..15|], P.zipWith (+) [10..15]) , goldenCapturedIO "lambda15" $ eval1 [1 .. 5 :: Integer] (foldlL (+) 0, P.sum) , goldenCapturedIO "lambda16" $ eval1 [1 .. 5 :: Integer] (foldlL (*) 1, P.product) , goldenCapturedIO "lambda17" $ eval1 [1 .. 5 :: Integer] ( foldlL (\soFar elt -> singleton elt ++ soFar) [] , P.foldl (\soFar elt -> elt : soFar) [] ) , goldenCapturedIO "lambda18" $ eval1 [1 .. 5 :: Integer] ( foldlL (\b t -> t^._1 + b + t^._2) 0 . zip [sEnum|10..15|] , P.foldl (\b (i, a) -> i + b + a) 0 . P.zip [ 10..15 ] ) , goldenCapturedIO "lambda19" $ eval1 [1 .. 5 :: Integer] (foldrL (+) 0, P.foldr (+) 0) , goldenCapturedIO "lambda20" $ eval1 [1 .. 5 :: Integer] (foldrL (*) 1, P.foldr (*) 1) , goldenCapturedIO "lambda21" $ eval1 [1 .. 5 :: Integer] ( foldrL (\elt soFar -> soFar ++ singleton elt) [] , P.foldr (\elt soFar -> soFar P.++ [elt]) [] ) , goldenCapturedIO "lambda22" $ eval2 [1 .. 10 :: Integer] [11..20 :: Integer] (zip, P.zip) , goldenCapturedIO "lambda23" $ eval2 [1 .. 10 :: Integer] [10, 9 .. 1 :: Integer] ( \a b -> foldrL (+) 0 ( map (\t -> t^._1+t^._2::SInteger) ( zip a b)) , \a b -> P.foldr (+) 0 (P.map (\t -> fst t+snd t::Integer ) (P.zip a b)) ) , goldenCapturedIO "lambda24" $ eval2 [1 .. 10 :: Integer] [11..20 :: Integer] (zipWithL (+), P.zipWith (+)) , goldenCapturedIO "lambda25" $ eval2 [1 .. 10 :: Integer] [10, 9 .. 1 :: Integer] ( \a b -> foldrL (+) 0 ( zipWithL (+) a b) , \a b -> P.foldr (+) 0 (P.zipWith (+) a b) ) , goldenCapturedIO "lambda26" $ eval1 ([[1..5], [1..10], [1..20]] :: [[Integer]]) (concat, P.concat) , goldenCapturedIO "lambda27" $ eval1 [2, 4, 6, 8, 10 :: Integer] (all (\x -> x `sMod` 2 .== 0), P.all (\x -> x `mod` 2 == 0)) , goldenCapturedIO "lambda28" $ eval1 [2, 4, 6, 1, 8, 10 :: Integer] (all (\x -> x `sMod` 2 .== 0), P.all (\x -> x `mod` 2 == 0)) , goldenCapturedIO "lambda29" $ eval1 [2, 4, 6, 8, 10 :: Integer] (any (\x -> x `sMod` 2 ./= 0), P.any (\x -> x `mod` 2 /= 0)) , goldenCapturedIO "lambda30" $ eval1 [2, 4, 6, 1, 8, 10 :: Integer] (any (\x -> x `sMod` 2 .== 0), P.any (\x -> x `mod` 2 == 0)) , goldenCapturedIO "lambda31" $ eval1 [1 .. 10 :: Integer] (filterL (\x -> x `sMod` 2 .== 0), P.filter (\x -> x `mod` 2 == 0)) , goldenCapturedIO "lambda32" $ eval1 [1 .. 10 :: Integer] (filterL (\x -> x `sMod` 2 ./= 0), P.filter (\x -> x `mod` 2 /= 0)) , goldenCapturedIO "lambda33" $ record $ \st -> show <$> lambdaStr st TopLevel (kindOf (Proxy @SInt8)) (0 :: SInt8) , goldenCapturedIO "lambda34" $ record $ \st -> show <$> lambdaStr st TopLevel (kindOf (Proxy @SInt8)) (\x -> x+1 :: SInt8) , goldenCapturedIO "lambda35" $ record $ \st -> show <$> lambdaStr st TopLevel (kindOf (Proxy @SInt8)) (\x y -> x+y :: SInt8) , goldenCapturedIO "lambda36" $ record $ \st -> constraintStr st $ \(Forall (_ :: SBool)) -> sTrue , goldenCapturedIO "lambda37" $ record $ \st -> constraintStr st $ \(Forall b) -> sNot b , goldenCapturedIO "lambda38" $ record $ \st -> constraintStr st $ \(Forall x) (Forall y) -> x .== (0 :: SInteger) .|| y , goldenCapturedIO "lambda40" $ record $ \st -> show <$> lambdaStr st TopLevel KUnbounded (0 :: SInteger) , goldenCapturedIO "lambda41" $ record $ \st -> show <$> lambdaStr st TopLevel KUnbounded (\x -> x+1 :: SInteger) , goldenCapturedIO "lambda42" $ record $ \st -> show <$> lambdaStr st TopLevel KUnbounded (\x y -> x+y :: SInteger) , goldenCapturedIO "lambda43" $ record $ \st -> show <$> lambdaStr st TopLevel (KBounded False 32) (0 :: SWord32) , goldenCapturedIO "lambda44" $ record $ \st -> show <$> lambdaStr st TopLevel (KBounded False 32) (\x -> x+1 :: SWord32) , goldenCapturedIO "lambda45" $ record $ \st -> show <$> lambdaStr st TopLevel (KBounded False 32) (\x y -> x+y :: SWord32) , goldenCapturedIO "lambda46" $ runSat ((.== 5) . add1) , goldenCapturedIO "lambda47" $ runSat2 (\a r -> a .== 5 .&& sumToN a .== r) , goldenCapturedIO "lambda47_c" $ runSat (sumToN 5 .==) , goldenCapturedIO "lambda48" $ runSat2 (\a r -> a .== [1,2,3::SInteger] .&& len a .== r) , goldenCapturedIO "lambda48_c" $ runSat (len [1,2,3::SInteger] .==) , goldenCapturedIO "lambda49" $ runSat2 (\a r -> a .== 20 .&& isEven a .== r) , goldenCapturedIO "lambda49_c" $ runSat (isEven 20 .==) , goldenCapturedIO "lambda50" $ runSat2 (\a r -> a .== 21 .&& isEven a .== r) , goldenCapturedIO "lambda50_c" $ runSat (isEven 21 .==) , goldenCapturedIO "lambda51" $ runSat2 (\a r -> a .== 20 .&& isOdd a .== r) , goldenCapturedIO "lambda51_c" $ runSat (isOdd 20 .==) , goldenCapturedIO "lambda52" $ runSat2 (\a r -> a .== 21 .&& isOdd a .== r) , goldenCapturedIO "lambda52_c" $ runSat (isOdd 21 .==) -- make sure we can pass globals , goldenCapturedIO "lambda53" $ runSat $ \x -> x .== smtFunction "foo" (+(x::SInteger)) x -- Make sure we can handle dependency orders , goldenCapturedIO "lambda54" $ runSat $ \x -> let foo = smtFunction "foo" (\a -> bar a + 1) bar = smtFunction "bar" (+1) in bar x + foo x .== (x :: SInteger) , goldenCapturedIO "lambda55" $ runSat $ \x -> let foo = smtFunction "foo" (\a -> bar a + 1) bar = smtFunction "bar" (+1) in foo x + bar x .== (x :: SInteger) , goldenCapturedIO "lambda56" $ runUnsat $ \x -> let foo = smtFunction "foo" (\a -> bar a + 1) bar = smtFunction "bar" (\a -> foo a + 1) in foo x + bar x .== (x :: SInteger) , goldenCapturedIO "lambda57" $ runSat $ \x -> let f1 = smtFunction "f1" (\a -> ite (a .== 0) 0 (1 + (f1 (a-1) + f2 (a-2)))) f2 = smtFunction "f2" (\a -> ite (a .== 0) 0 (1 + (f2 (a-1) + f3 (a-2)))) f3 = smtFunction "f3" (\a -> ite (a .== 0) 0 (1 + (f3 (a-1) + f4 (a-2)))) f4 = smtFunction "f4" (\a -> ite (a .== 0) 0 (1 + (f4 (a-1) + f1 (a-2)))) in f1 x .== (x :: SWord8) -- Quantified axioms , goldenCapturedIO "lambda58" $ record $ \st -> constraintStr st $ \(Forall b) (Exists c) -> sNot b .|| c , goldenCapturedIO "lambda59" $ record $ \st -> constraintStr st $ \(Forall x) (Exists y) -> x .== (0 :: SInteger) .|| y , goldenCapturedIO "lambda60" $ runAxSat $ constrain $ \(Forall x) (Exists y) (Exists z) -> y .> (x+z :: SInteger) , goldenCapturedIO "lambda61" $ runAxUnsat $ constrain $ \(Forall x) (Exists y) -> y .> (x :: SWord8) -- Quantified booleans , goldenCapturedIO "lambda62" $ \rf -> do m <- proveWith z3{verbose=True, redirectVerbose=Just rf} drinker appendFile rf ("\nRESULT:\n" <> show m <> "\n") `C.catch` (\(e :: C.SomeException) -> appendFile rf ("\nEXCEPTION CAUGHT:\n" <> show e <> "\n")) -- Special relations (kind of lambda related) , goldenCapturedIO "lambda63" $ runP $ quantifiedBool (\(Forall x) -> rel (x, x)) , goldenCapturedIO "lambda64" $ runP $ po .=> quantifiedBool (\(Forall x) -> rel (x, x)) , goldenCapturedIO "lambda65" $ runP $ poI .=> quantifiedBool (\(Forall x) -> leq (x, x)) , goldenCapturedIO "lambda66" $ runP $ let u = uninterpret "U" :: Relation Integer tcU = mkTransitiveClosure "tcU" u in quantifiedBool (\(Forall x) (Forall y) (Forall z) -> (u (x, y) .&& u (y, z)) .=> tcU (x, z)) , goldenCapturedIO "lambda67" $ runP $ let u = uninterpret "U" :: Relation Word8 tcU = mkTransitiveClosure "tcU" u in quantifiedBool (\(Forall x) (Forall y) (Forall z) -> (u (x, y) .&& u (y, z)) .=> tcU (x, z)) -- Not really lambda related, but kind of fits in here , goldenCapturedIO "lambda68" $ runS $ \(Forall x) -> uninterpret "F" x .== 2*x+(3::SInteger) , goldenCapturedIO "lambda69" $ runS $ \(Forall x) (Forall y) -> uninterpret "F" x y .== 2*x+(3-y::SInteger) -- Most skolems are tested inline, here's a fancy one! , goldenCapturedIO "lambda70" $ let phi :: ExistsUnique "x" Integer -> SBool phi (ExistsUnique x) = x .== 0 .|| x .== 1 nPhi :: Forall "x" Integer -> Exists "x_eu1" Integer -> Exists "x_eu2" Integer -> SBool nPhi = qNot phi snPhi :: Forall "x" Integer -> SBool snPhi = skolemize nPhi in runS snPhi , goldenCapturedIO "lambda71" $ \f -> sbv2smt def_foo >>= writeFile f , goldenCapturedIO "lambda72" $ \f -> sbv2smt def_bar >>= writeFile f , goldenCapturedIO "lambda73" $ \f -> sbv2smt def_baz >>= writeFile f , goldenCapturedIO "lambda74" $ \f -> sbv2smt def_e >>= writeFile f , goldenCapturedIO "lambda75" $ \f -> sbv2smt def_o >>= writeFile f , goldenCapturedIO "lambda76" $ \f -> sbv2smt (2 :: SInteger) >>= writeFile f , goldenCapturedIO "lambda77" $ \f -> sbv2smt (literal 'a' :: SChar) >>= writeFile f , goldenCapturedIO "lambda78" $ \f -> sbv2smt (literal [1,2,3] :: SList Integer) >>= writeFile f , goldenCapturedIO "lambda79" $ \f -> sbv2smt def_t1 >>= writeFile f , goldenCapturedIO "lambda80" $ \f -> sbv2smt def_t2 >>= writeFile f , goldenCapturedIO "lambda81" $ regularRun filterHead , goldenCapturedIO "lambda82" $ eval1 [1 .. 5 :: Integer] ( mapl (\x -> map (\y -> x + y) (literal [4, 5, 6])) , P.map (\x -> P.map (\y -> x + y) [4, 5, 6]) ) , goldenCapturedIO "lambda83" $ errorOut noFreeVars1 , goldenCapturedIO "lambda84" $ errorOut noFreeVars2 , goldenCapturedIO "lambda85" $ eval1 [1 .. 10 :: Integer] (partitionL (\x -> x `sMod` 2 .== 0), P.partition (\x -> x `mod` 2 == 0)) , goldenCapturedIO "lambda86" $ eval1 [1 .. 10 :: Integer] (partitionL (\x -> x `sMod` 2 ./= 0), P.partition (\x -> x `mod` 2 /= 0)) , let cls :: SInteger -> Closure SInteger (SInteger -> SInteger) cls x = Closure { closureEnv = x , closureFun = \env y -> env + y } in goldenCapturedIO "lambda87" $ eval2 [1 .. 3 :: Integer] [6 .. 8 :: Integer] ( \xs ys -> map (\x -> map (cls x) xs) ys , \xs ys -> P.map (\x -> P.map (\y -> x + y) xs) ys ) , let cls :: SList Integer -> Closure (SList Integer) (SList Integer -> SList Integer) cls ys = Closure { closureEnv = ys , closureFun = \env xs -> xs ++ env } in goldenCapturedIO "lambda88" $ eval2 [[1 .. 3 :: Integer], [4 .. 6 :: Integer]] [7 .. 9 :: Integer] ( \xss ys -> map (cls ys) xss , \xss ys -> P.map (P.++ ys) xss ) ] P.++ qc1 "lambdaQC1" P.sum (foldr ((+) @SInteger) (0::SInteger)) P.++ qc2 "lambdaQC2" (+) (smtFunction "sadd" ((+) :: SInteger -> SInteger -> SInteger)) P.++ qc1 "lambdaQC3" (\n -> let pn = abs n in (pn * (pn+1)) `sDiv` 2) (let ssum = smtFunction "ssum" $ \(n :: SInteger) -> let pn = abs n in ite (pn .== 0) 0 (pn + ssum (pn - 1)) in ssum) where def_foo, def_bar, def_baz, def_e, def_o :: SInteger -> SInteger def_foo = smtFunction "foo" $ \x -> def_bar (x-1) def_bar = smtFunction "bar" $ \x -> def_bar (x-1) def_baz = smtFunction "baz" $ \x -> x+1 def_e = smtFunction "e" $ \x -> def_o (x-1) def_o = smtFunction "o" $ \x -> def_e (x-1) def_t1 = smtFunction "foo" (\x -> select [1,2,3] (0 :: SWord32) (x::SInteger)) def_t2 = smtFunction "foo" (\x -> select [x+1,x+2,x+3] (0 :: SInteger) (x::SInteger)) mapl :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> SList a -> SList b mapl = map foldlL :: (SymVal a, SymVal b) => (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b foldlL = foldl foldrL :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b foldrL = foldr zipWithL :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c zipWithL = zipWith filterL :: SymVal a => (SBV a -> SBool) -> SList a -> SList a filterL = filter partitionL :: SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a] partitionL = partition rel, leq :: Relation Integer rel = uninterpret "R" leq = uncurry $ smtFunction "leq" (.<=) po = isPartialOrder "poR" rel poI = isPartialOrder "poI" leq regularRun tc goldFile = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just goldFile} tc appendFile goldFile ("\n FINAL:" <> show r <> "\nDONE!\n") record :: (State -> IO String) -> FilePath -> IO () record gen rf = do st <- mkNewState defaultSMTCfg (LambdaGen (Just 0)) appendFile rf . (P.++ "\n") =<< gen st runP b rf = runGen proveWith b rf runS b rf = runGen satWith b rf runGen a b rf = do m <- a z3{verbose=True, redirectVerbose=Just rf} b appendFile rf ("\nRESULT:\n" P.++ show m P.++ "\n") runSat f = runSatExpecting f Sat runUnsat f = runSatExpecting f Unsat runAxSat f = runSatAxExpecting f Sat runAxUnsat f = runSatAxExpecting f Unsat runSatAxExpecting f what rf = do m <- runSMTWith z3{verbose=True, redirectVerbose=Just rf} run appendFile rf ("\nRESULT:\n" P.++ m P.++ "\n") `C.catch` (\(e :: C.SomeException) -> appendFile rf ("\nEXCEPTION CAUGHT:\n" P.++ show e P.++ "\n")) where run = do _ <- f query $ do cs <- checkSat if cs /= what then error $ "Unexpected output: " P.++ show cs else if cs == Sat then showModel z3 <$> getModel else pure $ "All good, expecting: " P.++ show cs runSatExpecting f what rf = do m <- runSMTWith z3{verbose=True, redirectVerbose=Just rf} run appendFile rf ("\nRESULT:\n" P.++ m P.++ "\n") `C.catch` (\(e :: C.SomeException) -> appendFile rf ("\nEXCEPTION CAUGHT:\n" P.++ show e P.++ "\n")) where run = do arg <- free_ constrain $ f arg query $ do arg2 <- freshVar_ constrain $ f arg2 cs <- checkSat if cs /= what then error $ "Unexpected output: " P.++ show cs else if cs == Sat then showModel z3 <$> getModel else pure $ "All good, expecting: " P.++ show cs runSat2 f rf = do m <- runSMTWith z3{verbose=True, redirectVerbose=Just rf} run appendFile rf ("\nRESULT:\n" P.++ showModel z3 m P.++ "\n") where run = do arg1 <- free_ arg2 <- free_ constrain $ f arg1 arg2 query $ do arg3 <- freshVar_ arg4 <- freshVar_ constrain $ f arg3 arg4 cs <- checkSat case cs of Sat -> getModel _ -> error $ "Unexpected output: " P.++ show cs eval1 :: (SymVal a, SymVal b, Show a, Show b, Eq b) => a -> (SBV a -> SBV b, a -> b) -> FilePath -> IO () eval1 cArg sf rf = eval1Gen cArg sf rf z3{verbose=True, redirectVerbose=Just rf} eval1Gen :: (SymVal a, SymVal b, Show a, Show b, Eq b) => a -> (SBV a -> SBV b, a -> b) -> FilePath -> SMTConfig -> IO () eval1Gen cArg (sFun, cFun) rf cfg = do m <- runSMTWith cfg run appendFile rf ("\nRESULT:\n" P.++ showModel z3 m P.++ "\n") where run = do arg <- free_ res <- free_ constrain $ arg .== literal cArg constrain $ res .== sFun arg let concResult = cFun cArg query $ do cs <- checkSat case cs of Sat -> do resV <- getValue res unless (resV == concResult) $ error $ unlines [ "Bad output:" , " arg = " P.++ show cArg , " concrete = " P.++ show concResult , " symbolic = " P.++ show resV ] getModel _ -> error $ "Unexpected output: " P.++ show cs eval2 :: (SymVal a, SymVal b, SymVal c, Eq c, Show a, Show b, Show c) => a -> b -> (SBV a -> SBV b -> SBV c, a -> b -> c) -> FilePath -> IO () eval2 cArg1 cArg2 (sFun, cFun) rf = do m <- runSMTWith z3{verbose=True, redirectVerbose=Just rf} run appendFile rf ("\nRESULT:\n" P.++ showModel z3 m P.++ "\n") where run = do arg1 <- free_ arg2 <- free_ res <- free_ constrain $ arg1 .== literal cArg1 constrain $ arg2 .== literal cArg2 constrain $ res .== sFun arg1 arg2 let concResult = cFun cArg1 cArg2 query $ do cs <- checkSat case cs of Sat -> do resV <- getValue res unless (resV == concResult) $ error $ unlines [ "Bad output:" , " arg1 = " P.++ show cArg1 , " arg2 = " P.++ show cArg2 , " concrete = " P.++ show concResult , " symbolic = " P.++ show resV ] 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) -- No free vars noFreeVars1 :: SMTConfig -> IO SatResult noFreeVars1 cfg = satWith cfg $ do zs :: SList [Integer] <- free_ xs :: SList Integer <- free_ ys :: SList Integer <- free_ constrain $ xs .== literal [1,2,3::Integer] constrain $ ys .== literal [3,4,5::Integer] pure $ zs .== map (\(x :: SInteger) -> map (\(y :: SInteger) -> x+y) ys) xs -- No free vars noFreeVars2 :: SMTConfig -> IO ThmResult noFreeVars2 cfg = proveWith cfg $ do let ae :: SList [Integer] -> SList Integer -> SList [Integer] ae xs ys = map (++ ys) xs xs <- free_ ys <- free_ pure $ map (ae xs) ys .== nil -- This one is ok, because we're using the global xs. (i.e., no free vars) filterHead :: Symbolic String filterHead = do xs :: SList Integer <- free_ constrain $ filter (.> (head xs :: SInteger)) xs ./= filter (.> (4 :: SInteger)) xs query $ do cs <- checkSat case cs of Sat -> showModel z3 <$> getModel _ -> pure $ "Unexpected result: " <> show cs {- HLint ignore module "Use map once" -} {- HLint ignore module "Use sum" -} {- HLint ignore module "Fuse foldr/map" -} {- HLint ignore module "Use zipWith" -} {- HLint ignore module "Use uncurry" -} {- HLint ignore module "Use even" -} {- HLint ignore module "Use odd" -} {- HLint ignore module "Use product" -} {- HLint ignore module "Avoid lambda" -} {- HLint ignore module "Eta reduce" -}