Commit a7324769 authored by Iavor S. Diatchki's avatar Iavor S. Diatchki
Browse files

Add some useful functions for working with type literals.

parent eec29e91
......@@ -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)"
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment