| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Rerefined.Predicates
Contents
Description
Predicate re-exports, for when you're heavily using refinement types.
Synopsis
- data Succeed
- data Fail
- validateVia :: forall {k1} {k2} (pVia :: k1) (p :: k2) a. (Refine pVia a, Predicate p, KnownPredicateName p) => Proxy# p -> a -> Maybe RefineFailure
- data And (l :: k) (r :: k1)
- data Iff (l :: k) (r :: k1)
- data If (l :: k) (r :: k1)
- data Nand (l :: k) (r :: k1)
- data Nor (l :: k) (r :: k1)
- data Not (p :: k)
- data Or (l :: k) (r :: k1)
- data Xor (l :: k) (r :: k1)
- data RelOp
- data CompareValue (op :: RelOp) (sign :: Sign) (n :: Natural)
- data Sign
- data CompareLength (op :: RelOp) (n :: Natural)
Base
The unit predicate. Always succeeds.
Instances
| Predicate Succeed Source # | |||||
Defined in Rerefined.Predicate.Succeed Associated Types
| |||||
| Refine Succeed a Source # | |||||
Defined in Rerefined.Predicate.Succeed | |||||
| type PredicateName d Succeed Source # | |||||
Defined in Rerefined.Predicate.Succeed | |||||
Always fails.
Instances
| Predicate Fail Source # | |||||
Defined in Rerefined.Predicate.Fail Associated Types
| |||||
| Refine Fail a Source # | |||||
Defined in Rerefined.Predicate.Fail | |||||
| type PredicateName d Fail Source # | |||||
Defined in Rerefined.Predicate.Fail | |||||
validateVia :: forall {k1} {k2} (pVia :: k1) (p :: k2) a. (Refine pVia a, Predicate p, KnownPredicateName p) => Proxy# p -> a -> Maybe RefineFailure Source #
Implement validate for predicate p via pVia.
This is useful when you need a unique data type for a predicate (e.g. for instances, clarity), but the predicate it tests already exists. In such cases, it would be nice to reuse the existing predicate, while printing both predicates in failures i.e. "predicate X, implemented via predicate Y, failed with Z".
Call using visible type applications:
validate=validateVia@pVia
Logical
data And (l :: k) (r :: k1) Source #
Logical conjunction. Also AND logic gate.
Instances
| (Predicate l, Predicate r) => Predicate (And l r :: Type) Source # | Precedence of 3 (matching |
Defined in Rerefined.Predicate.Logical.And | |
| (Refine l a, Refine r a, KnownPredicateName (And l r)) => Refine (And l r :: Type) a Source # | |
Defined in Rerefined.Predicate.Logical.And | |
| type PredicateName d (And l r :: Type) Source # | |
Defined in Rerefined.Predicate.Logical.And | |
data Iff (l :: k) (r :: k1) Source #
Logical biconditional ("if and only if"). Also the XNOR logic gate, or equivalence (loosely).
Instances
| (Predicate l, Predicate r) => Predicate (Iff l r :: Type) Source # | Precedence of 4 (matching |
Defined in Rerefined.Predicate.Logical.Iff | |
| (Refine l a, Refine r a, KnownPredicateName (Iff l r)) => Refine (Iff l r :: Type) a Source # | |
Defined in Rerefined.Predicate.Logical.Iff | |
| type PredicateName d (Iff l r :: Type) Source # | |
Defined in Rerefined.Predicate.Logical.Iff | |
data If (l :: k) (r :: k1) Source #
Logical implication. "If l then r".
Instances
| (Predicate l, Predicate r) => Predicate (If l r :: Type) Source # | Precedence of 4 (matching |
Defined in Rerefined.Predicate.Logical.If | |
| (Refine l a, Refine r a, KnownPredicateName (If l r)) => Refine (If l r :: Type) a Source # | |
Defined in Rerefined.Predicate.Logical.If | |
| type PredicateName d (If l r :: Type) Source # | |
Defined in Rerefined.Predicate.Logical.If | |
data Nand (l :: k) (r :: k1) Source #
NAND logic gate. Also called the Sheffer stroke, or non-conjunction.
Instances
| (Predicate l, Predicate r) => Predicate (Nand l r :: Type) Source # | Precedence of 3 (matching |
Defined in Rerefined.Predicate.Logical.Nand | |
| (Refine l a, Refine r a, KnownPredicateName (Nand l r)) => Refine (Nand l r :: Type) a Source # | |
Defined in Rerefined.Predicate.Logical.Nand | |
| type PredicateName d (Nand l r :: Type) Source # | |
Defined in Rerefined.Predicate.Logical.Nand | |
data Nor (l :: k) (r :: k1) Source #
NOR logic gate. Also called non-disjunction, or joint denial.
Instances
| (Predicate l, Predicate r) => Predicate (Nor l r :: Type) Source # | Precedence of 2 (matching |
Defined in Rerefined.Predicate.Logical.Nor | |
| (Refine l a, Refine r a, KnownPredicateName (Nor l r)) => Refine (Nor l r :: Type) a Source # | |
Defined in Rerefined.Predicate.Logical.Nor | |
| type PredicateName d (Nor l r :: Type) Source # | |
Defined in Rerefined.Predicate.Logical.Nor | |
Logical negation. Also NOT logic gate, or logical complement.
Instances
| Predicate p => Predicate (Not p :: Type) Source # | Precedence of 9 (one below function application). |
Defined in Rerefined.Predicate.Logical.Not | |
| (Refine p a, KnownPredicateName (Not p)) => Refine (Not p :: Type) a Source # | |
Defined in Rerefined.Predicate.Logical.Not | |
| type PredicateName d (Not p :: Type) Source # | |
Defined in Rerefined.Predicate.Logical.Not | |
data Or (l :: k) (r :: k1) Source #
Logical disjunction. Also OR logic gate.
Instances
| (Predicate l, Predicate r) => Predicate (Or l r :: Type) Source # | Precedence of 2 (matching |
Defined in Rerefined.Predicate.Logical.Or | |
| (Refine l a, Refine r a, KnownPredicateName (Or l r)) => Refine (Or l r :: Type) a Source # | |
Defined in Rerefined.Predicate.Logical.Or | |
| type PredicateName d (Or l r :: Type) Source # | |
Defined in Rerefined.Predicate.Logical.Or | |
data Xor (l :: k) (r :: k1) Source #
Logical exclusive disjunction. Also XOR logic gate.
Instances
| (Predicate l, Predicate r) => Predicate (Xor l r :: Type) Source # | Precedence of 4 (matching |
Defined in Rerefined.Predicate.Logical.Xor | |
| (Refine l a, Refine r a, KnownPredicateName (Xor l r)) => Refine (Xor l r :: Type) a Source # | |
Defined in Rerefined.Predicate.Logical.Xor | |
| type PredicateName d (Xor l r :: Type) Source # | |
Defined in Rerefined.Predicate.Logical.Xor | |
Relational
Relational operator.
Constructor order is arbitrary due to NEQ, which obstructs ordering in a
meaningful way.
Note that these operators may be defined by combining Orderings in certain
ways: for example LT OR EQLTE, LT OR GTNEQ.
This is convenient for user intuition, permitting the use of e.g. LT as a
relational operator directly. However, it complicates type-level work, as now we
can't restrict relational operators to a given kind, and we have to handle
non-standard orderings like GT OR LT
data CompareValue (op :: RelOp) (sign :: Sign) (n :: Natural) Source #
Instances
| Predicate (CompareValue op sign n :: Type) Source # | Precedence of 4 (matching base relational operators e.g. |
Defined in Rerefined.Predicate.Relational.Value | |
| (KnownNat n, Num a, Ord a, ReifyRelOp op, ReifySignedNat sign n, KnownPredicateName (CompareValue op sign n)) => Refine (CompareValue op sign n :: Type) a Source # | |
Defined in Rerefined.Predicate.Relational.Value Methods validate :: Proxy# (CompareValue op sign n) -> a -> Maybe RefineFailure Source # | |
| type PredicateName d (CompareValue op sign n :: Type) Source # | |
Defined in Rerefined.Predicate.Relational.Value type PredicateName d (CompareValue op sign n :: Type) = ShowParen (d > 4) (((("Value " ++ ShowRelOp op) ++ ShowChar ' ') ++ ShowSign sign) ++ ShowNatDec n) | |
data CompareLength (op :: RelOp) (n :: Natural) Source #