{-# 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)
  -- ^ INVARIANT @'testIndex' < V.sum (V.map ('countZeros' 'testPol') 'testV')@
  , 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
      -- | k
      Int
      -- | size of the window to fill
      Int
      -- | random generator
      QCGen
      -- | the vector to fill
      (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 -- 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 (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)