module Acme.NumberSystem where
import GHC.TypeLits
import Language.Haskell.TH
type Less = (<=)
type family Add (m :: Nat) (n :: Nat) :: Nat
type family Sub (m :: Nat) (n :: Nat) :: Nat
numberSystem :: Integer -> Q [Dec]
numberSystem theBiggestNumber = return . concat $ lessThan ++ subs ++ [adds]
where
lessThan = map (\i -> map (\j ->
InstanceD [] (AppT (AppT (ConT (''Less)) (LitT (NumTyLit i))) (LitT (NumTyLit j))) []
) [i..theBiggestNumber]) [0..theBiggestNumber]
subs = map (\i -> map (\j ->
TySynInstD ''Sub [LitT (NumTyLit j), LitT (NumTyLit i)] (LitT (NumTyLit (j i)))
) [i..theBiggestNumber]) [0..theBiggestNumber]
adds = map (\i ->
TySynInstD ''Add [LitT (NumTyLit i), LitT (NumTyLit 1)] (LitT (NumTyLit (i + 1)))
) [0..theBiggestNumber]