{-# 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
  ,
    -- | INVARIANT @'testIndex' < V.sum (V.map ('countZeros' 'testPol') 'testV')@
    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"

-- | Check that when @findIthEmptyInV pol bv i@ yields 'JustFound'
--
-- 1. it yields the index of an inactive slot
-- 2. there are exactly @i@ inactive slots in the preceding slots
--
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 -- ^ k
      Int -- ^ size of the window to fill
      QCGen -- ^ random generator
      (V.Vector S) -- ^ the vector to fill

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 -- k <= szW && szV <= szW
      ss <- QC.vectorOf szV QC.arbitrary
      pure $ FillInWindowSetup pol k szW qcGen (V.fromList ss)

-- | Check that 'fillInWindow'
--
-- 1. does not decrease the count of active slots in the given window
-- 2. returns exactly the amount of activated slots
-- 3. never leaves less than the requested amount of slots in the given
--    window
--
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)