{-# LANGUAGE DataKinds #-}

module Test.Ouroboros.Consensus.ChainGenerator.Tests.Counting (tests) where

import Data.Proxy (Proxy (Proxy))
import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C
import qualified Test.QuickCheck as QC
import qualified Test.Tasty as TT
import qualified Test.Tasty.QuickCheck as TT

-----

tests :: [TT.TestTree]
tests :: [TestTree]
tests =
  [ TestName -> (NonNegative Int -> Int -> Int -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TT.testProperty TestName
"prop_withWindow" NonNegative Int -> Int -> Int -> Property
prop_withWindow
  ]

-----

prop_withWindow :: QC.NonNegative Int -> Int -> Int -> QC.Property
prop_withWindow :: NonNegative Int -> Int -> Int -> Property
prop_withWindow (QC.NonNegative Int
n) Int
i Int
m =
  case Size (ZonkAny 3) (ZonkAny 2)
-> Lbl "test"
-> Index (ZonkAny 3) (ZonkAny 2)
-> Size (ZonkAny 0) (ZonkAny 2)
-> SomeWindow "test" (ZonkAny 3) (ZonkAny 2)
forall {kelem} {klbl} outer (elem :: kelem) (lbl :: klbl) x.
Size outer elem
-> Lbl lbl
-> Index outer elem
-> Size x elem
-> SomeWindow lbl outer elem
C.withWindow (Int -> Size (ZonkAny 3) (ZonkAny 2)
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
n) (Lbl "test"
forall {k} (lbl :: k). Lbl lbl
C.Lbl :: C.Lbl "test") (Int -> Index (ZonkAny 3) (ZonkAny 2)
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
i) (Int -> Size (ZonkAny 0) (ZonkAny 2)
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
m) of
    C.SomeWindow Proxy skolem
Proxy (C.Contains (C.Count Int
i') (C.Count Int
m')) ->
      TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample ((Int, Int) -> TestName
forall a. Show a => a -> TestName
show (Int
i', Int
m')) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        [Property] -> Property
forall prop. Testable prop => [prop] -> Property
QC.conjoin
          [ if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
              then TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"neg i" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Int
i' Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Int
0
              else
                if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n
                  then TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"too large i" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Int
i' Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Int
n
                  else TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"nonneg i" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Int
i' Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Int
i
          , if Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
              then TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"neg m" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Int
m' Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Int
0
              else TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"nonneg m" (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
i' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n
          ]