parameterized-utils-2.1.11.0: Classes and data structures for working with data-kind indexed types

Copyright | (c) Galois Inc 2014-2019
Maintainer | Joe Hendrix <jhendrix@galois.com>
Safe Haskell | Trustworthy
Language | Haskell2010

Data.Parameterized.NatRepr

Contents

- Strict order
- Bitvector utilities
- LeqProof
- LeqProof combinators
- Arithmetic proof
- Re-exports typelists basics

Description

This defines a type `NatRepr` for representing a type-level natural at runtime. This can be used to branch on a type-level value. For each `n`, `NatRepr n` contains a single value containing the value `n`. This can be used to help use type-level variables on code with data dependendent types.

The `TestEquality` and `DecidableEq` instances for `NatRepr` are implemented using `unsafeCoerce`, as is the `isZeroNat` function. This should be typesafe because we maintain the invariant that the integer value contained in a NatRepr value matches its static type.

Synopsis

- data NatRepr (n :: Nat)
- natValue :: NatRepr n -> Natural
- intValue :: forall (n :: Nat). NatRepr n -> Integer
- knownNat :: forall (n :: Nat). KnownNat n => NatRepr n
- withKnownNat :: forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
- data IsZeroNat (n :: Natural) where
  - ZeroNat :: IsZeroNat 0
  - NonZeroNat :: forall (n1 :: Natural). IsZeroNat (n1 + 1)
- isZeroNat :: forall (n :: Nat). NatRepr n -> IsZeroNat n
- isZeroOrGT1 :: forall (n :: Nat). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
- data NatComparison (m :: Natural) (n :: Natural) where
  - NatLT :: forall (m :: Natural) (y :: Natural). (m + 1) <= (m + (y + 1)) => !(NatRepr y) -> NatComparison m (m + (y + 1))
  - NatEQ :: forall (m :: Natural). NatComparison m m
  - NatGT :: forall (n :: Natural) (y :: Natural). (n + 1) <= (n + (y + 1)) => !(NatRepr y) -> NatComparison (n + (y + 1)) n
- compareNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatComparison m n
- decNat :: forall (n :: Natural). 1 <= n => NatRepr n -> NatRepr (n - 1)
- predNat :: forall (n :: Natural). NatRepr (n + 1) -> NatRepr n
- incNat :: forall (n :: Nat). NatRepr n -> NatRepr (n + 1)
- addNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatRepr (m + n)
- subNat :: forall (n :: Nat) (m :: Nat). n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n)
- divNat :: forall (n :: Natural) (m :: Natural). 1 <= n => NatRepr (m * n) -> NatRepr n -> NatRepr m
- halfNat :: forall (n :: Natural). NatRepr (n + n) -> NatRepr n
- withDivModNat :: forall (n :: Nat) (m :: Nat) a. NatRepr n -> NatRepr m -> (forall (div :: Natural) (mod :: Natural). n ~ ((div * m) + mod) => NatRepr div -> NatRepr mod -> a) -> a
- natMultiply :: forall (n :: Nat) (m :: Nat). NatRepr n -> NatRepr m -> NatRepr (n * m)
- someNat :: Integral a => a -> Maybe (Some NatRepr)
- mkNatRepr :: Natural -> Some NatRepr
- maxNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> Some NatRepr
- natRec :: forall (p :: Nat) f. NatRepr p -> f 0 -> (forall (n :: Nat). NatRepr n -> f n -> f (n + 1)) -> f p
- natRecStrong :: forall (p :: Nat) f. NatRepr p -> f 0 -> (forall (n :: Nat). NatRepr n -> (forall (m :: Nat). m <= n => NatRepr m -> f m) -> f (n + 1)) -> f p
- natRecBounded :: forall (m :: Nat) (h :: Nat) f. m <= h => NatRepr m -> NatRepr h -> f 0 -> (forall (n :: Nat). n <= h => NatRepr n -> f n -> f (n + 1)) -> f (m + 1)
- natRecStrictlyBounded :: forall (m :: Nat) f. NatRepr m -> f 0 -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> f n -> f (n + 1)) -> f m
- natForEach :: forall (l :: Nat) (h :: Nat) a. NatRepr l -> NatRepr h -> (forall (n :: Nat). (l <= n, n <= h) => NatRepr n -> a) -> [a]
- natFromZero :: forall (h :: Nat) a. NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> a) -> [a]
- data NatCases (m :: Natural) (n :: Nat) where
  - NatCaseLT :: forall (m :: Natural) (n :: Nat). LeqProof (m + 1) n -> NatCases m n
  - NatCaseEQ :: forall (m :: Natural). NatCases m m
  - NatCaseGT :: forall (n :: Nat) (m :: Natural). LeqProof (n + 1) m -> NatCases m n
