{-# LANGUAGE TemplateHaskell, ConstraintKinds, TypeFamilies, DataKinds, MultiParamTypeClasses #-}
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

-- | Define the less than relation for numbers up to a number using Template Haskell.
-- | Also define subtraction.
-- | E.g. numberSystem 100
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]