-- SPDX-FileCopyrightText: 2022 Gregor Kleen <gregor.kleen@ifi.lmu.de>
--
-- SPDX-License-Identifier: AGPL-3.0-or-later

module Test.QuickCheck.Classes.Universe
  ( universeLaws
  , finiteLaws
  ) where

import ClassyPrelude
import Test.QuickCheck
import Test.QuickCheck.Classes
import Data.Proxy
import Data.Universe
import Data.List (genericLength, elemIndices)

universeLaws :: forall a. (Arbitrary a, Universe a, Eq a, Show a) => Proxy a -> Laws
universeLaws _ = Laws "Universe"
  [ ("universe contains everything", property $ \(a :: a) -> a `elem` universe)
  ]

finiteLaws :: forall a. (Arbitrary a, Finite a, Eq a, Show a) => Proxy a -> Laws
finiteLaws _ = Laws "Finite" $
  [ ("universeF is small", property $ genericLength (universeF :: [a]) <= toInteger (maxBound :: Word32))
  , ("universeF contains everything once", property $ \(a :: a) -> length (elemIndices a universeF) == 1)
  , ("universe is permutation of universeF", property $ all (\(a :: a) -> length (elemIndices a universeF) == 1) universeF)
  ]