- testNatCases :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatCases m n
- lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void
- lessThanAsymmetric :: forall (m :: Nat) f (n :: Natural). LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void
- widthVal :: forall (n :: Nat). NatRepr n -> Int
- minUnsigned :: forall (w :: Nat). NatRepr w -> Integer
- maxUnsigned :: forall (w :: Nat). NatRepr w -> Integer
- minSigned :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer
- maxSigned :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer
- toUnsigned :: forall (w :: Nat). NatRepr w -> Integer -> Integer
- toSigned :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer -> Integer
- unsignedClamp :: forall (w :: Nat). NatRepr w -> Integer -> Integer
- signedClamp :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer -> Integer
- data LeqProof (m :: Nat) (n :: Nat) where
  - LeqProof :: forall (m :: Nat) (n :: Nat). m <= n => LeqProof m n
- decideLeq :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void)
- testLeq :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
- testStrictLeq :: forall (m :: Nat) (n :: Nat). m <= n => NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)
- leqRefl :: forall f (n :: Nat). f n -> LeqProof n n
- leqSucc :: forall f (z :: Nat). f z -> LeqProof z (z + 1)
- leqTrans :: forall (m :: Nat) (n :: Nat) (p :: Nat). LeqProof m n -> LeqProof n p -> LeqProof m p
- leqZero :: forall (n :: Nat). LeqProof 0 n
- leqAdd2 :: forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat). LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
- leqSub2 :: forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat). LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
- leqMulCongr :: forall (a :: Nat) (x :: Nat) (b :: Nat) (y :: Nat). LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
- leqProof :: forall (m :: Nat) (n :: Nat) f g. m <= n => f m -> g n -> LeqProof m n
- withLeqProof :: forall (m :: Nat) (n :: Nat) a. LeqProof m n -> (m <= n => a) -> a
- isPosNat :: forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
- leqAdd :: forall f (m :: Nat) (n :: Nat) (p :: Natural). LeqProof m n -> f p -> LeqProof m (n + p)
- leqSub :: forall (m :: Nat) (n :: Nat) (p :: Nat). LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
- leqMulPos :: forall p q (x :: Natural) (y :: Natural). (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y)
- leqAddPos :: forall (m :: Natural) (n :: Natural) p q. (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)
- addIsLeq :: forall f (n :: Nat) g (m :: Natural). f n -> g m -> LeqProof n (n + m)
- withAddLeq :: forall (n :: Nat) (m :: Nat) a. NatRepr n -> NatRepr m -> (n <= (n + m) => NatRepr (n + m) -> a) -> a
- addPrefixIsLeq :: forall f (m :: Natural) g (n :: Nat). f m -> g n -> LeqProof n (m + n)
- withAddPrefixLeq :: forall (n :: Nat) (m :: Nat) a. NatRepr n -> NatRepr m -> (m <= (n + m) => a) -> a
- addIsLeqLeft1 :: forall (n :: Natural) (n' :: Natural) (m :: Nat). LeqProof (n + n') m -> LeqProof n m
- dblPosIsPos :: forall (n :: Nat). LeqProof 1 n -> LeqProof 1 (n + n)
- leqMulMono :: forall (x :: Natural) p q (y :: Nat). 1 <= x => p x -> q y -> LeqProof y (x * y)
- plusComm :: forall f (m :: Natural) g (n :: Natural). f m -> g n -> (m + n) :~: (n + m)
- plusAssoc :: forall f (m :: Natural) g (n :: Natural) h (o :: Natural). f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o)
- mulComm :: forall f (m :: Natural) g (n :: Natural). f m -> g n -> (m * n) :~: (n * m)
- plusMinusCancel :: forall f (m :: Natural) g (n :: Natural). f m -> g n -> ((m + n) - n) :~: m
- minusPlusCancel :: forall f (m :: Natural) g (n :: Natural). n <= m => f m -> g n -> ((m - n) + n) :~: m
- addMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural) f g h. f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
- withAddMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural) f g h a. f n -> g m -> h p -> (((n * p) + (m * p)) ~ ((n + m) * p) => a) -> a
- withSubMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural) f g h a. m <= n => f n -> g m -> h p -> (((n * p) - (m * p)) ~ ((n - m) * p) => a) -> a
- mulCancelR :: forall (c :: Natural) (n1 :: Natural) (n2 :: Natural) f1 f2 f3. (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> n1 :~: n2
- mul2Plus :: forall f (n :: Natural). f n -> (n + n) :~: (2 * n)
- lemmaMul :: forall (n :: Natural) p (w :: Natural) q. 1 <= n => p w -> q n -> (w + ((n - 1) * w)) :~: (n * w)
- type family (a :: Natural) + (b :: Natural) :: Natural where ...
- type family (a :: Natural) - (b :: Natural) :: Natural where ...
- type family (a :: Natural) * (b :: Natural) :: Natural where ...
- type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint)
- class TestEquality (f :: k -> Type) where
  - testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
