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]