Data/HList/Number.hs

   1 module Data.HList.Number
   2     ( HNat
   3
   4     , HZero
   5     , hZero
   6
   7     , HSucc
   8     , hSucc
   9     , hPred
  10
  11     , hNatLiteralT
  12     , hNatLiteralE
  13     , hNatLiteralP
  14     )
  15     where
  16
  17 import Language.Haskell.TH
  18
  19
  20 -- HNat
  21 class HNat n
  22
  23 -- HZero
  24 data HZero = HZero deriving Show
  25
  26 instance HNat HZero
  27
  28 hZero :: HZero
  29 hZero = HZero
  30
  31 -- HSucc
  32 data HSucc n = HSucc n deriving Show
  33
  34 instance HNat n => HNat (HSucc n)
  35
  36 hSucc :: HNat n => n -> HSucc n
  37 hSucc = HSucc
  38
  39 hPred :: HNat n => HSucc n -> n
  40 hPred (HSucc n) = n
  41
  42 -- TH
  43 hNatLiteralT :: Integral n => n -> Q Type
  44 hNatLiteralT n
  45     | n == 0    = conT (mkName "HZero")
  46     | otherwise = appT (conT (mkName "HSucc"))
  47                        (hNatLiteralT (n - 1))
  48
  49 hNatLiteralE :: Integral n => n -> Q Exp
  50 hNatLiteralE n
  51     | n == 0    = varE (mkName "hZero")
  52     | otherwise = appE (varE (mkName "hSucc"))
  53                        (hNatLiteralE (n - 1))
  54
  55 hNatLiteralP :: Integral n => n -> Q Pat
  56 hNatLiteralP n
  57     | n == 0    = varP (mkName "HZero")
  58     | otherwise = conP (mkName "HSucc") [hNatLiteralP n]