- data (a :: k) :~: (b :: k) where
  - Refl :: forall {k} (a :: k). a :~: a
- data Some (f :: k -> Type)

# Documentation

data NatRepr (n :: Nat) Source #

A runtime presentation of a type-level `Nat`.

This can be used for performing dynamic checks on a type-level natural numbers.

#### Instances

Instances details

TestEquality NatRepr Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) Source #
EqF NatRepr Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods eqF :: forall (a :: Nat). NatRepr a -> NatRepr a -> Bool Source #
HashableF NatRepr Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods hashWithSaltF :: forall (tp :: Nat). Int -> NatRepr tp -> Int Source # hashF :: forall (tp :: Nat). NatRepr tp -> Int Source #
OrdF NatRepr Source # |

Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

compareF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> OrderingF x y Source #

leqF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool Source #

ltF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool Source #

geqF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool Source #

gtF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool Source #

ShowF NatRepr Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods withShow :: forall p q (tp :: Nat) a. p NatRepr -> q tp -> (Show (NatRepr tp) => a) -> a Source # showF :: forall (tp :: Nat). NatRepr tp -> String Source # showsPrecF :: forall (tp :: Nat). Int -> NatRepr tp -> String -> String Source #
DecidableEq NatRepr Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods decEq :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #
IsRepr NatRepr Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Nat) r. NatRepr a -> (KnownRepr NatRepr a => r) -> r Source #
KnownNat n => KnownRepr NatRepr (n :: Nat) Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods knownRepr :: NatRepr n Source #
KnownNat n => Data (NatRepr n) Source # |

Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NatRepr n) Source #

toConstr :: NatRepr n -> Constr Source #

dataTypeOf :: NatRepr n -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NatRepr n)) Source #

gmapT :: (forall b. Data b => b -> b) -> NatRepr n -> NatRepr n Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NatRepr n -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NatRepr n -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) Source #

Show (NatRepr n) Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods showsPrec :: Int -> NatRepr n -> ShowS Source # show :: NatRepr n -> String Source # showList :: [NatRepr n] -> ShowS Source #
Eq (NatRepr m) Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods (==) :: NatRepr m -> NatRepr m -> Bool Source # (/=) :: NatRepr m -> NatRepr m -> Bool Source #
Hashable (NatRepr n) Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods hashWithSalt :: Int -> NatRepr n -> Int Source # hash :: NatRepr n -> Int Source #
PolyEq (NatRepr m) (NatRepr n) Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n) Source # polyEq :: NatRepr m -> NatRepr n -> Bool Source #

