{-# 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 ( AsKey, DynamicSortedIdx (DynamicSortedIdx), ITEOp (symIte), LogicalOp (symNot, (.&&), (.||)), Mergeable (rootStrategy), MergingStrategy (NoStrategy, SimpleStrategy), Solvable (con, ssym), StrategyList (StrategyList), SymBool, Union, buildStrategyList, mrgIf, mrgSingle, resolveStrategy, ) import Grisette.Internal.Core.Data.Class.AsKey (AsKey1) 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 (AsKey SymBool) in testGroup "Mergeable for SymBool" [ testCase "true condition" $ do 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 (AsKey SymBool) (AsKey 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 (AsKey SymBool) (AsKey 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 AsKey SymBool / Just v" $ do let (idxsJ, SimpleStrategy fJ) = resolveStrategy rootStrategy (Just (ssym "a") :: Maybe (AsKey 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 ([] :: [AsKey SymBool]) [DynamicSortedIdx (0 :: Int)] [(ssym "a", [], [], [])], testCase "[v1, v2]" $ testMergeableSimpleEquivClass [ssym "a" :: AsKey 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" :: AsKey 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" :: AsKey SymBool, ssym "c"], ssym "d" :: AsKey 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" :: AsKey SymBool, ssym "c"], ssym "d" :: AsKey SymBool, [ssym "f" :: AsKey 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" :: AsKey SymBool, ssym "c"], ssym "d" :: AsKey SymBool, [ssym "f" :: AsKey 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" :: AsKey SymBool, ssym "c"], ssym "d" :: AsKey SymBool, [ssym "f" :: AsKey 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" :: AsKey SymBool, ssym "c"], ssym "d" :: AsKey SymBool, [ssym "f" :: AsKey SymBool], [2 :: Integer, 3], 2 :: Integer, Just (ssym "a" :: AsKey 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" :: AsKey SymBool, ssym "c"], ssym "d" :: AsKey SymBool, [ssym "f" :: AsKey SymBool], [2 :: Integer, 3], 2 :: Integer, Just (ssym "a" :: AsKey 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 (AsKey SymBool) -> AsKey SymBool = \case Just x -> x; Nothing -> (con True) f2 :: Maybe (AsKey SymBool) -> AsKey SymBool = \case Just x -> (symNot x); Nothing -> (con False) in testGroup "Function" [ testCase "Simply mergeable result" $ do case rootStrategy :: MergingStrategy (Maybe (AsKey SymBool) -> AsKey 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 (AsKey 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 (AsKey SymBool) Maybe (AsKey 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 (AsKey SymBool) Maybe (AsKey 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 (AsKey1 Union) (AsKey SymBool)) let st1 :: StateLazy.StateT Integer (AsKey1 Union) (AsKey SymBool) = StateLazy.StateT $ \(x :: Integer) -> mrgSingle (ssym "a", x + 2) let st2 :: StateLazy.StateT Integer (AsKey1 Union) (AsKey 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 (AsKey1 Union) (AsKey SymBool)) let st1 :: StateStrict.StateT Integer (AsKey1 Union) (AsKey SymBool) = StateStrict.StateT $ \(x :: Integer) -> mrgSingle (ssym "a", x + 2) let st2 :: StateStrict.StateT Integer (AsKey1 Union) (AsKey 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 (AsKey SymBool, Integer) (AsKey1 Union) (AsKey SymBool, Integer)) let c1 :: ContT (AsKey SymBool, Integer) (AsKey1 Union) (AsKey SymBool, Integer) = ContT $ \f -> f (ssym "a", 2) let c2 :: ContT (AsKey SymBool, Integer) (AsKey1 Union) (AsKey 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, AsKey SymBool) (Integer, AsKey SymBool) (Integer, AsKey SymBool) (AsKey1 Union) (Integer, AsKey SymBool) ) let rws1 :: RWSTLazy.RWST (Integer, AsKey SymBool) (Integer, AsKey SymBool) (Integer, AsKey SymBool) (AsKey1 Union) (Integer, AsKey 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, AsKey SymBool) (Integer, AsKey SymBool) (Integer, AsKey SymBool) (AsKey1 Union) (Integer, AsKey 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 :: AsKey1 Union ( (Integer, AsKey SymBool), (Integer, AsKey SymBool), (Integer, AsKey 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, AsKey SymBool) (Integer, AsKey SymBool) (Integer, AsKey SymBool) (AsKey1 Union) (Integer, AsKey SymBool) ) let rws1 :: RWSTStrict.RWST (Integer, AsKey SymBool) (Integer, AsKey SymBool) (Integer, AsKey SymBool) (AsKey1 Union) (Integer, AsKey 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, AsKey SymBool) (Integer, AsKey SymBool) (Integer, AsKey SymBool) (AsKey1 Union) (Integer, AsKey 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 :: AsKey1 Union ( (Integer, AsKey SymBool), (Integer, AsKey SymBool), (Integer, AsKey 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 (AsKey1 Union) (AsKey SymBool)) let w1 :: WriterLazy.WriterT Integer (AsKey1 Union) (AsKey SymBool) = WriterLazy.WriterT $ mrgSingle (ssym "a", 1) let w2 :: WriterLazy.WriterT Integer (AsKey1 Union) (AsKey SymBool) = WriterLazy.WriterT $ mrgSingle (ssym "b", 2) let w3 :: WriterLazy.WriterT Integer (AsKey1 Union) (AsKey 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 (AsKey1 Union) (AsKey SymBool)) let w1 :: WriterStrict.WriterT Integer (AsKey1 Union) (AsKey SymBool) = WriterStrict.WriterT $ mrgSingle (ssym "a", 1) let w2 :: WriterStrict.WriterT Integer (AsKey1 Union) (AsKey SymBool) = WriterStrict.WriterT $ mrgSingle (ssym "b", 2) let w3 :: WriterStrict.WriterT Integer (AsKey1 Union) (AsKey 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 (AsKey1 Union) Integer) let r1 :: ReaderT Integer (AsKey1 Union) Integer = ReaderT $ \(x :: Integer) -> mrgSingle $ x + 2 let r2 :: ReaderT Integer (AsKey1 Union) 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" :: AsKey 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 (AsKey SymBool)) [DynamicSortedIdx False] [ ( ssym "a", IdentityT Nothing, IdentityT Nothing, IdentityT Nothing ) ], testCase "IdentityT (Just v)" $ testMergeableSimpleEquivClass (IdentityT $ Just $ ssym "a" :: IdentityT Maybe (AsKey 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 (AsKey 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 (AsKey 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 (AsKey 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 (AsKey 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 LT] [(ssym "a", LT, LT, LT)], testCase "EQ" $ testMergeableSimpleEquivClass EQ [DynamicSortedIdx EQ] [(ssym "a", EQ, EQ, EQ)], testCase "GT" $ testMergeableSimpleEquivClass GT [DynamicSortedIdx GT] [(ssym "a", GT, GT, GT)] ] ] ]