{-# LANGUAGE UndecidableInstances #-}

{- | Turn type-level 'Natural's into 'Symbol's.

/Warning:/ GHC may error out if you pass an 'SNat' that's too large to the
singled functions, due to reduction stack size. Follow the error message
instructions if you think you need it. This seems not to happen with @:k!@,
probably due to different settings.
-}

module TypeLevelShow.Natural where

import TypeLevelShow.Natural.Digit
import Singleraeh.Natural
import Singleraeh.Equality ( testEqElse )
import Singleraeh.Symbol ( sConsSymbol )
import GHC.TypeLits
import DeFun.Core
import Unsafe.Coerce ( unsafeCoerce )

type ShowNatBin      n = ShowNatBase  2 ShowNatDigitHexLowerSym n
type ShowNatOct      n = ShowNatBase  8 ShowNatDigitHexLowerSym n
type ShowNatDec      n = ShowNatBase 10 ShowNatDigitHexLowerSym n
type ShowNatHexLower n = ShowNatBase 16 ShowNatDigitHexLowerSym n
type ShowNatHexUpper n = ShowNatBase 16 ShowNatDigitHexUpperSym n

sShowNatBin :: SNat n -> SSymbol (ShowNatBin n)
sShowNatBin :: forall (n :: Nat). SNat n -> SSymbol (ShowNatBin n)
sShowNatBin = SNat 2
-> Lam SNat SChar ShowNatDigitHexLowerSym
-> SNat n
-> SSymbol (ShowNatBase 2 ShowNatDigitHexLowerSym n)
forall (base :: Nat) (showDigit :: Nat ~> Char) (n :: Nat).
SNat base
-> Lam SNat SChar showDigit
-> SNat n
-> SSymbol (ShowNatBase base showDigit n)
sShowNatBase (forall (n :: Nat). KnownNat n => SNat n
SNat @2) Lam SNat SChar ShowNatDigitHexLowerSym
sShowNatDigitHexLower

sShowNatOct :: SNat n -> SSymbol (ShowNatOct n)
sShowNatOct :: forall (n :: Nat). SNat n -> SSymbol (ShowNatOct n)
sShowNatOct = SNat 8
-> Lam SNat SChar ShowNatDigitHexLowerSym
-> SNat n
-> SSymbol (ShowNatBase 8 ShowNatDigitHexLowerSym n)
forall (base :: Nat) (showDigit :: Nat ~> Char) (n :: Nat).
SNat base
-> Lam SNat SChar showDigit
-> SNat n
-> SSymbol (ShowNatBase base showDigit n)
sShowNatBase (forall (n :: Nat). KnownNat n => SNat n
SNat @8) Lam SNat SChar ShowNatDigitHexLowerSym
sShowNatDigitHexLower

sShowNatDec :: SNat n -> SSymbol (ShowNatDec n)
sShowNatDec :: forall (n :: Nat). SNat n -> SSymbol (ShowNatDec n)
sShowNatDec = SNat 10
-> Lam SNat SChar ShowNatDigitHexLowerSym
-> SNat n
-> SSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n)
forall (base :: Nat) (showDigit :: Nat ~> Char) (n :: Nat).
SNat base
-> Lam SNat SChar showDigit
-> SNat n
-> SSymbol (ShowNatBase base showDigit n)
sShowNatBase (forall (n :: Nat). KnownNat n => SNat n
SNat @10) Lam SNat SChar ShowNatDigitHexLowerSym
sShowNatDigitHexLower

sShowNatHexLower :: SNat n -> SSymbol (ShowNatHexLower n)
sShowNatHexLower :: forall (n :: Nat). SNat n -> SSymbol (ShowNatHexLower n)
sShowNatHexLower = SNat 16
-> Lam SNat SChar ShowNatDigitHexLowerSym
-> SNat n
-> SSymbol (ShowNatBase 16 ShowNatDigitHexLowerSym n)
forall (base :: Nat) (showDigit :: Nat ~> Char) (n :: Nat).
SNat base
-> Lam SNat SChar showDigit
-> SNat n
-> SSymbol (ShowNatBase base showDigit n)
sShowNatBase (forall (n :: Nat). KnownNat n => SNat n
SNat @16) Lam SNat SChar ShowNatDigitHexLowerSym
sShowNatDigitHexLower

