{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
module Test.Ouroboros.Consensus.ChainGenerator.Tests.BitVector (tests) where
import Data.Monoid (Endo (Endo, appEndo))
import qualified Data.Vector.Unboxed as V
import GHC.Generics (Generic)
import qualified System.Random.Stateful as R
import qualified Test.Ouroboros.Consensus.ChainGenerator.BitVector as BV
import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C
import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S
import Test.Ouroboros.Consensus.ChainGenerator.Slot
(E (EmptySlotE, SlotE), POL, PreImage, S)
import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some
import qualified Test.QuickCheck as QC
import Test.QuickCheck.Random (QCGen)
import qualified Test.Tasty as TT
import qualified Test.Tasty.QuickCheck as TT
import qualified Test.Util.QuickCheck as QC
tests :: [TT.TestTree]
tests :: [TestTree]
tests = [
TestName -> (SomeFindTestSetup -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TT.testProperty TestName
"prop_findIthEmptyInV" SomeFindTestSetup -> Property
prop_findIthEmptyInV,
TestName -> (FillInWindowSetup -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TT.testProperty TestName
"prop_fillInWindow" FillInWindowSetup -> Property
prop_fillInWindow
]
data SomeFindTestSetup = forall pol. TestPOL pol => SomeFindTestSetup (FindTestSetup pol)
instance Show SomeFindTestSetup where
showsPrec :: Int -> SomeFindTestSetup -> ShowS
showsPrec Int
p (SomeFindTestSetup FindTestSetup pol
testSetup) =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ TestName -> ShowS
showString TestName
"SomeFindTestSetup " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> FindTestSetup pol -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 FindTestSetup pol
testSetup
data ProxyPol (pol :: S.Pol) = ProxyPol
deriving (ProxyPol pol -> ProxyPol pol -> Bool
(ProxyPol pol -> ProxyPol pol -> Bool)
-> (ProxyPol pol -> ProxyPol pol -> Bool) -> Eq (ProxyPol pol)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (pol :: Pol). ProxyPol pol -> ProxyPol pol -> Bool
$c== :: forall (pol :: Pol). ProxyPol pol -> ProxyPol pol -> Bool
== :: ProxyPol pol -> ProxyPol pol -> Bool
$c/= :: forall (pol :: Pol). ProxyPol pol -> ProxyPol pol -> Bool
/= :: ProxyPol pol -> ProxyPol pol -> Bool
Eq)
instance TestPOL pol => Show (ProxyPol pol) where
showsPrec :: Int -> ProxyPol pol -> ShowS
showsPrec Int
p ProxyPol pol
pol =
Int -> ShowBuilder (ProxyPol pol) -> ShowS
forall a.
NoFun "runShowsPrec" a (AbsError "runShowsPrec" a) =>
Int -> ShowBuilder a -> ShowS
Some.runShowsPrec Int
p
(ShowBuilder (ProxyPol pol) -> ShowS)
-> ShowBuilder (ProxyPol pol) -> ShowS
forall a b. (a -> b) -> a -> b
$ ProxyPol pol -> TestName -> ShowBuilder (ProxyPol pol)
forall a. a -> TestName -> ShowBuilder a
Some.showCtor ProxyPol pol
pol (TestName
"ProxyPol :: ProxyPol " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProxyPol pol -> TestName
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> TestName
forall (proxy :: Pol -> *). proxy pol -> TestName
showPol ProxyPol pol
pol)
instance TestPOL pol => Read (ProxyPol pol) where
readPrec :: ReadPrec (ProxyPol pol)
readPrec =
ReadBuilder (ProxyPol pol) -> ReadPrec (ProxyPol pol)
forall a.
NoFun "runReadPrec" a (AbsError "runReadPrec" a) =>
ReadBuilder a -> ReadPrec a
Some.runReadPrec
(ReadBuilder (ProxyPol pol) -> ReadPrec (ProxyPol pol))
-> ReadBuilder (ProxyPol pol) -> ReadPrec (ProxyPol pol)
forall a b. (a -> b) -> a -> b
$ ProxyPol pol -> TestName -> ReadBuilder (ProxyPol pol)
forall a. a -> TestName -> ReadBuilder a
Some.readCtor ProxyPol pol
pol (ProxyPol pol -> TestName
forall a. Show a => a -> TestName
show ProxyPol pol
pol)
where
pol :: ProxyPol pol
pol = ProxyPol pol
forall (pol :: Pol). ProxyPol pol
ProxyPol :: ProxyPol pol
data TestB
instance QC.Arbitrary (ProxyPol pol) where
arbitrary :: Gen (ProxyPol pol)
arbitrary = ProxyPol pol -> Gen (ProxyPol pol)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProxyPol pol
forall (pol :: Pol). ProxyPol pol
ProxyPol
shrink :: ProxyPol pol -> [ProxyPol pol]
shrink = ProxyPol pol -> [ProxyPol pol]
forall a. a -> [a]
QC.shrinkNothing
data SomePol = forall pol. TestPOL pol => SomePol (ProxyPol pol)
deriving instance Show SomePol
data FindTestSetup (pol :: S.Pol) = FindTestSetup {
forall (pol :: Pol). FindTestSetup pol -> ProxyPol pol
testPol :: ProxyPol pol
,
forall (pol :: Pol).
FindTestSetup pol -> Index TestB (PreImage pol 'EmptySlotE)
testIndex :: C.Index TestB (PreImage pol EmptySlotE)
,
forall (pol :: Pol). FindTestSetup pol -> Vector TestB 'SlotE S
testV :: C.Vector TestB SlotE S
}
deriving (FindTestSetup pol -> FindTestSetup pol -> Bool
(FindTestSetup pol -> FindTestSetup pol -> Bool)
-> (FindTestSetup pol -> FindTestSetup pol -> Bool)
-> Eq (FindTestSetup pol)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (pol :: Pol). FindTestSetup pol -> FindTestSetup pol -> Bool
$c== :: forall (pol :: Pol). FindTestSetup pol -> FindTestSetup pol -> Bool
== :: FindTestSetup pol -> FindTestSetup pol -> Bool
$c/= :: forall (pol :: Pol). FindTestSetup pol -> FindTestSetup pol -> Bool
/= :: FindTestSetup pol -> FindTestSetup pol -> Bool
Eq, (forall x. FindTestSetup pol -> Rep (FindTestSetup pol) x)
-> (forall x. Rep (FindTestSetup pol) x -> FindTestSetup pol)
-> Generic (FindTestSetup pol)
forall x. Rep (FindTestSetup pol) x -> FindTestSetup pol
forall x. FindTestSetup pol -> Rep (FindTestSetup pol) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (pol :: Pol) x.
Rep (FindTestSetup pol) x -> FindTestSetup pol
forall (pol :: Pol) x.
FindTestSetup pol -> Rep (FindTestSetup pol) x
$cfrom :: forall (pol :: Pol) x.
FindTestSetup pol -> Rep (FindTestSetup pol) x
from :: forall x. FindTestSetup pol -> Rep (FindTestSetup pol) x
$cto :: forall (pol :: Pol) x.
Rep (FindTestSetup pol) x -> FindTestSetup pol
to :: forall x. Rep (FindTestSetup pol) x -> FindTestSetup pol
Generic, ReadPrec [FindTestSetup pol]
ReadPrec (FindTestSetup pol)
Int -> ReadS (FindTestSetup pol)
ReadS [FindTestSetup pol]
(Int -> ReadS (FindTestSetup pol))
-> ReadS [FindTestSetup pol]
-> ReadPrec (FindTestSetup pol)
-> ReadPrec [FindTestSetup pol]
-> Read (FindTestSetup pol)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall (pol :: Pol). TestPOL pol => ReadPrec [FindTestSetup pol]
forall (pol :: Pol). TestPOL pol => ReadPrec (FindTestSetup pol)
forall (pol :: Pol).
TestPOL pol =>
Int -> ReadS (FindTestSetup pol)
forall (pol :: Pol). TestPOL pol => ReadS [FindTestSetup pol]
$creadsPrec :: forall (pol :: Pol).
TestPOL pol =>
Int -> ReadS (FindTestSetup pol)
readsPrec :: Int -> ReadS (FindTestSetup pol)
$creadList :: forall (pol :: Pol). TestPOL pol => ReadS [FindTestSetup pol]
readList :: ReadS [FindTestSetup pol]
$creadPrec :: forall (pol :: Pol). TestPOL pol => ReadPrec (FindTestSetup pol)
readPrec :: ReadPrec (FindTestSetup pol)
$creadListPrec :: forall (pol :: Pol). TestPOL pol => ReadPrec [FindTestSetup pol]
readListPrec :: ReadPrec [FindTestSetup pol]
Read, Int -> FindTestSetup pol -> ShowS
[FindTestSetup pol] -> ShowS
FindTestSetup pol -> TestName
(Int -> FindTestSetup pol -> ShowS)
-> (FindTestSetup pol -> TestName)
-> ([FindTestSetup pol] -> ShowS)
-> Show (FindTestSetup pol)
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
forall (pol :: Pol).
TestPOL pol =>
Int -> FindTestSetup pol -> ShowS
forall (pol :: Pol). TestPOL pol => [FindTestSetup pol] -> ShowS
forall (pol :: Pol). TestPOL pol => FindTestSetup pol -> TestName
$cshowsPrec :: forall (pol :: Pol).
TestPOL pol =>
Int -> FindTestSetup pol -> ShowS
showsPrec :: Int -> FindTestSetup pol -> ShowS
$cshow :: forall (pol :: Pol). TestPOL pol => FindTestSetup pol -> TestName
show :: FindTestSetup pol -> TestName
$cshowList :: forall (pol :: Pol). TestPOL pol => [FindTestSetup pol] -> ShowS
showList :: [FindTestSetup pol] -> ShowS
Show)
instance QC.Arbitrary SomePol where
arbitrary :: Gen SomePol
arbitrary = do
inverted <- Gen Bool
forall a. Arbitrary a => Gen a
QC.arbitrary
if inverted then
pure $ SomePol (ProxyPol :: ProxyPol S.Inverted)
else
pure $ SomePol (ProxyPol :: ProxyPol S.NotInverted)
shrink :: SomePol -> [SomePol]
shrink = SomePol -> [SomePol]
forall a. a -> [a]
QC.shrinkNothing
instance QC.Arbitrary SomeFindTestSetup where
arbitrary :: Gen SomeFindTestSetup
arbitrary = do
SomePol (_ :: ProxyPol pol) <- Gen SomePol
forall a. Arbitrary a => Gen a
QC.arbitrary
SomeFindTestSetup <$> (QC.arbitrary :: QC.Gen (FindTestSetup pol))
shrink :: SomeFindTestSetup -> [SomeFindTestSetup]
shrink (SomeFindTestSetup FindTestSetup pol
x) = [ FindTestSetup pol -> SomeFindTestSetup
forall (pol :: Pol).
TestPOL pol =>
FindTestSetup pol -> SomeFindTestSetup
SomeFindTestSetup FindTestSetup pol
y | FindTestSetup pol
y <- FindTestSetup pol -> [FindTestSetup pol]
forall a. Arbitrary a => a -> [a]
QC.shrink FindTestSetup pol
x ]
instance TestPOL pol => QC.Arbitrary (FindTestSetup pol) where
arbitrary :: Gen (FindTestSetup pol)
arbitrary = do
let testPol :: ProxyPol pol
testPol = ProxyPol pol
forall (pol :: Pol). ProxyPol pol
ProxyPol :: ProxyPol pol
v <- [S] -> Vector S
forall a. Unbox a => [a] -> Vector a
V.fromList ([S] -> Vector S) -> Gen [S] -> Gen (Vector S)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen [S]
forall a. Arbitrary a => Gen a
QC.arbitrary
let tc = ProxyPol pol -> Vector S -> Int
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> Vector S -> Int
targetCount ProxyPol pol
testPol Vector S
v
i <- if 0 == tc then QC.discard else QC.choose (0, tc - 1)
pure FindTestSetup {
testPol
,
testIndex = C.Count i
,
testV = C.Vector v
}
shrink :: FindTestSetup pol -> [FindTestSetup pol]
shrink FindTestSetup pol
x =
[ FindTestSetup pol
y
| FindTestSetup pol
y <- FindTestSetup pol -> [FindTestSetup pol]
forall a.
(Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) =>
a -> [a]
QC.genericShrink FindTestSetup pol
x
, let FindTestSetup {Index TestB (PreImage pol 'EmptySlotE)
testIndex :: forall (pol :: Pol).
FindTestSetup pol -> Index TestB (PreImage pol 'EmptySlotE)
testIndex :: Index TestB (PreImage pol 'EmptySlotE)
testIndex, ProxyPol pol
testPol :: forall (pol :: Pol). FindTestSetup pol -> ProxyPol pol
testPol :: ProxyPol pol
testPol, Vector TestB 'SlotE S
testV :: forall (pol :: Pol). FindTestSetup pol -> Vector TestB 'SlotE S
testV :: Vector TestB 'SlotE S
testV} = FindTestSetup pol
y
, Index TestB (PreImage pol 'EmptySlotE) -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Index TestB (PreImage pol 'EmptySlotE)
testIndex Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ProxyPol pol -> Vector S -> Int
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> Vector S -> Int
targetCount ProxyPol pol
testPol (Vector TestB 'SlotE S -> Vector S
forall {k1} {k2} (base :: k1) (elem :: k2) a.
Vector base elem a -> Vector a
C.getVector Vector TestB 'SlotE S
testV)
]
targetCount :: TestPOL pol => proxy pol -> V.Vector S -> Int
targetCount :: forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> Vector S -> Int
targetCount proxy pol
pol = Vector S -> Int
forall a. Unbox a => Vector a -> Int
V.length (Vector S -> Int) -> (Vector S -> Vector S) -> Vector S -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S -> Bool) -> Vector S -> Vector S
forall a. Unbox a => (a -> Bool) -> Vector a -> Vector a
V.filter (Bool -> Bool
not (Bool -> Bool) -> (S -> Bool) -> S -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy pol -> S -> Bool
forall (pol :: Pol) (proxy :: Pol -> *).
POL pol =>
proxy pol -> S -> Bool
forall (proxy :: Pol -> *). proxy pol -> S -> Bool
S.test proxy pol
pol)
class POL pol => TestPOL (pol :: S.Pol) where showPol :: proxy pol -> String
instance TestPOL S.Inverted where showPol :: forall (proxy :: Pol -> *). proxy 'Inverted -> TestName
showPol proxy 'Inverted
_pol = TestName
"Inverted"
instance TestPOL S.NotInverted where showPol :: forall (proxy :: Pol -> *). proxy 'NotInverted -> TestName
showPol proxy 'NotInverted
_pol = TestName
"NotInverted"
prop_findIthEmptyInV :: SomeFindTestSetup -> QC.Property
prop_findIthEmptyInV :: SomeFindTestSetup -> Property
prop_findIthEmptyInV SomeFindTestSetup
testSetup = case SomeFindTestSetup
testSetup of
SomeFindTestSetup FindTestSetup {
Index TestB (PreImage pol 'EmptySlotE)
testIndex :: forall (pol :: Pol).
FindTestSetup pol -> Index TestB (PreImage pol 'EmptySlotE)
testIndex :: Index TestB (PreImage pol 'EmptySlotE)
testIndex
,
ProxyPol pol
testPol :: forall (pol :: Pol). FindTestSetup pol -> ProxyPol pol
testPol :: ProxyPol pol
testPol
,
Vector TestB 'SlotE S
testV :: forall (pol :: Pol). FindTestSetup pol -> Vector TestB 'SlotE S
testV :: Vector TestB 'SlotE S
testV
} -> case ProxyPol pol
-> Vector TestB 'SlotE S
-> Index TestB (PreImage pol 'EmptySlotE)
-> MaybeFound TestB
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S
-> Index base (PreImage pol 'EmptySlotE)
-> MaybeFound base
BV.findIthEmptyInV ProxyPol pol
testPol Vector TestB 'SlotE S
testV Index TestB (PreImage pol 'EmptySlotE)
testIndex of
MaybeFound TestB
BV.NothingFound -> TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"NothingFound" Bool
False
BV.JustFound Index TestB 'SlotE
i ->
Property -> Property
forall a. a -> a
id
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (ProxyPol pol -> TestName
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> TestName
forall (proxy :: Pol -> *). proxy pol -> TestName
showPol ProxyPol pol
testPol)
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample
(let C.Vector Vector S
v = Vector TestB 'SlotE S
testV
in
TestName
"v =" TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> (S -> Endo TestName) -> Vector S -> Endo TestName
forall m a. (Monoid m, Unbox a) => (a -> m) -> Vector a -> m
V.foldMap (ShowS -> Endo TestName
forall a. (a -> a) -> Endo a
Endo (ShowS -> Endo TestName) -> (S -> ShowS) -> S -> Endo TestName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. S -> ShowS
S.showS) Vector S
v Endo TestName -> ShowS
forall a. Endo a -> a -> a
`appEndo` TestName
""
)
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"i = " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Index TestB 'SlotE -> TestName
forall a. Show a => a -> TestName
show Index TestB 'SlotE
i)
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
( Property -> Property
forall a. a -> a
id
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"i isn't the position of a post-polarization-0 in w!"
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ ProxyPol pol -> Vector TestB 'SlotE S -> Index TestB 'SlotE -> Bool
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol -> Vector base 'SlotE S -> Index base 'SlotE -> Bool
BV.testV ProxyPol pol
testPol Vector TestB 'SlotE S
testV Index TestB 'SlotE
i Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Bool
False
)
Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&.
( let targetsInPrecedingWords :: Int
targetsInPrecedingWords =
ProxyPol pol -> Vector S -> Int
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> Vector S -> Int
targetCount ProxyPol pol
testPol (Vector S -> Int) -> Vector S -> Int
forall a b. (a -> b) -> a -> b
$ Int -> Vector S -> Vector S
forall a. Unbox a => Int -> Vector a -> Vector a
V.take (Index TestB 'SlotE -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Index TestB 'SlotE
i) (Vector S -> Vector S) -> Vector S -> Vector S
forall a b. (a -> b) -> a -> b
$ Vector TestB 'SlotE S -> Vector S
forall {k1} {k2} (base :: k1) (elem :: k2) a.
Vector base elem a -> Vector a
C.getVector Vector TestB 'SlotE S
testV
in
Property -> Property
forall a. a -> a
id
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"There are not testIndex-many post-polarization-0s preceding i!"
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Int
targetsInPrecedingWords Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Index TestB (PreImage pol 'EmptySlotE) -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Index TestB (PreImage pol 'EmptySlotE)
testIndex
)
data FillInWindowSetup =
FillInWindowSetup
SomePol
Int
Int
QCGen
(V.Vector S)
instance Show FillInWindowSetup where
showsPrec :: Int -> FillInWindowSetup -> ShowS
showsPrec Int
p (FillInWindowSetup SomePol
spol Int
k Int
szW QCGen
qcGen Vector S
v) =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ TestName -> ShowS
showString TestName
"FillInWindowSetup"
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
showString TestName
"\n pol = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomePol -> ShowS
forall a. Show a => a -> ShowS
shows SomePol
spol
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
showString TestName
"\n k = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Show a => a -> ShowS
shows Int
k
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
showString TestName
"\n qcGen = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QCGen -> ShowS
forall a. Show a => a -> ShowS
shows QCGen
qcGen
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
showString TestName
"\n szW = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Show a => a -> ShowS
shows Int
szW
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
showString TestName
"\n v = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
forall a. Show a => a -> ShowS
shows (Vector S -> TestName
showBitVector Vector S
v)
showBitVector :: V.Vector S -> String
showBitVector :: Vector S -> TestName
showBitVector Vector S
v =
Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
bvLen [ if Bool
b then Char
'1' else Char
'0' | S
s <- Vector S -> [S]
forall a. Unbox a => Vector a -> [a]
V.toList Vector S
v, let b :: Bool
b = Proxy 'NotInverted -> S -> Bool
forall (pol :: Pol) (proxy :: Pol -> *).
POL pol =>
proxy pol -> S -> Bool
forall (proxy :: Pol -> *). proxy 'NotInverted -> S -> Bool
S.test Proxy 'NotInverted
S.notInverted S
s ]
TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ if Int
szV Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
bvLen then TestName
"..." else TestName
""
where
szV :: Int
szV = Vector S -> Int
forall a. Unbox a => Vector a -> Int
V.length Vector S
v
bvLen :: Int
bvLen = Int
80
instance QC.Arbitrary FillInWindowSetup where
arbitrary :: Gen FillInWindowSetup
arbitrary = do
pol <- Gen SomePol
forall a. Arbitrary a => Gen a
QC.arbitrary
QC.NonNegative k <- QC.arbitrary
QC.NonNegative k1 <- QC.arbitrary
QC.NonNegative k2 <- QC.arbitrary
qcGen <- QC.arbitrary
let szV = Int
k1
szW = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
k Int
szV Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k2
ss <- QC.vectorOf szV QC.arbitrary
pure $ FillInWindowSetup pol k szW qcGen (V.fromList ss)
prop_fillInWindow :: FillInWindowSetup -> QC.Property
prop_fillInWindow :: FillInWindowSetup -> Property
prop_fillInWindow
(FillInWindowSetup
(SomePol ProxyPol pol
pol)
Int
k
Int
szW
QCGen
qcGen
Vector S
v
) = QCGen -> (forall s. STGenM QCGen s -> ST s Property) -> Property
forall g a.
RandomGen g =>
g -> (forall s. STGenM g s -> ST s a) -> a
R.runSTGen_ QCGen
qcGen ((forall s. STGenM QCGen s -> ST s Property) -> Property)
-> (forall s. STGenM QCGen s -> ST s Property) -> Property
forall a b. (a -> b) -> a -> b
$ \STGenM QCGen s
g -> do
vmv <- Vector S -> ST s (MVector (PrimState (ST s)) S)
forall a (m :: * -> *).
(Unbox a, PrimMonad m) =>
Vector a -> m (MVector (PrimState m) a)
V.thaw Vector S
v
let mv = MVector s S -> MVector Any 'SlotE s S
forall {k} {k1} (base :: k) (elem :: k1) s a.
MVector s a -> MVector base elem s a
C.MVector MVector s S
vmv
szV = Vector S -> Int
forall a. Unbox a => Vector a -> Int
V.length Vector S
v
actives0 <- C.getCount <$> BV.countActivesInMV pol mv
c <- C.getCount <$> BV.fillInWindow pol (BV.SomeDensityWindow (C.Count k) (C.Count szW)) g mv
actives1 <- C.getCount <$> BV.countActivesInMV pol mv
mvFrozen <- V.freeze vmv
pure $
QC.counterexample (showPol pol) $
QC.counterexample ("actives0 = " ++ show actives0) $
QC.counterexample ("actives1 = " ++ show actives1) $
QC.counterexample ("szV = " ++ show szV) $
QC.counterexample ("v = " ++ show (showBitVector mvFrozen)) $
(QC.counterexample "actives0 <= actives1" $ actives0 `QC.le` actives1)
QC..&&.
(QC.counterexample "c == actives1" $ c QC.=== actives1)
QC..&&.
(QC.counterexample "k <= actives1 + szW - szV" $ k `QC.le` actives1 + szW - szV)