{-# 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 Any Any
-> Lbl "test"
-> Index Any Any
-> Size Any Any
-> SomeWindow "test" Any Any
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 Any Any
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 Any Any
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
i) (Int -> Size Any Any
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
              ]