| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | None |
| Language | Haskell2010 |
Grisette.Utils
Description
Synopsis
- unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b
- data NatRepr (n :: Nat)
- natValue :: forall (n :: Nat). NatRepr n -> Natural
- natRepr :: forall (n :: Nat). KnownNat n => NatRepr 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 :: Nat). 1 <= n => NatRepr m -> NatRepr n -> NatRepr (Div m n)
- halfNat :: forall (n :: Natural). NatRepr (n + n) -> NatRepr n
- data KnownProof (n :: Nat) where
- KnownProof :: forall (n :: Nat). KnownNat n => KnownProof n
- hasRepr :: forall (n :: Nat). NatRepr n -> KnownProof n
- withKnownProof :: forall (n :: Nat) r. KnownProof n -> (KnownNat n => r) -> r
- unsafeKnownProof :: forall (n :: Nat). Natural -> KnownProof n
- knownAdd :: forall (m :: Nat) (n :: Nat). KnownProof m -> KnownProof n -> KnownProof (m + n)
- data LeqProof (m :: Nat) (n :: Nat) where
- withLeqProof :: forall (m :: Nat) (n :: Nat) r. LeqProof m n -> (m <= n => r) -> r
- unsafeLeqProof :: forall (m :: Nat) (n :: Nat). LeqProof m n
- testLeq :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
- leqRefl :: forall f (n :: Nat). f n -> LeqProof n n
- leqSucc :: forall f (n :: Nat). f n -> LeqProof n (n + 1)
- leqTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). LeqProof a b -> LeqProof b c -> LeqProof a c
- leqZero :: forall (n :: Nat). LeqProof 0 n
- leqAdd2 :: forall (xl :: Nat) (xh :: Nat) (yl :: Nat) (yh :: Nat). LeqProof xl xh -> LeqProof yl yh -> LeqProof (xl + yl) (xh + yh)
- leqAdd :: forall (m :: Nat) (n :: Nat) f (o :: Natural). LeqProof m n -> f o -> LeqProof m (n + o)
- leqAddPos :: forall (m :: Natural) (n :: Natural) p q. (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)
Utilities for type-level natural numbers.
Unsafe axiom
unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b Source #
Assert a proof of equality between two types. This is unsafe if used improperly, so use this with caution!
Runtime representation of type-level natural numbers
data NatRepr (n :: Nat) Source #
A runtime representation of type-level natural numbers. This can be used for performing dynamic checks on type-level natural numbers.
natValue :: forall (n :: Nat). NatRepr n -> Natural Source #
The underlying runtime natural number value of a type-level natural number.
natRepr :: forall (n :: Nat). KnownNat n => NatRepr n Source #
Construct a runtime representation of a type-level natural number when its runtime value is known.
decNat :: forall (n :: Natural). 1 <= n => NatRepr n -> NatRepr (n - 1) Source #
Decrement a NatRepr by 1.
addNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatRepr (m + n) Source #
Addition of two NatReprs.
subNat :: forall (n :: Nat) (m :: Nat). n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n) Source #
Subtraction of two NatReprs.
divNat :: forall (n :: Natural) (m :: Nat). 1 <= n => NatRepr m -> NatRepr n -> NatRepr (Div m n) Source #
Division of two NatReprs.
Proof of KnownNat
data KnownProof (n :: Nat) where Source #
'KnownProof n' is a type whose values are only inhabited when n has
a known runtime value.
Constructors
| KnownProof :: forall (n :: Nat). KnownNat n => KnownProof n |
hasRepr :: forall (n :: Nat). NatRepr n -> KnownProof n Source #
Construct a KnownProof given the runtime representation.
withKnownProof :: forall (n :: Nat) r. KnownProof n -> (KnownNat n => r) -> r Source #
Introduces the KnownNat constraint when it's proven.
unsafeKnownProof :: forall (n :: Nat). Natural -> KnownProof n Source #
Construct a KnownProof given the runtime value.
Note: This function is unsafe, as it does not check that the runtime representation is consistent with the type-level representation. You should ensure the consistency yourself or the program can crash or generate incorrect results.
knownAdd :: forall (m :: Nat) (n :: Nat). KnownProof m -> KnownProof n -> KnownProof (m + n) Source #
Adding two type-level natural numbers with known runtime values gives a type-level natural number with a known runtime value.
Proof of (<=) for type-level natural numbers
data LeqProof (m :: Nat) (n :: Nat) where Source #
'LeqProof m n' is a type whose values are only inhabited when m <= n.
withLeqProof :: forall (m :: Nat) (n :: Nat) r. LeqProof m n -> (m <= n => r) -> r Source #
Introduces the m <= n constraint when it's proven.
unsafeLeqProof :: forall (m :: Nat) (n :: Nat). LeqProof m n Source #
Construct a LeqProof.
Note: This function is unsafe, as it does not check that the left-hand side is less than or equal to the right-hand side. You should ensure the consistency yourself or the program can crash or generate incorrect results.
leqSucc :: forall f (n :: Nat). f n -> LeqProof n (n + 1) Source #
A natural number is less than or equal to its successor.
leqTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). LeqProof a b -> LeqProof b c -> LeqProof a c Source #
Apply transitivity to LeqProof.
leqZero :: forall (n :: Nat). LeqProof 0 n Source #
Zero is less than or equal to any natural number.
leqAdd2 :: forall (xl :: Nat) (xh :: Nat) (yl :: Nat) (yh :: Nat). LeqProof xl xh -> LeqProof yl yh -> LeqProof (xl + yl) (xh + yh) Source #
Add both sides of two inequalities.