{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Grisette.Core.Data.Class.MergeableTests (mergeableTests) where import Control.Monad.Cont (ContT (ContT, runContT)) import Control.Monad.Except (ExceptT (ExceptT)) import Control.Monad.Identity ( Identity (Identity), IdentityT (IdentityT), ) import qualified Control.Monad.RWS.Lazy as RWSTLazy import qualified Control.Monad.RWS.Strict as RWSTStrict import Control.Monad.Reader (ReaderT (ReaderT, runReaderT)) import qualified Control.Monad.State.Lazy as StateLazy import qualified Control.Monad.State.Strict as StateStrict import Control.Monad.Trans.Maybe (MaybeT (MaybeT)) import qualified Control.Monad.Writer.Lazy as WriterLazy import qualified Control.Monad.Writer.Strict as WriterStrict import qualified Data.ByteString.Char8 as C import Data.Functor.Sum (Sum (InL, InR)) import Data.Int (Int16, Int32, Int64, Int8) import Data.Word (Word16, Word32, Word64, Word8) import GHC.Stack (HasCallStack) import Grisette ( DynamicSortedIdx (DynamicSortedIdx), ITEOp (symIte), LogicalOp (symNot, (.&&), (.||)), Mergeable (rootStrategy), MergingStrategy (NoStrategy, SimpleStrategy), Solvable (con, ssym), StrategyList (StrategyList), SymBool, UnionM, buildStrategyList, mrgIf, mrgSingle, resolveStrategy, ) import Test.Framework (Test, testGroup) import Test.Framework.Providers.HUnit (testCase) import Test.Framework.Providers.QuickCheck2 (testProperty) import Test.HUnit (Assertion, assertFailure, (@?=)) import Test.QuickCheck (ioProperty) testMergeableSimpleEquivClass :: (HasCallStack, Mergeable x, Show x, Eq x) => x -> [DynamicSortedIdx] -> [(SymBool, x, x, x)] -> Assertion testMergeableSimpleEquivClass x idxs cases = do let (idxsT, s) = resolveStrategy rootStrategy x case s of SimpleStrategy m -> do idxsT @?= idxs go cases where go [] = return () go ((c, t, f, r) : xs) = do fst (resolveStrategy rootStrategy t) @?= idxs fst (resolveStrategy rootStrategy f) @?= idxs fst (resolveStrategy rootStrategy r) @?= idxs m c t f @?= r go xs _ -> assertFailure $ "Bad strategy type for " ++ show x mergeableTests :: Test mergeableTests = testGroup "Mergeable" [ testGroup "Mergeable for common types" [ let SimpleStrategy f = rootStrategy :: MergingStrategy SymBool in testGroup "Mergeable for SymBool" [ testCase "true condition" $ f (con True) (ssym "a") (ssym "b") @?= ssym "a", testCase "false condition" $ f (con False) (ssym "a") (ssym "b") @?= ssym "b", testCase "general condition" $ f (ssym "a") (ssym "b") (ssym "c") @?= symIte (ssym "a") (ssym "b") (ssym "c") ], testProperty "Bool" $ ioProperty . \(x :: Bool) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Integer" $ ioProperty . \(x :: Integer) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Char" $ ioProperty . \(x :: Char) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Int" $ ioProperty . \(x :: Int) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Int8" $ ioProperty . \(x :: Int8) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Int16" $ ioProperty . \(x :: Int16) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Int32" $ ioProperty . \(x :: Int32) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Int64" $ ioProperty . \(x :: Int64) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Word" $ ioProperty . \(x :: Word) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Word8" $ ioProperty . \(x :: Word8) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Word16" $ ioProperty . \(x :: Word16) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Word32" $ ioProperty . \(x :: Word32) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "Word64" $ ioProperty . \(x :: Word64) -> testMergeableSimpleEquivClass x [DynamicSortedIdx x] [(ssym "a", x, x, x)], testProperty "()" $ ioProperty . \(x :: ()) -> testMergeableSimpleEquivClass x [] [(ssym "a", x, x, x)], testProperty "ByteString" $ ioProperty . \(x :: String) -> let b = C.pack x in testMergeableSimpleEquivClass b [DynamicSortedIdx b] [(ssym "a", b, b, b)], testGroup "Either" [ testGroup "Either Integer Integer" [ testProperty "Left x" $ ioProperty . \(x :: Integer) -> do testMergeableSimpleEquivClass (Left x :: Either Integer Integer) [DynamicSortedIdx False, DynamicSortedIdx x] [(ssym "a", Left x, Left x, Left x)], testProperty "Right x" $ ioProperty . \(x :: Integer) -> do testMergeableSimpleEquivClass (Right x :: Either Integer Integer) [DynamicSortedIdx True, DynamicSortedIdx x] [(ssym "a", Right x, Right x, Right x)] ], testGroup "Either SymBool SymBool" [ testCase "Left v" $ do let (idxsL, SimpleStrategy fL) = resolveStrategy rootStrategy (Left (ssym "a") :: Either SymBool SymBool) idxsL @?= [DynamicSortedIdx False] fL (ssym "a") (Left $ ssym "b") (Left $ ssym "c") @?= Left (symIte (ssym "a") (ssym "b") (ssym "c")), testCase "Right v" $ do let (idxsR, SimpleStrategy fR) = resolveStrategy rootStrategy (Right (ssym "a") :: Either SymBool SymBool) idxsR @?= [DynamicSortedIdx True] fR (ssym "a") (Right $ ssym "b") (Right $ ssym "c") @?= Right (symIte (ssym "a") (ssym "b") (ssym "c")) ] ], testGroup "Maybe" [ testGroup "Maybe Integer" [ testProperty "Nothing" $ ioProperty . \(_ :: Integer) -> do testMergeableSimpleEquivClass (Nothing :: Maybe Integer) [DynamicSortedIdx False] [(ssym "a", Nothing, Nothing, Nothing)], testProperty "Just v" $ ioProperty . \(x :: Integer) -> do testMergeableSimpleEquivClass (Just x :: Maybe Integer) [DynamicSortedIdx True, DynamicSortedIdx x] [(ssym "a", Just x, Just x, Just x)] ], testCase "Maybe SymBool / Just v" $ do let (idxsJ, SimpleStrategy fJ) = resolveStrategy rootStrategy (Just (ssym "a") :: Maybe SymBool) idxsJ @?= [DynamicSortedIdx True] fJ (ssym "a") (Just $ ssym "b") (Just $ ssym "c") @?= Just (symIte (ssym "a") (ssym "b") (ssym "c")) ], testGroup "List" [ testCase "BuildStrategyList" $ do case buildStrategyList @Integer rootStrategy [1, 2, 3] of StrategyList idxs _ -> do idxs @?= [ [DynamicSortedIdx (1 :: Integer)], [DynamicSortedIdx (2 :: Integer)], [DynamicSortedIdx (3 :: Integer)] ], testProperty "List for ordered type" $ ioProperty . \(x :: [Integer]) -> do testMergeableSimpleEquivClass x [ DynamicSortedIdx (length x), DynamicSortedIdx $ buildStrategyList rootStrategy x ] [(ssym "a", x, x, x)], testProperty "Nested List for ordered type" $ ioProperty . \(x :: [[Integer]]) -> do testMergeableSimpleEquivClass x [ DynamicSortedIdx (length x), DynamicSortedIdx $ buildStrategyList rootStrategy x ] [(ssym "a", x, x, x)], testGroup "[SymBool]" [ testCase "[]" $ testMergeableSimpleEquivClass ([] :: [SymBool]) [DynamicSortedIdx (0 :: Int)] [(ssym "a", [], [], [])], testCase "[v1, v2]" $ testMergeableSimpleEquivClass [ssym "a" :: SymBool, ssym "b"] [DynamicSortedIdx (2 :: Int)] [ ( ssym "a", [ssym "b", ssym "c"], [ssym "d", ssym "e"], [ symIte (ssym "a") (ssym "b") (ssym "d"), symIte (ssym "a") (ssym "c") (ssym "e") ] ) ] ] ], testCase "(,)" $ testMergeableSimpleEquivClass ([1 :: Integer], [ssym "b" :: SymBool, ssym "c"]) [ DynamicSortedIdx (1 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [1 :: Integer], DynamicSortedIdx (2 :: Int) ] [ ( ssym "a", ([1], [ssym "c", ssym "d"]), ([1], [ssym "f", ssym "g"]), ( [1], [ symIte (ssym "a") (ssym "c") (ssym "f"), symIte (ssym "a") (ssym "d") (ssym "g") ] ) ) ], testCase "(,,)" $ testMergeableSimpleEquivClass ( [1 :: Integer], [ssym "b" :: SymBool, ssym "c"], ssym "d" :: SymBool ) [ DynamicSortedIdx (1 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [1 :: Integer], DynamicSortedIdx (2 :: Int) ] [ ( ssym "a", ([1], [ssym "c", ssym "d"], ssym "e"), ([1], [ssym "f", ssym "g"], ssym "h"), ( [1], [ symIte (ssym "a") (ssym "c") (ssym "f"), symIte (ssym "a") (ssym "d") (ssym "g") ], symIte (ssym "a") (ssym "e") (ssym "h") ) ) ], testCase "(,,,)" $ testMergeableSimpleEquivClass ( [1 :: Integer], [ssym "b" :: SymBool, ssym "c"], ssym "d" :: SymBool, [ssym "f" :: SymBool] ) [ DynamicSortedIdx (1 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [1 :: Integer], DynamicSortedIdx (2 :: Int), DynamicSortedIdx (1 :: Int) ] [ ( ssym "a", ([1], [ssym "c", ssym "d"], ssym "e", [ssym "i"]), ([1], [ssym "f", ssym "g"], ssym "h", [ssym "j"]), ( [1], [ symIte (ssym "a") (ssym "c") (ssym "f"), symIte (ssym "a") (ssym "d") (ssym "g") ], symIte (ssym "a") (ssym "e") (ssym "h"), [symIte (ssym "a") (ssym "i") (ssym "j")] ) ) ], testCase "(,,,,)" $ testMergeableSimpleEquivClass ( [1 :: Integer], [ssym "b" :: SymBool, ssym "c"], ssym "d" :: SymBool, [ssym "f" :: SymBool], [2 :: Integer, 3] ) [ DynamicSortedIdx (1 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [1 :: Integer], DynamicSortedIdx (2 :: Int), DynamicSortedIdx (1 :: Int), DynamicSortedIdx (2 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [2 :: Integer, 3] ] [ ( ssym "a", ([1], [ssym "c", ssym "d"], ssym "e", [ssym "i"], [2, 3]), ([1], [ssym "f", ssym "g"], ssym "h", [ssym "j"], [2, 3]), ( [1], [ symIte (ssym "a") (ssym "c") (ssym "f"), symIte (ssym "a") (ssym "d") (ssym "g") ], symIte (ssym "a") (ssym "e") (ssym "h"), [symIte (ssym "a") (ssym "i") (ssym "j")], [2, 3] ) ) ], testCase "(,,,,,)" $ testMergeableSimpleEquivClass ( [1 :: Integer], [ssym "b" :: SymBool, ssym "c"], ssym "d" :: SymBool, [ssym "f" :: SymBool], [2 :: Integer, 3], 2 :: Integer ) [ DynamicSortedIdx (1 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [1 :: Integer], DynamicSortedIdx (2 :: Int), DynamicSortedIdx (1 :: Int), DynamicSortedIdx (2 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [2 :: Integer, 3], DynamicSortedIdx (2 :: Integer) ] [ ( ssym "a", ([1], [ssym "c", ssym "d"], ssym "e", [ssym "i"], [2, 3], 2), ([1], [ssym "f", ssym "g"], ssym "h", [ssym "j"], [2, 3], 2), ( [1], [ symIte (ssym "a") (ssym "c") (ssym "f"), symIte (ssym "a") (ssym "d") (ssym "g") ], symIte (ssym "a") (ssym "e") (ssym "h"), [symIte (ssym "a") (ssym "i") (ssym "j")], [2, 3], 2 ) ) ], testCase "(,,,,,,)" $ testMergeableSimpleEquivClass ( [1 :: Integer], [ssym "b" :: SymBool, ssym "c"], ssym "d" :: SymBool, [ssym "f" :: SymBool], [2 :: Integer, 3], 2 :: Integer, Just (ssym "a" :: SymBool) ) [ DynamicSortedIdx (1 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [1 :: Integer], DynamicSortedIdx (2 :: Int), DynamicSortedIdx (1 :: Int), DynamicSortedIdx (2 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [2 :: Integer, 3], DynamicSortedIdx (2 :: Integer), DynamicSortedIdx True ] [ ( ssym "a", ( [1], [ssym "c", ssym "d"], ssym "e", [ssym "i"], [2, 3], 2, Just (ssym "k") ), ( [1], [ssym "f", ssym "g"], ssym "h", [ssym "j"], [2, 3], 2, Just (ssym "l") ), ( [1], [ symIte (ssym "a") (ssym "c") (ssym "f"), symIte (ssym "a") (ssym "d") (ssym "g") ], symIte (ssym "a") (ssym "e") (ssym "h"), [symIte (ssym "a") (ssym "i") (ssym "j")], [2, 3], 2, Just $ symIte (ssym "a") (ssym "k") (ssym "l") ) ) ], testCase "(,,,,,,,)" $ testMergeableSimpleEquivClass ( [1 :: Integer], [ssym "b" :: SymBool, ssym "c"], ssym "d" :: SymBool, [ssym "f" :: SymBool], [2 :: Integer, 3], 2 :: Integer, Just (ssym "a" :: SymBool), Left 1 :: Either Integer Integer ) [ DynamicSortedIdx (1 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [1 :: Integer], DynamicSortedIdx (2 :: Int), DynamicSortedIdx (1 :: Int), DynamicSortedIdx (2 :: Int), DynamicSortedIdx $ buildStrategyList rootStrategy [2 :: Integer, 3], DynamicSortedIdx (2 :: Integer), DynamicSortedIdx True, DynamicSortedIdx False, DynamicSortedIdx (1 :: Integer) ] [ ( ssym "a", ( [1], [ssym "c", ssym "d"], ssym "e", [ssym "i"], [2, 3], 2, Just (ssym "k"), Left 1 ), ( [1], [ssym "f", ssym "g"], ssym "h", [ssym "j"], [2, 3], 2, Just (ssym "l"), Left 1 ), ( [1], [ symIte (ssym "a") (ssym "c") (ssym "f"), symIte (ssym "a") (ssym "d") (ssym "g") ], symIte (ssym "a") (ssym "e") (ssym "h"), [symIte (ssym "a") (ssym "i") (ssym "j")], [2, 3], 2, Just $ symIte (ssym "a") (ssym "k") (ssym "l"), Left 1 ) ) ], let f1 :: Maybe SymBool -> SymBool = \case Just x -> x; Nothing -> (con True) f2 :: Maybe SymBool -> SymBool = \case Just x -> (symNot x); Nothing -> (con False) in testGroup "Function" [ testCase "Simply mergeable result" $ do case rootStrategy :: MergingStrategy (Maybe SymBool -> SymBool) of SimpleStrategy f -> do let r = f (ssym "a") f1 f2 r (Just (ssym "x")) @?= symIte (ssym "a") (ssym "x") (symNot (ssym "x")) r Nothing @?= symIte (ssym "a") (con True) (con False) _ -> assertFailure "Bad mergeable strategy type", testCase "Other mergeable result" $ do case rootStrategy :: MergingStrategy (Maybe SymBool -> Integer) of NoStrategy -> return () _ -> assertFailure "Bad mergeable strategy type" ], testGroup "MaybeT" [ testGroup "MaybeT Maybe Integer" [ testCase "MaybeT Nothing" $ testMergeableSimpleEquivClass (MaybeT Nothing :: MaybeT Maybe Integer) [DynamicSortedIdx False] [ ( ssym "a", MaybeT Nothing, MaybeT Nothing, MaybeT Nothing ) ], testCase "MaybeT (Just Nothing)" $ testMergeableSimpleEquivClass (MaybeT $ Just Nothing :: MaybeT Maybe Integer) [DynamicSortedIdx True, DynamicSortedIdx False] [ ( ssym "a", MaybeT $ Just Nothing, MaybeT $ Just Nothing, MaybeT $ Just Nothing ) ], testProperty "MaybeT (Just (Just v))" $ ioProperty . \(x :: Integer) -> do testMergeableSimpleEquivClass (MaybeT $ Just $ Just x :: MaybeT Maybe Integer) [ DynamicSortedIdx True, DynamicSortedIdx True, DynamicSortedIdx x ] [ ( ssym "a", MaybeT $ Just $ Just x, MaybeT $ Just $ Just x, MaybeT $ Just $ Just x ) ] ], testCase "MaybeT Maybe SymBool / MaybeT (Just (Just v))" $ do let (idxsJ, SimpleStrategy fJ) = resolveStrategy rootStrategy ( MaybeT (Just (Just (ssym "a"))) :: MaybeT Maybe SymBool ) idxsJ @?= [DynamicSortedIdx True, DynamicSortedIdx True] fJ (ssym "a") (MaybeT $ Just $ Just $ ssym "b") (MaybeT $ Just $ Just $ ssym "c") @?= MaybeT (Just (Just (symIte (ssym "a") (ssym "b") (ssym "c")))) ], testGroup "ExceptT" [ testGroup "ExceptT Integer Maybe Integer" [ testCase "ExceptT Nothing" $ testMergeableSimpleEquivClass (ExceptT Nothing :: ExceptT Integer Maybe Integer) [DynamicSortedIdx False] [ ( ssym "a", ExceptT Nothing, ExceptT Nothing, ExceptT Nothing ) ], testProperty "ExceptT (Just (Left v))" $ ioProperty . \(x :: Integer) -> do testMergeableSimpleEquivClass ( ExceptT $ Just $ Left x :: ExceptT Integer Maybe Integer ) [ DynamicSortedIdx True, DynamicSortedIdx False, DynamicSortedIdx x ] [ ( ssym "a", ExceptT $ Just $ Left x, ExceptT $ Just $ Left x, ExceptT $ Just $ Left x ) ], testProperty "ExceptT (Just (Right v))" $ ioProperty . \(x :: Integer) -> do testMergeableSimpleEquivClass ( ExceptT $ Just $ Right x :: ExceptT Integer Maybe Integer ) [ DynamicSortedIdx True, DynamicSortedIdx True, DynamicSortedIdx x ] [ ( ssym "a", ExceptT $ Just $ Right x, ExceptT $ Just $ Right x, ExceptT $ Just $ Right x ) ] ], testGroup "ExceptT SymBool Maybe SymBool" [ testCase "ExceptT (Just (Left v))" $ do let (idxsJL, SimpleStrategy fJL) = resolveStrategy rootStrategy ( ExceptT (Just (Left (ssym "a"))) :: ExceptT SymBool Maybe SymBool ) idxsJL @?= [DynamicSortedIdx True, DynamicSortedIdx False] fJL (ssym "a") (ExceptT $ Just $ Left $ ssym "b") (ExceptT $ Just $ Left $ ssym "c") @?= ExceptT (Just (Left (symIte (ssym "a") (ssym "b") (ssym "c")))), testCase "ExceptT (Just (Right v))" $ do let (idxsJR, SimpleStrategy fJR) = resolveStrategy rootStrategy ( ExceptT (Just (Right (ssym "a"))) :: ExceptT SymBool Maybe SymBool ) idxsJR @?= [DynamicSortedIdx True, DynamicSortedIdx True] fJR (ssym "a") (ExceptT $ Just $ Right $ ssym "b") (ExceptT $ Just $ Right $ ssym "c") @?= ExceptT (Just (Right (symIte (ssym "a") (ssym "b") (ssym "c")))) ] ], testGroup "StateT" [ testCase "Lazy StateT" $ do let SimpleStrategy s = rootStrategy :: MergingStrategy (StateLazy.StateT Integer UnionM SymBool) let st1 :: StateLazy.StateT Integer UnionM SymBool = StateLazy.StateT $ \(x :: Integer) -> mrgSingle (ssym "a", x + 2) let st2 :: StateLazy.StateT Integer UnionM SymBool = StateLazy.StateT $ \(x :: Integer) -> mrgSingle (ssym "b", x * 2) let st3 = s (ssym "c") st1 st2 StateLazy.runStateT st3 2 @?= mrgSingle (symIte (ssym "c") (ssym "a") (ssym "b"), 4) StateLazy.runStateT st3 3 @?= mrgIf (ssym "c") (mrgSingle (ssym "a", 5)) (mrgSingle (ssym "b", 6)), testCase "Strict StateT" $ do let SimpleStrategy s = rootStrategy :: MergingStrategy (StateStrict.StateT Integer UnionM SymBool) let st1 :: StateStrict.StateT Integer UnionM SymBool = StateStrict.StateT $ \(x :: Integer) -> mrgSingle (ssym "a", x + 2) let st2 :: StateStrict.StateT Integer UnionM SymBool = StateStrict.StateT $ \(x :: Integer) -> mrgSingle (ssym "b", x * 2) let st3 = s (ssym "c") st1 st2 StateStrict.runStateT st3 2 @?= mrgSingle (symIte (ssym "c") (ssym "a") (ssym "b"), 4) StateStrict.runStateT st3 3 @?= mrgIf (ssym "c") (mrgSingle (ssym "a", 5)) (mrgSingle (ssym "b", 6)) ], testCase "ContT" $ do let SimpleStrategy s = rootStrategy :: MergingStrategy (ContT (SymBool, Integer) UnionM (SymBool, Integer)) let c1 :: ContT (SymBool, Integer) UnionM (SymBool, Integer) = ContT $ \f -> f (ssym "a", 2) let c2 :: ContT (SymBool, Integer) UnionM (SymBool, Integer) = ContT $ \f -> f (ssym "b", 3) let c3 = s (ssym "c") c1 c2 runContT c3 ( \(a, x) -> mrgIf (ssym "p") (mrgSingle (a, x)) (mrgSingle (symNot a, x + 1)) ) @?= mrgIf (ssym "c") ( mrgIf (ssym "p") (mrgSingle (ssym "a", 2)) (mrgSingle (symNot $ ssym "a", 3)) ) ( mrgIf (ssym "p") (mrgSingle (ssym "b", 3)) (mrgSingle (symNot $ ssym "b", 4)) ), testGroup "RWST" [ testCase "Lazy RWST" $ do let SimpleStrategy s = rootStrategy :: MergingStrategy ( RWSTLazy.RWST (Integer, SymBool) (Integer, SymBool) (Integer, SymBool) UnionM (Integer, SymBool) ) let rws1 :: RWSTLazy.RWST (Integer, SymBool) (Integer, SymBool) (Integer, SymBool) UnionM (Integer, SymBool) = RWSTLazy.RWST $ \(ir, br) (is, bs) -> mrgSingle ( (ir + is, br .&& bs), (ir - is, br .|| bs), (ir * is, bs .&& br) ) let rws2 :: RWSTLazy.RWST (Integer, SymBool) (Integer, SymBool) (Integer, SymBool) UnionM (Integer, SymBool) = RWSTLazy.RWST $ \(ir, br) (is, bs) -> mrgSingle ( (ir + is, br .|| bs), (ir - is, br .&& bs), (ir * is, bs .|| br) ) let rws3 = s (ssym "c") rws1 rws2 let res1 :: UnionM ( (Integer, SymBool), (Integer, SymBool), (Integer, SymBool) ) = mrgIf (ssym "c") ( mrgSingle ( (1, ssym "a" .&& ssym "b"), (-1, ssym "a" .|| ssym "b"), (0, ssym "b" .&& ssym "a") ) ) ( mrgSingle ( (1, ssym "a" .|| ssym "b"), (-1, ssym "a" .&& ssym "b"), (0, ssym "b" .|| ssym "a") ) ) RWSTLazy.runRWST rws3 (0, ssym "a") (1, ssym "b") @?= res1, testCase "Strict RWST" $ do let SimpleStrategy s = rootStrategy :: MergingStrategy ( RWSTStrict.RWST (Integer, SymBool) (Integer, SymBool) (Integer, SymBool) UnionM (Integer, SymBool) ) let rws1 :: RWSTStrict.RWST (Integer, SymBool) (Integer, SymBool) (Integer, SymBool) UnionM (Integer, SymBool) = RWSTStrict.RWST $ \(ir, br) (is, bs) -> mrgSingle ( (ir + is, br .&& bs), (ir - is, br .|| bs), (ir * is, bs .&& br) ) let rws2 :: RWSTStrict.RWST (Integer, SymBool) (Integer, SymBool) (Integer, SymBool) UnionM (Integer, SymBool) = RWSTStrict.RWST $ \(ir, br) (is, bs) -> mrgSingle ( (ir + is, br .|| bs), (ir - is, br .&& bs), (ir * is, bs .|| br) ) let rws3 = s (ssym "c") rws1 rws2 let res1 :: UnionM ( (Integer, SymBool), (Integer, SymBool), (Integer, SymBool) ) = mrgIf (ssym "c") ( mrgSingle ( (1, "a" .&& "b"), (-1, "a" .|| "b"), (0, "b" .&& "a") ) ) ( mrgSingle ( (1, "a" .|| "b"), (-1, "a" .&& "b"), (0, "b" .|| "a") ) ) RWSTStrict.runRWST rws3 (0, ssym "a") (1, ssym "b") @?= res1 ], testGroup "WriterT" [ testCase "Lazy WriterT" $ do let SimpleStrategy s = rootStrategy :: MergingStrategy (WriterLazy.WriterT Integer UnionM SymBool) let w1 :: WriterLazy.WriterT Integer UnionM SymBool = WriterLazy.WriterT $ mrgSingle (ssym "a", 1) let w2 :: WriterLazy.WriterT Integer UnionM SymBool = WriterLazy.WriterT $ mrgSingle (ssym "b", 2) let w3 :: WriterLazy.WriterT Integer UnionM SymBool = WriterLazy.WriterT $ mrgSingle (ssym "c", 1) let w4 = s (ssym "d") w1 w2 let w5 = s (ssym "d") w1 w3 WriterLazy.runWriterT w4 @?= mrgIf (ssym "d") (mrgSingle (ssym "a", 1)) (mrgSingle (ssym "b", 2)) WriterLazy.runWriterT w5 @?= mrgSingle (symIte (ssym "d") (ssym "a") (ssym "c"), 1), testCase "Strict WriterT" $ do let SimpleStrategy s = rootStrategy :: MergingStrategy (WriterStrict.WriterT Integer UnionM SymBool) let w1 :: WriterStrict.WriterT Integer UnionM SymBool = WriterStrict.WriterT $ mrgSingle (ssym "a", 1) let w2 :: WriterStrict.WriterT Integer UnionM SymBool = WriterStrict.WriterT $ mrgSingle (ssym "b", 2) let w3 :: WriterStrict.WriterT Integer UnionM SymBool = WriterStrict.WriterT $ mrgSingle (ssym "c", 1) let w4 = s (ssym "d") w1 w2 let w5 = s (ssym "d") w1 w3 WriterStrict.runWriterT w4 @?= mrgIf (ssym "d") (mrgSingle (ssym "a", 1)) (mrgSingle (ssym "b", 2)) WriterStrict.runWriterT w5 @?= mrgSingle (symIte (ssym "d") (ssym "a") (ssym "c"), 1) ], testCase "ReaderT" $ do let SimpleStrategy s = rootStrategy :: MergingStrategy (ReaderT Integer UnionM Integer) let r1 :: ReaderT Integer UnionM Integer = ReaderT $ \(x :: Integer) -> mrgSingle $ x + 2 let r2 :: ReaderT Integer UnionM Integer = ReaderT $ \(x :: Integer) -> mrgSingle $ x * 2 let r3 = s (ssym "c") r1 r2 runReaderT r3 2 @?= mrgSingle 4 runReaderT r3 3 @?= mrgIf (ssym "c") (mrgSingle 5) (mrgSingle 6), testGroup "Identity" [ testProperty "Identity Integer" $ ioProperty . \x -> do testMergeableSimpleEquivClass (Identity x :: Identity Integer) [DynamicSortedIdx x] [(ssym "a", Identity x, Identity x, Identity x)], testCase "Identity SymBool" $ do testMergeableSimpleEquivClass (Identity (ssym "a" :: SymBool)) [] [ ( ssym "a", Identity $ ssym "b", Identity $ ssym "c", Identity $ symIte (ssym "a") (ssym "b") (ssym "c") ) ] ], testGroup "IdentityT Maybe Integer" [ testGroup "IdentityT Maybe Integer" [ testCase "IdentityT Nothing" $ testMergeableSimpleEquivClass (IdentityT Nothing :: IdentityT Maybe Integer) [DynamicSortedIdx False] [ ( ssym "a", IdentityT Nothing, IdentityT Nothing, IdentityT Nothing ) ], testProperty "IdentityT (Just v)" $ ioProperty . \x -> do testMergeableSimpleEquivClass (IdentityT $ Just x :: IdentityT Maybe Integer) [DynamicSortedIdx True, DynamicSortedIdx x] [ ( ssym "a", IdentityT $ Just x, IdentityT $ Just x, IdentityT $ Just x ) ] ], testGroup "IdentityT Maybe SymBool" [ testCase "IdentityT Nothing" $ testMergeableSimpleEquivClass (IdentityT Nothing :: IdentityT Maybe SymBool) [DynamicSortedIdx False] [ ( ssym "a", IdentityT Nothing, IdentityT Nothing, IdentityT Nothing ) ], testCase "IdentityT (Just v)" $ testMergeableSimpleEquivClass (IdentityT $ Just $ ssym "a" :: IdentityT Maybe SymBool) [DynamicSortedIdx True] [ ( ssym "a", IdentityT $ Just $ ssym "b", IdentityT $ Just $ ssym "c", IdentityT $ Just $ symIte (ssym "a") (ssym "b") (ssym "c") ) ] ] ], testGroup "Sum" [ testGroup "Sum Maybe Maybe Integer" [ testCase "InL Nothing" $ testMergeableSimpleEquivClass (InL Nothing :: Sum Maybe Maybe Integer) [DynamicSortedIdx False, DynamicSortedIdx False] [(ssym "a", InL Nothing, InL Nothing, InL Nothing)], testProperty "InL (Just v)" $ ioProperty . \x -> do testMergeableSimpleEquivClass (InL $ Just x :: Sum Maybe Maybe Integer) [ DynamicSortedIdx False, DynamicSortedIdx True, DynamicSortedIdx x ] [(ssym "a", InL $ Just x, InL $ Just x, InL $ Just x)], testCase "InR Nothing" $ testMergeableSimpleEquivClass (InR Nothing :: Sum Maybe Maybe Integer) [DynamicSortedIdx True, DynamicSortedIdx False] [(ssym "a", InR Nothing, InR Nothing, InR Nothing)], testProperty "InR (Just v)" $ ioProperty . \x -> do testMergeableSimpleEquivClass (InR $ Just x :: Sum Maybe Maybe Integer) [ DynamicSortedIdx True, DynamicSortedIdx True, DynamicSortedIdx x ] [(ssym "a", InR $ Just x, InR $ Just x, InR $ Just x)] ], testGroup "Sum Maybe Maybe SymBool" [ testCase "InL Nothing" $ testMergeableSimpleEquivClass (InL Nothing :: Sum Maybe Maybe SymBool) [DynamicSortedIdx False, DynamicSortedIdx False] [(ssym "a", InL Nothing, InL Nothing, InL Nothing)], testCase "InL (Just v)" $ testMergeableSimpleEquivClass (InL $ Just $ ssym "a" :: Sum Maybe Maybe SymBool) [DynamicSortedIdx False, DynamicSortedIdx True] [ ( ssym "a", InL $ Just $ ssym "b", InL $ Just $ ssym "c", InL $ Just $ symIte (ssym "a") (ssym "b") (ssym "c") ) ], testCase "InR Nothing" $ testMergeableSimpleEquivClass (InR Nothing :: Sum Maybe Maybe SymBool) [DynamicSortedIdx True, DynamicSortedIdx False] [(ssym "a", InR Nothing, InR Nothing, InR Nothing)], testCase "InR (Just v)" $ testMergeableSimpleEquivClass (InR $ Just $ ssym "a" :: Sum Maybe Maybe SymBool) [DynamicSortedIdx True, DynamicSortedIdx True] [ ( ssym "a", InR $ Just $ ssym "b", InR $ Just $ ssym "c", InR $ Just $ symIte (ssym "a") (ssym "b") (ssym "c") ) ] ] ], testGroup "Ordering" [ testCase "LT" $ testMergeableSimpleEquivClass LT [DynamicSortedIdx False] [(ssym "a", LT, LT, LT)], testCase "EQ" $ testMergeableSimpleEquivClass EQ [DynamicSortedIdx True, DynamicSortedIdx False] [(ssym "a", EQ, EQ, EQ)], testCase "GT" $ testMergeableSimpleEquivClass GT [DynamicSortedIdx True, DynamicSortedIdx True] [(ssym "a", GT, GT, GT)] ] ] ]