{-# 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 (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TypeQ -> TypeQ -> TypeQ
appT (Name -> TypeQ
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. (Eq a, Num a) => a -> TypeQ
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 -> TypeQ
con a
0 = Name -> TypeQ
conT ''O
    con a
1 = Name -> TypeQ
conT ''I
    con a
_ = [Char] -> TypeQ
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
sigE [|undefined|] (Integer -> TypeQ
natT Integer
n)