grisette-0.7.0.0: test/Grisette/Core/Data/Class/SymOrdTests.hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Grisette.Core.Data.Class.SymOrdTests (sordTests) where
import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
( Identity (Identity),
IdentityT (IdentityT),
)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import Data.Bifunctor (Bifunctor (bimap))
import qualified Data.ByteString as B
import Data.Foldable (traverse_)
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
( ITEOp (symIte),
LogicalOp (symNot, (.&&), (.||)),
SymEq ((.==)),
SymOrd (symCompare, (.<), (.<=), (.>), (.>=)),
Union,
mrgIf,
mrgMax,
mrgMin,
mrgSingle,
symMax,
symMin,
)
import Grisette.Core.Data.Class.TestValues
( conBool,
ssymBool,
)
import Grisette.Lib.Control.Monad (mrgReturn)
import Grisette.SymPrim (SymBool, SymInteger)
import Grisette.TestUtil.SymbolicAssertion ((.@?=))
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit (Assertion, (@?=))
import Test.QuickCheck (ioProperty)
concreteOrdOkProp :: (HasCallStack, SymOrd a, Ord a) => (a, a) -> Assertion
concreteOrdOkProp (i, j) = do
i .<= j @?= conBool (i <= j)
i .< j @?= conBool (i < j)
i .>= j @?= conBool (i >= j)
i .> j @?= conBool (i > j)
symCompare i j @?= (mrgReturn $ compare i j :: Union Ordering)
symbolicProdOrdOkProp ::
(HasCallStack, Show v, Show vl, Show vr, SymOrd v, SymOrd vl, SymOrd vr) =>
v ->
v ->
vl ->
vr ->
vl ->
vr ->
Assertion
symbolicProdOrdOkProp l r ll lr rl rr = do
l .<= r .@?= ((ll .< rl) .|| ((ll .== rl) .&& (lr .<= rr)))
l .< r .@?= ((ll .< rl) .|| ((ll .== rl) .&& (lr .< rr)))
l .>= r .@?= ((ll .> rl) .|| ((ll .== rl) .&& (lr .>= rr)))
l .> r .@?= ((ll .> rl) .|| ((ll .== rl) .&& (lr .> rr)))
l
`symCompare` r
@?= ( ( do
lc <- symCompare ll rl
case lc of
EQ -> symCompare lr rr
_ -> mrgReturn lc
) ::
Union Ordering
)
sordTests :: Test
sordTests =
testGroup
"SymOrd"
[ testGroup
"SymOrd for common types"
[ testGroup
"SymBool"
[ testCase "Concrete SymBool" $ do
conBool False .<= conBool False @?= conBool True
conBool False .< conBool False @?= conBool False
conBool False .>= conBool False @?= conBool True
conBool False .> conBool False @?= conBool False
conBool False .<= conBool True @?= conBool True
conBool False .< conBool True @?= conBool True
conBool False .>= conBool True @?= conBool False
conBool False .> conBool True @?= conBool False
conBool True .<= conBool False @?= conBool False
conBool True .< conBool False @?= conBool False
conBool True .>= conBool False @?= conBool True
conBool True .> conBool False @?= conBool True
conBool True .<= conBool True @?= conBool True
conBool True .< conBool True @?= conBool False
conBool True .>= conBool True @?= conBool True
conBool True .> conBool True @?= conBool False,
testCase "Symbolic SymBool" $ do
ssymBool "a"
.<= ssymBool "b"
@?= (symNot (ssymBool "a"))
.|| (ssymBool "b")
ssymBool "a"
.< ssymBool "b"
@?= (symNot (ssymBool "a"))
.&& (ssymBool "b")
ssymBool "a"
.>= ssymBool "b"
@?= (ssymBool "a")
.|| (symNot (ssymBool "b"))
ssymBool "a"
.> ssymBool "b"
@?= (ssymBool "a")
.&& (symNot (ssymBool "b"))
symCompare (ssymBool "a") (ssymBool "b")
@?= ( mrgIf
((symNot (ssymBool "a")) .&& (ssymBool "b"))
(mrgSingle LT)
( mrgIf
((ssymBool "a") .== (ssymBool "b"))
(mrgSingle EQ)
(mrgSingle GT)
) ::
Union Ordering
)
],
testProperty "Bool" (ioProperty . concreteOrdOkProp @Bool),
testProperty "Integer" (ioProperty . concreteOrdOkProp @Integer),
testProperty "Char" (ioProperty . concreteOrdOkProp @Char),
testProperty "Int" (ioProperty . concreteOrdOkProp @Int),
testProperty "Int8" (ioProperty . concreteOrdOkProp @Int8),
testProperty "Int16" (ioProperty . concreteOrdOkProp @Int16),
testProperty "Int32" (ioProperty . concreteOrdOkProp @Int32),
testProperty "Int64" (ioProperty . concreteOrdOkProp @Int64),
testProperty "Word" (ioProperty . concreteOrdOkProp @Word),
testProperty "Word8" (ioProperty . concreteOrdOkProp @Word8),
testProperty "Word16" (ioProperty . concreteOrdOkProp @Word16),
testProperty "Word32" (ioProperty . concreteOrdOkProp @Word32),
testProperty "Word64" (ioProperty . concreteOrdOkProp @Word64),
testGroup
"List"
[ testProperty "[Integer]" $
ioProperty . concreteOrdOkProp @[Integer],
testProperty "[String]" $
ioProperty . concreteOrdOkProp @[String],
testCase "[SymBool]" $ do
([] :: [SymBool]) .<= [] @?= conBool True
([] :: [SymBool]) .< [] @?= conBool False
([] :: [SymBool]) .>= [] @?= conBool True
([] :: [SymBool]) .> [] @?= conBool False
([] :: [SymBool])
`symCompare` []
@?= (mrgSingle EQ :: Union Ordering)
[] .<= [ssymBool "a"] @?= conBool True
[] .< [ssymBool "a"] @?= conBool True
[] .>= [ssymBool "a"] @?= conBool False
[] .> [ssymBool "a"] @?= conBool False
[]
`symCompare` [ssymBool "a"]
@?= (mrgSingle LT :: Union Ordering)
[ssymBool "a"] .<= [] @?= conBool False
[ssymBool "a"] .< [] @?= conBool False
[ssymBool "a"] .>= [] @?= conBool True
[ssymBool "a"] .> [] @?= conBool True
[ssymBool "a"]
`symCompare` []
@?= (mrgSingle GT :: Union Ordering)
[ssymBool "a", ssymBool "b"]
.<= [ssymBool "c"]
@?= (ssymBool "a" .< ssymBool "c" :: SymBool)
[ssymBool "a", ssymBool "b"]
.< [ssymBool "c"]
@?= (ssymBool "a" .< ssymBool "c" :: SymBool)
[ssymBool "a", ssymBool "b"]
.>= [ssymBool "c"]
@?= ( (ssymBool "a" .> ssymBool "c")
.|| (ssymBool "a" .== ssymBool "c") ::
SymBool
)
[ssymBool "a", ssymBool "b"]
.> [ssymBool "c"]
@?= ( (ssymBool "a" .> ssymBool "c")
.|| (ssymBool "a" .== ssymBool "c") ::
SymBool
)
[ssymBool "a"]
`symCompare` [ssymBool "b"]
@?= (ssymBool "a" `symCompare` ssymBool "b" :: Union Ordering)
[ssymBool "a"]
.<= [ssymBool "b", ssymBool "c"]
@?= ( (ssymBool "a" .< ssymBool "b")
.|| (ssymBool "a" .== ssymBool "b") ::
SymBool
)
[ssymBool "a"]
.< [ssymBool "b", ssymBool "c"]
@?= ( (ssymBool "a" .< ssymBool "b")
.|| (ssymBool "a" .== ssymBool "b") ::
SymBool
)
[ssymBool "a"]
.>= [ssymBool "b", ssymBool "c"]
@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
[ssymBool "a"]
.> [ssymBool "b", ssymBool "c"]
@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
[ssymBool "a"]
`symCompare` [ssymBool "b", ssymBool "c"]
@?= ( mrgIf
(ssymBool "a" .< ssymBool "b")
(mrgSingle LT)
( mrgIf
(ssymBool "a" .== ssymBool "b")
(mrgSingle LT)
(mrgSingle GT)
) ::
Union Ordering
)
[ssymBool "a", ssymBool "b"]
.<= [ssymBool "c", ssymBool "d"]
@?= ( (ssymBool "a" .< ssymBool "c")
.|| ( ssymBool "a"
.== ssymBool "c"
.&& ( (ssymBool "b" .< ssymBool "d")
.|| (ssymBool "b" .== ssymBool "d")
)
) ::
SymBool
)
[ssymBool "a", ssymBool "b"]
.< [ssymBool "c", ssymBool "d"]
@?= ( (ssymBool "a" .< ssymBool "c")
.|| ( ssymBool "a"
.== ssymBool "c"
.&& (ssymBool "b" .< ssymBool "d")
) ::
SymBool
)
[ssymBool "a", ssymBool "b"]
.>= [ssymBool "c", ssymBool "d"]
@?= ( (ssymBool "a" .> ssymBool "c")
.|| ( ssymBool "a"
.== ssymBool "c"
.&& ( (ssymBool "b" .> ssymBool "d")
.|| (ssymBool "b" .== ssymBool "d")
)
) ::
SymBool
)
[ssymBool "a", ssymBool "b"]
.> [ssymBool "c", ssymBool "d"]
@?= ( (ssymBool "a" .> ssymBool "c")
.|| ( ssymBool "a"
.== ssymBool "c"
.&& (ssymBool "b" .> ssymBool "d")
) ::
SymBool
)
[ssymBool "a", ssymBool "b"]
`symCompare` [ssymBool "c", ssymBool "d"]
@?= ( mrgIf
(ssymBool "a" .< ssymBool "c")
(mrgSingle LT)
( mrgIf
(ssymBool "a" .== ssymBool "c")
(ssymBool "b" `symCompare` ssymBool "d")
(mrgSingle GT)
) ::
Union Ordering
)
],
testGroup
"Maybe"
[ testProperty "Maybe Integer" $
ioProperty . concreteOrdOkProp @(Maybe Integer),
testCase "Maybe SymBool" $ do
(Nothing :: Maybe SymBool) .<= Nothing .@?= conBool True
(Nothing :: Maybe SymBool) .< Nothing .@?= conBool False
(Nothing :: Maybe SymBool) .>= Nothing .@?= conBool True
(Nothing :: Maybe SymBool) .> Nothing .@?= conBool False
(Nothing :: Maybe SymBool)
`symCompare` Nothing
@?= (mrgSingle EQ :: Union Ordering)
Nothing .<= Just (ssymBool "a") .@?= conBool True
Nothing .< Just (ssymBool "a") .@?= conBool True
Nothing .>= Just (ssymBool "a") .@?= conBool False
Nothing .> Just (ssymBool "a") .@?= conBool False
Nothing
`symCompare` Just (ssymBool "a")
@?= (mrgSingle LT :: Union Ordering)
Just (ssymBool "a") .<= Nothing .@?= conBool False
Just (ssymBool "a") .< Nothing .@?= conBool False
Just (ssymBool "a") .>= Nothing .@?= conBool True
Just (ssymBool "a") .> Nothing .@?= conBool True
Just (ssymBool "a")
`symCompare` Nothing
@?= (mrgSingle GT :: Union Ordering)
Just (ssymBool "a")
.<= Just (ssymBool "b")
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
Just (ssymBool "a")
.< Just (ssymBool "b")
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
Just (ssymBool "a")
.>= Just (ssymBool "b")
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
Just (ssymBool "a")
.> Just (ssymBool "b")
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
Just (ssymBool "a")
`symCompare` Just (ssymBool "b")
@?= ( ssymBool "a" `symCompare` ssymBool "b" ::
Union Ordering
)
],
testGroup
"MaybeT"
[ testProperty "MaybeT Maybe Integer" $
ioProperty
. concreteOrdOkProp @(MaybeT Maybe Integer)
. bimap MaybeT MaybeT,
testCase "MaybeT Maybe SymBool" $ do
(MaybeT Nothing :: MaybeT Maybe SymBool)
.<= MaybeT Nothing
.@?= conBool True
(MaybeT Nothing :: MaybeT Maybe SymBool)
.<= MaybeT (Just (Just (ssymBool "a")))
.@?= conBool True
MaybeT (Just (Just (ssymBool "a")))
.<= (MaybeT Nothing :: MaybeT Maybe SymBool)
.@?= conBool False
MaybeT (Just (Just (ssymBool "a")))
.<= ( MaybeT (Just (Just (ssymBool "b"))) ::
MaybeT Maybe SymBool
)
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
(MaybeT Nothing :: MaybeT Maybe SymBool)
.< MaybeT Nothing
.@?= conBool False
(MaybeT Nothing :: MaybeT Maybe SymBool)
.< MaybeT (Just (Just (ssymBool "a")))
.@?= conBool True
MaybeT (Just (Just (ssymBool "a")))
.< (MaybeT Nothing :: MaybeT Maybe SymBool)
.@?= conBool False
MaybeT (Just (Just (ssymBool "a")))
.< ( MaybeT (Just (Just (ssymBool "b"))) ::
MaybeT Maybe SymBool
)
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
(MaybeT Nothing :: MaybeT Maybe SymBool)
.>= MaybeT Nothing
.@?= conBool True
(MaybeT Nothing :: MaybeT Maybe SymBool)
.>= MaybeT (Just (Just (ssymBool "a")))
.@?= conBool False
MaybeT (Just (Just (ssymBool "a")))
.>= (MaybeT Nothing :: MaybeT Maybe SymBool)
.@?= conBool True
MaybeT (Just (Just (ssymBool "a")))
.>= ( MaybeT (Just (Just (ssymBool "b"))) ::
MaybeT Maybe SymBool
)
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
(MaybeT Nothing :: MaybeT Maybe SymBool)
.> MaybeT Nothing
.@?= conBool False
(MaybeT Nothing :: MaybeT Maybe SymBool)
.> MaybeT (Just (Just (ssymBool "a")))
.@?= conBool False
MaybeT (Just (Just (ssymBool "a")))
.> (MaybeT Nothing :: MaybeT Maybe SymBool)
.@?= conBool True
MaybeT (Just (Just (ssymBool "a")))
.> ( MaybeT (Just (Just (ssymBool "b"))) ::
MaybeT Maybe SymBool
)
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
(MaybeT Nothing :: MaybeT Maybe SymBool)
`symCompare` MaybeT Nothing
@?= (mrgSingle EQ :: Union Ordering)
(MaybeT Nothing :: MaybeT Maybe SymBool)
`symCompare` MaybeT (Just (Just (ssymBool "a")))
@?= (mrgSingle LT :: Union Ordering)
MaybeT (Just (Just (ssymBool "a")))
`symCompare` (MaybeT Nothing :: MaybeT Maybe SymBool)
@?= (mrgSingle GT :: Union Ordering)
MaybeT (Just (Just (ssymBool "a")))
`symCompare` ( MaybeT (Just (Just (ssymBool "b"))) ::
MaybeT Maybe SymBool
)
@?= ( ssymBool "a" `symCompare` ssymBool "b" ::
Union Ordering
)
],
testGroup
"Either"
[ testProperty "Either Integer Integer" $
ioProperty . concreteOrdOkProp @(Either Integer Integer),
testCase "Either SymBool SymBool" $ do
(Left (ssymBool "a") :: Either SymBool SymBool)
.<= Left (ssymBool "b")
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
(Left (ssymBool "a") :: Either SymBool SymBool)
.< Left (ssymBool "b")
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
(Left (ssymBool "a") :: Either SymBool SymBool)
.>= Left (ssymBool "b")
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
(Left (ssymBool "a") :: Either SymBool SymBool)
.> Left (ssymBool "b")
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
(Left (ssymBool "a") :: Either SymBool SymBool)
`symCompare` Left (ssymBool "b")
@?= (ssymBool "a" `symCompare` ssymBool "b")
(Left (ssymBool "a") :: Either SymBool SymBool)
.<= Right (ssymBool "b")
.@?= conBool True
(Left (ssymBool "a") :: Either SymBool SymBool)
.< Right (ssymBool "b")
.@?= conBool True
(Left (ssymBool "a") :: Either SymBool SymBool)
.>= Right (ssymBool "b")
.@?= conBool False
(Left (ssymBool "a") :: Either SymBool SymBool)
.> Right (ssymBool "b")
.@?= conBool False
(Left (ssymBool "a") :: Either SymBool SymBool)
`symCompare` Right (ssymBool "b")
@?= (mrgSingle LT :: Union Ordering)
(Right (ssymBool "a") :: Either SymBool SymBool)
.<= Left (ssymBool "b")
.@?= conBool False
(Right (ssymBool "a") :: Either SymBool SymBool)
.< Left (ssymBool "b")
.@?= conBool False
(Right (ssymBool "a") :: Either SymBool SymBool)
.>= Left (ssymBool "b")
.@?= conBool True
(Right (ssymBool "a") :: Either SymBool SymBool)
.> Left (ssymBool "b")
.@?= conBool True
(Right (ssymBool "a") :: Either SymBool SymBool)
`symCompare` Left (ssymBool "b")
@?= (mrgSingle GT :: Union Ordering)
(Right (ssymBool "a") :: Either SymBool SymBool)
.<= Right (ssymBool "b")
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
(Right (ssymBool "a") :: Either SymBool SymBool)
.< Right (ssymBool "b")
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
(Right (ssymBool "a") :: Either SymBool SymBool)
.>= Right (ssymBool "b")
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
(Right (ssymBool "a") :: Either SymBool SymBool)
.> Right (ssymBool "b")
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
(Right (ssymBool "a") :: Either SymBool SymBool)
`symCompare` Right (ssymBool "b")
@?= (ssymBool "a" `symCompare` ssymBool "b")
],
testGroup
"ExceptT"
[ testProperty
"ExceptT Integer Maybe Integer"
$ ioProperty
. concreteOrdOkProp @(ExceptT Integer Maybe Integer)
. bimap ExceptT ExceptT,
testCase "ExceptT SymBool Maybe SymBool" $ do
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.<= ExceptT Nothing
.@?= conBool True
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.<= ExceptT (Just (Left (ssymBool "a")))
.@?= conBool True
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.<= ExceptT (Just (Right (ssymBool "a")))
.@?= conBool True
ExceptT (Just (Left (ssymBool "a")))
.<= (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.@?= conBool False
ExceptT (Just (Right (ssymBool "a")))
.<= (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.@?= conBool False
ExceptT (Just (Left (ssymBool "a")))
.<= ( ExceptT (Just (Left (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
ExceptT (Just (Right (ssymBool "a")))
.<= ( ExceptT (Just (Left (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= conBool False
ExceptT (Just (Left (ssymBool "a")))
.<= ( ExceptT (Just (Right (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= conBool True
ExceptT (Just (Right (ssymBool "a")))
.<= ( ExceptT (Just (Right (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.< ExceptT Nothing
.@?= conBool False
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.< ExceptT (Just (Left (ssymBool "a")))
.@?= conBool True
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.< ExceptT (Just (Right (ssymBool "a")))
.@?= conBool True
ExceptT (Just (Left (ssymBool "a")))
.< (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.@?= conBool False
ExceptT (Just (Right (ssymBool "a")))
.< (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.@?= conBool False
ExceptT (Just (Left (ssymBool "a")))
.< ( ExceptT (Just (Left (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
ExceptT (Just (Right (ssymBool "a")))
.< ( ExceptT (Just (Left (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= conBool False
ExceptT (Just (Left (ssymBool "a")))
.< ( ExceptT (Just (Right (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= conBool True
ExceptT (Just (Right (ssymBool "a")))
.< ( ExceptT (Just (Right (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.>= ExceptT Nothing
.@?= conBool True
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.>= ExceptT (Just (Left (ssymBool "a")))
.@?= conBool False
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.>= ExceptT (Just (Right (ssymBool "a")))
.@?= conBool False
ExceptT (Just (Left (ssymBool "a")))
.>= (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.@?= conBool True
ExceptT (Just (Right (ssymBool "a")))
.>= (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.@?= conBool True
ExceptT (Just (Left (ssymBool "a")))
.>= ( ExceptT (Just (Left (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
ExceptT (Just (Right (ssymBool "a")))
.>= ( ExceptT (Just (Left (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= conBool True
ExceptT (Just (Left (ssymBool "a")))
.>= ( ExceptT (Just (Right (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= conBool False
ExceptT (Just (Right (ssymBool "a")))
.>= ( ExceptT (Just (Right (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.> ExceptT Nothing
.@?= conBool False
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.> ExceptT (Just (Left (ssymBool "a")))
.@?= conBool False
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.> ExceptT (Just (Right (ssymBool "a")))
.@?= conBool False
ExceptT (Just (Left (ssymBool "a")))
.> (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.@?= conBool True
ExceptT (Just (Right (ssymBool "a")))
.> (ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
.@?= conBool True
ExceptT (Just (Left (ssymBool "a")))
.> ( ExceptT (Just (Left (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
ExceptT (Just (Right (ssymBool "a")))
.> ( ExceptT (Just (Left (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= conBool True
ExceptT (Just (Left (ssymBool "a")))
.> ( ExceptT (Just (Right (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= conBool False
ExceptT (Just (Right (ssymBool "a")))
.> ( ExceptT (Just (Right (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
`symCompare` ExceptT Nothing
@?= (mrgSingle EQ :: Union Ordering)
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
`symCompare` ExceptT (Just (Left (ssymBool "a")))
@?= (mrgSingle LT :: Union Ordering)
(ExceptT Nothing :: ExceptT SymBool Maybe SymBool)
`symCompare` ExceptT (Just (Right (ssymBool "a")))
@?= (mrgSingle LT :: Union Ordering)
ExceptT (Just (Left (ssymBool "a")))
`symCompare` ( ExceptT Nothing ::
ExceptT SymBool Maybe SymBool
)
@?= (mrgSingle GT :: Union Ordering)
ExceptT (Just (Right (ssymBool "a")))
`symCompare` ( ExceptT Nothing ::
ExceptT SymBool Maybe SymBool
)
@?= (mrgSingle GT :: Union Ordering)
ExceptT (Just (Left (ssymBool "a")))
`symCompare` ( ExceptT (Just (Left (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
@?= (ssymBool "a" `symCompare` ssymBool "b" :: Union Ordering)
ExceptT (Just (Right (ssymBool "a")))
`symCompare` ( ExceptT (Just (Left (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
@?= (mrgSingle GT :: Union Ordering)
ExceptT (Just (Left (ssymBool "a")))
`symCompare` ( ExceptT (Just (Right (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
@?= (mrgSingle LT :: Union Ordering)
ExceptT (Just (Right (ssymBool "a")))
`symCompare` ( ExceptT (Just (Right (ssymBool "b"))) ::
ExceptT SymBool Maybe SymBool
)
@?= ( ssymBool "a" `symCompare` ssymBool "b" ::
Union Ordering
)
],
testProperty "()" (ioProperty . concreteOrdOkProp @()),
testGroup
"(,)"
[ testProperty "(Integer, Integer)" $
ioProperty . concreteOrdOkProp @(Integer, Integer),
testCase "(SymBool, SymBool)" $ do
let l = (ssymBool "a", ssymBool "c")
let r = (ssymBool "b", ssymBool "d")
let ll = ssymBool "a"
let lr = ssymBool "c"
let rl = ssymBool "b"
let rr = ssymBool "d"
symbolicProdOrdOkProp l r ll lr rl rr
],
testGroup
"(,,)"
[ testProperty "(Integer, Integer, Integer)" $
ioProperty . concreteOrdOkProp @(Integer, Integer, Integer),
testCase "(SymBool, SymBool, SymBool)" $ do
let l = (ssymBool "a", ssymBool "c", ssymBool "e")
let r = (ssymBool "b", ssymBool "d", ssymBool "f")
let ll = ssymBool "a"
let lr = (ssymBool "c", ssymBool "e")
let rl = ssymBool "b"
let rr = (ssymBool "d", ssymBool "f")
symbolicProdOrdOkProp l r ll lr rl rr
],
testGroup
"(,,,)"
[ testProperty
"(Integer, Integer, Integer, Integer)"
$ ioProperty
. concreteOrdOkProp @(Integer, Integer, Integer, Integer),
testCase "(SymBool, SymBool, SymBool, SymBool)" $ do
let l = (ssymBool "a", ssymBool "c", ssymBool "e", ssymBool "g")
let r = (ssymBool "b", ssymBool "d", ssymBool "f", ssymBool "h")
let ll = (ssymBool "a", ssymBool "c")
let lr = (ssymBool "e", ssymBool "g")
let rl = (ssymBool "b", ssymBool "d")
let rr = (ssymBool "f", ssymBool "h")
symbolicProdOrdOkProp l r ll lr rl rr
],
testGroup
"(,,,,)"
[ testProperty
"(Integer, Integer, Integer, Integer, Integer)"
$ ioProperty
. concreteOrdOkProp
@(Integer, Integer, Integer, Integer, Integer),
testCase "(SymBool, SymBool, SymBool, SymBool, SymBool)" $ do
let l =
( ssymBool "a",
ssymBool "c",
ssymBool "e",
ssymBool "g",
ssymBool "i"
)
let r =
( ssymBool "b",
ssymBool "d",
ssymBool "f",
ssymBool "h",
ssymBool "j"
)
let ll = (ssymBool "a", ssymBool "c")
let lr = (ssymBool "e", ssymBool "g", ssymBool "i")
let rl = (ssymBool "b", ssymBool "d")
let rr = (ssymBool "f", ssymBool "h", ssymBool "j")
symbolicProdOrdOkProp l r ll lr rl rr
],
testGroup
"(,,,,,)"
[ testProperty
"(Integer, Integer, Integer, Integer, Integer, Integer)"
$ ioProperty
. concreteOrdOkProp
@( Integer,
Integer,
Integer,
Integer,
Integer,
Integer
),
testCase
"(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
$ do
let l =
( ssymBool "a",
ssymBool "c",
ssymBool "e",
ssymBool "g",
ssymBool "i",
ssymBool "k"
)
let r =
( ssymBool "b",
ssymBool "d",
ssymBool "f",
ssymBool "h",
ssymBool "j",
ssymBool "l"
)
let ll = (ssymBool "a", ssymBool "c", ssymBool "e")
let lr = (ssymBool "g", ssymBool "i", ssymBool "k")
let rl = (ssymBool "b", ssymBool "d", ssymBool "f")
let rr = (ssymBool "h", ssymBool "j", ssymBool "l")
symbolicProdOrdOkProp l r ll lr rl rr
],
testGroup
"(,,,,,,)"
[ testProperty
"(Integer, Integer, Integer, Integer, Integer, Integer, Integer)"
$ ioProperty
. concreteOrdOkProp @(Integer, Integer, Integer, Integer, Integer, Integer, Integer),
testCase
"(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
$ do
let l =
( ssymBool "a",
ssymBool "c",
ssymBool "e",
ssymBool "g",
ssymBool "i",
ssymBool "k",
ssymBool "m"
)
let r =
( ssymBool "b",
ssymBool "d",
ssymBool "f",
ssymBool "h",
ssymBool "j",
ssymBool "l",
ssymBool "n"
)
let ll = (ssymBool "a", ssymBool "c", ssymBool "e")
let lr =
( ssymBool "g",
ssymBool "i",
ssymBool "k",
ssymBool "m"
)
let rl = (ssymBool "b", ssymBool "d", ssymBool "f")
let rr =
( ssymBool "h",
ssymBool "j",
ssymBool "l",
ssymBool "n"
)
symbolicProdOrdOkProp l r ll lr rl rr
],
testGroup
"(,,,,,,,)"
[ testProperty
"(Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer)"
( ioProperty
. concreteOrdOkProp
@( Integer,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer
)
),
testCase
"(SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool, SymBool)"
$ do
let l =
( ssymBool "a",
ssymBool "c",
ssymBool "e",
ssymBool "g",
ssymBool "i",
ssymBool "k",
ssymBool "m",
ssymBool "o"
)
let r =
( ssymBool "b",
ssymBool "d",
ssymBool "f",
ssymBool "h",
ssymBool "j",
ssymBool "l",
ssymBool "n",
ssymBool "p"
)
let ll =
( ssymBool "a",
ssymBool "c",
ssymBool "e",
ssymBool "g"
)
let lr =
( ssymBool "i",
ssymBool "k",
ssymBool "m",
ssymBool "o"
)
let rl =
( ssymBool "b",
ssymBool "d",
ssymBool "f",
ssymBool "h"
)
let rr =
( ssymBool "j",
ssymBool "l",
ssymBool "n",
ssymBool "p"
)
symbolicProdOrdOkProp l r ll lr rl rr
],
testGroup
"Sum"
[ testProperty
"Sum Maybe Maybe Integer"
( ioProperty . \v ->
let eitherToSum ::
Either (Maybe Integer) (Maybe Integer) ->
Sum Maybe Maybe Integer
eitherToSum (Left x) = InL x
eitherToSum (Right x) = InR x
in concreteOrdOkProp (bimap eitherToSum eitherToSum v)
),
testCase "Sum Maybe Maybe SymBool" $ do
(InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.<= InL (Just $ ssymBool "b")
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
(InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.< InL (Just $ ssymBool "b")
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
(InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.>= InL (Just $ ssymBool "b")
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
(InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.> InL (Just $ ssymBool "b")
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
(InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.<= InR (Just $ ssymBool "b")
.@?= conBool True
(InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.< InR (Just $ ssymBool "b")
.@?= conBool True
(InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.>= InR (Just $ ssymBool "b")
.@?= conBool False
(InL $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.> InR (Just $ ssymBool "b")
.@?= conBool False
(InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.<= InR (Just $ ssymBool "b")
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
(InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.< InR (Just $ ssymBool "b")
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
(InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.>= InR (Just $ ssymBool "b")
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
(InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.> InR (Just $ ssymBool "b")
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
(InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.<= InL (Just $ ssymBool "b")
.@?= conBool False
(InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.< InL (Just $ ssymBool "b")
.@?= conBool False
(InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.>= InL (Just $ ssymBool "b")
.@?= conBool True
(InR $ Just $ ssymBool "a" :: Sum Maybe Maybe SymBool)
.> InL (Just $ ssymBool "b")
.@?= conBool True
],
testGroup
"WriterT"
[ testGroup
"Lazy"
[ testProperty
"WriterT Integer (Either Integer) Integer"
( ioProperty
. \( v1 :: Either Integer (Integer, Integer),
v2 :: Either Integer (Integer, Integer)
) ->
concreteOrdOkProp
( WriterLazy.WriterT v1,
WriterLazy.WriterT v2
)
),
testCase "WriterT SymBool (Either SymBool) SymBool" $ do
( WriterLazy.WriterT $ Left $ ssymBool "a" ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.<= WriterLazy.WriterT (Left $ ssymBool "b")
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
( WriterLazy.WriterT $ Left $ ssymBool "a" ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.< WriterLazy.WriterT (Left $ ssymBool "b")
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
( WriterLazy.WriterT $ Left $ ssymBool "a" ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.>= WriterLazy.WriterT (Left $ ssymBool "b")
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
( WriterLazy.WriterT $ Left $ ssymBool "a" ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.> WriterLazy.WriterT (Left $ ssymBool "b")
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
( WriterLazy.WriterT $ Left $ ssymBool "a" ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
`symCompare` WriterLazy.WriterT (Left $ ssymBool "b")
@?= ( ssymBool "a" `symCompare` ssymBool "b" ::
Union Ordering
)
( WriterLazy.WriterT $ Left $ ssymBool "a" ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.<= WriterLazy.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= conBool True
( WriterLazy.WriterT $ Left $ ssymBool "a" ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.< WriterLazy.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= conBool True
( WriterLazy.WriterT $ Left $ ssymBool "a" ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.>= WriterLazy.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= conBool False
( WriterLazy.WriterT $ Left $ ssymBool "a" ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.> WriterLazy.WriterT (Right (ssymBool "b", ssymBool "d"))
.@?= conBool False
( WriterLazy.WriterT $ Left $ ssymBool "a" ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
`symCompare` WriterLazy.WriterT
(Right (ssymBool "b", ssymBool "d"))
@?= (mrgSingle LT :: Union Ordering)
( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.<= WriterLazy.WriterT (Left $ ssymBool "b")
.@?= conBool False
( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.< WriterLazy.WriterT (Left $ ssymBool "b")
.@?= conBool False
( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.>= WriterLazy.WriterT (Left $ ssymBool "b")
.@?= conBool True
( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.> WriterLazy.WriterT (Left $ ssymBool "b")
.@?= conBool True
( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
`symCompare` WriterLazy.WriterT (Left $ ssymBool "b")
@?= (mrgSingle GT :: Union Ordering)
( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.<= WriterLazy.WriterT (Right (ssymBool "b", ssymBool "d"))
.@?= ( (ssymBool "a", ssymBool "c")
.<= (ssymBool "b", ssymBool "d") ::
SymBool
)
( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.< WriterLazy.WriterT (Right (ssymBool "b", ssymBool "d"))
.@?= ( (ssymBool "a", ssymBool "c")
.< (ssymBool "b", ssymBool "d") ::
SymBool
)
( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.>= WriterLazy.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= ( (ssymBool "a", ssymBool "c")
.>= (ssymBool "b", ssymBool "d") ::
SymBool
)
( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
.> WriterLazy.WriterT (Right (ssymBool "b", ssymBool "d"))
.@?= ( (ssymBool "a", ssymBool "c")
.> (ssymBool "b", ssymBool "d") ::
SymBool
)
( WriterLazy.WriterT $ Right (ssymBool "a", ssymBool "c") ::
WriterLazy.WriterT SymBool (Either SymBool) SymBool
)
`symCompare` WriterLazy.WriterT
(Right (ssymBool "b", ssymBool "d"))
@?= ( (ssymBool "a", ssymBool "c")
`symCompare` (ssymBool "b", ssymBool "d") ::
Union Ordering
)
],
testGroup
"Strict"
[ testProperty
"WriterT Integer (Either Integer) Integer"
( ioProperty
. \( v1 :: Either Integer (Integer, Integer),
v2 :: Either Integer (Integer, Integer)
) ->
concreteOrdOkProp
( WriterStrict.WriterT v1,
WriterStrict.WriterT v2
)
),
testCase "WriterT Integer (Either Integer) Integer" $ do
( WriterStrict.WriterT $ Left $ ssymBool "a" ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.<= WriterStrict.WriterT (Left $ ssymBool "b")
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
( WriterStrict.WriterT $ Left $ ssymBool "a" ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.< WriterStrict.WriterT (Left $ ssymBool "b")
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
( WriterStrict.WriterT $ Left $ ssymBool "a" ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.>= WriterStrict.WriterT (Left $ ssymBool "b")
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
( WriterStrict.WriterT $ Left $ ssymBool "a" ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.> WriterStrict.WriterT (Left $ ssymBool "b")
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
( WriterStrict.WriterT $ Left $ ssymBool "a" ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
`symCompare` WriterStrict.WriterT (Left $ ssymBool "b")
@?= ( ssymBool "a" `symCompare` ssymBool "b" ::
Union Ordering
)
( WriterStrict.WriterT $ Left $ ssymBool "a" ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.<= WriterStrict.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= conBool True
( WriterStrict.WriterT $ Left $ ssymBool "a" ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.< WriterStrict.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= conBool True
( WriterStrict.WriterT $ Left $ ssymBool "a" ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.>= WriterStrict.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= conBool False
( WriterStrict.WriterT $ Left $ ssymBool "a" ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.> WriterStrict.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= conBool False
( WriterStrict.WriterT $ Left $ ssymBool "a" ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
`symCompare` WriterStrict.WriterT
(Right (ssymBool "b", ssymBool "d"))
@?= (mrgSingle LT :: Union Ordering)
( WriterStrict.WriterT $
Right (ssymBool "a", ssymBool "c") ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.<= WriterStrict.WriterT (Left $ ssymBool "b")
.@?= conBool False
( WriterStrict.WriterT $
Right (ssymBool "a", ssymBool "c") ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.< WriterStrict.WriterT (Left $ ssymBool "b")
.@?= conBool False
( WriterStrict.WriterT $
Right (ssymBool "a", ssymBool "c") ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.>= WriterStrict.WriterT (Left $ ssymBool "b")
.@?= conBool True
( WriterStrict.WriterT $
Right (ssymBool "a", ssymBool "c") ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.> WriterStrict.WriterT (Left $ ssymBool "b")
.@?= conBool True
( WriterStrict.WriterT $
Right (ssymBool "a", ssymBool "c") ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
`symCompare` WriterStrict.WriterT (Left $ ssymBool "b")
@?= (mrgSingle GT :: Union Ordering)
( WriterStrict.WriterT $
Right (ssymBool "a", ssymBool "c") ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.<= WriterStrict.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= ( (ssymBool "a", ssymBool "c")
.<= (ssymBool "b", ssymBool "d") ::
SymBool
)
( WriterStrict.WriterT $
Right (ssymBool "a", ssymBool "c") ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.< WriterStrict.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= ( (ssymBool "a", ssymBool "c")
.< (ssymBool "b", ssymBool "d") ::
SymBool
)
( WriterStrict.WriterT $
Right (ssymBool "a", ssymBool "c") ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.>= WriterStrict.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= ( (ssymBool "a", ssymBool "c")
.>= (ssymBool "b", ssymBool "d") ::
SymBool
)
( WriterStrict.WriterT $
Right (ssymBool "a", ssymBool "c") ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
.> WriterStrict.WriterT
(Right (ssymBool "b", ssymBool "d"))
.@?= ( (ssymBool "a", ssymBool "c")
.> (ssymBool "b", ssymBool "d") ::
SymBool
)
( WriterStrict.WriterT $
Right (ssymBool "a", ssymBool "c") ::
WriterStrict.WriterT SymBool (Either SymBool) SymBool
)
`symCompare` WriterStrict.WriterT
(Right (ssymBool "b", ssymBool "d"))
@?= ( (ssymBool "a", ssymBool "c")
`symCompare` (ssymBool "b", ssymBool "d") ::
Union Ordering
)
]
],
testGroup
"Identity"
[ testProperty
"Identity Integer"
( ioProperty . \(v1 :: Integer, v2) ->
concreteOrdOkProp (Identity v1, Identity v2)
),
testCase "Identity SymBool" $ do
(Identity $ ssymBool "a" :: Identity SymBool)
.<= Identity (ssymBool "b")
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
(Identity $ ssymBool "a" :: Identity SymBool)
.< Identity (ssymBool "b")
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
(Identity $ ssymBool "a" :: Identity SymBool)
.>= Identity (ssymBool "b")
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
(Identity $ ssymBool "a" :: Identity SymBool)
.> Identity (ssymBool "b")
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
],
testGroup
"IdentityT"
[ testProperty
"IdentityT (Either Integer) Integer"
( ioProperty . \(v1 :: Either Integer Integer, v2) ->
concreteOrdOkProp (IdentityT v1, IdentityT v2)
),
testCase "IdentityT (Either SymBool) SymBool" $ do
( IdentityT $ Left $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.<= IdentityT (Left $ ssymBool "b")
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
( IdentityT $ Left $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.< IdentityT (Left $ ssymBool "b")
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
( IdentityT $ Left $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.>= IdentityT (Left $ ssymBool "b")
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
( IdentityT $ Left $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.> IdentityT (Left $ ssymBool "b")
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
( IdentityT $ Left $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
`symCompare` IdentityT (Left $ ssymBool "b")
@?= (ssymBool "a" `symCompare` ssymBool "b")
( IdentityT $ Left $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.<= IdentityT (Right $ ssymBool "b")
.@?= conBool True
( IdentityT $ Left $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.< IdentityT (Right $ ssymBool "b")
.@?= conBool True
( IdentityT $ Left $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.>= IdentityT (Right $ ssymBool "b")
.@?= conBool False
( IdentityT $ Left $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.> IdentityT (Right $ ssymBool "b")
.@?= conBool False
( IdentityT $ Left $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
`symCompare` IdentityT (Right $ ssymBool "b")
@?= (mrgSingle LT :: Union Ordering)
( IdentityT $ Right $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.<= IdentityT (Left $ ssymBool "b")
.@?= conBool False
( IdentityT $ Right $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.< IdentityT (Left $ ssymBool "b")
.@?= conBool False
( IdentityT $ Right $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.>= IdentityT (Left $ ssymBool "b")
.@?= conBool True
( IdentityT $ Right $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.> IdentityT (Left $ ssymBool "b")
.@?= conBool True
( IdentityT $ Right $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
`symCompare` IdentityT (Left $ ssymBool "b")
@?= (mrgSingle GT :: Union Ordering)
( IdentityT $ Right $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.<= IdentityT (Right $ ssymBool "b")
.@?= (ssymBool "a" .<= ssymBool "b" :: SymBool)
( IdentityT $ Right $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.< IdentityT (Right $ ssymBool "b")
.@?= (ssymBool "a" .< ssymBool "b" :: SymBool)
( IdentityT $ Right $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.>= IdentityT (Right $ ssymBool "b")
.@?= (ssymBool "a" .>= ssymBool "b" :: SymBool)
( IdentityT $ Right $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
.> IdentityT (Right $ ssymBool "b")
.@?= (ssymBool "a" .> ssymBool "b" :: SymBool)
( IdentityT $ Right $ ssymBool "a" ::
IdentityT (Either SymBool) SymBool
)
`symCompare` IdentityT (Right $ ssymBool "b")
@?= (ssymBool "a" `symCompare` ssymBool "b")
],
testCase "ByteString" $ do
let bytestrings :: [B.ByteString] =
["", "a", "b", "ab", "ba", "aa", "bb"]
traverse_
concreteOrdOkProp
[(x, y) | x <- bytestrings, y <- bytestrings]
],
testCase "symMax" $ do
symMax (1 :: SymInteger) 2 @?= 2
let [a, b] = ["a", "b"] :: [SymInteger]
symMax a b .@?= symIte (a .>= b) a b,
testCase "symMin" $ do
symMin (1 :: SymInteger) 2 @?= 1
let [a, b] = ["a", "b"] :: [SymInteger]
symMin a b .@?= symIte (a .>= b) b a,
testCase "mrgMax" $ do
mrgMax [1] [0, 3] @?= (mrgReturn [1] :: Union [SymInteger])
let [a, b, c] = ["a", "b", "c"] :: [SymInteger]
(mrgMax [a] [b, c] :: Union [SymInteger])
.@?= (mrgIf (a .<= b) (return [b, c]) (return [a])),
testCase "mrgMin" $ do
mrgMin [1] [0, 3] @?= (mrgReturn [0, 3] :: Union [SymInteger])
let [a, b, c] = ["a", "b", "c"] :: [SymInteger]
(mrgMin [a] [b, c] :: Union [SymInteger])
.@?= (mrgIf (b .< a) (return [b, c]) (return [a]))
]