{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveDataTypeable #-}

module Type.Data.Num.Decimal.Digit where

import qualified Type.Data.Num.Unary.Literal as UnaryLit

import Type.Base.Proxy (Proxy(Proxy))

import Data.Typeable (Typeable)


newtype Singleton d = Singleton Int

singleton :: (C d) => Singleton d
singleton :: Singleton d
singleton =
    Singleton Dec0
-> Singleton Dec1
-> Singleton Dec2
-> Singleton Dec3
-> Singleton Dec4
-> Singleton Dec5
-> Singleton Dec6
-> Singleton Dec7
-> Singleton Dec8
-> Singleton Dec9
-> Singleton d
forall d (f :: * -> *).
C d =>
f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f d
switch
        (Int -> Singleton Dec0
forall d. Int -> Singleton d
Singleton Int
0)
        (Int -> Singleton Dec1
forall d. Int -> Singleton d
Singleton Int
1)
        (Int -> Singleton Dec2
forall d. Int -> Singleton d
Singleton Int
2)
        (Int -> Singleton Dec3
forall d. Int -> Singleton d
Singleton Int
3)
        (Int -> Singleton Dec4
forall d. Int -> Singleton d
Singleton Int
4)
        (Int -> Singleton Dec5
forall d. Int -> Singleton d
Singleton Int
5)
        (Int -> Singleton Dec6
forall d. Int -> Singleton d
Singleton Int
6)
        (Int -> Singleton Dec7
forall d. Int -> Singleton d
Singleton Int
7)
        (Int -> Singleton Dec8
forall d. Int -> Singleton d
Singleton Int
8)
        (Int -> Singleton Dec9
forall d. Int -> Singleton d
Singleton Int
9)

class C d where
    switch ::
        f Dec0 ->
        f Dec1 ->
        f Dec2 ->
        f Dec3 ->
        f Dec4 ->
        f Dec5 ->
        f Dec6 ->
        f Dec7 ->
        f Dec8 ->
        f Dec9 ->
        f d

class C d => Pos d where
    switchPos ::
        f Dec1 ->
        f Dec2 ->
        f Dec3 ->
        f Dec4 ->
        f Dec5 ->
        f Dec6 ->
        f Dec7 ->
        f Dec8 ->
        f Dec9 ->
        f d

data Dec0 deriving (Typeable)
instance C    Dec0 where switch :: f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec0
switch f Dec0
x f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec0
x
instance Show Dec0 where show :: Dec0 -> String
show Dec0
_ = String
"0"

data Dec1 deriving (Typeable)
instance Pos  Dec1 where switchPos :: f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec1
switchPos f Dec1
x f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec1
x
instance C    Dec1 where switch :: f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec1
switch  f Dec0
_ f Dec1
x f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec1
x
instance Show Dec1 where show :: Dec1 -> String
show Dec1
_ = String
"1"

data Dec2 deriving (Typeable)
instance Pos  Dec2 where switchPos :: f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec2
switchPos f Dec1
_ f Dec2
x f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec2
x
instance C    Dec2 where switch :: f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec2
switch  f Dec0
_ f Dec1
_ f Dec2
x f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec2
x
instance Show Dec2 where show :: Dec2 -> String
show Dec2
_ = String
"2"

data Dec3 deriving (Typeable)
instance Pos  Dec3 where switchPos :: f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec3
switchPos f Dec1
_ f Dec2
_ f Dec3
x f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec3
x
instance C    Dec3 where switch :: f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec3
switch  f Dec0
_ f Dec1
_ f Dec2
_ f Dec3
x f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec3
x
instance Show Dec3 where show :: Dec3 -> String
show Dec3
_ = String
"3"

data Dec4 deriving (Typeable)
instance Pos  Dec4 where switchPos :: f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec4
switchPos f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
x f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec4
x
instance C    Dec4 where switch :: f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec4
switch  f Dec0
_ f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
x f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec4
x
instance Show Dec4 where show :: Dec4 -> String
show Dec4
_ = String
"4"

data Dec5 deriving (Typeable)
instance Pos  Dec5 where switchPos :: f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec5
switchPos f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
x f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec5
x
instance C    Dec5 where switch :: f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec5
switch  f Dec0
_ f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
x f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
_ = f Dec5
x
instance Show Dec5 where show :: Dec5 -> String
show Dec5
_ = String
"5"

data Dec6 deriving (Typeable)
instance Pos  Dec6 where switchPos :: f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec6
switchPos f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
x f Dec7
_ f Dec8
_ f Dec9
_ = f Dec6
x
instance C    Dec6 where switch :: f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec6
switch  f Dec0
_ f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
x f Dec7
_ f Dec8
_ f Dec9
_ = f Dec6
x
instance Show Dec6 where show :: Dec6 -> String
show Dec6
_ = String
"6"

data Dec7 deriving (Typeable)
instance Pos  Dec7 where switchPos :: f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec7
switchPos f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
x f Dec8
_ f Dec9
_ = f Dec7
x
instance C    Dec7 where switch :: f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec7
switch  f Dec0
_ f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
x f Dec8
_ f Dec9
_ = f Dec7
x
instance Show Dec7 where show :: Dec7 -> String
show Dec7
_ = String
"7"

data Dec8 deriving (Typeable)
instance Pos  Dec8 where switchPos :: f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec8
switchPos f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
x f Dec9
_ = f Dec8
x
instance C    Dec8 where switch :: f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec8
switch  f Dec0
_ f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
x f Dec9
_ = f Dec8
x
instance Show Dec8 where show :: Dec8 -> String
show Dec8
_ = String
"8"

data Dec9 deriving (Typeable)
instance Pos  Dec9 where switchPos :: f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec9
switchPos f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
x = f Dec9
x
instance C    Dec9 where switch :: f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f Dec9
switch  f Dec0
_ f Dec1
_ f Dec2
_ f Dec3
_ f Dec4
_ f Dec5
_ f Dec6
_ f Dec7
_ f Dec8
_ f Dec9
x = f Dec9
x
instance Show Dec9 where show :: Dec9 -> String
show Dec9
_ = String
"9"


reify :: Integer -> (forall d. C d => Proxy d -> w) -> w
reify :: Integer -> (forall d. C d => Proxy d -> w) -> w
reify Integer
n forall d. C d => Proxy d -> w
f =
   if Integer
nInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
0
     then Proxy Dec0 -> w
forall d. C d => Proxy d -> w
f (Proxy Dec0
forall a. Proxy a
Proxy :: Proxy Dec0)
     else Integer -> (forall d. Pos d => Proxy d -> w) -> w
forall w. Integer -> (forall d. Pos d => Proxy d -> w) -> w
reifyPos Integer
n forall d. Pos d => Proxy d -> w
forall d. C d => Proxy d -> w
f

reifyPos :: Integer -> (forall d. Pos d => Proxy d -> w) -> w
reifyPos :: Integer -> (forall d. Pos d => Proxy d -> w) -> w
reifyPos Integer
n forall d. Pos d => Proxy d -> w
f =
   case Integer
n of
     Integer
1 -> Proxy Dec1 -> w
forall d. Pos d => Proxy d -> w
f (Proxy Dec1
forall a. Proxy a
Proxy :: Proxy Dec1)
     Integer
2 -> Proxy Dec2 -> w
forall d. Pos d => Proxy d -> w
f (Proxy Dec2
forall a. Proxy a
Proxy :: Proxy Dec2)
     Integer
3 -> Proxy Dec3 -> w
forall d. Pos d => Proxy d -> w
f (Proxy Dec3
forall a. Proxy a
Proxy :: Proxy Dec3)
     Integer
4 -> Proxy Dec4 -> w
forall d. Pos d => Proxy d -> w
f (Proxy Dec4
forall a. Proxy a
Proxy :: Proxy Dec4)
     Integer
5 -> Proxy Dec5 -> w
forall d. Pos d => Proxy d -> w
f (Proxy Dec5
forall a. Proxy a
Proxy :: Proxy Dec5)
     Integer
6 -> Proxy Dec6 -> w
forall d. Pos d => Proxy d -> w
f (Proxy Dec6
forall a. Proxy a
Proxy :: Proxy Dec6)
     Integer
7 -> Proxy Dec7 -> w
forall d. Pos d => Proxy d -> w
f (Proxy Dec7
forall a. Proxy a
Proxy :: Proxy Dec7)
     Integer
8 -> Proxy Dec8 -> w
forall d. Pos d => Proxy d -> w
f (Proxy Dec8
forall a. Proxy a
Proxy :: Proxy Dec8)
     Integer
9 -> Proxy Dec9 -> w
forall d. Pos d => Proxy d -> w
f (Proxy Dec9
forall a. Proxy a
Proxy :: Proxy Dec9)
     Integer
_ -> String -> w
forall a. HasCallStack => String -> a
error String
"digit must be a number from 0 to 9"


type family ToUnary n
type instance ToUnary Dec0 = UnaryLit.U0
type instance ToUnary Dec1 = UnaryLit.U1
type instance ToUnary Dec2 = UnaryLit.U2
type instance ToUnary Dec3 = UnaryLit.U3
type instance ToUnary Dec4 = UnaryLit.U4
type instance ToUnary Dec5 = UnaryLit.U5
type instance ToUnary Dec6 = UnaryLit.U6
type instance ToUnary Dec7 = UnaryLit.U7
type instance ToUnary Dec8 = UnaryLit.U8
type instance ToUnary Dec9 = UnaryLit.U9