Commits

Aleksey Khudyakov  committed 654ddfe

Add function with{Nat,Int} and Some{Nat,Int} data types

Implementation is taken from finite-fields package and minor modification
were made

Fixes #1

  • Participants
  • Parent commits 501215e

Comments (0)

Files changed (3)

File TypeLevel/Number/Int.hs

 {-# OPTIONS_GHC  -fno-warn-orphans #-}
 
+{-# LANGUAGE DeriveDataTypeable    #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE EmptyDataDecls        #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE FlexibleContexts      #-}
                         , 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
 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
 

File TypeLevel/Number/Nat.hs

 {-# OPTIONS_GHC  -fno-warn-orphans #-}
 
+{-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE EmptyDataDecls        #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE TemplateHaskell       #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE DeriveDataTypeable    #-}
 -- |
 -- Module      : TypeLevel.Number.Nat
 -- Copyright   : Alexey Khudyakov
                         , O
                         , Z
                         , Nat(..)
+                          -- ** Lifting
+                        , SomeNat(..)
+                        , withNat
                           -- * Template haskell utilities
                           -- $TH
                         , natT
                         , 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
 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
 

File TypeLevel/Number/Nat/TH.hs

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