{-# 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
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"
nat :: Integer -> ExpQ
nat :: Integer -> ExpQ
nat Integer
n = ExpQ -> TypeQ -> ExpQ
sigE [|undefined|] (Integer -> TypeQ
natT Integer
n)