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 <[email protected]> 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)" + + + _______________________________________________ Cvs-libraries mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-libraries
