[commit: base] type-nats: Add some useful functions for working with type literals. (2a15567)

[Iavor Diatchki]

Repository : ssh://darcs.haskell.org//srv/darcs/packages/base

On branch  : type-nats

http://hackage.haskell.org/trac/ghc/changeset/2a155674568ad7af5fd72ec801d897513fdc71ac

>---------------------------------------------------------------

commit 2a155674568ad7af5fd72ec801d897513fdc71ac
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Mon Mar 19 20:09:03 2012 -0700

    Add some useful functions for working with type literals.

>---------------------------------------------------------------

 GHC/TypeLits.hs |  102 +++++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 files changed, 99 insertions(+), 3 deletions(-)

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index 707df69..06c05e2 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE GADTs #-}
 {-# OPTIONS_GHC -XNoImplicitPrelude #-}
 {-| This module is an internal GHC module.  It declares the constants used
 in the implementation of type-level natural numbers.  The programmer interface
@@ -13,18 +14,33 @@ module GHC.TypeLits
   ( -- * Kinds
     Nat, Symbol
 
-    -- * Singleton type
+    -- * Singleton types
   , TNat(..), TSymbol(..)
 
-    -- * Linking type nad value level
+    -- * Linking type and value level
   , NatI(..), SymbolI(..)
 
+    -- * Working with singletons
+  , tNatInteger, withTNat, tNatThat
+  , tSymbolString, withTSymbol, tSymbolThat
+
     -- * Functions on type nats
   , type (<=), type (+), type (*), type (^)
+
+    -- * Destructing type-nats.
+  , isZero, IsZero(..)
+  , isEven, IsEven(..)
   ) where
 
-import GHC.Num(Integer)
+import GHC.Base(Bool(..), ($), otherwise, (==), (.))
+import GHC.Num(Integer, (-))
 import GHC.Base(String)
+import GHC.Read(Read(..))
+import GHC.Show(Show(..))
+import Unsafe.Coerce(unsafeCoerce)
+import Data.Bits(testBit,shiftR)
+import Data.Maybe(Maybe(..))
+import Data.List((++))
 
 -- | This is the *kind* of type-level natural numbers.
 data Nat
@@ -93,3 +109,83 @@ type family (m :: Nat) * (n :: Nat) :: Nat
 type family (m :: Nat) ^ (n :: Nat) :: Nat
 
 
+--------------------------------------------------------------------------------
+
+{-# INLINE tNatInteger #-}
+{-# INLINE withTNat #-}
+{-# INLINE tNatThat #-}
+
+
+tNatInteger :: TNat n -> Integer
+tNatInteger (TNat n) = n
+
+withTNat :: NatI n => (TNat n -> a) -> a
+withTNat f = f tNat
+
+tNatThat :: NatI n => (Integer -> Bool) -> Maybe (TNat n)
+tNatThat p = withTNat $ \x -> if p (tNatInteger x) then Just x else Nothing
+
+instance Show (TNat n) where
+  showsPrec p = showsPrec p . tNatInteger
+
+instance NatI n => Read (TNat n) where
+  readsPrec p cs = do (x,ys) <- readsPrec p cs
+                      case tNatThat (== x) of
+                        Just y  -> [(y,ys)]
+                        Nothing -> []
+
+
+--------------------------------------------------------------------------------
+
+tSymbolString :: TSymbol s -> String
+tSymbolString (TSymbol s) = s
+
+withTSymbol :: SymbolI s => (TSymbol s -> a) -> a
+withTSymbol f = f tSymbol
+
+tSymbolThat :: SymbolI s => (String -> Bool) -> Maybe (TSymbol s)
+tSymbolThat p = withTSymbol $ \x -> if p (tSymbolString x) then Just x
+                                                           else Nothing
+
+instance Show (TSymbol n) where
+  showsPrec p = showsPrec p . tSymbolString
+
+instance SymbolI n => Read (TSymbol n) where
+  readsPrec p cs = do (x,ys) <- readsPrec p cs
+                      case tSymbolThat (== x) of
+                        Just y  -> [(y,ys)]
+                        Nothing -> []
+
+
+
+--------------------------------------------------------------------------------
+
+data IsZero :: Nat -> * where
+  IsZero :: IsZero 0
+  IsSucc :: !(TNat n) -> IsZero (n + 1)
+
+isZero :: TNat n -> IsZero n
+isZero (TNat n) | n == 0    = unsafeCoerce IsZero
+                | otherwise = unsafeCoerce (IsSucc (TNat (n-1)))
+
+instance Show (IsZero n) where
+  show IsZero     = "0"
+  show (IsSucc n) = "(" ++ show n ++ " + 1)"
+
+data IsEven :: Nat -> * where
+  IsEvenZero :: IsEven 0
+  IsEven     :: !(TNat (n+1)) -> IsEven (2 * (n + 1))
+  IsOdd      :: !(TNat n)     -> IsEven (2 * n + 1)
+
+isEven :: TNat n -> IsEven n
+isEven (TNat n) | n == 0      = unsafeCoerce IsEvenZero
+                | testBit n 0 = unsafeCoerce (IsOdd  (TNat (n `shiftR` 1)))
+                | otherwise   = unsafeCoerce (IsEven (TNat (n `shiftR` 1)))
+
+instance Show (IsEven n) where
+  show IsEvenZero = "0"
+  show (IsEven x) = "(2 * " ++ show x ++ ")"
+  show (IsOdd  x) = "(2 * " ++ show x ++ " + 1)"
+
+
+