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

Copyright | (C) 2013-2016 University of Twente 2016 Myrtle Software Ltd 2022 QBayLogic B.V.
License | BSD2 (see the file LICENSE)
Maintainer | QBayLogic B.V. <devops@qbaylogic.com>
Safe Haskell | Trustworthy
Language | Haskell2010

Extensions

- Cpp
- MonoLocalBinds
- TemplateHaskell
- TemplateHaskellQuotes
- ScopedTypeVariables
- AllowAmbiguousTypes
- BangPatterns
- ViewPatterns
- GADTs
- GADTSyntax
- DataKinds
- InstanceSigs
- StandaloneDeriving
- DeriveDataTypeable
- DeriveFunctor
- DeriveTraversable
- DeriveFoldable
- DeriveGeneric
- DefaultSignatures
- DeriveLift
- DerivingStrategies
- MagicHash
- KindSignatures
- PostfixOperators
- TupleSections
- RankNTypes
- TypeOperators
- ExplicitNamespaces
- ExplicitForAll
- BinaryLiterals
- TypeApplications

Clash.Promoted.Nat

Contents

- Singleton natural numbers
  - Data type
  - Construction
  - Conversion
  - Conversion (ambiguous types)
  - Arithmetic
    - Partial
    - Specialised
    - Comparison
- Unary/Peano-encoded natural numbers
  - Data type
  - Construction
  - Conversion
  - Arithmetic
    - Partial
- Base-2 encoded natural numbers
  - Data type
  - Construction
  - Conversion
  - Pretty printing base-2 encoded natural numbers
  - Arithmetic
    - Partial
  - Normalisation
- Constraints on natural numbers

Description

Synopsis

- data SNat (n :: Nat) where
  - SNat :: forall (n :: Nat). KnownNat n => SNat n
- snatProxy :: forall (n :: Nat) proxy. KnownNat n => proxy n -> SNat n
- withSNat :: forall (n :: Nat) a. KnownNat n => (SNat n -> a) -> a
- snatToInteger :: forall (n :: Nat). SNat n -> Integer
- snatToNatural :: forall (n :: Nat). SNat n -> Natural
- snatToNum :: forall a (n :: Nat). Num a => SNat n -> a
- natToInteger :: forall (n :: Nat). KnownNat n => Integer
- natToNatural :: forall (n :: Nat). KnownNat n => Natural
- natToNum :: forall (n :: Nat) a. (Num a, KnownNat n) => a
- addSNat :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNat (a + b)
- mulSNat :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNat (a * b)
- powSNat :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNat (a ^ b)
- minSNat :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNat (Min a b)
- maxSNat :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNat (Max a b)
- succSNat :: forall (a :: Nat). SNat a -> SNat (a + 1)
- subSNat :: forall (a :: Natural) (b :: Natural). SNat (a + b) -> SNat b -> SNat a
- divSNat :: forall (b :: Natural) (a :: Nat). 1 <= b => SNat a -> SNat b -> SNat (Div a b)
- modSNat :: forall (b :: Natural) (a :: Nat). 1 <= b => SNat a -> SNat b -> SNat (Mod a b)
- flogBaseSNat :: forall (base :: Natural) (x :: Natural). (2 <= base, 1 <= x) => SNat base -> SNat x -> SNat (FLog base x)
- clogBaseSNat :: forall (base :: Natural) (x :: Natural). (2 <= base, 1 <= x) => SNat base -> SNat x -> SNat (CLog base x)
- logBaseSNat :: forall (base :: Nat) (x :: Nat). FLog base x ~ CLog base x => SNat base -> SNat x -> SNat (Log base x)
- predSNat :: forall (a :: Natural). SNat (a + 1) -> SNat a
- pow2SNat :: forall (a :: Nat). SNat a -> SNat (2 ^ a)
- data SNatLE (a :: Natural) (b :: Natural) where
  - SNatLE :: forall (a :: Natural) (b :: Natural). a <= b => SNatLE a b
  - SNatGT :: forall (a :: Natural) (b :: Natural). (b + 1) <= a => SNatLE a b
- compareSNat :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
- data UNat (a :: Nat) where
  - UZero :: UNat 0
  - USucc :: forall (n :: Natural). UNat n -> UNat (n + 1)
