clash-prelude-1.4.1: Clash: a functional hardware description language - Prelude library

Clash.Promoted.Nat

Description

Synopsis

# Singleton natural numbers

## Data type

data SNat (n :: Nat) where Source #

Singleton value for a type-level natural number n

Constructors

 SNat :: KnownNat n => SNat n

#### Instances

Instances details
 Lift (SNat n :: Type) Source # Instance detailsDefined in Clash.Promoted.Nat Methodslift :: SNat n -> Q Exp #liftTyped :: SNat n -> Q (TExp (SNat n)) # Show (SNat n) Source # Instance detailsDefined in Clash.Promoted.Nat MethodsshowsPrec :: Int -> SNat n -> ShowS #show :: SNat n -> String #showList :: [SNat n] -> ShowS # ShowX (SNat n) Source # Instance detailsDefined in Clash.Promoted.Nat MethodsshowsPrecX :: Int -> SNat n -> ShowS Source #showX :: SNat n -> String Source #showListX :: [SNat n] -> ShowS Source #

## Construction

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

Create an SNat n from a proxy for n

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

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

## Conversion

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

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

snatToNum :: forall a n. Num a => SNat n -> a Source #

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

## Conversion (ambiguous types)

natToInteger :: forall n. KnownNat n => Integer Source #

Same as snatToInteger and natVal, but doesn't take term arguments. Example usage:

>>> natToInteger @5
5


natToNatural :: forall n. KnownNat n => Natural Source #

Same as snatToNatural and natVal, but doesn't take term arguments. Example usage:

>>> natToNatural @5
5


natToNum :: forall n a. (Num a, KnownNat n) => a Source #

Same as snatToNum, but doesn't take term arguments. Example usage:

>>> natToNum @5 @Int
5


## Arithmetic

addSNat :: SNat a -> SNat b -> SNat (a + b) infixl 6 Source #

mulSNat :: SNat a -> SNat b -> SNat (a * b) infixl 7 Source #

Multiply two singleton natural numbers

powSNat :: SNat a -> SNat b -> SNat (a ^ b) infixr 8 Source #

Power of two singleton natural numbers

minSNat :: SNat a -> SNat b -> SNat (Min a b) Source #

maxSNat :: SNat a -> SNat b -> SNat (Max a b) Source #

succSNat :: SNat a -> SNat (a + 1) Source #

Successor of a singleton natural number

### Partial

subSNat :: SNat (a + b) -> SNat b -> SNat a infixl 6 Source #

Subtract two singleton natural numbers

divSNat :: 1 <= b => SNat a -> SNat b -> SNat (Div a b) infixl 7 Source #

Division of two singleton natural numbers

modSNat :: 1 <= b => SNat a -> SNat b -> SNat (Mod a b) infixl 7 Source #

Modulo of two singleton natural numbers

Arguments

 :: (2 <= base, 1 <= x) => SNat base Base -> SNat x -> SNat (FLog base x)

Floor of the logarithm of a natural number

Arguments

 :: (2 <= base, 1 <= x) => SNat base Base -> SNat x -> SNat (CLog base x)

Ceiling of the logarithm of a natural number

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

predSNat :: SNat (a + 1) -> SNat a Source #

Predecessor of a singleton natural number

### Specialised

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

Power of two of a singleton natural number

### Comparison

data SNatLE a b where Source #

Ordering relation between two Nats

Constructors

 SNatLE :: forall a b. a <= b => SNatLE a b SNatGT :: forall a b. (b + 1) <= a => SNatLE a b

compareSNat :: forall a b. SNat a -> SNat b -> SNatLE a b Source #

Get an ordering relation between two SNats

# Unary/Peano-encoded natural numbers

## Data type

data UNat :: Nat -> Type where Source #

Unary representation of a type-level natural

NB: Not synthesizable

Constructors

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

#### Instances

