implementing type-level strings...

[hs-rrdtool.git] / Data / HList / Number.hs

diff --git a/Data/HList/Number.hs b/Data/HList/Number.hs
new file mode 100644 (file)
index 0000000..ed9b513
--- /dev/null
+++ b/Data/HList/Number.hs
@@ -0,0 +1,58 @@
+module Data.HList.Number
+    ( HNat
+
+    , HZero
+    , hZero
+
+    , HSucc
+    , hSucc
+    , hPred
+
+    , hNatLiteralT
+    , hNatLiteralE
+    , hNatLiteralP
+    )
+    where
+
+import Language.Haskell.TH
+
+
+-- HNat
+class HNat n
+
+-- HZero
+data HZero = HZero deriving Show
+
+instance HNat HZero
+
+hZero :: HZero
+hZero = HZero
+
+-- HSucc
+data HSucc n = HSucc n deriving Show
+
+instance HNat n => HNat (HSucc n)
+
+hSucc :: HNat n => n -> HSucc n
+hSucc = HSucc
+
+hPred :: HNat n => HSucc n -> n
+hPred (HSucc n) = n
+
+-- TH
+hNatLiteralT :: Integral n => n -> Q Type
+hNatLiteralT n
+    | n == 0    = conT (mkName "HZero")
+    | otherwise = appT (conT (mkName "HSucc"))
+                       (hNatLiteralT (n - 1))
+
+hNatLiteralE :: Integral n => n -> Q Exp
+hNatLiteralE n
+    | n == 0    = varE (mkName "hZero")
+    | otherwise = appE (varE (mkName "hSucc"))
+                       (hNatLiteralE (n - 1))
+
+hNatLiteralP :: Integral n => n -> Q Pat
+hNatLiteralP n
+    | n == 0    = varP (mkName "HZero")
+    | otherwise = conP (mkName "HSucc") [hNatLiteralP n]