- toUNat :: forall (n :: Nat). SNat n -> UNat n
- fromUNat :: forall (n :: Nat). UNat n -> SNat n
- addUNat :: forall (n :: Nat) (m :: Nat). UNat n -> UNat m -> UNat (n + m)
- mulUNat :: forall (n :: Nat) (m :: Nat). UNat n -> UNat m -> UNat (n * m)
- powUNat :: forall (n :: Nat) (m :: Nat). UNat n -> UNat m -> UNat (n ^ m)
- predUNat :: forall (n :: Natural). UNat (n + 1) -> UNat n
- subUNat :: forall (m :: Natural) (n :: Natural). UNat (m + n) -> UNat n -> UNat m
- data BNat (a :: Nat) where
  - BT :: BNat 0
  - B0 :: forall (n :: Natural). BNat n -> BNat (2 * n)
  - B1 :: forall (n :: Natural). BNat n -> BNat ((2 * n) + 1)
- toBNat :: forall (n :: Nat). SNat n -> BNat n
- fromBNat :: forall (n :: Nat). BNat n -> SNat n
- showBNat :: forall (n :: Nat). BNat n -> String
- succBNat :: forall (n :: Nat). BNat n -> BNat (n + 1)
- addBNat :: forall (n :: Nat) (m :: Nat). BNat n -> BNat m -> BNat (n + m)
- mulBNat :: forall (n :: Nat) (m :: Nat). BNat n -> BNat m -> BNat (n * m)
- powBNat :: forall (n :: Nat) (m :: Nat). BNat n -> BNat m -> BNat (n ^ m)
- predBNat :: forall (n :: Natural). 1 <= n => BNat n -> BNat (n - 1)
- div2BNat :: forall (n :: Natural). BNat (2 * n) -> BNat n
- div2Sub1BNat :: forall (n :: Natural). BNat ((2 * n) + 1) -> BNat n
- log2BNat :: forall (n :: Natural). BNat (2 ^ n) -> BNat n
- stripZeros :: forall (n :: Nat). BNat n -> BNat n
- leToPlus :: forall (k :: Nat) (n :: Nat) r. k <= n => (forall (m :: Natural). n ~ (k + m) => r) -> r
- leToPlusKN :: forall (k :: Nat) (n :: Nat) r. (k <= n, KnownNat k, KnownNat n) => (forall (m :: Natural). (n ~ (k + m), KnownNat m) => r) -> r

# Singleton natural numbers

## Data type

data SNat (n :: Nat) where Source #

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 :: forall (n :: Nat). KnownNat n => SNat n |

#### Instances

Instances details

Lift (SNat n :: Type) Source # |
Instance details Defined in Clash.Promoted.Nat Methods lift :: Quote m => SNat n -> m Exp Source # liftTyped :: forall (m :: Type -> Type). Quote m => SNat n -> Code m (SNat n) Source #
ShowX (SNat n) Source # |
Instance details Defined in Clash.Promoted.Nat Methods showsPrecX :: Int -> SNat n -> ShowS Source # showX :: SNat n -> String Source # showListX :: [SNat n] -> ShowS Source #
Show (SNat n) Source # |
Instance details Defined in Clash.Promoted.Nat Methods showsPrec :: Int -> SNat n -> ShowS Source # show :: SNat n -> String Source # showList :: [SNat n] -> ShowS Source #

## Construction

snatProxy :: forall (n :: Nat) proxy. KnownNat n => proxy n -> SNat n Source #

Create an ``SNat` n` from a proxy for n

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

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

## Conversion

snatToInteger :: forall (n :: Nat). SNat n -> Integer Source #

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

snatToNatural :: forall (n :: Nat). SNat n -> Natural Source #

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

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

Reify the type-level `Nat` `n` to it's term-level `Num`ber.

## Conversion (ambiguous types)

natToInteger :: forall (n :: Nat). KnownNat n => Integer Source #

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

    >>> natToInteger @5
    5

natToNatural :: forall (n :: Nat). KnownNat n => Natural Source #

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

    >>> natToNatural @5
    5

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

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

    >>> natToNum @5 @Int
    5

## Arithmetic

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

Add two singleton natural numbers

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

Multiply two singleton natural numbers

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

Power of two singleton natural numbers

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

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

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

Successor of a singleton natural number

### Partial

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

Subtract two singleton natural numbers

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

Division of two singleton natural numbers

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

Modulo of two singleton natural numbers

flogBaseSNat Source #

Arguments

:: forall (base :: Natural) (x :: Natural). (2 <= base, 1 <= x) |
=> SNat base | Base
-> SNat x |
-> SNat (FLog base x) |

Floor of the logarithm of a natural number

clogBaseSNat Source #

Arguments

