type-level-numbers 0.1.0.4 → 0.1.1.0
raw patch · 5 files changed
+114/−16 lines, 5 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ TypeLevel.Number.Int: data SomeInt
+ TypeLevel.Number.Int: instance Show SomeInt
+ TypeLevel.Number.Int: instance Typeable SomeInt
+ TypeLevel.Number.Int: withInt :: Integral i => (forall n. IntT n => n -> a) -> i -> a
+ TypeLevel.Number.Nat: SomeNat :: n -> SomeNat
+ TypeLevel.Number.Nat: data SomeNat
+ TypeLevel.Number.Nat: instance Show SomeNat
+ TypeLevel.Number.Nat: instance Typeable SomeNat
+ TypeLevel.Number.Nat: withNat :: Integral i => (forall n. Nat n => n -> a) -> i -> a
+ TypeLevel.Reify: instance (Data t, Data a) => Data (Witness t a)
+ TypeLevel.Reify: instance Eq a => Eq (Witness t a)
+ TypeLevel.Reify: instance Typeable Witness
Files
- TypeLevel/Number/Int.hs +57/−5
- TypeLevel/Number/Nat.hs +45/−4
- TypeLevel/Number/Nat/TH.hs +1/−4
- TypeLevel/Reify.hs +5/−1
- type-level-numbers.cabal +6/−2
TypeLevel/Number/Int.hs view
@@ -1,3 +1,8 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}++{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-}@@ -26,11 +31,15 @@ , D0 , D1 , IntT(..)+ -- ** Lifting+ , SomeInt+ , withInt -- * Template haskell utilities , intT , module TypeLevel.Number.Classes ) where +import Data.Typeable (Typeable) import Language.Haskell.TH import TypeLevel.Number.Classes@@ -43,8 +52,9 @@ splitToTrits x | n == 0 = 0 : splitToTrits rest | n == 1 = 1 : splitToTrits rest | n == 2 = -1 : splitToTrits (rest + 1)- where- (rest,n) = divMod x 3+ where+ (rest,n) = divMod x 3+splitToTrits _ = error "Internal error" -- | Generate type for integer number. intT :: Integer -> TypeQ@@ -84,9 +94,51 @@ instance Show ZZ where show _ = "[0:Z]"-instance IntT (Dn n) => Show (Dn n) where show n = "["++show (toInt n)++":Z]"-instance IntT (D0 n) => Show (D0 n) where show n = "["++show (toInt n)++":Z]"-instance IntT (D1 n) => Show (D1 n) where show n = "["++show (toInt n)++":Z]"+instance IntT (Dn n) => Show (Dn n) where show n = "["++show (toInt n :: Integer)++":Z]"+instance IntT (D0 n) => Show (D0 n) where show n = "["++show (toInt n :: Integer)++":Z]"+instance IntT (D1 n) => Show (D1 n) where show n = "["++show (toInt n :: Integer)++":Z]"+++-- | Some natural number+data SomeInt where+ SomeInt :: IntT n => n -> SomeInt+ deriving Typeable++instance Show SomeInt where+ showsPrec d (SomeInt n) = showParen (d > 10) $+ showString "withInt SomeInt " . shows (toInt n :: Integer)++++-- | Apply function which could work with any 'Nat' value only know at runtime.+withInt :: forall i a. (Integral i) => (forall n. IntT n => n -> a) -> i -> a+withInt f i0+ | i0 == 0 = f (undefined :: ZZ)+ | otherwise = cont (fromIntegral i0) f f f+ where+ cont :: Integer -> (forall n m. (IntT n, n ~ Dn m) => n -> a)+ -> (forall n m. (IntT n, n ~ D0 m) => n -> a)+ -> (forall n m. (IntT n, n ~ D1 m) => n -> a) -> a+ cont (-1) kN _ _ = kN (undefined :: Dn ZZ)+ cont 1 _ _ k1 = k1 (undefined :: D1 ZZ)+ cont i kN k0 k1 = cont i' kN' k0' k1'+ where+ (i',bit) = case divMod i 3 of+ (x,2) -> (x+1,-1)+ x -> x+ kN' :: forall n m. (IntT n, n ~ Dn m) => n -> a+ kN' _ | bit == -1 = kN (undefined :: Dn n)+ | bit == 0 = k0 (undefined :: D0 n)+ | otherwise = k1 (undefined :: D1 n)+ k0' :: forall n m. (IntT n, n ~ D0 m) => n -> a+ k0' _ | bit == -1 = kN (undefined :: Dn n)+ | bit == 0 = k0 (undefined :: D0 n)+ | otherwise = k1 (undefined :: D1 n)++ k1' :: forall n m. (IntT n, n ~ D1 m) => n -> a+ k1' _ | bit == -1 = kN (undefined :: Dn n)+ | bit == 0 = k0 (undefined :: D0 n)+ | otherwise = k1 (undefined :: D1 n) ---------------------------------------------------------------- -- Number normalization
TypeLevel/Number/Nat.hs view
@@ -1,3 +1,6 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}++{-# LANGUAGE GADTs #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-}@@ -7,6 +10,8 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DeriveDataTypeable #-} -- | -- Module : TypeLevel.Number.Nat -- Copyright : Alexey Khudyakov@@ -48,6 +53,9 @@ , O , Z , Nat(..)+ -- ** Lifting+ , SomeNat(..)+ , withNat -- * Template haskell utilities -- $TH , natT@@ -55,8 +63,9 @@ , module TypeLevel.Number.Classes ) where -import Data.Word (Word8,Word16,Word32,Word64)-import Data.Int (Int8, Int16, Int32, Int64 )+import Data.Word (Word8,Word16,Word32,Word64)+import Data.Int (Int8, Int16, Int32, Int64 )+import Data.Typeable (Typeable) import TypeLevel.Number.Classes import TypeLevel.Number.Nat.Types@@ -97,6 +106,38 @@ instance (Nat n, Positive n) => Pos n +-- | Some natural number+data SomeNat where+ SomeNat :: Nat n => n -> SomeNat+ deriving Typeable++instance Show SomeNat where+ showsPrec d (SomeNat n) = showParen (d > 10) $+ showString "withNat SomeNat " . shows (toInt n :: Integer)++++-- | Apply function which could work with any 'Nat' value only know at runtime.+withNat :: forall i a. (Integral i) => (forall n. Nat n => n -> a) -> i -> a+withNat f i0+ | i0 < 0 = error "TypeLevel.Number.Nat.withNat: negative number"+ | i0 == 0 = f (undefined :: Z)+ | otherwise = cont (fromIntegral i0) f f+ where+ cont :: Integer -> (forall n m. (Nat n, n ~ O m) => n -> a)+ -> (forall n m. (Nat n, n ~ I m) => n -> a) -> a+ cont 1 _ k1 = k1 (undefined :: I Z)+ cont i k0 k1 = cont (i `quot` 2) k0' k1'+ where+ k0' :: forall n m. (Nat n, n ~ O m) => n -> a+ k0' _ | odd i = k1 (undefined :: I n)+ | otherwise = k0 (undefined :: O n)+ k1' :: forall n m. (Nat n, n ~ I m) => n -> a+ k1' _ | odd i = k1 (undefined :: I n)+ | otherwise = k0 (undefined :: O n)+++ ---------------------------------------------------------------- -- Data conversion @@ -167,8 +208,8 @@ -- Show instances. -- Nat contexts are used to ensure correctness of numbers. instance Show Z where show _ = "[0:N]"-instance Nat (O n) => Show (O n) where show n = "["++show (toInt n)++":N]"-instance Nat (I n) => Show (I n) where show n = "["++show (toInt n)++":N]"+instance Nat (O n) => Show (O n) where show n = "["++show (toInt n :: Integer)++":N]"+instance Nat (I n) => Show (I n) where show n = "["++show (toInt n :: Integer)++":N]" ---------------------------------------------------------------- -- Next number.
TypeLevel/Number/Nat/TH.hs view
@@ -1,8 +1,5 @@ {-# LANGUAGE TemplateHaskell #-}-module TypeLevel.Number.Nat.TH ( nat- , natT- ) where-+module TypeLevel.Number.Nat.TH where import Language.Haskell.TH import TypeLevel.Number.Nat.Types
TypeLevel/Reify.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE DeriveDataTypeable #-} -- | -- Module : TypeLevel.Reify -- Copyright : Alexey Khudyakov@@ -11,9 +12,12 @@ , Reify(..) ) where +import Data.Data (Data,Typeable) ++-- | Value with type tag data Witness t a = Witness { getValue :: a }- deriving Show+ deriving (Show,Eq,Typeable,Data) -- | Convert type level into value level using class Reify t a where
type-level-numbers.cabal view
@@ -1,5 +1,5 @@ Name: type-level-numbers-Version: 0.1.0.4+Version: 0.1.1.0 Synopsis: Type level numbers implemented using type families. Description:@@ -22,6 +22,10 @@ So far comparison of numbers, subtraction and multiplication of numbers are supported. .+ Changes in 0.1.1.0+ .+ * @withNat@, @withInt@, @SomeNat and @SomeInt@ added.+ . Changes in 0.1.0.3 . * Fix build for GHC 7.4@@ -53,7 +57,7 @@ Library- ghc-options: -Wall -fno-warn-orphans+ ghc-options: -Wall Build-Depends: base >=3 && <5, template-haskell > 2.0 Exposed-modules: TypeLevel.Number.Classes