content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  {-# Language CPP #-}
  
  module Test.Fin
    ( finTests
    , genFin
    )
  where
  
  import           Numeric.Natural (Natural)
  
  import           Hedgehog
  import qualified Hedgehog.Gen as HG
  import           Hedgehog.Range (linear)
  import           Test.Tasty (TestTree, testGroup)
  import           Test.Tasty.Hedgehog (testPropertyNamed)
  import           Test.Tasty.HUnit (assertBool, testCase)
  
  import           Data.Parameterized.NatRepr
  import           Data.Parameterized.Fin
  import           Data.Parameterized.Some (Some(Some))
  
  #if __GLASGOW_HASKELL__ >= 806
  import qualified Hedgehog.Classes as HC
  #endif
  
  genNatRepr :: (Monad m) => Natural -> GenT m (Some NatRepr)
  genNatRepr bound =
    do x0 <- HG.integral (linear 0 bound)
       return (mkNatRepr x0)
  
  genFin :: (1 <= n, Monad m) => NatRepr n -> GenT m (Fin n)
  genFin n =
    do Some x <- genNatRepr (natValue n - 1 :: Natural)
       return $
         case testLeq (incNat x) n of
           Just LeqProof -> mkFin x
           Nothing -> error "Impossible"
  
  prop_count_true :: Property
  prop_count_true = property $
    do Some n <- forAll (genNatRepr 100)
       finToNat (countFin n (\_ _ -> True)) === natValue n
  
  prop_count_false :: Property
  prop_count_false = property $
    do Some n <- forAll (genNatRepr 100)
       finToNat (countFin n (\_ _ -> False)) === 0
  
  finTests :: IO TestTree
  finTests =
    testGroup "Fin" <$>
      return
        [ testCase "minBound <= maxBound (1)" $
            assertBool
              "minBound <= maxBound (1)"
              ((minBound :: Fin 1) <= (minBound :: Fin 1))
        , testCase "minBound <= maxBound (2)" $
            assertBool
              "minBound <= maxBound (2)"
              ((minBound :: Fin 2) <= (minBound :: Fin 2))
  
        , testPropertyNamed "count-true" "prop_count_true" prop_count_true
        , testPropertyNamed "count-false" "prop_count_false" prop_count_false
  
  #if __GLASGOW_HASKELL__ >= 806
        , testCase "Eq-Fin-laws-1" $
            assertBool "Eq-Fin-laws-1" =<<
              HC.lawsCheck (HC.eqLaws (genFin (knownNat @1)))
  
        , testCase "Ord-Fin-laws-1" $
            assertBool "Ord-Fin-laws-1" =<<
              HC.lawsCheck (HC.ordLaws (genFin (knownNat @1)))
  
        , testCase "Eq-Fin-laws-10" $
            assertBool "Eq-Fin-laws-10" =<<
              HC.lawsCheck (HC.eqLaws (genFin (knownNat @10)))
  
        , testCase "Ord-Fin-laws-10" $
            assertBool "Ord-Fin-laws-10" =<<
              HC.lawsCheck (HC.ordLaws (genFin (knownNat @10)))
  #endif
        ]
  