    {-# LANGUAGE TemplateHaskell #-}
    module TypeLevel.Number.Nat.TH where

    import Language.Haskell.TH
    import TypeLevel.Number.Nat.Types

    splitToBits :: Integer -> [Int]
    splitToBits :: Integer -> [Int]
    splitToBits Integer
    0 = []
    splitToBits Integer
    x | Integer -> Bool
    forall a. Integral a => a -> Bool
    odd Integer
    x     = Int
    1 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : Integer -> [Int]
    splitToBits Integer
    rest
                  | Bool
    otherwise = Int
    0 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : Integer -> [Int]
    splitToBits Integer
    rest
                    where rest :: Integer
    rest = Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    2

    -- | Create type for natural number.
    natT :: Integer -> TypeQ
    natT :: Integer -> TypeQ
    natT Integer
    n | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0    = (TypeQ -> TypeQ -> TypeQ) -> TypeQ -> [TypeQ] -> TypeQ
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TypeQ -> TypeQ -> TypeQ
    forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
    appT (Name -> TypeQ
    forall (m :: * -> *). Quote m => Name -> m Type
    conT ''Z) ([TypeQ] -> TypeQ) -> (Integer -> [TypeQ]) -> Integer -> TypeQ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> TypeQ) -> [Int] -> [TypeQ]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> TypeQ
    forall {a} {m :: * -> *}. (Eq a, Num a, Quote m) => a -> m Type
    con ([Int] -> [TypeQ]) -> (Integer -> [Int]) -> Integer -> [TypeQ]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> [Int]
    splitToBits (Integer -> TypeQ) -> Integer -> TypeQ
    forall a b. (a -> b) -> a -> b
    $ Integer
    n
           | Bool
    otherwise = [Char] -> TypeQ
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "natT: negative number is supplied"
      where
        con :: a -> m Type
    con a
    0 = Name -> m Type
    forall (m :: * -> *). Quote m => Name -> m Type
    conT ''O
        con a
    1 = Name -> m Type
    forall (m :: * -> *). Quote m => Name -> m Type
    conT ''I
        con a
    _ = [Char] -> m Type
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "natT: Strange bit nor 0 nor 1"

    -- | Create value for type level natural. Value itself is undefined.
    nat :: Integer -> ExpQ
    nat :: Integer -> ExpQ
    nat Integer
    n = ExpQ -> TypeQ -> ExpQ
    forall (m :: * -> *). Quote m => m Exp -> m Type -> m Exp
    sigE [|undefined|] (Integer -> TypeQ
    natT Integer
    n)