module Data.TypeLevel.Num.Sets (Pos, Nat, toNum, toInt, reifyIntegral) where
import Data.TypeLevel.Num.Reps
class NatI n where
toNum :: Num a => n -> a
toInt :: Nat n => n -> Int
toInt = toNum
class NatI n => PosI n
class NatI n => Nat n
instance NatI n => Nat n
class PosI n => Pos n
instance PosI n => Pos n
instance NatI D0 where toNum _ = fromInteger 0
instance NatI D1 where toNum _ = fromInteger 1
instance NatI D2 where toNum _ = fromInteger 2
instance NatI D3 where toNum _ = fromInteger 3
instance NatI D4 where toNum _ = fromInteger 4
instance NatI D5 where toNum _ = fromInteger 5
instance NatI D6 where toNum _ = fromInteger 6
instance NatI D7 where toNum _ = fromInteger 7
instance NatI D8 where toNum _ = fromInteger 8
instance NatI D9 where toNum _ = fromInteger 9
instance PosI x => NatI (x :* D0) where toNum n = subLastDec n
instance PosI x => NatI (x :* D1) where toNum n = subLastDec n + fromInteger 1
instance PosI x => NatI (x :* D2) where toNum n = subLastDec n + fromInteger 2
instance PosI x => NatI (x :* D3) where toNum n = subLastDec n + fromInteger 3
instance PosI x => NatI (x :* D4) where toNum n = subLastDec n + fromInteger 4
instance PosI x => NatI (x :* D5) where toNum n = subLastDec n + fromInteger 5
instance PosI x => NatI (x :* D6) where toNum n = subLastDec n + fromInteger 6
instance PosI x => NatI (x :* D7) where toNum n = subLastDec n + fromInteger 7
instance PosI x => NatI (x :* D8) where toNum n = subLastDec n + fromInteger 8
instance PosI x => NatI (x :* D9) where toNum n = subLastDec n + fromInteger 9
instance PosI D1
instance PosI D2
instance PosI D3
instance PosI D4
instance PosI D5
instance PosI D6
instance PosI D7
instance PosI D8
instance PosI D9
instance PosI x => PosI (x :* D0)
instance PosI x => PosI (x :* D1)
instance PosI x => PosI (x :* D2)
instance PosI x => PosI (x :* D3)
instance PosI x => PosI (x :* D4)
instance PosI x => PosI (x :* D5)
instance PosI x => PosI (x :* D6)
instance PosI x => PosI (x :* D7)
instance PosI x => PosI (x :* D8)
instance PosI x => PosI (x :* D9)
reifyIntegral :: Integral i => i -> (forall n . Nat n => n -> r) -> r
reifyIntegral i f
| i < 0 = error "reifyIntegral: integral < 0"
| i == 0 = f (undefined :: D0)
| otherwise = reifyIntegralp i f
where reifyIntegralp :: Integral i => i -> (forall n . Pos n => n -> r) -> r
reifyIntegralp i f
| i < 10 = case i of
1 -> f (undefined :: D1)
2 -> f (undefined :: D2); 3 -> f (undefined :: D3)
4 -> f (undefined :: D4); 5 -> f (undefined :: D5)
6 -> f (undefined :: D6); 7 -> f (undefined :: D7)
8 -> f (undefined :: D8); 9 -> f (undefined :: D9)
| otherwise =
case m of
0 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D0))
1 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D1))
2 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D2))
3 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D3))
4 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D4))
5 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D5))
6 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D6))
7 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D7))
8 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D8))
9 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D9))
where (d,m) = divMod i 10
subLastDec :: (Num a, NatI (x :* d), NatI x) => x :* d -> a
subLastDec = (10*).toNum.div10Dec
div10Dec :: NatI (x :* d) => x :* d -> x
div10Dec _ = undefined