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

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

splitToBits :: Integer -> [Int]
splitToBits :: Integer -> [Int]
splitToBits 0 = []
splitToBits x :: Integer
x | Integer -> Bool
forall a. Integral a => a -> Bool
odd Integer
x     = 1 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: Integer -> [Int]
splitToBits Integer
rest
              | Bool
otherwise = 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` 2


-- | Create type for natural number.
natT :: Integer -> TypeQ
natT :: Integer -> TypeQ
natT n :: Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 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 "natT: negative number is supplied"
  where
    con :: a -> TypeQ
con 0 = Name -> TypeQ
conT ''O
    con 1 = Name -> TypeQ
conT ''I
    con _ = [Char] -> TypeQ
forall a. HasCallStack => [Char] -> a
error "natT: Strange bit nor 0 nor 1"

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