CLaSH.Promoted.Nat

Singleton natural numbers

Data type

data SNat n where

Singleton value for a type-level natural number n

• CLaSH.Promoted.Nat.Literals contains a list of predefined SNat literals
• CLaSH.Promoted.Nat.TH has functions to easily create large ranges of new SNat literals

Constructors

SNat :: KnownNat n => SNat n

Instances

Show (SNat n)

Methods

showsPrec :: Int -> SNat n -> ShowS

show :: SNat n -> String

showList :: [SNat n] -> ShowS

Lift (SNat n)

Methods

lift :: SNat n -> Q Exp

ShowX (SNat n)

Methods

showsPrecX :: Int -> SNat n -> ShowS

showX :: SNat n -> String

showListX :: [SNat n] -> ShowS

Construction

snatProxy :: KnownNat n => proxy n -> SNat n

Create an SNat n from a proxy for n

withSNat :: KnownNat n => (SNat n -> a) -> a

Supply a function with a singleton natural n according to the context

snat :: KnownNat n => SNat n

Deprecated: Use SNat instead of snat

Create a singleton literal for a type-level natural number

Conversion

snatToInteger :: SNat n -> Integer

Reify the type-level Nat n to it's term-level Integer representation.

snatToNum :: Num a => SNat n -> a

Reify the type-level Nat n to it's term-level Number.

Arithmetic

addSNat :: SNat a -> SNat b -> SNat (a + b)

Add two singleton natural numbers

mulSNat :: SNat a -> SNat b -> SNat (a * b)

Multiply two singleton natural numbers

powSNat :: SNat a -> SNat b -> SNat (a ^ b)

Power of two singleton natural numbers

Partial

subSNat :: SNat (a + b) -> SNat b -> SNat a

Subtract two singleton natural numbers

divSNat :: 1 <= b => SNat a -> SNat b -> SNat (Div a b)

Division of two singleton natural numbers

modSNat :: 1 <= b => SNat a -> SNat b -> SNat (Mod a b)

Modulo of two singleton natural numbers

flogBaseSNat

Arguments

:: (2 <= base, 1 <= x)

=> SNat base

Base

-> SNat x

-> SNat (FLog base x)

Floor of the logarithm of a natural number

clogBaseSNat

Arguments

:: (2 <= base, 1 <= x)

=> SNat base

Base

-> SNat x

-> SNat (CLog base x)

Ceiling of the logarithm of a natural number

logBaseSNat

Arguments

:: FLog base x ~ CLog base x

=> SNat base

Base

-> SNat x

-> SNat (Log base x)

Exact integer logarithm of a natural number

NB: Only works when the argument is a power of the base

Specialised

pow2SNat :: SNat a -> SNat (2 ^ a)

Power of two of a singleton natural number

Unary/Peano-encoded natural numbers

Data type

data UNat :: Nat -> * where

Unary representation of a type-level natural

NB: Not synthesisable

Constructors

UZero :: UNat 0

USucc :: UNat n -> UNat (n + 1)

Instances

KnownNat n => Show (UNat n)

Methods

showsPrec :: Int -> UNat n -> ShowS

show :: UNat n -> String

showList :: [UNat n] -> ShowS

KnownNat n => ShowX (UNat n)

Methods

showsPrecX :: Int -> UNat n -> ShowS

showX :: UNat n -> String

showListX :: [UNat n] -> ShowS

Construction

toUNat :: SNat n -> UNat n

Convert a singleton natural number to its unary representation

NB: Not synthesisable

Conversion

fromUNat :: UNat n -> SNat n

Convert a unary-encoded natural number to its singleton representation

NB: Not synthesisable

Arithmetic

addUNat :: UNat n -> UNat m -> UNat (n + m)

Add two unary-encoded natural numbers

NB: Not synthesisable

mulUNat :: UNat n -> UNat m -> UNat (n * m)

Multiply two unary-encoded natural numbers

NB: Not synthesisable

powUNat :: UNat n -> UNat m -> UNat (n ^ m)

Power of two unary-encoded natural numbers

NB: Not synthesisable

Partial

predUNat :: UNat (n + 1) -> UNat n

Predecessor of a unary-encoded natural number

NB: Not synthesisable

subUNat :: UNat (m + n) -> UNat n -> UNat m

Subtract two unary-encoded natural numbers

NB: Not synthesisable

Base-2 encoded natural numbers

Data type

data BNat :: Nat -> * where

Base-2 encoded natural number

• NB: The LSB is the left/outer-most constructor:
• NB: Not synthesisable

>>> B0 (B1 (B1 BT))
b6

Constructors

• Starting/Terminating element:

  BT :: BNat 0
  

• Append a zero (0):

  B0 :: BNat n -> BNat (2 * n)
  

• Append a one (1):

  B1 :: BNat n -> BNat ((2 * n) + 1)
  

Constructors

BT :: BNat 0

B0 :: BNat n -> BNat (2 * n)

B1 :: BNat n -> BNat ((2 * n) + 1)

Instances

KnownNat n => Show (BNat n)

Methods

showsPrec :: Int -> BNat n -> ShowS

show :: BNat n -> String

showList :: [BNat n] -> ShowS

KnownNat n => ShowX (BNat n)

Methods

showsPrecX :: Int -> BNat n -> ShowS

showX :: BNat n -> String

showListX :: [BNat n] -> ShowS

Construction

toBNat :: SNat n -> BNat n

Convert a singleton natural number to its base-2 representation

NB: Not synthesisable

Conversion

fromBNat :: BNat n -> SNat n

Convert a base-2 encoded natural number to its singleton representation

NB: Not synthesisable

Pretty printing base-2 encoded natural numbers

showBNat :: BNat n -> String

Show a base-2 encoded natural as a binary literal

NB: The LSB is shown as the right-most bit

>>> d789
d789
>>> toBNat d789
b789
>>> showBNat (toBNat d789)
"0b1100010101"
>>> 0b1100010101 :: Integer
789

Arithmetic

succBNat :: BNat n -> BNat (n + 1)

Successor of a base-2 encoded natural number

NB: Not synthesisable

addBNat :: BNat n -> BNat m -> BNat (n + m)

Add two base-2 encoded natural numbers

NB: Not synthesisable

mulBNat :: BNat n -> BNat m -> BNat (n * m)

Multiply two base-2 encoded natural numbers

NB: Not synthesisable

powBNat :: BNat n -> BNat m -> BNat (n ^ m)

Power of two base-2 encoded natural numbers

NB: Not synthesisable

Partial

predBNat :: BNat (n + 1) -> BNat n

Predecessor of a base-2 encoded natural number

NB: Not synthesisable

div2BNat :: BNat (2 * n) -> BNat n

Divide a base-2 encoded natural number by 2

NB: Not synthesisable

div2Sub1BNat :: BNat ((2 * n) + 1) -> BNat n

Subtract 1 and divide a base-2 encoded natural number by 2

NB: Not synthesisable

log2BNat :: BNat (2 ^ n) -> BNat n

Get the log2 of a base-2 encoded natural number

NB: Not synthesisable

Normalisation

stripZeros :: BNat n -> BNat n

Strip non-contributing zero's from a base-2 encoded natural number

>>> B1 (B0 (B0 (B0 BT)))
b1
>>> showBNat (B1 (B0 (B0 (B0 BT))))
"0b0001"
>>> showBNat (stripZeros (B1 (B0 (B0 (B0 BT)))))
"0b1"
>>> stripZeros (B1 (B0 (B0 (B0 BT))))
b1

NB: Not synthesisable