{-# 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 Test.Ouroboros.Consensus.ChainGenerator.Slot
( E (EmptySlotE, SlotE)
, POL
, PreImage
, S
)
import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as 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 (ZonkAny 0) '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)