| Copyright | (c) Galois Inc 2014-2015 |
|---|---|
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
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 vlaue
n. This can be used to help use type-level variables on code
with data dependendent types.
The TestEquality instance for NatRepr is 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.
- data NatRepr (n :: Nat)
- natValue :: NatRepr n -> Integer
- knownNat :: forall n. KnownNat n => NatRepr n
- withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
- data IsZeroNat n where
- ZeroNat :: IsZeroNat 0
- NonZeroNat :: IsZeroNat (n + 1)
- isZeroNat :: NatRepr n -> IsZeroNat n
- data NatComparison m n where
- NatLT :: !(NatRepr y) -> NatComparison x (x + (y + 1))
- NatEQ :: NatComparison x x
- NatGT :: !(NatRepr y) -> NatComparison (x + (y + 1)) x
- compareNat :: NatRepr m -> NatRepr n -> NatComparison m n
- decNat :: 1 <= n => NatRepr n -> NatRepr (n - 1)
- predNat :: NatRepr (n + 1) -> NatRepr n
- incNat :: NatRepr n -> NatRepr (n + 1)
- addNat :: NatRepr m -> NatRepr n -> NatRepr (m + n)
- subNat :: n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n)
- halfNat :: NatRepr (n + n) -> NatRepr n
- withDivModNat :: forall n m a. NatRepr n -> NatRepr m -> (forall div mod. n ~ ((div * m) + mod) => NatRepr div -> NatRepr mod -> a) -> a
- natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)
- someNat :: Integer -> Maybe (Some NatRepr)
- maxNat :: NatRepr m -> NatRepr n -> Some NatRepr
- natRec :: forall m f. NatRepr m -> f 0 -> (forall n. NatRepr n -> f n -> f (n + 1)) -> f m
- natForEach :: forall l h a. NatRepr l -> NatRepr h -> (forall n. (l <= n, n <= h) => NatRepr n -> a) -> [a]
- data NatCases m n where
- testNatCases :: forall m n. NatRepr m -> NatRepr n -> NatCases m n
- widthVal :: NatRepr n -> Int
- minUnsigned :: NatRepr w -> Integer
- maxUnsigned :: NatRepr w -> Integer
- minSigned :: 1 <= w => NatRepr w -> Integer
- maxSigned :: 1 <= w => NatRepr w -> Integer
- toUnsigned :: NatRepr w -> Integer -> Integer
- toSigned :: 1 <= w => NatRepr w -> Integer -> Integer
- unsignedClamp :: NatRepr w -> Integer -> Integer
- signedClamp :: 1 <= w => NatRepr w -> Integer -> Integer
- data LeqProof m n where
- testLeq :: forall m n. NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
- testStrictLeq :: forall m n. m <= n => NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)
- leqRefl :: forall f n. f n -> LeqProof n n
- leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p
- leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
- leqSub2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
- leqMulCongr :: LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
- leqProof :: m <= n => f m -> f n -> LeqProof m n
- withLeqProof :: LeqProof m n -> (m <= n => a) -> a
- isPosNat :: NatRepr n -> Maybe (LeqProof 1 n)
- leqAdd :: forall f m n p. LeqProof m n -> f p -> LeqProof m (n + p)
- leqSub :: forall m n p. LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
- leqMulPos :: forall p q x y. (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y)
- addIsLeq :: f n -> g m -> LeqProof n (n + m)
- withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> (n <= (n + m) => NatRepr (n + m) -> a) -> a
- addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n)
- withAddPrefixLeq :: NatRepr n -> NatRepr m -> (m <= (n + m) => a) -> a
- addIsLeqLeft1 :: forall n n' m. LeqProof (n + n') m -> LeqProof n m
- dblPosIsPos :: forall n. LeqProof 1 n -> LeqProof 1 (n + n)
- plusComm :: forall f m g n. f m -> g n -> (m + n) :~: (n + m)
- plusMinusCancel :: forall f m g n. f m -> g n -> ((m + n) - n) :~: m
- withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p -> (((n * p) + (m * p)) ~ ((n + m) * p) => a) -> a
- type family (a :: Nat) + (b :: Nat) :: Nat where ...
- type family (a :: Nat) - (b :: Nat) :: Nat where ...
- type family (a :: Nat) * (b :: Nat) :: Nat where ...
- type (<=) (x :: Nat) (y :: Nat) = (~) Bool ((<=?) x y) True
- class TestEquality k (f :: k -> *) where
- data (k :~: (a :: k)) (b :: k) :: forall k. k -> k -> * where
- data Some (f :: k -> *)
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.
knownNat :: forall n. KnownNat n => NatRepr n Source #
This generates a NatRepr from a type-level context.
withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r Source #
Deprecated: This function is potentially unsafe and is schedueled to be removed.
data NatComparison m n where Source #
Result of comparing two numbers.
Constructors
| NatLT :: !(NatRepr y) -> NatComparison x (x + (y + 1)) | |
| NatEQ :: NatComparison x x | |
| NatGT :: !(NatRepr y) -> NatComparison (x + (y + 1)) x |
compareNat :: NatRepr m -> NatRepr n -> NatComparison m n Source #
withDivModNat :: forall n m a. NatRepr n -> NatRepr m -> (forall div mod. n ~ ((div * m) + mod) => NatRepr div -> NatRepr mod -> a) -> a Source #
maxNat :: NatRepr m -> NatRepr n -> Some NatRepr Source #
Return the maximum of two nat representations.
natRec :: forall m f. NatRepr m -> f 0 -> (forall n. NatRepr n -> f n -> f (n + 1)) -> f m Source #
Recursor for natural numbeers.
natForEach :: forall l h a. NatRepr l -> NatRepr h -> (forall n. (l <= n, n <= h) => NatRepr n -> a) -> [a] Source #
Apply a function to each element in a range; return the list of values obtained.
Bitvector utilities
minUnsigned :: NatRepr w -> Integer Source #
Return minimum unsigned value for bitvector with given width (always 0).
maxUnsigned :: NatRepr w -> Integer Source #
Return maximum unsigned value for bitvector with given width.
minSigned :: 1 <= w => NatRepr w -> Integer Source #
Return minimum value for bitvector in 2s complement with given width.
maxSigned :: 1 <= w => NatRepr w -> Integer Source #
Return maximum value for bitvector in 2s complement with given width.
toSigned :: 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 :: NatRepr w -> Integer -> Integer Source #
unsignedClamp w i rounds i to the nearest value between
0 and 2^w-i (inclusive).
signedClamp :: 1 <= w => NatRepr w -> Integer -> Integer Source #
signedClamp w i rounds i to the nearest value between
-2^(w-1) and 2^(w-1)-i (inclusive).
LeqProof
data LeqProof m n where Source #
LeqProof m n is a type whose values are only inhabited when m
is less than or equal to n.
testLeq :: forall m n. NatRepr m -> NatRepr n -> Maybe (LeqProof m n) Source #
x checks whether testLeq yx is less than or equal to y.
testStrictLeq :: forall m n. m <= n => NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n) Source #
leqAdd2 :: 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 :: 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 :: LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y) Source #
Congruence rule for multiplication
LeqProof combinators
withLeqProof :: LeqProof m n -> (m <= n => a) -> a Source #
leqAdd :: forall f m n p. 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 n p. 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 y. (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y) Source #
Multiplying two positive numbers results in a positive number.
withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> (n <= (n + m) => NatRepr (n + m) -> a) -> a Source #
addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n) Source #
Arithmetic proof
plusComm :: forall f m g n. f m -> g n -> (m + n) :~: (n + m) Source #
Produce evidence that + is commutative.
plusMinusCancel :: forall f m g n. f m -> g n -> ((m + n) - n) :~: m Source #
Cancel an add followed b a subtract
withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p -> (((n * p) + (m * p)) ~ ((n + m) * p) => a) -> a Source #
Re-exports typelists basics
type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 #
Subtraction of type-level naturals.
Since: 4.7.0.0
type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #
Multiplication of type-level naturals.
type (<=) (x :: Nat) (y :: Nat) = (~) Bool ((<=?) x y) True infix 4 #
Comparison of type-level naturals, as a constraint.
class TestEquality k (f :: k -> *) where #
This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.
Minimal complete definition
Methods
testEquality :: f a -> f b -> Maybe ((:~:) k a b) #
Conditionally prove the equality of a and b.
Instances
| TestEquality Nat NatRepr # | |
| TestEquality Symbol SymbolRepr # | |
| TestEquality k (Nonce k) # | |
| TestEquality k (Nonce k s) # | |
| TestEquality k ((:~:) k a) | Since: 4.7.0.0 |
| TestEquality k (Index k l) # | |
| TestEquality k (Index k ctx) # | |
| TestEquality k (Index k ctx) # | |
| TestEquality k ((:~~:) k1 k a) | Since: 4.10.0.0 |
| TestEquality k f => TestEquality [k] (List k f) # | |
| TestEquality k f => TestEquality (Ctx k) (Assignment k f) # | |
| TestEquality k f => TestEquality (Ctx k) (Assignment k f) # | |
data (k :~: (a :: k)) (b :: k) :: forall k. k -> k -> * where infix 4 #
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: 4.7.0.0
Instances
| Category k ((:~:) k) | Since: 4.7.0.0 |
| TestEquality k ((:~:) k a) | Since: 4.7.0.0 |
| NFData2 ((:~:) *) | Since: 1.4.3.0 |
| NFData1 ((:~:) * a) | Since: 1.4.3.0 |
| (~) k a b => Bounded ((:~:) k a b) | Since: 4.7.0.0 |
| (~) k a b => Enum ((:~:) k a b) | Since: 4.7.0.0 |
| Eq ((:~:) k a b) | |
| Ord ((:~:) k a b) | |
| (~) k a b => Read ((:~:) k a b) | Since: 4.7.0.0 |
| Show ((:~:) k a b) | |
| NFData ((:~:) k a b) | Since: 1.4.3.0 |