sShowNatHexUpper :: SNat n -> SSymbol (ShowNatHexUpper n)
sShowNatHexUpper :: forall (n :: Nat). SNat n -> SSymbol (ShowNatHexUpper n)
sShowNatHexUpper = SNat 16
-> Lam SNat SChar ShowNatDigitHexUpperSym
-> SNat n
-> SSymbol (ShowNatBase 16 ShowNatDigitHexUpperSym n)
forall (base :: Nat) (showDigit :: Nat ~> Char) (n :: Nat).
SNat base
-> Lam SNat SChar showDigit
-> SNat n
-> SSymbol (ShowNatBase base showDigit n)
sShowNatBase (forall (n :: Nat). KnownNat n => SNat n
SNat @16) Lam SNat SChar ShowNatDigitHexUpperSym
sShowNatDigitHexUpper

-- | Render a type-level 'Natural' in the given base using the given digit
--   renderer.
--
-- The digit renderer is guaranteed to be called with @0 <= n < base@.
type family ShowNatBase base showDigit n where
    -- | Our algorithm returns the empty 'Symbol' for 0, so handle it here.
    ShowNatBase base showDigit 0 = "0"
    ShowNatBase base showDigit n = ShowNatBase' base showDigit "" n

sShowNatBase
    :: SNat base -> Lam SNat SChar showDigit -> SNat n
    -> SSymbol (ShowNatBase base showDigit n)
sShowNatBase :: forall (base :: Nat) (showDigit :: Nat ~> Char) (n :: Nat).
SNat base
-> Lam SNat SChar showDigit
-> SNat n
-> SSymbol (ShowNatBase base showDigit n)
sShowNatBase SNat base
sbase Lam SNat SChar showDigit
sf SNat n
sn =
      SNat n
-> SNat 0
-> ((n ~ 0) => SSymbol (ShowNatBase base showDigit n))
-> SSymbol (ShowNatBase base showDigit n)
-> SSymbol (ShowNatBase base showDigit n)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat n
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @0) (forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol @"0")
    (SSymbol (ShowNatBase base showDigit n)
 -> SSymbol (ShowNatBase base showDigit n))
