{-# 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
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"
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)