Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse code

Add Reify instances for Word* and Int* types with range checks where

appropriate
  • Loading branch information...
commit 5102fc80fe7333afe8945a3f926bae7f23a1cee1 1 parent b938d94
Aleksey Khudyakov authored
65 TypeLevel/Number/Nat.hs
@@ -54,38 +54,22 @@ module TypeLevel.Number.Nat ( -- * Natural numbers
54 54 , module TypeLevel.Number.Classes
55 55 ) where
56 56
  57 +import Data.Word (Word8,Word16,Word32,Word64)
  58 +import Data.Int (Int8, Int16, Int32, Int64 )
  59 +
  60 +
57 61 import Language.Haskell.TH
58 62
59 63 import TypeLevel.Number.Classes
60 64 import TypeLevel.Number.Nat.Types
  65 +import TypeLevel.Number.Nat.TH
61 66 import TypeLevel.Reify
62 67
63   -splitToBits :: Integer -> [Int]
64   -splitToBits 0 = []
65   -splitToBits x | odd x = 1 : splitToBits rest
66   - | otherwise = 0 : splitToBits rest
67   - where rest = x `div` 2
68   -
69 68 -- $TH
70 69 -- Here is usage example for natT:
71 70 --
72 71 -- > n123 :: $(natT 123)
73 72 -- > n123 = undefined
74   ---
75   --- This require type splices which are supprted by GHC>=6.12.
76   -
77   --- | Create type for natural number.
78   -natT :: Integer -> TypeQ
79   -natT n | n >= 0 = foldr appT [t| Z |] . map con . splitToBits $ n
80   - | otherwise = error "natT: negative number is supplied"
81   - where
82   - con 0 = [t| O |]
83   - con 1 = [t| I |]
84   - con _ = error "natT: Strange bit nor 0 nor 1"
85   -
86   --- | Create value for type level natural. Value itself is undefined.
87   -nat :: Integer -> ExpQ
88   -nat n = sigE [|undefined|] (natT n)
89 73
90 74 ----------------------------------------------------------------
91 75
@@ -128,6 +112,45 @@ instance Reify Z Int where witness = Witness 0
128 112 instance (Nat (O n)) => Reify (O n) Int where witness = Witness $ toInt (undefined :: O n)
129 113 instance (Nat (I n)) => Reify (I n) Int where witness = Witness $ toInt (undefined :: I n)
130 114
  115 +-- To Word8
  116 +instance Reify Z Word8 where witness = Witness 0
  117 +instance (Nat (O n), (O n) `Lesser` $(natT 0x100)) => Reify (O n) Word8 where witness = Witness $ toInt (undefined :: O n)
  118 +instance (Nat (I n), (I n) `Lesser` $(natT 0x100)) => Reify (I n) Word8 where witness = Witness $ toInt (undefined :: I n)
  119 +
  120 +-- To Word16
  121 +instance Reify Z Word16 where witness = Witness 0
  122 +instance (Nat (O n), (O n) `Lesser` $(natT 0x10000)) => Reify (O n) Word16 where witness = Witness $ toInt (undefined :: O n)
  123 +instance (Nat (I n), (I n) `Lesser` $(natT 0x10000)) => Reify (I n) Word16 where witness = Witness $ toInt (undefined :: I n)
  124 +
  125 +-- To Word32 (No checks. Won't to default centext stack length)
  126 +instance Reify Z Word32 where witness = Witness 0
  127 +instance (Nat (O n)) => Reify (O n) Word32 where witness = Witness $ toInt (undefined :: O n)
  128 +instance (Nat (I n)) => Reify (I n) Word32 where witness = Witness $ toInt (undefined :: I n)
  129 +
  130 +-- To Word64 (No checks. Won't to default centext stack length)
  131 +instance Reify Z Word64 where witness = Witness 0
  132 +instance (Nat (O n)) => Reify (O n) Word64 where witness = Witness $ toInt (undefined :: O n)
  133 +instance (Nat (I n)) => Reify (I n) Word64 where witness = Witness $ toInt (undefined :: I n)
  134 +
  135 +-- To Int8
  136 +instance Reify Z Int8 where witness = Witness 0
  137 +instance (Nat (O n), (O n) `Lesser` $(natT 0x80)) => Reify (O n) Int8 where witness = Witness $ toInt (undefined :: O n)
  138 +instance (Nat (I n), (I n) `Lesser` $(natT 0x80)) => Reify (I n) Int8 where witness = Witness $ toInt (undefined :: I n)
  139 +
  140 +-- To Int16
  141 +instance Reify Z Int16 where witness = Witness 0
  142 +instance (Nat (O n), (O n) `Lesser` $(natT 0x8000)) => Reify (O n) Int16 where witness = Witness $ toInt (undefined :: O n)
  143 +instance (Nat (I n), (I n) `Lesser` $(natT 0x8000)) => Reify (I n) Int16 where witness = Witness $ toInt (undefined :: I n)
  144 +
  145 +-- To Int32 (No checks. Won't to default centext stack length)
  146 +instance Reify Z Int32 where witness = Witness 0
  147 +instance (Nat (O n)) => Reify (O n) Int32 where witness = Witness $ toInt (undefined :: O n)
  148 +instance (Nat (I n)) => Reify (I n) Int32 where witness = Witness $ toInt (undefined :: I n)
  149 +
  150 +-- To Int64 (No checks. Won't to default centext stack length)
  151 +instance Reify Z Int64 where witness = Witness 0
  152 +instance (Nat (O n)) => Reify (O n) Int64 where witness = Witness $ toInt (undefined :: O n)
  153 +instance (Nat (I n)) => Reify (I n) Int64 where witness = Witness $ toInt (undefined :: I n)
131 154
132 155 ----------------------------------------------------------------
133 156 -- Number normalization
28 TypeLevel/Number/Nat/TH.hs
... ... @@ -0,0 +1,28 @@
  1 +{-# LANGUAGE TemplateHaskell #-}
  2 +module TypeLevel.Number.Nat.TH ( nat
  3 + , natT
  4 + ) where
  5 +
  6 +
  7 +import Language.Haskell.TH
  8 +import TypeLevel.Number.Nat.Types
  9 +
  10 +splitToBits :: Integer -> [Int]
  11 +splitToBits 0 = []
  12 +splitToBits x | odd x = 1 : splitToBits rest
  13 + | otherwise = 0 : splitToBits rest
  14 + where rest = x `div` 2
  15 +
  16 +
  17 +-- | Create type for natural number.
  18 +natT :: Integer -> TypeQ
  19 +natT n | n >= 0 = foldr appT [t| Z |] . map con . splitToBits $ n
  20 + | otherwise = error "natT: negative number is supplied"
  21 + where
  22 + con 0 = [t| O |]
  23 + con 1 = [t| I |]
  24 + con _ = error "natT: Strange bit nor 0 nor 1"
  25 +
  26 +-- | Create value for type level natural. Value itself is undefined.
  27 +nat :: Integer -> ExpQ
  28 +nat n = sigE [|undefined|] (natT n)
1  type-numbers.cabal
@@ -44,5 +44,6 @@ Library
44 44 TypeLevel.Boolean
45 45 TypeLevel.Reify
46 46 Other-modules: TypeLevel.Number.Nat.Types
  47 + TypeLevel.Number.Nat.TH
47 48 TypeLevel.Number.Int.Types
48 49 TypeLevel.Util

0 comments on commit 5102fc8

Please sign in to comment.
Something went wrong with that request. Please try again.