nat-sized-numbers 0.2.0.0 → 0.3.0.0
raw patch · 4 files changed
+528/−329 lines, 4 filesdep +deepseqdep +hedgehogdep −smallcheckdep ~QuickCheckdep ~basedep ~doctest
Dependencies added: deepseq, hedgehog
Dependencies removed: smallcheck
Dependency ranges changed: QuickCheck, base, doctest, nat-sized-numbers
Files
- nat-sized-numbers.cabal +8/−7
- src/Numeric/Sized/IntOfSize.hs +163/−62
- src/Numeric/Sized/WordOfSize.hs +180/−71
- test/Spec.hs +177/−189
nat-sized-numbers.cabal view
@@ -1,5 +1,5 @@ name: nat-sized-numbers-version: 0.2.0.0+version: 0.3.0.0 synopsis: Variable-sized numbers from type-level nats. description: Variable-sized numbers from type-level nats. homepage: https://github.com/oisdk/nat-sized-numbers#readme@@ -16,7 +16,8 @@ hs-source-dirs: src exposed-modules: Numeric.Sized.IntOfSize , Numeric.Sized.WordOfSize- build-depends: base >= 4.7 && < 5+ build-depends: base >=4.6 && <5+ , deepseq >=1.4 default-language: Haskell2010 ghc-options: -Wall @@ -24,11 +25,11 @@ type: exitcode-stdio-1.0 hs-source-dirs: test main-is: Spec.hs- build-depends: base- , nat-sized-numbers- , QuickCheck >= 2.8- , smallcheck >= 1.1- , doctest >= 0.11+ build-depends: base >= 4.6 && <5+ , nat-sized-numbers >=0.1.0.0+ , hedgehog >=0.1+ , QuickCheck >=1.0+ , doctest >=0.3.0 ghc-options: -threaded -rtsopts -with-rtsopts=-N default-language: Haskell2010
src/Numeric/Sized/IntOfSize.hs view
@@ -1,130 +1,231 @@+{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} --- | This module exports the 'IntOfSize' type and associated functions.+-- | This module exports integers with arbitrary sizes. module Numeric.Sized.IntOfSize (IntOfSize(..)+ ,KnownSize+ ,BoundingInt ,allIntsOfSize) where +import GHC.TypeLits+import Data.Int+import Control.DeepSeq import Data.Bits import Data.Coerce import Data.Function import Data.Proxy-import GHC.Generics-import GHC.TypeLits import Data.Ix -- $setup -- >>> :set -XDataKinds --- | An integer type with a size decided by a type-level nat. Numeric operations--- wraparound by default:+-- | The minimum size int type that will properly encapsulate an int+-- of a given size.+type family BoundingInt (n :: Nat) :: * where+ BoundingInt 0 = Int8+ BoundingInt 1 = Int8+ BoundingInt 2 = Int8+ BoundingInt 3 = Int8+ BoundingInt 4 = Int8+ BoundingInt 5 = Int8+ BoundingInt 6 = Int8+ BoundingInt 7 = Int8+ BoundingInt 8 = Int8+ BoundingInt 9 = Int16+ BoundingInt 10 = Int16+ BoundingInt 11 = Int16+ BoundingInt 12 = Int16+ BoundingInt 13 = Int16+ BoundingInt 14 = Int16+ BoundingInt 15 = Int16+ BoundingInt 16 = Int16+ BoundingInt 17 = Int32+ BoundingInt 18 = Int32+ BoundingInt 19 = Int32+ BoundingInt 20 = Int32+ BoundingInt 21 = Int32+ BoundingInt 22 = Int32+ BoundingInt 23 = Int32+ BoundingInt 24 = Int32+ BoundingInt 25 = Int32+ BoundingInt 26 = Int32+ BoundingInt 27 = Int32+ BoundingInt 28 = Int32+ BoundingInt 29 = Int32+ BoundingInt 30 = Int32+ BoundingInt 31 = Int32+ BoundingInt 32 = Int32+ BoundingInt 33 = Int64+ BoundingInt 34 = Int64+ BoundingInt 35 = Int64+ BoundingInt 36 = Int64+ BoundingInt 37 = Int64+ BoundingInt 38 = Int64+ BoundingInt 39 = Int64+ BoundingInt 40 = Int64+ BoundingInt 41 = Int64+ BoundingInt 42 = Int64+ BoundingInt 43 = Int64+ BoundingInt 44 = Int64+ BoundingInt 45 = Int64+ BoundingInt 46 = Int64+ BoundingInt 47 = Int64+ BoundingInt 48 = Int64+ BoundingInt 49 = Int64+ BoundingInt 50 = Int64+ BoundingInt 51 = Int64+ BoundingInt 52 = Int64+ BoundingInt 53 = Int64+ BoundingInt 54 = Int64+ BoundingInt 55 = Int64+ BoundingInt 56 = Int64+ BoundingInt 57 = Int64+ BoundingInt 58 = Int64+ BoundingInt 59 = Int64+ BoundingInt 60 = Int64+ BoundingInt 61 = Int64+ BoundingInt 62 = Int64+ BoundingInt 63 = Int64+ BoundingInt 64 = Int64+ BoundingInt n = Integer+++-- | A signed integer type with a size decided by a type-level nat. Numeric+-- operations wraparound by default: ----- >>> (127 :: IntOfSize 8) + 1--- -128+-- >>> (3 :: IntOfSize 3) + 1+-- -4+--+-- The type wrapped is the smallest word type which can contain the+-- desired word size. For instance, a @'IntOfSize' 8@ wraps a+-- @'Int8'@, whereas a @'IntOfSize' 9@ wraps a @'Int16'@.+--+-- Truncation to the correct size is performed as little as possible+-- while maintaining the correct semantics. This means that operations+-- should be as fast as those on the underlying type. newtype IntOfSize (n :: Nat) = IntOfSize- { getIntOfSize :: Integer- } deriving (Generic, Ix)+ { getIntOfSize :: BoundingInt n+ } -instance KnownNat n =>+type MaxBoundForSize n = (2 ^ (n - 1)) - 1++-- | In practice, every type-level `@Nat@` conforms to this+-- constraint; it is needed here to provide static information.+type KnownSize n+ = ( KnownNat ((2 ^ (n - 1)) - 1)+ , Integral (BoundingInt n)+ , Bits (BoundingInt n)+ , KnownNat n+ , Show (BoundingInt n)+ , Read (BoundingInt n))++instance KnownSize n => Bounded (IntOfSize n) where minBound = IntOfSize (shift (-1) (fromInteger (natVal (Proxy :: Proxy n) - 1)))- maxBound = IntOfSize (shift 1 (fromInteger (natVal (Proxy :: Proxy n) - 1)) - 1)+ maxBound = IntOfSize (fromInteger (natVal (Proxy :: Proxy (MaxBoundForSize n)))) type CoerceBinary a b = (a -> a -> a) -> (b -> b -> b) -instance KnownNat n =>- Bits (IntOfSize n) where- (.&.) = (coerce :: CoerceBinary Integer (IntOfSize n)) (.&.)- (.|.) = (coerce :: CoerceBinary Integer (IntOfSize n)) (.|.)- xor = trunc .: (coerce :: CoerceBinary Integer (IntOfSize n)) xor- complement =- trunc . (coerce :: (Integer -> Integer) -> IntOfSize n -> IntOfSize n) complement- shift =- trunc .:- (coerce :: (Integer -> Int -> Integer) -> IntOfSize n -> Int -> IntOfSize n)- shift- rotate =- trunc .:- (coerce :: (Integer -> Int -> Integer) -> IntOfSize n -> Int -> IntOfSize n)- rotate- bit = trunc . IntOfSize . bit- bitSize = fromInteger . natVal- bitSizeMaybe = Just . fromInteger . natVal- isSigned _ = True- testBit =- (coerce :: (Integer -> Int -> Bool) -> IntOfSize n -> Int -> Bool)- testBit- popCount =- (coerce :: (Integer -> Int) -> IntOfSize n -> Int) popCount- trunc- :: KnownNat n+ :: KnownSize n => IntOfSize n -> IntOfSize n trunc x- | testBit x (fromInteger (natVal x) - 1) = x .|. minBound- | otherwise = x .&. maxBound+ | testBit' x (fromInteger (natVal x) - 1) = x .|.. minBound+ | otherwise = x .&.. maxBound+ where+ (.&..) = (coerce :: CoerceBinary (BoundingInt n) (IntOfSize n)) (.&.)+ (.|..) = (coerce :: CoerceBinary (BoundingInt n) (IntOfSize n)) (.|.)+ testBit' =+ (coerce :: (BoundingInt n -> Int -> Bool) -> IntOfSize n -> Int -> Bool)+ testBit convBinary- :: KnownNat n- => CoerceBinary Integer (IntOfSize n)-convBinary f = trunc .: coerce f+ :: KnownSize n+ => CoerceBinary (BoundingInt n) (IntOfSize n)+convBinary f x y = trunc (coerce f x y) -instance KnownNat n =>+instance KnownSize n => Num (IntOfSize n) where+ {-# INLINE (+) #-} (+) = convBinary (+)+ {-# INLINE (*) #-} (*) = convBinary (*)- negate y = complement y + 1+ {-# INLINE negate #-}+ (-) = convBinary (-)+ {-# INLINE (-) #-}+ negate y = complement' y + 1 where+ complement' =+ trunc . (coerce :: (BoundingInt n -> BoundingInt n) -> IntOfSize n -> IntOfSize n) complement+ {-# INLINE fromInteger #-} fromInteger = trunc . IntOfSize . fromInteger- abs = id- signum (IntOfSize x) = IntOfSize (signum x)+ abs = trunc . coerce (abs :: BoundingInt n -> BoundingInt n) . trunc+ signum = coerce (signum :: BoundingInt n -> BoundingInt n) . trunc -instance KnownNat n =>+instance KnownSize n => Eq (IntOfSize n) where (==) = (==) `on` getIntOfSize . trunc -instance KnownNat n =>+instance KnownSize n => Ord (IntOfSize n) where compare = compare `on` getIntOfSize . trunc -instance KnownNat n =>+instance KnownSize n => Real (IntOfSize n) where toRational = toRational . getIntOfSize -instance KnownNat n =>+instance KnownSize n => Enum (IntOfSize n) where fromEnum = fromEnum . getIntOfSize toEnum = trunc . IntOfSize . toEnum enumFrom x = [x .. maxBound]+ enumFromThen x y+ | x < y = [x,y..maxBound]+ | otherwise = [x,y..minBound] -instance KnownNat n =>+instance KnownSize n => Integral (IntOfSize n) where toInteger = toInteger . getIntOfSize quotRem x y = (convBinary quot x y, convBinary rem x y)--(.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d-(.:) = (.) . (.)--instance KnownNat n =>- FiniteBits (IntOfSize n) where- finiteBitSize = fromInteger . natVal+ quot = convBinary quot+ rem = convBinary rem+ div = convBinary div+ mod = convBinary mod -- | Generate all values, in a sensible order -- -- >>> allIntsOfSize :: [IntOfSize 4] -- [0,-1,1,-2,2,-3,3,-4,4,-5,5,-6,6,-7,7,-8] allIntsOfSize- :: KnownNat n+ :: KnownSize n => [IntOfSize n] allIntsOfSize = f [0 .. maxBound ] (drop 1 [0,-1 .. minBound]) where f (x:xs) ys = x : f ys xs f [] ys = ys -instance KnownNat n =>+instance KnownSize n => Show (IntOfSize n) where showsPrec n = showsPrec n . getIntOfSize . trunc++instance KnownSize n =>+ Read (IntOfSize n) where+ readsPrec =+ (coerce :: (Int -> String -> [(BoundingInt n, String)]) -> Int -> String -> [(IntOfSize n, String)])+ readsPrec+ {-# INLINE readsPrec #-}++instance NFData (BoundingInt n) => NFData (IntOfSize n) where+ rnf (IntOfSize n) = rnf n++deriving instance (KnownSize n, Ix (BoundingInt n)) => Ix (IntOfSize n)
src/Numeric/Sized/WordOfSize.hs view
@@ -1,126 +1,235 @@+{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} --- | This module exports the 'WordOfSize' type and associated functions.+-- | Arbitrary sized unsigned integers and related functions. module Numeric.Sized.WordOfSize- (WordOfSize(..)- ,allWordsOfSize)- where+ ( WordOfSize(..)+ , BoundingWord+ , KnownSize+ , allWordsOfSize+ ) where +import Data.Word+import GHC.TypeLits+import Numeric.Natural+ import Data.Bits+ import Data.Coerce+ import Data.Function-import Data.Ix import Data.Proxy-import GHC.Generics-import GHC.TypeLits-import Numeric.Natural +import Control.DeepSeq+import Data.Ix+ -- $setup -- >>> :set -XDataKinds +-- | For a given size, the smallest type which encapsulates that size.+type family BoundingWord (n :: Nat) :: * where+ BoundingWord 0 = Word8+ BoundingWord 1 = Word8+ BoundingWord 2 = Word8+ BoundingWord 3 = Word8+ BoundingWord 4 = Word8+ BoundingWord 5 = Word8+ BoundingWord 6 = Word8+ BoundingWord 7 = Word8+ BoundingWord 8 = Word8+ BoundingWord 9 = Word16+ BoundingWord 10 = Word16+ BoundingWord 11 = Word16+ BoundingWord 12 = Word16+ BoundingWord 13 = Word16+ BoundingWord 14 = Word16+ BoundingWord 15 = Word16+ BoundingWord 16 = Word16+ BoundingWord 17 = Word32+ BoundingWord 18 = Word32+ BoundingWord 19 = Word32+ BoundingWord 20 = Word32+ BoundingWord 21 = Word32+ BoundingWord 22 = Word32+ BoundingWord 23 = Word32+ BoundingWord 24 = Word32+ BoundingWord 25 = Word32+ BoundingWord 26 = Word32+ BoundingWord 27 = Word32+ BoundingWord 28 = Word32+ BoundingWord 29 = Word32+ BoundingWord 30 = Word32+ BoundingWord 31 = Word32+ BoundingWord 32 = Word32+ BoundingWord 33 = Word64+ BoundingWord 34 = Word64+ BoundingWord 35 = Word64+ BoundingWord 36 = Word64+ BoundingWord 37 = Word64+ BoundingWord 38 = Word64+ BoundingWord 39 = Word64+ BoundingWord 40 = Word64+ BoundingWord 41 = Word64+ BoundingWord 42 = Word64+ BoundingWord 43 = Word64+ BoundingWord 44 = Word64+ BoundingWord 45 = Word64+ BoundingWord 46 = Word64+ BoundingWord 47 = Word64+ BoundingWord 48 = Word64+ BoundingWord 49 = Word64+ BoundingWord 50 = Word64+ BoundingWord 51 = Word64+ BoundingWord 52 = Word64+ BoundingWord 53 = Word64+ BoundingWord 54 = Word64+ BoundingWord 55 = Word64+ BoundingWord 56 = Word64+ BoundingWord 57 = Word64+ BoundingWord 58 = Word64+ BoundingWord 59 = Word64+ BoundingWord 60 = Word64+ BoundingWord 61 = Word64+ BoundingWord 62 = Word64+ BoundingWord 63 = Word64+ BoundingWord 64 = Word64+ BoundingWord n = Natural+ -- | An unsigned integer type with a size decided by a type-level nat. Numeric -- operations wraparound by default: ----- >>> (255 :: WordOfSize 8) + 1+-- >>> (7 :: WordOfSize 3) + 1 -- 0+--+-- The type wrapped is the smallest word type which can contain the+-- desired word size. For instance, a @'WordOfSize' 8@ wraps a+-- @'Word8'@, whereas a @'WordOfSize' 9@ wraps a @'Word16'@.+--+-- Truncation to the correct size is performed as little as possible+-- while maintaining the correct semantics. This means that operations+-- should be as fast as those on the underlying type. newtype WordOfSize (n :: Nat) = WordOfSize- { getWordOfSize :: Natural- } deriving (Generic, Ix)+ { getWordOfSize :: BoundingWord n+ } -instance KnownNat n =>+type MaxBoundForSize n = (2 ^ n) - 1++-- | In practice, every type-level `@Nat@` conforms to this+-- constraint; it is needed here to provide static information.+type KnownSize n+ = ( KnownNat ((2 ^ n) - 1)+ , Integral (BoundingWord n)+ , Bits (BoundingWord n)+ , KnownNat n+ , Show (BoundingWord n)+ , Read (BoundingWord n))++instance KnownSize n => Bounded (WordOfSize n) where minBound = WordOfSize 0- maxBound = WordOfSize (shift 1 (fromInteger (natVal (Proxy :: Proxy n))) - 1)+ {-# INLINE minBound #-}+ maxBound =+ WordOfSize (fromInteger (natVal (Proxy :: Proxy (MaxBoundForSize n)))) type CoerceBinary a b = (a -> a -> a) -> (b -> b -> b) -instance KnownNat n =>- Bits (WordOfSize n) where- (.&.) = (coerce :: CoerceBinary Natural (WordOfSize n)) (.&.)- (.|.) = (coerce :: CoerceBinary Natural (WordOfSize n)) (.|.)- xor = trunc .: (coerce :: CoerceBinary Natural (WordOfSize n)) xor- complement =- trunc . (coerce :: (Natural -> Natural) -> WordOfSize n -> WordOfSize n) complement- shift =- trunc .:- (coerce :: (Natural -> Int -> Natural) -> WordOfSize n -> Int -> WordOfSize n)- shift- rotate =- trunc .:- (coerce :: (Natural -> Int -> Natural) -> WordOfSize n -> Int -> WordOfSize n)- rotate- bit = trunc . WordOfSize . bit- bitSize = fromInteger . natVal- bitSizeMaybe = Just . fromInteger . natVal- isSigned _ = False- testBit =- (coerce :: (Natural -> Int -> Bool) -> WordOfSize n -> Int -> Bool)- testBit- popCount =- (coerce :: (Natural -> Int) -> WordOfSize n -> Int) popCount- trunc- :: KnownNat n+ :: KnownSize n => WordOfSize n -> WordOfSize n-trunc = (.&.) maxBound+trunc = convBinary (.&.) maxBound+{-# INLINE trunc #-} -convBinary- :: KnownNat n- => CoerceBinary Natural (WordOfSize n)-convBinary f = trunc .: coerce f+convBinary :: CoerceBinary (BoundingWord n) (WordOfSize n)+convBinary = coerce+{-# INLINE convBinary #-} -instance KnownNat n =>+instance KnownSize n => Num (WordOfSize n) where (+) = convBinary (+)+ {-# INLINE (+) #-} (*) = convBinary (*)- negate y = (maxBound `xor` y) + 1- fromInteger = trunc . WordOfSize . fromInteger+ {-# INLINE (*) #-}+ negate =+ succ .+ (coerce :: CoerceBinary (BoundingWord n) (WordOfSize n)) xor maxBound+ {-# INLINE negate #-}+ fromInteger = trunc . (WordOfSize #. fromInteger)+ {-# INLINE fromInteger #-} abs = id- signum (WordOfSize x) = WordOfSize (signum x)+ {-# INLINE abs #-}+ signum =+ (coerce :: (BoundingWord n -> BoundingWord n) -> WordOfSize n -> WordOfSize n)+ signum+ {-# INLINE signum #-} -instance KnownNat n =>+instance KnownSize n => Eq (WordOfSize n) where- (==) = (==) `on` getWordOfSize . trunc+ (==) = (==) `on` getWordOfSize #. trunc+ {-# INLINE (==) #-} -instance KnownNat n =>+instance KnownSize n => Show (WordOfSize n) where- showsPrec n = showsPrec n . getWordOfSize . trunc+ showsPrec n = showsPrec n . getWordOfSize #. trunc -instance KnownNat n =>+instance KnownSize n =>+ Read (WordOfSize n) where+ readsPrec =+ (coerce :: (Int -> String -> [(BoundingWord n, String)]) -> Int -> String -> [(WordOfSize n, String)])+ readsPrec+ {-# INLINE readsPrec #-}++instance KnownSize n => Ord (WordOfSize n) where- compare = compare `on` getWordOfSize . trunc+ compare = compare `on` getWordOfSize #. trunc -instance KnownNat n =>+instance KnownSize n => Real (WordOfSize n) where- toRational = toRational . getWordOfSize+ toRational = toRational . getWordOfSize #. trunc -instance KnownNat n =>+instance KnownSize n => Enum (WordOfSize n) where- fromEnum = fromEnum . getWordOfSize+ fromEnum = fromEnum . getWordOfSize #. trunc toEnum = trunc . WordOfSize . toEnum enumFrom x = [x .. maxBound]+ enumFromThen x y+ | x < y = [x,y..maxBound]+ | otherwise = [x,y..minBound] -instance KnownNat n =>+instance KnownSize n => Integral (WordOfSize n) where- toInteger = toInteger . getWordOfSize+ toInteger = toInteger . getWordOfSize #. trunc+ {-# INLINE toInteger #-} quotRem x y = (convBinary quot x y, convBinary rem x y)--(.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d-(.:) = (.) . (.)--instance KnownNat n =>- FiniteBits (WordOfSize n) where- finiteBitSize = fromInteger . natVal+ {-# INLINE quotRem #-}+ quot = convBinary quot+ {-# INLINE quot #-}+ rem = convBinary rem+ {-# INLINE rem #-} -- | Generates all words of a given size ----- >>> allWordOfSize :: [WordOfSize 3]+-- >>> allWordsOfSize :: [WordOfSize 3] -- [0,1,2,3,4,5,6,7] allWordsOfSize- :: KnownNat n+ :: KnownSize n => [WordOfSize n] allWordsOfSize = [minBound .. maxBound]++instance NFData (BoundingWord n) => NFData (WordOfSize n) where+ rnf (WordOfSize n) = rnf n++deriving instance (KnownSize n, Ix (BoundingWord n)) => Ix (WordOfSize n)++infixr 9 #.+(#.) :: Coercible b c => (b -> c) -> (a -> b) -> a -> c+(#.) _ = coerce+{-# INLINE (#.) #-}
test/Spec.hs view
@@ -1,214 +1,202 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeFamilies #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ScopedTypeVariables #-} -module Main- (main)- where+import Hedgehog+import qualified Hedgehog.Gen as Gen+import qualified Hedgehog.Range as Range+import Test.DocTest -import Data.Function-import Data.Int-import Data.Proxy-import Data.Word-import GHC.TypeLits-import Numeric.Natural-import Numeric.Sized.IntOfSize import Numeric.Sized.WordOfSize-import Test.DocTest-import Test.QuickCheck hiding (generate)-import qualified Test.SmallCheck as SmallCheck-import Test.SmallCheck.Series+import Numeric.Sized.IntOfSize -instance KnownNat n =>- Arbitrary (IntOfSize n) where- arbitrary = arbitraryBoundedEnum+import Control.Monad -instance KnownNat n =>- Arbitrary (WordOfSize n) where- arbitrary = arbitraryBoundedEnum+import Data.Data -instance (KnownNat n, Monad m) =>- Serial m (IntOfSize n) where- series = generate (`take` allIntsOfSize)+default () -instance (KnownNat n, Monad m) =>- Serial m (WordOfSize n) where- series = generate (`take` allWordsOfSize)+binaryProp+ :: forall a.+ Integral a+ => (forall t. Integral t => t -> t -> t)+ -> Integer+ -> Integer+ -> (Integer -> Integer -> Bool)+ -> Property+binaryProp op lb ub cond = property $ do+ x <- forAll (Gen.integral (Range.linear lb ub))+ y <- forAll (Gen.integral (Range.linear lb ub))+ guard (cond x y)+ let zb = op x y+ let zt = op (fromInteger x :: a) (fromInteger y)+ zb === toInteger zt -type family IntType (n :: Nat) :: * where- IntType 8 = Int8- IntType 16 = Int16- IntType 32 = Int32- IntType 64 = Int64+ordProps+ :: forall a.+ (Ord a, Show a, Typeable a)+ => Gen IO a+ -> Property+ordProps xs = property $ do+ x <- forAll xs+ info "reflexive"+ x === x+ info "irreflexive"+ assert (not (x < x))+ y <- forAll xs+ info "Ord functions behave same as default implementations"+ case compare x y of+ LT -> do+ assert (x < y)+ assert (x /= y)+ assert (not (x == y))+ assert (x <= y)+ assert (not (x >= y)) -type family WordType (n :: Nat) :: * where- WordType 8 = Word8- WordType 16 = Word16- WordType 32 = Word32- WordType 64 = Word64+ info "antisymmetric"+ assert (y > x)+ info "irreflexive"+ assert (not (x > y))+ info "transitive"+ z <- forAll xs+ when (z > y) (assert (z > x))+ EQ -> do+ assert (x == y)+ assert (not (x /= y))+ assert (not (x < y))+ assert (not (x > y))+ assert (x <= y)+ assert (x >= y) -sameConvAs- :: (Integral n, Integral m, Integral i, Show i)- => Proxy n -> Proxy m -> i -> Property-sameConvAs (_ :: Proxy n) (_ :: Proxy m) (x :: i) =- ((fromIntegral :: n -> i) . (fromIntegral :: i -> n)) x ===- ((fromIntegral :: m -> i) . (fromIntegral :: i -> m)) x+ info "symmetric"+ assert (y == x)+ info "transitive"+ z <- forAll xs+ assert $ (x == z) == (y == z)+ GT -> do+ assert (x > y)+ assert (x /= y)+ assert (not (x == y))+ assert (x >= y)+ assert (not (x <= y)) -sameConvI- :: (KnownNat n, Integral (IntType n))- => Proxy n -> Integer -> Property-sameConvI (_ :: Proxy n) =- sameConvAs (Proxy :: Proxy (IntOfSize n)) (Proxy :: Proxy (IntType n))+ info "irreflexive"+ assert (not (x < y))+ info "antisymmetric"+ assert (y < x)+ info "transitive"+ z <- forAll xs+ when (z < y) (assert (z < x)) -sameConvW- :: (KnownNat n, Integral (WordType n))- => Proxy n -> Natural -> Property-sameConvW (_ :: Proxy n) =- sameConvAs (Proxy :: Proxy (WordOfSize n)) (Proxy :: Proxy (WordType n))+holdsForLength :: Foldable f => (a -> Bool) -> f a -> Int+holdsForLength p = flip (foldr f id ) 0 where+ f e a i | p e = a (i + 1)+ | otherwise = i -sameFncAs- :: (Integral n, Integral m, Integral i, Show i)- => (forall a. Integral a =>- a -> a -> a)- -> Proxy n- -> Proxy m- -> i- -> i- -> Property-sameFncAs f (_ :: Proxy n) (_ :: Proxy m) (x :: i) (y :: i) =- (fromIntegral :: n -> i) ((f `on` (fromIntegral :: i -> n)) x y) ===- (fromIntegral :: m -> i) ((f `on` (fromIntegral :: i -> m)) x y)+enumProps+ :: forall a.+ (Enum a, Show a, Typeable a, Ord a)+ => (Int -> Bool) -> Gen IO Int -> Gen IO a -> Property+enumProps p ig eg = property $ do+ x <- forAll ig+ info "from . to"+ (fromEnum . toEnum @a) x === x+ info "to . from"+ n <- forAll eg+ (toEnum . fromEnum) n === n+ info "[n..]"+ let lhs1 = take 100 $ map fromEnum [n..]+ rhs1 = take 100 $ [fromEnum n..]+ len1 = min (holdsForLength p lhs1) (holdsForLength p rhs1)+ take len1 lhs1 === take len1 rhs1+ info "[n,m..]"+ m <- forAll eg+ let lhs2 = take 100 $ map fromEnum [n,m..]+ rhs2 = take 100 $ [fromEnum n, fromEnum m..]+ len2 = min (holdsForLength p lhs2) (holdsForLength p rhs2)+ take len2 lhs2 === take len2 rhs2+ when (m >= n) $ do+ info "[n..m]"+ map fromEnum [n..m] === [fromEnum n..fromEnum m]+ l <- forAll eg+ when (((l > n) == (n > m)) && (l /= n)) $ do+ info "[l,n..m]"+ map fromEnum [l,n..m] === [fromEnum l, fromEnum n..fromEnum m] -sameFncI, sameFncINZRhs- :: (KnownNat n, Integral (IntType n))- => (forall a. Integral a =>- a -> a -> a)- -> Proxy n- -> Integer- -> Integer- -> Property-sameFncI f (_ :: Proxy n) =- sameFncAs f (Proxy :: Proxy (IntOfSize n)) (Proxy :: Proxy (IntType n)) -sameFncINZRhs f n x y = y /= 0 ==> sameFncI f n x y+prop_Word3Add :: Property+prop_Word3Add = binaryProp @(WordOfSize 3) (+) 0 7 (\x y -> x + y <= 7) -sameFncW, sameFncWNZRhs- :: (KnownNat n, Integral (WordType n))- => (forall a. Integral a =>- a -> a -> a)- -> Proxy n- -> Natural- -> Natural- -> Property-sameFncW f (_ :: Proxy n) =- sameFncAs f (Proxy :: Proxy (WordOfSize n)) (Proxy :: Proxy (WordType n))+prop_Word3Mul :: Property+prop_Word3Mul = binaryProp @(WordOfSize 3) (*) 0 7 (\x y -> x * y <= 7) -sameFncWNZRhs f n x y = y /= 0 ==> sameFncW f n x y+prop_Word3Sub :: Property+prop_Word3Sub = withDiscards 1000 $ binaryProp @(WordOfSize 3) (-) 0 7 (>=) -sameFncAsS- :: (Integral n, Integral m, Show n)- => (forall a. Integral a =>- a -> a -> a)- -> Proxy n- -> Proxy m- -> n- -> n- -> Either String String-sameFncAsS f (_ :: Proxy n) (_ :: Proxy m) x y =- if (fromIntegral :: n -> m) (f x y) ==- (f `on` (fromIntegral :: n -> m)) x y- then Right ""- else Left (show x ++ " " ++ show y)+prop_Word3Rem :: Property+prop_Word3Rem = binaryProp @(WordOfSize 3) rem 0 7 (\_ y -> y > 0) -sameFncWS- :: (KnownNat n, Integral (WordType n))- => (forall a. Integral a =>- a -> a -> a)- -> Proxy n- -> WordOfSize n- -> WordOfSize n- -> Either String String-sameFncWS f (_ :: Proxy n) =- sameFncAsS f (Proxy :: Proxy (WordOfSize n)) (Proxy :: Proxy (WordType n))+prop_Word3Quot :: Property+prop_Word3Quot = binaryProp @(WordOfSize 3) quot 0 7 (\_ y -> y > 0) -sameFncWNZRhsS- :: (KnownNat n, Integral (WordType n), Monad m)- => (forall a. Integral a =>- a -> a -> a)- -> Proxy n- -> WordOfSize n- -> WordOfSize n- -> SmallCheck.Property m-sameFncWNZRhsS f n x y = y /= 0 SmallCheck.==> sameFncWS f n x y+prop_Word3Ord :: Property+prop_Word3Ord = ordProps (Gen.integral (Range.linear @(WordOfSize 3) 0 7)) -sameFncIS- :: (KnownNat n, Integral (IntType n))- => (forall a. Integral a =>- a -> a -> a)- -> Proxy n- -> IntOfSize n- -> IntOfSize n- -> Either String String-sameFncIS f (_ :: Proxy n) =- sameFncAsS f (Proxy :: Proxy (IntOfSize n)) (Proxy :: Proxy (IntType n))+prop_Word3Enum :: Property+prop_Word3Enum =+ enumProps+ (inBounds 0 7)+ (Gen.integral (Range.linear 0 7))+ (Gen.integral (Range.linear @(WordOfSize 3) 0 7)) -sameFncINZRhsS- :: (KnownNat n, Integral (IntType n), Monad m, Bounded (IntOfSize n))- => (forall a. Integral a =>- a -> a -> a)- -> Proxy n- -> IntOfSize n- -> IntOfSize n- -> SmallCheck.Property m-sameFncINZRhsS f n x y =- y /= 0 && (x /= minBound || y /= -1) SmallCheck.==> sameFncIS f n x y+inBounds :: Ord a => a -> a -> a -> Bool+inBounds lb ub x = x >= lb && x <= ub -testAll- :: Testable a- => (forall n. (KnownNat n, Integral (WordType n), Integral (IntType n)) =>- Proxy n -> a)- -> IO ()-testAll prop = do- quickCheck (prop (Proxy :: Proxy 8))- quickCheck (prop (Proxy :: Proxy 16))- quickCheck (prop (Proxy :: Proxy 32))- quickCheck (prop (Proxy :: Proxy 64))+prop_Int3Add :: Property+prop_Int3Add =+ withDiscards 1000 $+ binaryProp+ @(IntOfSize 3)+ (+)+ (-4)+ 3+ (\x y ->+ inBounds (-4) 3 (x + y)) -main :: IO ()+prop_Int3Mul :: Property+prop_Int3Mul =+ withDiscards 1000 $+ binaryProp+ @(IntOfSize 3)+ (*)+ (-4)+ 3+ (\x y ->+ inBounds (-4) 3 (x * y))++prop_Int3Sub :: Property+prop_Int3Sub = binaryProp @(IntOfSize 3) (-) (-4) 3 (\x y -> inBounds (-4) 3 (x - y))++prop_Int3Rem :: Property+prop_Int3Rem = binaryProp @(IntOfSize 3) rem (-4) 3 (\_ y -> y /= 0)++prop_Int3Quot :: Property+prop_Int3Quot = binaryProp @(IntOfSize 3) quot (-4) 3 (\x y -> y /= 0 && inBounds (-4) 3 (quot x y))++prop_Int3Ord :: Property+prop_Int3Ord = ordProps (Gen.integral (Range.linear @(IntOfSize 3) (-3) 4))++prop_Int3Enum :: Property+prop_Int3Enum =+ enumProps+ (inBounds (-4) 3)+ (Gen.integral (Range.linear (-4) 3))+ (Gen.integral (Range.linear @(IntOfSize 3) (-4) 3))++main :: IO Bool main = do- testAll sameConvI- testAll sameConvW- testAll (sameFncI (+))- testAll (sameFncW (+))- testAll (sameFncI (*))- testAll (sameFncW (*))- testAll (sameFncI (-))- testAll (sameFncW (-))- testAll (sameFncINZRhs div)- testAll (sameFncWNZRhs div)- testAll (sameFncINZRhs mod)- testAll (sameFncWNZRhs mod)- testAll (sameFncINZRhs rem)- testAll (sameFncWNZRhs rem)- testAll (sameFncINZRhs quot)- testAll (sameFncWNZRhs quot)- SmallCheck.smallCheck 100000 (sameFncWS (+) (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncIS (+) (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncWS (*) (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncIS (*) (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncWS (-) (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncIS (-) (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncWNZRhsS div (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncINZRhsS div (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncWNZRhsS mod (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncINZRhsS mod (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncWNZRhsS rem (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncINZRhsS rem (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncWNZRhsS quot (Proxy :: Proxy 8))- SmallCheck.smallCheck 100000 (sameFncINZRhsS quot (Proxy :: Proxy 8))- doctest ["-isrc", "src/"]+ doctest ["-isrc","src/"]+ $$(checkConcurrent)