Copyright | (c) Galois Inc 2014-2019 |
---|---|
Maintainer | Joe Hendrix <jhendrix@galois.com> |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
Data.Parameterized.NatRepr
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
- 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
- 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
- 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
- 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
TestEquality NatRepr Source # | |
Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) # | |
EqF NatRepr Source # | |
HashableF NatRepr Source # | |
Defined in Data.Parameterized.NatRepr.Internal | |
OrdF NatRepr Source # | |
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 # | |
DecidableEq NatRepr Source # | |
IsRepr NatRepr Source # | |
KnownNat n => KnownRepr NatRepr (n :: Nat) Source # | |
Defined in Data.Parameterized.NatRepr.Internal | |
KnownNat n => Data (NatRepr n) Source # | |
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) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NatRepr n) toConstr :: NatRepr n -> Constr dataTypeOf :: NatRepr n -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NatRepr n)) gmapT :: (forall b. Data b => b -> b) -> NatRepr n -> NatRepr n gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r gmapQ :: (forall d. Data d => d -> u) -> NatRepr n -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> NatRepr n -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) | |
Show (NatRepr n) Source # | |
Eq (NatRepr m) Source # | |
Hashable (NatRepr n) Source # | |
Defined in Data.Parameterized.NatRepr.Internal | |
PolyEq (NatRepr m) (NatRepr n) 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) |
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 #
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 #
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 #
someNat :: Integral a => a -> Maybe (Some NatRepr) Source #
Turn an Integral
value into a NatRepr
. Returns Nothing
if the given value is negative.
maxNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> Some NatRepr Source #
Return the maximum of two nat representations.
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.
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.
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
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
.
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
checks whether testLeq
yx
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 #
leqTrans :: forall (m :: Nat) (n :: Nat) (p :: Nat). LeqProof m n -> LeqProof n p -> LeqProof m p Source #
Apply transitivity to LeqProof
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 #
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 #
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 #
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
class TestEquality (f :: k -> Type) where #
Methods
testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #
Instances
TestEquality SNat | |
Defined in GHC.TypeNats Methods testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) # | |
TestEquality NatRepr Source # | |
Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) # | |
TestEquality PeanoRepr Source # | |
Defined in Data.Parameterized.Peano | |
TestEquality BoolRepr Source # | |
Defined in Data.Parameterized.BoolRepr Methods testEquality :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> Maybe (a :~: b) # | |
TestEquality SChar | |
Defined in GHC.TypeLits Methods testEquality :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) # | |
TestEquality SSymbol | |
Defined in GHC.TypeLits Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) # | |
TestEquality SymbolRepr Source # | |
Defined in Data.Parameterized.SymbolRepr Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b) # | |
TestEquality (TypeRep :: k -> Type) | |
Defined in Data.Typeable.Internal Methods testEquality :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) # | |
TestEquality (Nonce :: k -> Type) Source # | |
Defined in Data.Parameterized.Nonce.Unsafe Methods testEquality :: forall (a :: k) (b :: k). Nonce a -> Nonce b -> Maybe (a :~: b) # | |
TestEquality ((:~:) a :: k -> Type) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) # | |
TestEquality (Index ctx :: k -> Type) Source # | |
Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: k) (b :: k). Index ctx a -> Index ctx b -> Maybe (a :~: b) # | |
TestEquality (Index l :: k -> Type) Source # | |
Defined in Data.Parameterized.List Methods testEquality :: forall (a :: k) (b :: k). Index l a -> Index l b -> Maybe (a :~: b) # | |
TestEquality (Nonce s :: k -> Type) Source # | |
Defined in Data.Parameterized.Nonce Methods testEquality :: forall (a :: k) (b :: k). Nonce s a -> Nonce s b -> Maybe (a :~: b) # | |
TestEquality ((:~~:) a :: k -> Type) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) # | |
TestEquality f => TestEquality (Compose f g :: k2 -> Type) | |
Defined in Data.Functor.Compose Methods testEquality :: forall (a :: k2) (b :: k2). Compose f g a -> Compose f g b -> Maybe (a :~: b) # | |
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source # | |
Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) # | |
TestEquality f => TestEquality (List f :: [k] -> Type) Source # | |
Defined in Data.Parameterized.List Methods testEquality :: forall (a :: [k]) (b :: [k]). List f a -> List f b -> Maybe (a :~: b) # | |
(TestEquality f, TestEquality g) => TestEquality (PairRepr f g :: (k1, k2) -> Type) Source # | |
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) # |
data (a :: k) :~: (b :: k) where #
Instances
Category ((:~:) :: k -> k -> Type) | |
TestCoercion ((:~:) a :: k -> Type) | |
Defined in Data.Type.Coercion Methods testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) | |
TestEquality ((:~:) a :: k -> Type) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) # | |
NFData2 ((:~:) :: Type -> Type -> Type) | |
Defined in Control.DeepSeq | |
NFData1 ((:~:) a) | |
Defined in Control.DeepSeq | |
(a ~ b, Data a) => Data (a :~: b) | |
Defined in 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) gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) toConstr :: (a :~: b) -> Constr dataTypeOf :: (a :~: b) -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) | |
a ~ b => Bounded (a :~: b) | |
Defined in Data.Type.Equality | |
a ~ b => Enum (a :~: b) | |
Defined in Data.Type.Equality | |
a ~ b => Read (a :~: b) | |
Defined in Data.Type.Equality | |
Show (a :~: b) | |
NFData (a :~: b) | |
Defined in Control.DeepSeq | |
Eq (a :~: b) | |
Ord (a :~: b) | |
Defined in Data.Type.Equality | |
HasDict (a ~ b) (a :~: b) | |
Defined in Data.Constraint |
data Some (f :: k -> Type) Source #
Instances
OrdC (Some :: (k -> Type) -> Type) Source # | |
TestEqualityC (Some :: (k -> Type) -> Type) Source # | This instance demonstrates where the above class is useful: namely, in types with existential quantification. |
Defined in Data.Parameterized.ClassesC | |
FoldableF (Some :: (k -> Type) -> Type) Source # | |
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 # | |
TraversableF (Some :: (k -> Type) -> Type) Source # | |
ShowF f => Show (Some f) Source # | |
TestEquality f => Eq (Some f) Source # | |
OrdF f => Ord (Some f) Source # | |
(HashableF f, TestEquality f) => Hashable (Some f) Source # | |
Defined in Data.Parameterized.Some |