{- - Copyright (C) 2019 Koz Ross - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program. If not, see . -} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeInType #-} module Main where -- base import Data.Kind (Type) import Data.Word (Word8, Word16, Word64) import Foreign.Storable (Storable) import GHC.Exts (proxy#) import GHC.Generics (Generic) import GHC.TypeNats (Nat, KnownNat, natVal') -- binary import Data.Binary (Binary) -- deepseq import Control.DeepSeq (NFData) -- finitary import Data.Finitary (Finitary(..)) -- finitary-derive import Data.Finitary.Finiteness (Finiteness(..)) import Data.Finitary.PackBytes (PackBytes) import Data.Finitary.PackWords (PackWords) import Data.Finitary.PackInto (PackInto) import qualified Data.Finitary.PackBits as Safe import qualified Data.Finitary.PackBits.Unsafe as Unsafe import qualified Data.Finitary.PackBytes as PackBytes import qualified Data.Finitary.PackWords as PackWords -- finite-typelits import Data.Finite (Finite) -- hashable import Data.Hashable (Hashable(..)) -- hedgehog import Hedgehog import qualified Hedgehog.Gen as G import qualified Hedgehog.Range as R -- hedgehog-classes import Hedgehog.Classes -- vector import Data.Vector.Unboxed (Unbox) -------------------------------------------------------------------------------- data Foo = Bar | Baz Word8 Word16 | Quux Word16 deriving (Eq, Show, Generic, Finitary) deriving (Ord, Bounded, NFData, Hashable, Binary) via (Finiteness Foo) data Big = Big Word64 Word64 | Mediums Foo Foo Foo Foo deriving (Eq, Show, Generic, Finitary) deriving (Ord, Bounded, NFData, Hashable, Binary) via (Finiteness Big) genFoo :: MonadGen m => m Foo genFoo = do c <- G.element @_ @Word [ 0, 1, 2 ] case c of 0 -> pure Bar 1 -> do w1 <- G.word8 (R.linear 0 maxBound) w2 <- G.word16 (R.linear 0 maxBound) pure ( Baz w1 w2 ) _ -> do w1 <- G.word16 (R.linear 0 maxBound) pure ( Quux w1 ) genBig :: MonadGen m => m Big genBig = do c <- G.element @_ @Word [ 0, 1 ] case c of 0 -> do w1 <- G.word64 (R.linear 0 maxBound) w2 <- G.word64 (R.linear 0 maxBound) pure ( Big w1 w2 ) _ -> do foo1 <- genFoo foo2 <- genFoo foo3 <- genFoo foo4 <- genFoo pure ( Mediums foo1 foo2 foo3 foo4 ) -- Generators choose :: forall (a :: Type) m . (MonadGen m, Finitary a) => m a choose = fromFinite <$> chooseFinite chooseFinite :: forall (n :: Nat) m . (KnownNat n, MonadGen m) => m (Finite n) chooseFinite = fromIntegral <$> G.integral (R.linear 0 limit) where limit = subtract @Integer 1 . fromIntegral $ natVal' @n proxy# finitenessLaws :: (Show a, Binary a, Ord a) => Gen a -> [Laws] finitenessLaws p = [binaryLaws p, ordLaws p] packLaws :: (Eq a, Show a, Storable a) => Gen a -> [Laws] packLaws p = [storableLaws p] vectorLaws :: (Eq a, Show a, Unbox a) => Gen a -> [Laws] vectorLaws p = [muvectorLaws p] ordIsMonotonic :: forall (a :: Type) (t :: Type -> Type) . (Finitary a, Show a, Ord a, Ord (t a)) => (a -> t a) -> Property ordIsMonotonic f = property $ do x <- forAll $ choose @a y <- forAll $ choose @a (x < y) === (f x < f y) roundTrips :: forall (a :: Type) (t :: Type -> Type) . (Finitary a, Show a, Ord a) => Gen a -> (a -> t a) -> (t a -> a) -> Property roundTrips gen pack unpack = property $ do a <- forAll $ gen case pack a of !packed -> case unpack packed of roundTripped -> a === roundTripped finitenessTests :: [(String,[Laws])] finitenessTests = [ ("Small Finiteness", finitenessLaws @Foo choose) , ("Big Finiteness" , finitenessLaws @Big choose) ] packTests :: [(String,[Laws])] packTests = [ ("Small PackBytes" , packLaws @(PackBytes Foo) choose) , ("Big PackBytes" , packLaws @(PackBytes Big) choose) , ("Small PackWords" , packLaws @(PackWords Foo) choose) , ("Big PackWords" , packLaws @(PackWords Big) choose) , ("Small packed into Word64", packLaws @(PackInto Foo Word64) choose) ] vectorTests :: [(String,[Laws])] vectorTests = [ ("Small PackBits" , vectorLaws @(Safe.PackBits Foo) choose) , ("Small unsafe PackBits", vectorLaws @(Unsafe.PackBits Foo) choose) , ("Small PackBytes" , vectorLaws @(PackBytes Foo) choose) , ("Small PackWords" , vectorLaws @(PackWords Foo) choose) , ("Big PackBits" , vectorLaws @(Safe.PackBits Big) choose) , ("Big unsafe PackBits" , vectorLaws @(Unsafe.PackBits Big) choose) , ("Big PackBytes" , vectorLaws @(PackBytes Big) choose) , ("Big PackWords" , vectorLaws @(PackWords Big) choose) ] monotonicTests :: Group monotonicTests = Group "Monotonicity" [ ("Small PackBits" , ordIsMonotonic @Foo Safe.Packed) , ("Small unsafe PackBits", ordIsMonotonic @Foo Unsafe.Packed) , ("Small PackBytes" , ordIsMonotonic @Foo PackBytes.Packed) , ("Small PackWords" , ordIsMonotonic @Foo PackWords.Packed) , ("Big PackBits" , ordIsMonotonic @Big Safe.Packed) , ("Big unsafe PackBits" , ordIsMonotonic @Big Unsafe.Packed) , ("Big PackBytes" , ordIsMonotonic @Big PackBytes.Packed) , ("Big PackWords" , ordIsMonotonic @Big PackWords.Packed) ] roundTripTests :: Group roundTripTests = Group "Round-tripping" [ ("Small PackBits" , roundTrips @Foo genFoo Safe.Packed ( \ ( Safe.Packed x ) -> x ) ) , ("Small unsafe PackBits", roundTrips @Foo genFoo Unsafe.Packed ( \ ( Unsafe.Packed x ) -> x ) ) , ("Small PackBytes" , roundTrips @Foo genFoo PackBytes.Packed ( \ ( PackBytes.Packed x ) -> x ) ) , ("Small PackWords" , roundTrips @Foo genFoo PackWords.Packed ( \ ( PackWords.Packed x ) -> x ) ) , ("Big PackBits" , roundTrips @Big genBig Safe.Packed ( \ ( Safe.Packed x ) -> x ) ) , ("Big unsafe PackBits" , roundTrips @Big genBig Unsafe.Packed ( \ ( Unsafe.Packed x ) -> x ) ) , ("Big PackBytes" , roundTrips @Big genBig PackBytes.Packed ( \ ( PackBytes.Packed x ) -> x ) ) , ("Big PackWords" , roundTrips @Big genBig PackWords.Packed ( \ ( PackWords.Packed x ) -> x ) ) ] checkTest :: Either [(String,[Laws])] Group -> IO Bool checkTest ( Left laws ) = lawsCheckMany laws checkTest ( Right group ) = checkParallel group main :: IO Bool main = and <$> traverse checkTest [ Left finitenessTests, Left packTests, Left vectorTests, Right monotonicTests, Right roundTripTests ]