Instances details
 KnownNat n => Show (UNat n) Source # Instance detailsDefined in Clash.Promoted.Nat MethodsshowsPrec :: Int -> UNat n -> ShowS #show :: UNat n -> String #showList :: [UNat n] -> ShowS # KnownNat n => ShowX (UNat n) Source # Instance detailsDefined in Clash.Promoted.Nat MethodsshowsPrecX :: Int -> UNat n -> ShowS Source #showX :: UNat n -> String Source #showListX :: [UNat n] -> ShowS Source #

## Construction

toUNat :: forall n. SNat n -> UNat n Source #

Convert a singleton natural number to its unary representation

NB: Not synthesizable

## Conversion

fromUNat :: UNat n -> SNat n Source #

Convert a unary-encoded natural number to its singleton representation

NB: Not synthesizable

## Arithmetic

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

NB: Not synthesizable

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

Multiply two unary-encoded natural numbers

NB: Not synthesizable

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

Power of two unary-encoded natural numbers

NB: Not synthesizable

### Partial

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

Predecessor of a unary-encoded natural number

NB: Not synthesizable

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

Subtract two unary-encoded natural numbers

NB: Not synthesizable

# Base-2 encoded natural numbers

## Data type

data BNat :: Nat -> Type where Source #

Base-2 encoded natural number

• NB: The LSB is the left/outer-most constructor:
• NB: Not synthesizable
>>> 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

Instances details
 KnownNat n => Show (BNat n) Source # Instance detailsDefined in Clash.Promoted.Nat MethodsshowsPrec :: Int -> BNat n -> ShowS #show :: BNat n -> String #showList :: [BNat n] -> ShowS # KnownNat n => ShowX (BNat n) Source # Instance detailsDefined in Clash.Promoted.Nat MethodsshowsPrecX :: Int -> BNat n -> ShowS Source #showX :: BNat n -> String Source #showListX :: [BNat n] -> ShowS Source #

## Construction

toBNat :: SNat n -> BNat n Source #

Convert a singleton natural number to its base-2 representation

NB: Not synthesizable

## Conversion

fromBNat :: BNat n -> SNat n Source #

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

NB: Not synthesizable

## Pretty printing base-2 encoded natural numbers

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

Successor of a base-2 encoded natural number

NB: Not synthesizable

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

Add two base-2 encoded natural numbers

NB: Not synthesizable

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

Multiply two base-2 encoded natural numbers

NB: Not synthesizable

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

Power of two base-2 encoded natural numbers

NB: Not synthesizable

### Partial

predBNat :: 1 <= n => BNat n -> BNat (n - 1) Source #

Predecessor of a base-2 encoded natural number

NB: Not synthesizable

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

Divide a base-2 encoded natural number by 2

NB: Not synthesizable

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

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

NB: Not synthesizable

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

Get the log2 of a base-2 encoded natural number

NB: Not synthesizable

## Normalisation

stripZeros :: BNat n -> BNat n Source #

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 synthesizable

# Constraints on natural numbers

Arguments

 :: forall (k :: Nat) (n :: Nat) r. k <= n => (forall m. n ~ (k + m) => r) Context with the (n ~ (k + m)) constraint -> r

Change a function that has an argument with an (n ~ (k + m)) constraint to a function with an argument that has an (k <= n) constraint.

### Examples

Expand

Example 1

f :: Index (n+1) -> Index (n + 1) -> Bool

g :: forall n. (1 <= n) => Index n -> Index n -> Bool
g a b = leToPlus @1 @n (f a b)


Example 2

head :: Vec (n + 1) a -> a

head' :: forall n a. (1 <= n) => Vec n a -> a
head' = leToPlus 1 n head


Arguments

 :: forall (k :: Nat) (n :: Nat) r. (k <= n, KnownNat k, KnownNat n) => (forall m. (n ~ (k + m), KnownNat m) => r) Context with the (n ~ (k + m)) constraint -> r

Same as leToPlus with added KnownNat constraints