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
Unary/Peano-encoded natural numbers
Base-2 encoded natural numbers
Constraints on natural numbers

Description

Synopsis

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

Instances

Instances details

Lift (SNat n :: Type) Source #
Instance details Defined in Clash.Promoted.Nat Methods lift :: SNat n -> Q Exp # liftTyped :: SNat n -> Q (TExp (SNat n)) #
Show (SNat n) Source #
Instance details Defined in Clash.Promoted.Nat Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
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 #

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

snatToInteger :: SNat n -> Integer Source #

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

snatToNatural :: SNat n -> Natural Source #

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 #

Add two singleton natural numbers

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

flogBaseSNat Source #

Arguments

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

Floor of the logarithm of a natural number

clogBaseSNat Source #

Arguments

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

Ceiling of the logarithm of a natural number

logBaseSNat Source #

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

Instances

Instances details

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

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 details Defined in Clash.Promoted.Nat Methods showsPrec :: Int -> UNat n -> ShowS # show :: UNat n -> String # showList :: [UNat n] -> ShowS #
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 #

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 #

Add two unary-encoded natural numbers

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 details Defined in Clash.Promoted.Nat Methods showsPrec :: Int -> BNat n -> ShowS # show :: BNat n -> String # showList :: [BNat n] -> ShowS #
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 #

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

showBNat :: 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 :: 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

leToPlus Source #

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

leToPlusKN Source #

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