diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2017 Donnacha Oisín Kidney + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/nat-sized-numbers.cabal b/nat-sized-numbers.cabal new file mode 100644 --- /dev/null +++ b/nat-sized-numbers.cabal @@ -0,0 +1,37 @@ +name: nat-sized-numbers +version: 0.1.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 +license: MIT +license-file: LICENSE +author: Donnacha Oisín Kidney +maintainer: mail@doisinkidney.com +copyright: 2016 Donnacha Oisín Kidney +category: Numeric +build-type: Simple +cabal-version: >=1.10 + +library + hs-source-dirs: src + exposed-modules: Numeric.Sized.IntOfSize + , Numeric.Sized.WordOfSize + build-depends: base >= 4.7 && < 5 + default-language: Haskell2010 + ghc-options: -Wall + +test-suite nat-sized-numbers-test + 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 + ghc-options: -threaded -rtsopts -with-rtsopts=-N + default-language: Haskell2010 + +source-repository head + type: git + location: https://github.com/oisdk/nat-sized-numbers diff --git a/src/Numeric/Sized/IntOfSize.hs b/src/Numeric/Sized/IntOfSize.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Sized/IntOfSize.hs @@ -0,0 +1,128 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | This module exports the 'IntOfSize' type and associated functions. +module Numeric.Sized.IntOfSize + (IntOfSize(..) + ,allIntsOfSize) + where + +import Data.Bits +import Data.Coerce +import Data.Function +import Data.Proxy +import GHC.Generics +import GHC.TypeLits + +-- $setup +-- >>> :set -XDataKinds + +-- | An integer type with a size decided by a type-level nat. Numeric operations +-- wraparound by default: +-- +-- >>> (127 :: IntOfSize 8) + 1 +-- -128 +newtype IntOfSize (n :: Nat) = IntOfSize + { getIntOfSize :: Integer + } deriving (Generic) + +instance KnownNat 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) + +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 + => IntOfSize n -> IntOfSize n +trunc x + | testBit x (fromInteger (natVal x) - 1) = x .|. minBound + | otherwise = x .&. maxBound + +convBinary + :: KnownNat n + => CoerceBinary Integer (IntOfSize n) +convBinary f = trunc .: coerce f + +instance KnownNat n => + Num (IntOfSize n) where + (+) = convBinary (+) + (*) = convBinary (*) + negate y = complement y + 1 + fromInteger = trunc . IntOfSize . fromInteger + abs = id + signum (IntOfSize x) = IntOfSize (signum x) + +instance KnownNat n => + Eq (IntOfSize n) where + (==) = (==) `on` getIntOfSize . trunc + +instance KnownNat n => + Ord (IntOfSize n) where + compare = compare `on` getIntOfSize . trunc + +instance KnownNat n => + Real (IntOfSize n) where + toRational = toRational . getIntOfSize + +instance KnownNat n => + Enum (IntOfSize n) where + fromEnum = fromEnum . getIntOfSize + toEnum = trunc . IntOfSize . toEnum + enumFrom x = [x .. maxBound] + +instance KnownNat 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 + +-- | 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 + => [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 => + Show (IntOfSize n) where + showsPrec n = showsPrec n . getIntOfSize . trunc diff --git a/src/Numeric/Sized/WordOfSize.hs b/src/Numeric/Sized/WordOfSize.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Sized/WordOfSize.hs @@ -0,0 +1,124 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | This module exports the 'WordOfSize' type and associated functions. +module Numeric.Sized.WordOfSize + (WordOfSize(..) + ,allWordsOfSize) + where + +import Data.Bits +import Data.Coerce +import Data.Function +import Data.Proxy +import GHC.Generics +import GHC.TypeLits +import Numeric.Natural + +-- $setup +-- >>> :set -XDataKinds + +-- | An unsigned integer type with a size decided by a type-level nat. Numeric +-- operations wraparound by default: +-- +-- >>> (255 :: WordOfSize 8) + 1 +-- 0 +newtype WordOfSize (n :: Nat) = WordOfSize + { getWordOfSize :: Natural + } deriving (Generic) + +instance KnownNat n => + Bounded (WordOfSize n) where + minBound = WordOfSize 0 + maxBound = WordOfSize (shift 1 (fromInteger (natVal (Proxy :: Proxy n))) - 1) + +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 + => WordOfSize n -> WordOfSize n +trunc = (.&.) maxBound + +convBinary + :: KnownNat n + => CoerceBinary Natural (WordOfSize n) +convBinary f = trunc .: coerce f + +instance KnownNat n => + Num (WordOfSize n) where + (+) = convBinary (+) + (*) = convBinary (*) + negate y = (maxBound `xor` y) + 1 + fromInteger = trunc . WordOfSize . fromInteger + abs = id + signum (WordOfSize x) = WordOfSize (signum x) + +instance KnownNat n => + Eq (WordOfSize n) where + (==) = (==) `on` getWordOfSize . trunc + +instance KnownNat n => + Show (WordOfSize n) where + showsPrec n = showsPrec n . getWordOfSize . trunc + +instance KnownNat n => + Ord (WordOfSize n) where + compare = compare `on` getWordOfSize . trunc + +instance KnownNat n => + Real (WordOfSize n) where + toRational = toRational . getWordOfSize + +instance KnownNat n => + Enum (WordOfSize n) where + fromEnum = fromEnum . getWordOfSize + toEnum = trunc . WordOfSize . toEnum + enumFrom x = [x .. maxBound] + +instance KnownNat n => + Integral (WordOfSize n) where + toInteger = toInteger . getWordOfSize + 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 + +-- | Generates all words of a given size +-- +-- >>> allWordOfSize :: [WordOfSize 3] +-- [0,1,2,3,4,5,6,7] +allWordsOfSize + :: KnownNat n + => [WordOfSize n] +allWordsOfSize = [minBound .. maxBound] diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,214 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Main + (main) + where + +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 + +instance KnownNat n => + Arbitrary (IntOfSize n) where + arbitrary = arbitraryBoundedEnum + +instance KnownNat n => + Arbitrary (WordOfSize n) where + arbitrary = arbitraryBoundedEnum + +instance (KnownNat n, Monad m) => + Serial m (IntOfSize n) where + series = generate (`take` allIntsOfSize) + +instance (KnownNat n, Monad m) => + Serial m (WordOfSize n) where + series = generate (`take` allWordsOfSize) + +type family IntType (n :: Nat) :: * where + IntType 8 = Int8 + IntType 16 = Int16 + IntType 32 = Int32 + IntType 64 = Int64 + +type family WordType (n :: Nat) :: * where + WordType 8 = Word8 + WordType 16 = Word16 + WordType 32 = Word32 + WordType 64 = Word64 + +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 + +sameConvI + :: (KnownNat n, Integral (IntType n)) + => Proxy n -> Integer -> Property +sameConvI (_ :: Proxy n) = + sameConvAs (Proxy :: Proxy (IntOfSize n)) (Proxy :: Proxy (IntType n)) + +sameConvW + :: (KnownNat n, Integral (WordType n)) + => Proxy n -> Natural -> Property +sameConvW (_ :: Proxy n) = + sameConvAs (Proxy :: Proxy (WordOfSize n)) (Proxy :: Proxy (WordType n)) + +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) + +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 + +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)) + +sameFncWNZRhs f n x y = y /= 0 ==> sameFncW f n x y + +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) + +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)) + +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 + +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)) + +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 + +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)) + +main :: IO () +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/"]