natValue :: NatRepr n -> Natural Source #

The underlying natural value of the number.

intValue :: forall (n :: Nat). NatRepr n -> Integer Source #

knownNat :: forall (n :: Nat). KnownNat n => NatRepr n Source #

This generates a NatRepr from a type-level context.

withKnownNat :: forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r Source #

data IsZeroNat (n :: Natural) where Source #

Constructors

ZeroNat :: IsZeroNat 0 |
NonZeroNat :: forall (n1 :: Natural). IsZeroNat (n1 + 1) |

isZeroNat :: forall (n :: Nat). NatRepr n -> IsZeroNat n Source #

isZeroOrGT1 :: forall (n :: Nat). NatRepr n -> Either (n :~: 0) (LeqProof 1 n) Source #

Every nat is either zero or >= 1.

data NatComparison (m :: Natural) (n :: Natural) where Source #

Result of comparing two numbers.

Constructors

NatLT :: forall (m :: Natural) (y :: Natural). (m + 1) <= (m + (y + 1)) => !(NatRepr y) -> NatComparison m (m + (y + 1)) |
NatEQ :: forall (m :: Natural). NatComparison m m |
NatGT :: forall (n :: Natural) (y :: Natural). (n + 1) <= (n + (y + 1)) => !(NatRepr y) -> NatComparison (n + (y + 1)) n |

compareNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatComparison m n Source #

decNat :: forall (n :: Natural). 1 <= n => NatRepr n -> NatRepr (n - 1) Source #

Decrement a `NatRepr`

predNat :: forall (n :: Natural). NatRepr (n + 1) -> NatRepr n Source #

Get the predecessor of a nat

incNat :: forall (n :: Nat). NatRepr n -> NatRepr (n + 1) Source #

Increment a `NatRepr`

addNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatRepr (m + n) Source #

subNat :: forall (n :: Nat) (m :: Nat). n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n) Source #

divNat :: forall (n :: Natural) (m :: Natural). 1 <= n => NatRepr (m * n) -> NatRepr n -> NatRepr m Source #

halfNat :: forall (n :: Natural). NatRepr (n + n) -> NatRepr n Source #

withDivModNat :: forall (n :: Nat) (m :: Nat) a. NatRepr n -> NatRepr m -> (forall (div :: Natural) (mod :: Natural). n ~ ((div * m) + mod) => NatRepr div -> NatRepr mod -> a) -> a Source #

natMultiply :: forall (n :: Nat) (m :: Nat). NatRepr n -> NatRepr m -> NatRepr (n * m) Source #

someNat :: Integral a => a -> Maybe (Some NatRepr) Source #

Turn an `Integral` value into a `NatRepr`. Returns `Nothing` if the given value is negative.

mkNatRepr :: Natural -> Some NatRepr Source #

Turn a `Natural` into the corresponding `NatRepr`

maxNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> Some NatRepr Source #

Return the maximum of two nat representations.

natRec Source #

Arguments

:: forall (p :: Nat) f. NatRepr p |
-> f 0 | base case
-> (forall (n :: Nat). NatRepr n -> f n -> f (n + 1)) |
-> f p |

Recursor for natural numbeers.

natRecStrong Source #

Arguments

:: forall (p :: Nat) f. NatRepr p |
-> f 0 | base case
-> (forall (n :: Nat). NatRepr n -> (forall (m :: Nat). m <= n => NatRepr m -> f m) -> f (n + 1)) | inductive step
-> f p |

Strong induction variant of the recursor.

natRecBounded :: forall (m :: Nat) (h :: Nat) f. m <= h => NatRepr m -> NatRepr h -> f 0 -> (forall (n :: Nat). n <= h => NatRepr n -> f n -> f (n + 1)) -> f (m + 1) Source #

Bounded recursor for natural numbers.

