int-cast-0.1.1.0: Data/IntCast.hs
{-# LANGUAGE CPP, DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
#if __GLASGOW_HASKELL__ < 707
#error This code requires GHC 7.7+
#endif
#include "MachDeps.h"
#include "HsBaseConfig.h"
-- |
-- Module: Data.IntCast
-- Copyright: © 2014 Herbert Valerio Riedel
-- License: BSD-style (see the LICENSE file)
--
-- Maintainer: Herbert Valerio Riedel <hvr@gnu.org>
-- Stability: experimental
-- Portability: GHC ≥ 7.8
--
-- This module provides for statically or dynamically checked
-- conversions between 'Integral' types.
module Data.IntCast
( -- * Conversion functions
-- ** statically checked
intCast
, intCastIso
, intCastEq
-- ** dynamically checked
, intCastMaybe
-- * Registering new integer types
-- |
-- * For 'intCastMaybe' you need to provide type-class instances of 'Bits'
-- (and 'Integral').
--
-- * For 'intCast', 'intCastIso', and 'intCastEq' simply
-- declare instances for the 'IntBaseType' type-family (as well
-- as type-class instances of 'Integral') as described below.
, IntBaseType
, IntBaseTypeK(..)
-- * Type-level predicates
-- | The following type-level predicates are used by 'intCast',
-- 'intCastIso', and 'intCastEq' respectively.
, IsIntSubType
, IsIntBaseSubType
, IsIntTypeIso
, IsIntBaseTypeIso
, IsIntTypeEq
, IsIntBaseTypeEq
) where
-- Haskell 2010+
import Data.Int
import Data.Word
import Foreign.C.Types
-- non-Haskell 2010
import GHC.TypeLits
import Data.Bits
import Data.Type.Equality
-- | (Kind) Meta-information about integral types.
--
-- If also a 'Bits' instance is defined, the type-level information
-- provided by 'IntBaseType' ought to match the meta-information that
-- is conveyed by the 'Bits' class' 'isSigned' and 'bitSizeMaybe'
-- methods.
data IntBaseTypeK
-- | fixed-width /n/-bit integers with value range [-2ⁿ⁻¹, 2ⁿ⁻¹-1].
= FixedIntTag Nat
-- | fixed-width /n/-bit integers with value range [0, 2ⁿ-1].
| FixedWordTag Nat
-- | integers with value range ]-∞,+∞[.
| BigIntTag
-- | naturals with value range [0,+∞[.
| BigWordTag
-- | The (open) type family 'IntBaseType' encodes type-level
-- information about the value range of an integral type.
--
-- This module also provides type family instances for the standard
-- Haskell 2010 integral types (including "Foreign.C.Types").
--
-- Here's a simple example for registering a custom type with the
-- "Data.IntCast" facilities:
--
-- @
-- /-- user-implemented unsigned 4-bit integer/
-- data Nibble = …
--
-- /-- declare meta-information/
-- type instance 'IntBaseType' MyWord7 = 'FixedIntTag' 4
--
-- /-- user-implemented signed 7-bit integer/
-- data MyInt7 = …
--
-- /-- declare meta-information/
-- type instance 'IntBaseType' MyWord7 = 'FixedIntTag' 7
-- @
--
-- The type-level predicate 'IsIntSubType' provides a partial
-- ordering based on the types above. See also 'intCast'.
type family IntBaseType a :: IntBaseTypeK
type instance IntBaseType Integer = BigIntTag
-- Haskell2010 Basic fixed-width Integer Types
type instance IntBaseType Int8 = FixedIntTag 8
type instance IntBaseType Int16 = FixedIntTag 16
type instance IntBaseType Int32 = FixedIntTag 32
type instance IntBaseType Int64 = FixedIntTag 64
type instance IntBaseType Word8 = FixedWordTag 8
type instance IntBaseType Word16 = FixedWordTag 16
type instance IntBaseType Word32 = FixedWordTag 32
type instance IntBaseType Word64 = FixedWordTag 64
#if defined(WORD_SIZE_IN_BITS)
type instance IntBaseType Int = FixedIntTag WORD_SIZE_IN_BITS
type instance IntBaseType Word = FixedWordTag WORD_SIZE_IN_BITS
#else
#error Cannot determine bit-size of 'Int'/'Word' type
#endif
-- Haskell2010 FFI Integer Types
type instance IntBaseType CChar = IntBaseType HTYPE_CHAR
type instance IntBaseType CInt = IntBaseType HTYPE_INT
type instance IntBaseType CIntMax = IntBaseType HTYPE_INTMAX_T
type instance IntBaseType CIntPtr = IntBaseType HTYPE_INTPTR_T
type instance IntBaseType CLLong = IntBaseType HTYPE_LONG_LONG
type instance IntBaseType CLong = IntBaseType HTYPE_LONG
type instance IntBaseType CPtrdiff = IntBaseType HTYPE_PTRDIFF_T
type instance IntBaseType CSChar = IntBaseType HTYPE_SIGNED_CHAR
type instance IntBaseType CShort = IntBaseType HTYPE_SHORT
type instance IntBaseType CSigAtomic = IntBaseType HTYPE_SIG_ATOMIC_T
type instance IntBaseType CSize = IntBaseType HTYPE_SIZE_T
type instance IntBaseType CUChar = IntBaseType HTYPE_UNSIGNED_CHAR
type instance IntBaseType CUInt = IntBaseType HTYPE_UNSIGNED_INT
type instance IntBaseType CUIntMax = IntBaseType HTYPE_UINTMAX_T
type instance IntBaseType CUIntPtr = IntBaseType HTYPE_UINTPTR_T
type instance IntBaseType CULLong = IntBaseType HTYPE_UNSIGNED_LONG_LONG
type instance IntBaseType CULong = IntBaseType HTYPE_UNSIGNED_LONG
type instance IntBaseType CUShort = IntBaseType HTYPE_UNSIGNED_SHORT
-- Internal class providing the partial order of (improper) subtype-relations
type family IsIntBaseSubType a b :: Bool where
-- this relation is reflexive
IsIntBaseSubType a a = True
-- Every integer is a subset of 'Integer'
IsIntBaseSubType a BigIntTag = True
-- Even though Haskell2010 doesn't provide naturals, we can use the
-- tag 'Nat' to denote such entities
IsIntBaseSubType (FixedWordTag a) BigWordTag = True
-- sub-type relations between fixed-with types
IsIntBaseSubType (FixedIntTag a) (FixedIntTag b) = a <=? b
IsIntBaseSubType (FixedWordTag a) (FixedWordTag b) = a <=? b
IsIntBaseSubType (FixedWordTag a) (FixedIntTag b) = a+1 <=? b
-- everything else is not a sub-type
IsIntBaseSubType a b = False
type IsIntSubType a b = IsIntBaseSubType (IntBaseType a) (IntBaseType b)
-- Same bit-size predicate
type family IsIntBaseTypeIso a b :: Bool where
IsIntBaseTypeIso a a = True
IsIntBaseTypeIso (FixedIntTag n) (FixedWordTag n) = True
IsIntBaseTypeIso (FixedWordTag n) (FixedIntTag n) = True
IsIntBaseTypeIso a b = False
type IsIntTypeIso a b = IsIntBaseTypeIso (IntBaseType a) (IntBaseType b)
type family IsIntBaseTypeEq (a :: IntBaseTypeK) (b :: IntBaseTypeK) :: Bool where
IsIntBaseTypeEq a a = True
IsIntBaseTypeEq a b = False
type IsIntTypeEq a b = IsIntBaseTypeEq (IntBaseType a) (IntBaseType b)
type instance a == b = IsIntBaseTypeEq a b
-- | Statically checked integer conversion which satisfies the property
--
-- * @'toInteger' ≡ 'toInteger' . intCast@
--
-- Note: This is just a type-restricted alias of 'fromIntegral' and
-- should therefore lead to the same compiled code as if
-- 'fromIntegral' had been used instead of 'intCast'.
intCast :: (Integral a, Integral b, IsIntSubType a b ~ True) => a -> b
intCast = fromIntegral
{-# INLINE intCast #-}
-- | Statically checked integer conversion which satisfies the properties
--
-- * @∀β . 'intCastIso' ('intCastIso' a ∷ β) == a@
--
-- * @'toInteger' ('intCastIso' a) == 'toInteger' b (__if__ 'toInteger' a == 'toInteger' b)@
--
-- Note: This is just a type-restricted alias of 'fromIntegral' and
-- should therefore lead to the same compiled code as if
-- 'fromIntegral' had been used instead of 'intCast'.
intCastIso :: (Integral a, Integral b, IsIntTypeIso a b ~ True) => a -> b
intCastIso = fromIntegral
{-# INLINE intCastIso #-}
-- | Version of 'intCast' restricted to casts between types with same value domain.
intCastEq :: (Integral a, Integral b, IsIntTypeEq a b ~ True) => a -> b
intCastEq = fromIntegral
{-# INLINE intCastEq #-}
----------------------------------------------------------------------------
----------------------------------------------------------------------------
-- dynamically checked conversion
-- | 'Bits' class based value-level predicate with same semantics as 'IsIntSubType'
isBitSubType :: (Bits a, Bits b) => a -> b -> Bool
isBitSubType _x _y
-- reflexive
| xWidth == yWidth, xSigned == ySigned = True
-- Every integer is a subset of 'Integer'
| ySigned, Nothing == yWidth = True
| not xSigned, not ySigned, Nothing == yWidth = True
-- sub-type relations between fixed-with types
| xSigned == ySigned, Just xW <- xWidth, Just yW <- yWidth = xW <= yW
| not xSigned, ySigned, Just xW <- xWidth, Just yW <- yWidth = xW < yW
| otherwise = False
where
xWidth = bitSizeMaybe _x
xSigned = isSigned _x
yWidth = bitSizeMaybe _y
ySigned = isSigned _y
{-# INLINE isBitSubType #-}
-- | Run-time-checked integer conversion
--
-- This is an optimized version of the following generic code below
--
-- > intCastMaybeRef :: (Integral a, Integral b) => a -> Maybe b
-- > intCastMaybeRef x
-- > | toInteger x == toInteger y = Just y
-- > | otherwise = Nothing
-- > where
-- > y = fromIntegral x
--
-- The code above is rather inefficient as it needs to go via the
-- 'Integer' type. The function 'intCastMaybe', however, is marked @INLINEABLE@ and
-- if both integral types are statically known, GHC will be able
-- optimize the code signficantly (for @-O1@ and better).
--
-- For instance (as of GHC 7.8.1) the following definitions
--
-- > w16_to_i32 = intCastMaybe :: Word16 -> Maybe Int32
-- >
-- > i16_to_w16 = intCastMaybe :: Int16 -> Maybe Word16
--
-- are translated into the following (simplified) /GHC Core/ language
--
-- > w16_to_i32 = \x -> Just (case x of _ { W16# x# -> I32# (word2Int# x#) })
-- >
-- > i16_to_w16 = \x -> case eta of _
-- > { I16# b1 -> case tagToEnum# (<=# 0 b1) of _
-- > { False -> Nothing
-- > ; True -> Just (W16# (narrow16Word# (int2Word# b1)))
-- > }
-- > }
intCastMaybe :: (Integral a, Integral b, Bits a, Bits b) => a -> Maybe b
-- the code below relies on GHC optimizing away statically decidable branches
intCastMaybe x
| maybe True (<= x) yMinBound
, maybe True (x <=) yMaxBound = Just y
| otherwise = Nothing
where
y = fromIntegral x
xWidth = bitSizeMaybe x
yWidth = bitSizeMaybe y
yMinBound | isBitSubType x y = Nothing
| isSigned x, not (isSigned y) = Just 0
| isSigned x, isSigned y, Just yW <- yWidth
= Just (negate $ bit (yW-1)) -- N.B. assumes sub-type
| otherwise = Nothing
yMaxBound | isBitSubType x y = Nothing
| isSigned x, not (isSigned y), Just xW <- xWidth, Just yW <- yWidth
, xW <= yW+1 = Nothing -- max-bound beyond a's domain
| Just yW <- yWidth = if isSigned y then Just (bit (yW-1)-1) else Just (bit yW-1)
| otherwise = Nothing
{-# INLINEABLE intCastMaybe #-}