Copyright	(C) 2013-2016 University of Twente 2016 Myrtle Software Ltd
License	BSD2 (see the file LICENSE)
Maintainer	Christiaan Baaij <christiaan.baaij@gmail.com>
Safe Haskell	Trustworthy
Language	Haskell2010
Extensions	MonoLocalBinds TemplateHaskell TemplateHaskellQuotes ScopedTypeVariables AllowAmbiguousTypes GADTs GADTSyntax DataKinds MagicHash KindSignatures RankNTypes TypeOperators ExplicitNamespaces ExplicitForAll 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
snatToNum :: Num a => SNat 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)
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)
pow2SNat :: SNat a -> SNat (2 ^ a)
data UNat :: Nat -> * where
- UZero :: UNat 0
- USucc :: UNat n -> UNat (n + 1)
toUNat :: 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 -> * 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) f r. k <= n => f n -> (forall m. f (m + k) -> r) -> r
leToPlusKN :: forall (k :: Nat) (n :: Nat) f r. (k <= n, KnownNat n, KnownNat k) => f n -> (forall m. KnownNat m => f (m + k) -> r) -> r
plusToLe :: forall (k :: Nat) n f r. f (n + k) -> (forall m. k <= m => f m -> r) -> r
plusToLeKN :: forall (k :: Nat) n f r. (KnownNat n, KnownNat k) => f (n + k) -> (forall m. (KnownNat m, k <= m) => f 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

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 #
Lift (SNat n) Source #
Instance details Defined in Clash.Promoted.Nat Methods lift :: SNat n -> Q Exp #
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.

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

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

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

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

Specialised

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

Power of two of a singleton natural number

Unary/Peano-encoded natural numbers

Data type

data UNat :: Nat -> * where Source #

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) 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 :: SNat n -> UNat n Source #

Convert a singleton natural number to its unary representation

NB: Not synthesisable

Conversion

fromUNat :: UNat n -> SNat n Source #

Convert a unary-encoded natural number to its singleton representation

NB: Not synthesisable

Arithmetic

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

Add two unary-encoded natural numbers

NB: Not synthesisable

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

Multiply two unary-encoded natural numbers

NB: Not synthesisable

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

Power of two unary-encoded natural numbers

NB: Not synthesisable

Partial

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

Predecessor of a unary-encoded natural number

NB: Not synthesisable

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

Subtract two unary-encoded natural numbers

NB: Not synthesisable

Base-2 encoded natural numbers

Data type

data BNat :: Nat -> * where Source #

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) 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 synthesisable

Conversion

fromBNat :: BNat n -> SNat n Source #

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 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 synthesisable

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

Add two base-2 encoded natural numbers

NB: Not synthesisable

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

Multiply two base-2 encoded natural numbers

NB: Not synthesisable

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

Power of two base-2 encoded natural numbers

NB: Not synthesisable

Partial

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

Predecessor of a base-2 encoded natural number

NB: Not synthesisable

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

Divide a base-2 encoded natural number by 2

NB: Not synthesisable

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

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

NB: Not synthesisable

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

Get the log2 of a base-2 encoded natural number

NB: Not synthesisable

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 synthesisable

Constraints on natural numbers

leToPlus Source #

Arguments

:: forall (k :: Nat) (n :: Nat). k <= n
=> f n	Argument with the `(k <= n)` constraint
-> (forall m. f (m + k) -> r)	Function with the `(n + k)` constraint
-> r

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

NB It is the dual to plusToLe

Examples

Expand

Example 1

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

g :: (1 <= n) => Index n -> Index n -> Bool
g a b = leToPlus @1 $ \a' -> leToPlus @1 $ \b' -> f a' b'

Example 2

import Data.Bifunctor.Flip

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

head' :: (1 <= n) => Vec n a -> a
head' a = leToPlus @1 (Flip a) (head . runFlip)

leToPlusKN Source #

Arguments

:: forall (k :: Nat) (n :: Nat). (k <= n, KnownNat n, KnownNat k)
=> f n	Argument with the `(k <= n)` constraint
-> (forall m. KnownNat m => f (m + k) -> r)	Function with the `(n + k)` constraint
-> r

Same as leToPlus with added KnownNat constraints

plusToLe Source #

Arguments

:: forall (k :: Nat). f (n + k)	Argument with the `(n + k)` constraint
-> (forall m. k <= m => f m -> r)	Function with the `(k <= n)` constraint
-> r

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

NB It is the dual to leToPlus

Examples

Expand

Example 1

f :: (1 <= n) => Index n -> Index n -> Bool

g :: Index (n + 1) -> Index (n + 1) -> Bool
g a b = plusToLe @1 $ \a' -> plusToLe @1 $ \b' -> f a' b'

Example 2

import Datal.Bifunctor.Flip

fold :: (1 <= n) => (a -> a -> a) -> Vec n a -> a

fold' :: (a -> a -> a) -> Vec (n+1) a -> a
fold' f a = plusToLe @1 (Flip a) (fold f . runFlip)

plusToLeKN Source #

Arguments

:: forall (k :: Nat). (KnownNat n, KnownNat k)
=> f (n + k)	Argument with the `(n + k)` constraint
-> (forall m. (KnownNat m, k <= m) => f m -> r)	Function with the `(k <= n)` constraint
-> r

Same as plusToLe with added KnownNat constraints