If you can prove: - Base case: f 0 - Inductive step: if n <= h and (f n) then (f (n + 1)) You can conclude: for all n <= h, (f (n + 1)).

natRecStrictlyBounded :: forall (m :: Nat) f. NatRepr m -> f 0 -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> f n -> f (n + 1)) -> f m Source #

A version of `natRecBounded` which doesn't require the type index of the result to be greater than `0` and provides a strict inequality constraint.

natForEach :: forall (l :: Nat) (h :: Nat) a. NatRepr l -> NatRepr h -> (forall (n :: Nat). (l <= n, n <= h) => NatRepr n -> a) -> [a] Source #

Apply a function to each element in a range; return the list of values obtained.

natFromZero :: forall (h :: Nat) a. NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> a) -> [a] Source #

Apply a function to each element in a range starting at zero; return the list of values obtained.

data NatCases (m :: Natural) (n :: Nat) where Source #

Constructors

NatCaseLT :: forall (m :: Natural) (n :: Nat). LeqProof (m + 1) n -> NatCases m n |
NatCaseEQ :: forall (m :: Natural). NatCases m m |
NatCaseGT :: forall (n :: Nat) (m :: Natural). LeqProof (n + 1) m -> NatCases m n |

testNatCases :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatCases m n Source #

# Strict order

lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void Source #

The strict order (<), defined by n < m <-> n + 1 <= m, is irreflexive.

lessThanAsymmetric :: forall (m :: Nat) f (n :: Natural). LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void Source #

The strict order on the naturals is asymmetric

# Bitvector utilities

widthVal :: forall (n :: Nat). NatRepr n -> Int Source #

Return the value of the nat representation.

minUnsigned :: forall (w :: Nat). NatRepr w -> Integer Source #

Return minimum unsigned value for bitvector with given width (always 0).

maxUnsigned :: forall (w :: Nat). NatRepr w -> Integer Source #

Return maximum unsigned value for bitvector with given width.

minSigned :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer Source #

Return minimum value for bitvector in two's complement with given width.

maxSigned :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer Source #

Return maximum value for bitvector in two's complement with given width.

toUnsigned :: forall (w :: Nat). NatRepr w -> Integer -> Integer Source #

`toUnsigned w i` maps `i` to a `i `mod` 2^w`.

toSigned :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer -> Integer Source #

`toSigned w i` interprets the least-significant `w` bits in `i` as a signed number in two's complement notation and returns that value.

unsignedClamp :: forall (w :: Nat). NatRepr w -> Integer -> Integer Source #

`unsignedClamp w i` rounds `i` to the nearest value between `0` and `2^w-1` (inclusive).

signedClamp :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer -> Integer Source #

`signedClamp w i` rounds `i` to the nearest value between `-2^(w-1)` and `2^(w-1)-1` (inclusive).

# LeqProof

data LeqProof (m :: Nat) (n :: Nat) where Source #

`LeqProof m n` is a type whose values are only inhabited when `m` is less than or equal to `n`.

Constructors

LeqProof :: forall (m :: Nat) (n :: Nat). m <= n => LeqProof m n |

decideLeq :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void) Source #

(<=) is a decidable relation on nats.

testLeq :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> Maybe (LeqProof m n) Source #

`x `testLeq` y` checks whether `x` is less than or equal to `y`.

testStrictLeq :: forall (m :: Nat) (n :: Nat). m <= n => NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n) Source #

leqRefl :: forall f (n :: Nat). f n -> LeqProof n n Source #

Apply reflexivity to LeqProof

leqSucc :: forall f (z :: Nat). f z -> LeqProof z (z + 1) Source #

leqTrans :: forall (m :: Nat) (n :: Nat) (p :: Nat). LeqProof m n -> LeqProof n p -> LeqProof m p Source #

Apply transitivity to LeqProof

leqZero :: forall (n :: Nat). LeqProof 0 n Source #

Zero is less than or equal to any `Nat`.

leqAdd2 :: forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat). LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h) Source #

Add both sides of two inequalities

leqSub2 :: forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat). LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l) Source #

