packages feed

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 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