diff --git a/nat-sized-numbers.cabal b/nat-sized-numbers.cabal --- a/nat-sized-numbers.cabal +++ b/nat-sized-numbers.cabal @@ -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 diff --git a/src/Numeric/Sized/IntOfSize.hs b/src/Numeric/Sized/IntOfSize.hs --- a/src/Numeric/Sized/IntOfSize.hs +++ b/src/Numeric/Sized/IntOfSize.hs @@ -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) diff --git a/src/Numeric/Sized/WordOfSize.hs b/src/Numeric/Sized/WordOfSize.hs --- a/src/Numeric/Sized/WordOfSize.hs +++ b/src/Numeric/Sized/WordOfSize.hs @@ -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 (#.) #-} diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -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)