Subtract sides of two inequalities.

leqMulCongr :: forall (a :: Nat) (x :: Nat) (b :: Nat) (y :: Nat). LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y) Source #

Congruence rule for multiplication

# LeqProof combinators

leqProof :: forall (m :: Nat) (n :: Nat) f g. m <= n => f m -> g n -> LeqProof m n Source #

Create a leqProof using two proxies

withLeqProof :: forall (m :: Nat) (n :: Nat) a. LeqProof m n -> (m <= n => a) -> a Source #

isPosNat :: forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n) Source #

Test whether natural number is positive.

leqAdd :: forall f (m :: Nat) (n :: Nat) (p :: Natural). LeqProof m n -> f p -> LeqProof m (n + p) Source #

Produce proof that adding a value to the larger element in an LeqProof is larger

leqSub :: forall (m :: Nat) (n :: Nat) (p :: Nat). LeqProof m n -> LeqProof p m -> LeqProof (m - p) n Source #

Produce proof that subtracting a value from the smaller element is smaller.

leqMulPos :: forall p q (x :: Natural) (y :: Natural). (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y) Source #

Multiplying two positive numbers results in a positive number.

leqAddPos :: forall (m :: Natural) (n :: Natural) p q. (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n) Source #

addIsLeq :: forall f (n :: Nat) g (m :: Natural). f n -> g m -> LeqProof n (n + m) Source #

withAddLeq :: forall (n :: Nat) (m :: Nat) a. NatRepr n -> NatRepr m -> (n <= (n + m) => NatRepr (n + m) -> a) -> a Source #

addPrefixIsLeq :: forall f (m :: Natural) g (n :: Nat). f m -> g n -> LeqProof n (m + n) Source #

withAddPrefixLeq :: forall (n :: Nat) (m :: Nat) a. NatRepr n -> NatRepr m -> (m <= (n + m) => a) -> a Source #

addIsLeqLeft1 :: forall (n :: Natural) (n' :: Natural) (m :: Nat). LeqProof (n + n') m -> LeqProof n m Source #

dblPosIsPos :: forall (n :: Nat). LeqProof 1 n -> LeqProof 1 (n + n) Source #

leqMulMono :: forall (x :: Natural) p q (y :: Nat). 1 <= x => p x -> q y -> LeqProof y (x * y) Source #

# Arithmetic proof

plusComm :: forall f (m :: Natural) g (n :: Natural). f m -> g n -> (m + n) :~: (n + m) Source #

Produce evidence that `+` is commutative.

plusAssoc :: forall f (m :: Natural) g (n :: Natural) h (o :: Natural). f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o) Source #

Produce evidence that `+` is associative.

mulComm :: forall f (m :: Natural) g (n :: Natural). f m -> g n -> (m * n) :~: (n * m) Source #

Produce evidence that `*` is commutative.

plusMinusCancel :: forall f (m :: Natural) g (n :: Natural). f m -> g n -> ((m + n) - n) :~: m Source #

Cancel an add followed by a subtract

minusPlusCancel :: forall f (m :: Natural) g (n :: Natural). n <= m => f m -> g n -> ((m - n) + n) :~: m Source #

addMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural) f g h. f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p) Source #

withAddMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural) f g h a. f n -> g m -> h p -> (((n * p) + (m * p)) ~ ((n + m) * p) => a) -> a Source #

withSubMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural) f g h a. m <= n => f n -> g m -> h p -> (((n * p) - (m * p)) ~ ((n - m) * p) => a) -> a Source #

mulCancelR :: forall (c :: Natural) (n1 :: Natural) (n2 :: Natural) f1 f2 f3. (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> n1 :~: n2 Source #

mul2Plus :: forall f (n :: Natural). f n -> (n + n) :~: (2 * n) Source #

lemmaMul :: forall (n :: Natural) p (w :: Natural) q. 1 <= n => p w -> q n -> (w + ((n - 1) * w)) :~: (n * w) Source #

Used in `Vector`

# Re-exports typelists basics

type family (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6 Source #

Addition of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) - (b :: Natural) :: Natural where ... infixl 6 Source #

Subtraction of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) * (b :: Natural) :: Natural where ... infixl 7 Source #