:: forall (base :: Natural) (x :: Natural). (2 <= base, 1 <= x) |
=> SNat base | Base
-> SNat x |
-> SNat (CLog base x) |

Ceiling of the logarithm of a natural number

logBaseSNat Source #

Arguments

:: forall (base :: Nat) (x :: Nat). 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 :: forall (a :: Natural). SNat (a + 1) -> SNat a Source #

Predecessor of a singleton natural number

### Specialised

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

Power of two of a singleton natural number

### Comparison

data SNatLE (a :: Natural) (b :: Natural) where Source #

Ordering relation between two Nats

Constructors

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

#### Instances

Instances details

Show (SNatLE a b) Source # |
Instance details Defined in Clash.Promoted.Nat Methods showsPrec :: Int -> SNatLE a b -> ShowS Source # show :: SNatLE a b -> String Source # showList :: [SNatLE a b] -> ShowS Source #

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

Get an ordering relation between two SNats

# Unary/Peano-encoded natural numbers

## Data type

data UNat (a :: Nat) where Source #

Unary representation of a type-level natural

NB: Not synthesizable

Constructors

UZero :: UNat 0 |
USucc :: forall (n :: Natural). UNat n -> UNat (n + 1) |

#### Instances

Instances details

KnownNat n => ShowX (UNat n) Source # |
Instance details Defined in Clash.Promoted.Nat Methods showsPrecX :: Int -> UNat n -> ShowS Source # showX :: UNat n -> String Source # showListX :: [UNat n] -> ShowS Source #
KnownNat n => Show (UNat n) Source # |
Instance details Defined in Clash.Promoted.Nat Methods showsPrec :: Int -> UNat n -> ShowS Source # show :: UNat n -> String Source # showList :: [UNat n] -> ShowS Source #

## Construction

toUNat :: forall (n :: Nat). SNat n -> UNat n Source #

Convert a singleton natural number to its unary representation

NB: Not synthesizable

## Conversion

fromUNat :: forall (n :: Nat). UNat n -> SNat n Source #

Convert a unary-encoded natural number to its singleton representation

NB: Not synthesizable

## Arithmetic

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

Add two unary-encoded natural numbers

NB: Not synthesizable

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

Multiply two unary-encoded natural numbers

NB: Not synthesizable

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

Power of two unary-encoded natural numbers

NB: Not synthesizable

### Partial

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

Predecessor of a unary-encoded natural number

NB: Not synthesizable

subUNat :: forall (m :: Natural) (n :: Natural). 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 (a :: Nat) 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 :: forall (n :: Natural). BNat n -> BNat (2 * n) |
B1 :: forall (n :: Natural). BNat n -> BNat ((2 * n) + 1) |

#### Instances

Instances details

KnownNat n => ShowX (BNat n) Source # |
Instance details Defined in Clash.Promoted.Nat Methods showsPrecX :: Int -> BNat n -> ShowS Source # showX :: BNat n -> String Source # showListX :: [BNat n] -> ShowS Source #
KnownNat n => Show (BNat n) Source # |
Instance details Defined in Clash.Promoted.Nat Methods showsPrec :: Int -> BNat n -> ShowS Source # show :: BNat n -> String Source # showList :: [BNat n] -> ShowS Source #

## Construction

toBNat :: forall (n :: Nat). SNat n -> BNat n Source #

Convert a singleton natural number to its base-2 representation

NB: Not synthesizable

## Conversion

fromBNat :: forall (n :: Nat). 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

showBNat :: forall (n :: Nat). BNat n -> String Source #

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 :: forall (n :: Nat). BNat n -> BNat (n + 1) Source #

Successor of a base-2 encoded natural number

NB: Not synthesizable

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

Add two base-2 encoded natural numbers

NB: Not synthesizable

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

Multiply two base-2 encoded natural numbers

NB: Not synthesizable

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

Power of two base-2 encoded natural numbers

NB: Not synthesizable

### Partial

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

Predecessor of a base-2 encoded natural number

NB: Not synthesizable

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

Divide a base-2 encoded natural number by 2

NB: Not synthesizable

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

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

NB: Not synthesizable

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

Get the log2 of a base-2 encoded natural number

NB: Not synthesizable

## Normalisation

stripZeros :: forall (n :: Nat). 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

leToPlus Source #

Arguments

:: forall (k :: Nat) (n :: Nat) r. k <= n |
=> (forall (m :: Natural). 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

leToPlusKN Source #

Arguments

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

Same as `leToPlus` with added `KnownNat` constraints