type-level-show-0.3.0: Utilities for writing Show-like type families
Safe HaskellSafe-Inferred
LanguageGHC2021

TypeLevelShow.Natural

Description

Turn type-level Naturals into Symbols.

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.

Synopsis

Documentation

type ShowNatBin n = ShowNatBase 2 ShowNatDigitHexLowerSym n Source #

type ShowNatOct n = ShowNatBase 8 ShowNatDigitHexLowerSym n Source #

type ShowNatDec n = ShowNatBase 10 ShowNatDigitHexLowerSym n Source #

type ShowNatHexLower n = ShowNatBase 16 ShowNatDigitHexLowerSym n Source #

type ShowNatHexUpper n = ShowNatBase 16 ShowNatDigitHexUpperSym n Source #

sShowNatBin :: SNat n -> SSymbol (ShowNatBin n) Source #

sShowNatOct :: SNat n -> SSymbol (ShowNatOct n) Source #

sShowNatDec :: SNat n -> SSymbol (ShowNatDec n) Source #

sShowNatHexLower :: SNat n -> SSymbol (ShowNatHexLower n) Source #

sShowNatHexUpper :: SNat n -> SSymbol (ShowNatHexUpper n) Source #

type family ShowNatBase base showDigit n where ... Source #

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.

Equations

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) Source #

type family ShowNatBase' base showDigit acc n where ... Source #

Equations

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) Source #