grisette-0.13.0.1: test/Grisette/Core/Data/UnionBaseTests.hs
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Grisette.Core.Data.UnionBaseTests (unionBaseTests) where
import GHC.Generics (Generic)
import Grisette
( AsKey (AsKey),
ITEOp (symIte),
LogicalOp (symNot, (.&&), (.||)),
Mergeable (rootStrategy),
MergingStrategy (SortedStrategy),
Solvable (con),
SymInteger,
wrapStrategy,
)
import Grisette.Internal.Core.Data.UnionBase
( UnionBase (UnionIf, UnionSingle),
fullReconstruct,
ifWithLeftMost,
ifWithStrategy,
)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.HUnit ((@?=))
data TripleSum a b c = TS1 a | TS2 b | TS3 c deriving (Show, Eq, Generic)
instance
(Mergeable a, Mergeable b, Mergeable c) =>
Mergeable (TripleSum a b c)
where
rootStrategy =
SortedStrategy
(\case TS1 _ -> (0 :: Int); TS2 _ -> (1 :: Int); TS3 _ -> (2 :: Int))
( \case
0 -> wrapStrategy rootStrategy TS1 (\(TS1 x) -> x)
1 -> wrapStrategy rootStrategy TS2 (\(TS2 x) -> x)
2 -> wrapStrategy rootStrategy TS3 (\(TS3 x) -> x)
_ -> error "Bad"
)
unionBaseTests :: Test
unionBaseTests =
testGroup
"UnionBase"
[ testGroup
"ifWithLeftMost"
[ testCase
"ifWithLeftMost should maintain left most info on Singles"
$ do
AsKey
( ifWithLeftMost
False
"a"
(UnionSingle (1 :: Integer))
(UnionSingle 2)
)
@?= AsKey (UnionIf 1 False "a" (UnionSingle 1) (UnionSingle 2)),
testCase "ifWithLeftMost should maintain left most info on Ifs" $ do
AsKey
( ifWithLeftMost
True
"a"
( UnionIf
1
True
"b"
(UnionSingle (1 :: Integer))
(UnionSingle 2)
)
(UnionIf 3 True "c" (UnionSingle 3) (UnionSingle 4))
)
@?= AsKey
( UnionIf
1
True
"a"
( UnionIf
1
True
"b"
(UnionSingle (1 :: Integer))
(UnionSingle 2)
)
(UnionIf 3 True "c" (UnionSingle 3) (UnionSingle 4))
)
],
testGroup
"ifWithStrategy"
[ testGroup
"ifWithStrategy with concrete condition"
[ testCase "true" $ do
AsKey
( ifWithStrategy
rootStrategy
(con True)
(UnionSingle (1 :: Integer))
(UnionSingle 2)
)
@?= AsKey (UnionSingle 1),
testCase "false" $ do
AsKey
( ifWithStrategy
rootStrategy
(con False)
(UnionSingle (1 :: Integer))
(UnionSingle 2)
)
@?= AsKey (UnionSingle 2)
],
let a =
ifWithStrategy
rootStrategy
"a"
(UnionSingle (1 :: Integer))
(UnionSingle 2)
in testGroup
"ifWithStrategy with condition equal to sub conditions"
[ testCase "ifTrue" $ do
AsKey
(ifWithStrategy rootStrategy "a" a (UnionSingle 3))
@?= AsKey (UnionIf 1 True "a" (UnionSingle 1) (UnionSingle 3)),
testCase "ifFalse" $ do
AsKey
(ifWithStrategy rootStrategy "a" (UnionSingle 0) a)
@?= AsKey (UnionIf 0 True "a" (UnionSingle 0) (UnionSingle 2))
],
testCase "ifWithStrategy with simple mergeables" $ do
AsKey
( ifWithStrategy
rootStrategy
"a"
(UnionSingle ("b" :: AsKey SymInteger))
(UnionSingle "c")
)
@?= AsKey (UnionSingle (symIte "a" "b" "c")),
testGroup
"ifWithStrategy with ordered mergeables"
[ testGroup
"ifWithStrategy on Single/Single"
[ testGroup
"idxt < idxf"
[ testCase "Integer" $
AsKey
( ifWithStrategy
rootStrategy
"a"
(UnionSingle (1 :: Integer))
(UnionSingle 2)
)
@?= AsKey
( UnionIf
1
True
"a"
(UnionSingle 1)
(UnionSingle 2)
),
testCase "Maybe Integer" $
AsKey
( ifWithStrategy
rootStrategy
"a"
(UnionSingle Nothing)
(UnionSingle (Just (2 :: Integer)))
)
@?= AsKey
( UnionIf
Nothing
True
"a"
(UnionSingle Nothing)
(UnionSingle (Just 2))
)
],
testGroup
"idxt == idxf"
[ testGroup
"idxt == idxf as terminal"
[ testCase "Integer" $
AsKey
( ifWithStrategy
rootStrategy
"a"
(UnionSingle (1 :: Integer))
(UnionSingle 1)
)
@?= AsKey (UnionSingle 1),
testCase "Maybe Integer" $
AsKey
( ifWithStrategy
rootStrategy
"a"
(UnionSingle (Just ("b" :: AsKey SymInteger)))
(UnionSingle (Just "c"))
)
@?= AsKey (UnionSingle (Just (symIte "a" "b" "c")))
],
testGroup
"idxt == idxf but not terminal"
[ testCase "Maybe Integer" $
AsKey
( ifWithStrategy
rootStrategy
"a"
(UnionSingle (Just (1 :: Integer)))
(UnionSingle (Just (2 :: Integer)))
)
@?= AsKey
( UnionIf
(Just 1)
True
"a"
(UnionSingle $ Just 1)
(UnionSingle (Just 2))
),
testCase "Maybe (Maybe Integer)" $
AsKey
( ifWithStrategy
rootStrategy
"a"
(UnionSingle $ Just $ Just ("b" :: AsKey SymInteger))
(UnionSingle $ Just $ Just "c")
)
@?= AsKey (UnionSingle (Just (Just (symIte "a" "b" "c"))))
]
],
testGroup
"idxt > idxf"
[ testCase "Integer" $
AsKey
( ifWithStrategy
rootStrategy
"a"
(UnionSingle (2 :: Integer))
(UnionSingle 1)
)
@?= AsKey
( UnionIf
1
True
(symNot "a")
(UnionSingle 1)
(UnionSingle 2)
),
testCase "Maybe Integer" $
AsKey
( ifWithStrategy
rootStrategy
"a"
(UnionSingle (Just (2 :: Integer)))
(UnionSingle Nothing)
)
@?= AsKey
( UnionIf
Nothing
True
(symNot "a")
(UnionSingle Nothing)
(UnionSingle (Just 2))
)
]
],
testGroup
"ifWithStrategy on Single/If"
[ testGroup
"Degenerate to Single/Single when idxft == idxff"
[ testCase "Degenerated case with idxt < idxf" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle (Just (1 :: Integer)))
(UnionSingle (Just (2 :: Integer)))
AsKey
( ifWithStrategy
rootStrategy
"b"
(UnionSingle Nothing)
x
)
@?= AsKey
( UnionIf
Nothing
True
"b"
(UnionSingle Nothing)
( UnionIf
(Just 1)
True
"a"
(UnionSingle $ Just 1)
(UnionSingle (Just 2))
)
),
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle (Just (1 :: Integer)))
(UnionSingle (Just (3 :: Integer)))
in testGroup
"Degenerated case with idxt == idxf"
[ testCase "sub-idxt < sub-idxft" $
AsKey
( ifWithStrategy
rootStrategy
"b"
(UnionSingle $ Just 0)
x
)
@?= AsKey
( UnionIf
(Just 0)
True
"b"
(UnionSingle $ Just 0)
( UnionIf
(Just 1)
True
"a"
(UnionSingle $ Just 1)
(UnionSingle (Just 3))
)
),
testCase "sub-idxt == sub-idxft" $
AsKey
( ifWithStrategy
rootStrategy
"b"
(UnionSingle $ Just 1)
x
)
@?= AsKey
( UnionIf
(Just 1)
True
("b" .|| "a")
(UnionSingle $ Just 1)
(UnionSingle (Just 3))
),
testCase "subidxft < sub-idxt < sub-idxff" $
AsKey
( ifWithStrategy
rootStrategy
"b"
(UnionSingle $ Just 2)
x
)
@?= AsKey
( UnionIf
(Just 1)
True
((symNot "b") .&& "a")
(UnionSingle $ Just 1)
( UnionIf
(Just 2)
True
"b"
(UnionSingle $ Just 2)
(UnionSingle $ Just 3)
)
),
testCase "sub-idxt == sub-idxff" $
AsKey
( ifWithStrategy
rootStrategy
"b"
(UnionSingle $ Just 3)
x
)
@?= AsKey
( UnionIf
(Just 1)
True
((symNot "b") .&& "a")
(UnionSingle $ Just 1)
(UnionSingle (Just 3))
),
testCase "sub-idxff < sub-idxt" $
AsKey
( ifWithStrategy
rootStrategy
"b"
(UnionSingle $ Just 4)
x
)
@?= AsKey
( UnionIf
(Just 1)
True
((symNot "b") .&& "a")
(UnionSingle $ Just 1)
( UnionIf
(Just 3)
True
(symNot "b")
(UnionSingle $ Just 3)
(UnionSingle $ Just 4)
)
)
],
testCase "Degenerated case with idxt > idxf" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle (Left (1 :: Integer)))
(UnionSingle (Left (2 :: Integer)))
AsKey
( ifWithStrategy
rootStrategy
"b"
(UnionSingle $ Right (1 :: Integer))
x
)
@?= AsKey
( UnionIf
(Left 1)
True
(symNot "b")
( UnionIf
(Left 1)
True
"a"
(UnionSingle $ Left 1)
(UnionSingle (Left 2))
)
(UnionSingle $ Right 1)
)
],
testCase "idxt < idxft" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle (1 :: Integer))
(UnionSingle (3 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"b"
(UnionSingle 0)
x
)
@?= AsKey
( UnionIf
0
True
"b"
(UnionSingle 0)
( UnionIf
1
True
"a"
(UnionSingle 1)
(UnionSingle 3)
)
),
testCase "idxt == idxft" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle $ Left (1 :: Integer))
(UnionSingle $ Right (3 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"b"
(UnionSingle $ Left 0)
x
)
@?= AsKey
( UnionIf
(Left 0)
True
("b" .|| "a")
( UnionIf
(Left 0)
True
"b"
(UnionSingle $ Left 0)
(UnionSingle $ Left 1)
)
(UnionSingle $ Right 3)
),
testCase "idxt > idxft" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle $ Left (1 :: Integer))
(UnionSingle $ Right (3 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"b"
(UnionSingle $ Right 0)
x
)
@?= AsKey
( UnionIf
(Left 1)
True
((symNot "b") .&& "a")
(UnionSingle $ Left 1)
( UnionIf
(Right 0)
True
"b"
(UnionSingle $ Right 0)
(UnionSingle $ Right 3)
)
)
],
testGroup
"ifWithStrategy on If/Single"
[ testGroup
"Degenerate to Single/Single when idxtt == idxtf"
[ testCase "Degenerated case with idxt < idxf" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle (Left (1 :: Integer)))
(UnionSingle (Left (2 :: Integer)))
AsKey
( ifWithStrategy
rootStrategy
"b"
x
(UnionSingle $ Right (2 :: Integer))
)
@?= AsKey
( UnionIf
(Left 1)
True
"b"
( UnionIf
(Left 1)
True
"a"
(UnionSingle $ Left 1)
(UnionSingle (Left 2))
)
(UnionSingle $ Right 2)
),
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle (Just (1 :: Integer)))
(UnionSingle (Just (3 :: Integer)))
in testGroup
"Degenerated case with idxt == idxf"
[ testCase "sub-idxf < sub-idxtt" $
AsKey
( ifWithStrategy
rootStrategy
"b"
x
(UnionSingle $ Just 0)
)
@?= AsKey
( UnionIf
(Just 0)
True
(symNot "b")
(UnionSingle $ Just 0)
( UnionIf
(Just 1)
True
"a"
(UnionSingle $ Just 1)
(UnionSingle (Just 3))
)
),
testCase "sub-idxf == sub-idxtt" $
AsKey
( ifWithStrategy
rootStrategy
"b"
x
(UnionSingle $ Just 1)
)
@?= AsKey
( UnionIf
(Just 1)
True
((symNot "b") .|| "a")
(UnionSingle $ Just 1)
(UnionSingle (Just 3))
),
testCase "sub-idxtt < sub-idxf < sub-idxtf" $
AsKey
( ifWithStrategy
rootStrategy
"b"
x
(UnionSingle $ Just 2)
)
@?= AsKey
( UnionIf
(Just 1)
True
("b" .&& "a")
(UnionSingle $ Just 1)
( UnionIf
(Just 2)
True
(symNot "b")
(UnionSingle $ Just 2)
(UnionSingle $ Just 3)
)
),
testCase "sub-idxf == sub-idxtf" $
AsKey
( ifWithStrategy
rootStrategy
"b"
x
(UnionSingle $ Just 3)
)
@?= AsKey
( UnionIf
(Just 1)
True
("b" .&& "a")
(UnionSingle $ Just 1)
(UnionSingle (Just 3))
),
testCase "sub-idxtf < sub-idxf" $
AsKey
( ifWithStrategy
rootStrategy
"b"
x
(UnionSingle $ Just 4)
)
@?= AsKey
( UnionIf
(Just 1)
True
("b" .&& "a")
(UnionSingle $ Just 1)
( UnionIf
(Just 3)
True
"b"
(UnionSingle $ Just 3)
(UnionSingle $ Just 4)
)
)
],
testCase "Degenerated case with idxt > idxf" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle (Right (1 :: Integer)))
(UnionSingle (Right (2 :: Integer)))
AsKey
( ifWithStrategy
rootStrategy
"b"
x
(UnionSingle $ Left (1 :: Integer))
)
@?= AsKey
( UnionIf
(Left 1)
True
(symNot "b")
(UnionSingle $ Left 1)
( UnionIf
(Right 1)
True
"a"
(UnionSingle $ Right 1)
(UnionSingle (Right 2))
)
)
],
testCase "idxtt < idxf" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle $ Left (1 :: Integer))
(UnionSingle $ Right (3 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"b"
x
(UnionSingle $ Right 0)
)
@?= AsKey
( UnionIf
(Left 1)
True
("b" .&& "a")
(UnionSingle $ Left 1)
( UnionIf
(Right 0)
True
(symNot "b")
(UnionSingle $ Right 0)
(UnionSingle $ Right 3)
)
),
testCase "idxtt == idxf" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle $ Left (1 :: Integer))
(UnionSingle $ Right (3 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"b"
x
(UnionSingle $ Left 0)
)
@?= AsKey
( UnionIf
(Left 0)
True
((symNot "b") .|| "a")
( UnionIf
(Left 0)
True
(symNot "b")
(UnionSingle $ Left 0)
(UnionSingle $ Left 1)
)
(UnionSingle $ Right 3)
),
testCase "idxtt > idxf" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle (1 :: Integer))
(UnionSingle (3 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"b"
x
(UnionSingle 0)
)
@?= AsKey
( UnionIf
0
True
(symNot "b")
(UnionSingle 0)
(UnionIf 1 True "a" (UnionSingle 1) (UnionSingle 3))
)
],
testGroup
"ifWithStrategy on If/If"
[ testCase "Degenerate to Single/If when idxtt == idxtf" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle $ Left (1 :: Integer))
(UnionSingle $ Left (2 :: Integer))
let y =
ifWithStrategy
rootStrategy
"b"
(UnionSingle $ Left (1 :: Integer))
(UnionSingle $ Right (2 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"c"
x
y
)
@?= AsKey
( UnionIf
(Left 1)
True
("c" .|| "b")
( UnionIf
(Left 1)
True
((symNot "c") .|| "a")
(UnionSingle $ Left 1)
(UnionSingle $ Left 2)
)
(UnionSingle $ Right 2)
),
testCase "Degenerate to Single/If when idxff == idxft" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle $ Left (1 :: Integer))
(UnionSingle $ Left (2 :: Integer))
let y =
ifWithStrategy
rootStrategy
"b"
(UnionSingle $ Left (1 :: Integer))
(UnionSingle $ Right (2 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"c"
y
x
)
@?= AsKey
( UnionIf
(Left 1)
True
((symNot "c") .|| "b")
( UnionIf
(Left 1)
True
("c" .|| "a")
(UnionSingle $ Left 1)
(UnionSingle $ Left 2)
)
(UnionSingle $ Right 2)
),
testCase "Non-degenerated case when idxtt < idxft" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle $ TS1 (1 :: Integer))
(UnionSingle $ TS2 (2 :: Integer))
let y =
ifWithStrategy
rootStrategy
"b"
(UnionSingle $ TS2 (1 :: Integer))
(UnionSingle $ TS3 (2 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"c"
x
y
)
@?= AsKey
( UnionIf
(TS1 1)
True
("c" .&& "a")
(UnionSingle $ TS1 1)
( UnionIf
(TS2 1)
True
("c" .|| "b")
( UnionIf
(TS2 1)
True
(symNot "c")
(UnionSingle $ TS2 1)
(UnionSingle $ TS2 2)
)
(UnionSingle $ TS3 2)
)
),
testCase "Non-degenerated case when idxtt == idxft" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle $ TS1 (1 :: Integer))
(UnionSingle $ TS2 (2 :: Integer))
let y =
ifWithStrategy
rootStrategy
"b"
(UnionSingle $ TS1 (2 :: Integer))
(UnionSingle $ TS3 (2 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"c"
x
y
)
@?= AsKey
( UnionIf
(TS1 1)
True
(symIte "c" "a" "b")
( UnionIf
(TS1 1)
True
"c"
(UnionSingle $ TS1 1)
(UnionSingle $ TS1 2)
)
( UnionIf
(TS2 2)
True
"c"
(UnionSingle $ TS2 2)
(UnionSingle $ TS3 2)
)
),
testCase "Non-degenerated case when idxtt > idxft" $ do
let x =
ifWithStrategy
rootStrategy
"a"
(UnionSingle $ TS2 (1 :: Integer))
(UnionSingle $ TS3 (2 :: Integer))
let y =
ifWithStrategy
rootStrategy
"b"
(UnionSingle $ TS1 (1 :: Integer))
(UnionSingle $ TS2 (2 :: Integer))
AsKey
( ifWithStrategy
rootStrategy
"c"
x
y
)
@?= AsKey
( UnionIf
(TS1 1)
True
((symNot "c") .&& "b")
(UnionSingle $ TS1 1)
( UnionIf
(TS2 1)
True
((symNot "c") .|| "a")
( UnionIf
(TS2 1)
True
"c"
(UnionSingle $ TS2 1)
(UnionSingle $ TS2 2)
)
(UnionSingle $ TS3 2)
)
)
],
testCase "ifWithStrategy should tolerate non-merged Ifs" $ do
let x =
UnionIf
(Right 2)
False
"a"
(UnionSingle $ Right (2 :: Integer))
(UnionSingle $ Left (2 :: Integer))
let y =
UnionIf
(Right 3)
False
"b"
(UnionSingle $ Right 3)
(UnionSingle $ Left 1)
AsKey
( ifWithStrategy
rootStrategy
"c"
x
y
)
@?= AsKey
( UnionIf
(Left 1)
True
(symIte "c" (symNot "a") (symNot "b"))
( UnionIf
(Left 1)
True
(symNot "c")
(UnionSingle $ Left 1)
(UnionSingle $ Left 2)
)
( UnionIf
(Right 2)
True
"c"
(UnionSingle $ Right 2)
(UnionSingle $ Right 3)
)
)
]
],
testGroup
"fullReconstruct"
[ testCase "fullReconstruct should work" $ do
let x =
UnionIf
(Right 2)
False
"a"
(UnionSingle $ Right (2 :: Integer))
(UnionSingle $ Left (2 :: Integer))
let y =
UnionIf
(Right 3)
False
"b"
(UnionSingle $ Right 3)
(UnionSingle $ Left 1)
let z = UnionIf (Right 2) False "c" x y
AsKey (fullReconstruct rootStrategy z)
@?= AsKey
( UnionIf
(Left 1)
True
(symIte "c" (symNot "a") (symNot "b"))
( UnionIf
(Left 1)
True
(symNot "c")
(UnionSingle $ Left 1)
(UnionSingle $ Left 2)
)
( UnionIf
(Right 2)
True
"c"
(UnionSingle $ Right 2)
(UnionSingle $ Right 3)
)
)
]
]