Multiplication of type-level naturals.

Since: base-4.7.0.0

type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4 Source #

Comparison (<=) of comparable types, as a constraint.

Since: base-4.16.0.0

class TestEquality (f :: k -> Type) where Source #

This class contains types where you can learn the equality of two types from information contained in terms.

The result should be `Just Refl` if and only if the types applied to `f` are equal:

    testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b

Typically, only singleton types should inhabit this class. In that case type argument equality coincides with term equality:

    testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y

    isJust (testEquality x y) = x == y

Singleton types are not required, however, and so the latter two would-be laws are not in fact valid in general.

Methods

testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) Source #

Conditionally prove the equality of `a` and `b`.

#### Instances

Instances details

TestEquality SNat | Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeNats Methods testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) Source #
TestEquality NatRepr Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) Source #
TestEquality PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods testEquality :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b) Source #
TestEquality BoolRepr Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods testEquality :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> Maybe (a :~: b) Source #
TestEquality SChar | Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeLits Methods testEquality :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) Source #
TestEquality SSymbol | Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeLits Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) Source #
TestEquality SymbolRepr Source # |
Instance details Defined in Data.Parameterized.SymbolRepr Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b) Source #
TestEquality (TypeRep :: k -> Type) |
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods testEquality :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) Source #
TestEquality (Nonce :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.Nonce.Unsafe Methods testEquality :: forall (a :: k) (b :: k). Nonce a -> Nonce b -> Maybe (a :~: b) Source #
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
TestEquality (Index ctx :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: k) (b :: k). Index ctx a -> Index ctx b -> Maybe (a :~: b) Source #
TestEquality (Index l :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods testEquality :: forall (a :: k) (b :: k). Index l a -> Index l b -> Maybe (a :~: b) Source #
TestEquality (Nonce s :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.Nonce Methods testEquality :: forall (a :: k) (b :: k). Nonce s a -> Nonce s b -> Maybe (a :~: b) Source #
TestEquality ((:~~:) a :: k -> Type) | Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) Source #
TestEquality f => TestEquality (Compose f g :: k2 -> Type) | The deduction (via generativity) that if `g x :~: g y` then `x :~: y`. Since: base-4.14.0.0
Instance details Defined in Data.Functor.Compose Methods testEquality :: forall (a :: k2) (b :: k2). Compose f g a -> Compose f g b -> Maybe (a :~: b) Source #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) Source #
TestEquality f => TestEquality (List f :: [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods testEquality :: forall (a :: [k]) (b :: [k]). List f a -> List f b -> Maybe (a :~: b) Source #
(TestEquality f, TestEquality g) => TestEquality (PairRepr f g :: (k1, k2) -> Type) Source # |
Instance details Defined in Data.Parameterized.DataKind Methods testEquality :: forall (a :: (k1, k2)) (b :: (k1, k2)). PairRepr f g a -> PairRepr f g b -> Maybe (a :~: b) Source #

data (a :: k) :~: (b :: k) where infix 4 Source #

Propositional equality. If `a :~: b` is inhabited by some terminating value, then the type `a` is the same as the type `b`. To use this equality in practice, pattern-match on the `a :~: b` to get out the `Refl` constructor; in the body of the pattern-match, the compiler knows that `a ~ b`.

Since: base-4.7.0.0

Constructors

Refl :: forall {k} (a :: k). a :~: a |

#### Instances

Instances details

Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Control.Category Methods id :: forall (a :: k). a :~: a Source # (.) :: forall (b :: k) (c :: k) (a :: k). (b :~: c) -> (a :~: b) -> a :~: c Source #
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
NFData2 ((:~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> () Source #
NFData1 ((:~:) a) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a0 -> ()) -> (a :~: a0) -> () Source #
NFData (a :~: b) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods rnf :: (a :~: b) -> () Source #
(a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Data

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) Source #

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) Source #

toConstr :: (a :~: b) -> Constr Source #

dataTypeOf :: (a :~: b) -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) Source #

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #

a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound :: a :~: b Source # maxBound :: a :~: b Source #
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b Source #

pred :: (a :~: b) -> a :~: b Source #

toEnum :: Int -> a :~: b Source #

fromEnum :: (a :~: b) -> Int Source #

enumFrom :: (a :~: b) -> [a :~: b] Source #

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Source #

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Source #

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Source #

a ~ b => Read (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) Source # readList :: ReadS [a :~: b] Source # readPrec :: ReadPrec (a :~: b) Source # readListPrec :: ReadPrec [a :~: b] Source #
Show (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS Source # show :: (a :~: b) -> String Source # showList :: [a :~: b] -> ShowS Source #
Eq (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool Source # (/=) :: (a :~: b) -> (a :~: b) -> Bool Source #
Ord (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering Source #

(<) :: (a :~: b) -> (a :~: b) -> Bool Source #

(<=) :: (a :~: b) -> (a :~: b) -> Bool Source #

(>) :: (a :~: b) -> (a :~: b) -> Bool Source #

(>=) :: (a :~: b) -> (a :~: b) -> Bool Source #

max :: (a :~: b) -> (a :~: b) -> a :~: b Source #

min :: (a :~: b) -> (a :~: b) -> a :~: b Source #

HasDict (a ~ b) (a :~: b) |
Instance details Defined in Data.Constraint Methods evidence :: (a :~: b) -> Dict (a ~ b) Source #

data Some (f :: k -> Type) Source #

#### Instances

Instances details

OrdC (Some :: (k -> Type) -> Type) Source # |
Instance details Defined in Data.Parameterized.ClassesC Methods compareC :: (forall (x :: k) (y :: k). f x -> g y -> OrderingF x y) -> Some f -> Some g -> Ordering Source #
TestEqualityC (Some :: (k -> Type) -> Type) Source # | This instance demonstrates where the above class is useful: namely, in types with existential quantification.
Instance details Defined in Data.Parameterized.ClassesC Methods testEqualityC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> Some f -> Some f -> Bool Source #
FoldableF (Some :: (k -> Type) -> Type) Source # |

Instance details

Defined in Data.Parameterized.Some

Methods

foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> Some e -> m Source #

foldrF :: (forall (s :: k). e s -> b -> b) -> b -> Some e -> b Source #

foldlF :: (forall (s :: k). b -> e s -> b) -> b -> Some e -> b Source #

foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> Some e -> b Source #

foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> Some e -> b Source #

toListF :: (forall (tp :: k). f tp -> a) -> Some f -> [a] Source #

FunctorF (Some :: (k -> Type) -> Type) Source # |
Instance details Defined in Data.Parameterized.Some Methods fmapF :: (forall (x :: k). f x -> g x) -> Some f -> Some g Source #
TraversableF (Some :: (k -> Type) -> Type) Source # |
Instance details Defined in Data.Parameterized.Some Methods traverseF :: Applicative m => (forall (s :: k). e s -> m (f s)) -> Some e -> m (Some f) Source #
ShowF f => Show (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods showsPrec :: Int -> Some f -> ShowS Source # show :: Some f -> String Source # showList :: [Some f] -> ShowS Source #
TestEquality f => Eq (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods (==) :: Some f -> Some f -> Bool Source # (/=) :: Some f -> Some f -> Bool Source #
OrdF f => Ord (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods compare :: Some f -> Some f -> Ordering Source # (<) :: Some f -> Some f -> Bool Source # (<=) :: Some f -> Some f -> Bool Source # (>) :: Some f -> Some f -> Bool Source # (>=) :: Some f -> Some f -> Bool Source # max :: Some f -> Some f -> Some f Source # min :: Some f -> Some f -> Some f Source #
(HashableF f, TestEquality f) => Hashable (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods hashWithSalt :: Int -> Some f -> Int Source # hash :: Some f -> Int Source #