-> SSymbol (ShowNatBase base showDigit n)
-> SSymbol (ShowNatBase base showDigit n)
forall a b. (a -> b) -> a -> b
$ SSymbol (ShowNatBase' base showDigit "" n)
-> SSymbol (ShowNatBase base showDigit n)
forall a b. a -> b
unsafeCoerce (SSymbol (ShowNatBase' base showDigit "" n)
 -> SSymbol (ShowNatBase base showDigit n))
-> SSymbol (ShowNatBase' base showDigit "" n)
-> SSymbol (ShowNatBase base showDigit n)
forall a b. (a -> b) -> a -> b
$ SNat base
-> Lam SNat SChar showDigit
-> SSymbol ""
-> SNat n
-> SSymbol (ShowNatBase' base showDigit "" n)
forall (base :: Nat) (showDigit :: Nat ~> Char) (acc :: Symbol)
       (n :: Nat).
SNat base
-> Lam SNat SChar showDigit
-> SSymbol acc
-> SNat n
-> SSymbol (ShowNatBase' base showDigit acc n)
sShowNatBase' SNat base
sbase Lam SNat SChar showDigit
sf (forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol @"") SNat n
sn

type ShowNatBase' :: Natural -> (Natural ~> Char) -> Symbol -> Natural -> Symbol
type family ShowNatBase' base showDigit acc n where
    ShowNatBase' base showDigit acc 0 = acc
    ShowNatBase' base showDigit acc n = ShowNatBase' base showDigit
        (ConsSymbol (showDigit @@ (n `Mod` base)) acc) (n `Div` base)

sShowNatBase'
    :: SNat base -> Lam SNat SChar showDigit -> SSymbol acc -> SNat n
    -> SSymbol (ShowNatBase' base showDigit acc n)
sShowNatBase' :: forall (base :: Nat) (showDigit :: Nat ~> Char) (acc :: Symbol)
       (n :: Nat).
SNat base
-> Lam SNat SChar showDigit
-> SSymbol acc
-> SNat n
-> SSymbol (ShowNatBase' base showDigit acc n)
sShowNatBase' SNat base
sbase Lam SNat SChar showDigit
sShowDigit SSymbol acc
sacc SNat n
sn =
      SNat n
-> SNat 0
-> ((n ~ 0) => SSymbol (ShowNatBase' base showDigit acc n))
-> SSymbol (ShowNatBase' base showDigit acc n)
-> SSymbol (ShowNatBase' base showDigit acc n)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat n
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @0) SSymbol acc
SSymbol (ShowNatBase' base showDigit acc n)
(n ~ 0) => SSymbol (ShowNatBase' base showDigit acc n)
sacc
    (SSymbol (ShowNatBase' base showDigit acc n)
 -> SSymbol (ShowNatBase' base showDigit acc n))
-> SSymbol (ShowNatBase' base showDigit acc n)
-> SSymbol (ShowNatBase' base showDigit acc n)
forall a b. (a -> b) -> a -> b
$ SSymbol
  (ShowNatBase'
     base
     showDigit
     (ConsSymbol (App showDigit (Mod n base)) acc)
     (Div n base))
-> SSymbol (ShowNatBase' base showDigit acc n)
forall a b. a -> b
unsafeCoerce (SSymbol
   (ShowNatBase'
      base
      showDigit
      (ConsSymbol (App showDigit (Mod n base)) acc)
      (Div n base))
 -> SSymbol (ShowNatBase' base showDigit acc n))
-> SSymbol
     (ShowNatBase'
        base
        showDigit
        (ConsSymbol (App showDigit (Mod n base)) acc)
        (Div n base))
-> SSymbol (ShowNatBase' base showDigit acc n)
forall a b. (a -> b) -> a -> b
$
        SNat base
-> Lam SNat SChar showDigit
-> SSymbol (ConsSymbol (App showDigit (Mod n base)) acc)
-> SNat (Div n base)
-> SSymbol
     (ShowNatBase'
        base
        showDigit
        (ConsSymbol (App showDigit (Mod n base)) acc)
        (Div n base))
forall (base :: Nat) (showDigit :: Nat ~> Char) (acc :: Symbol)
       (n :: Nat).
SNat base
-> Lam SNat SChar showDigit
-> SSymbol acc
-> SNat n
-> SSymbol (ShowNatBase' base showDigit acc n)
sShowNatBase' SNat base
sbase Lam SNat SChar showDigit
sShowDigit
          (SChar (App showDigit (Mod n base))
-> SSymbol acc
-> SSymbol (ConsSymbol (App showDigit (Mod n base)) acc)
forall (ch :: Char) (str :: Symbol).
SChar ch -> SSymbol str -> SSymbol (ConsSymbol ch str)
sConsSymbol (Lam SNat SChar showDigit
sShowDigit Lam SNat SChar showDigit
-> SNat (Mod n base) -> SChar (App showDigit (Mod n base))
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ (SNat n
sn SNat n -> SNat base -> SNat (Mod n base)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Mod n m)
`sMod` SNat base
sbase)) SSymbol acc
sacc)
          (SNat n
sn SNat n -> SNat base -> SNat (Div n base)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Div n m)
`sDiv` SNat base
sbase)