Rerefined.Predicates

Predicate re-exports, for when you're heavily using refinement types.

Base

data Succeed

The unit predicate. Always succeeds.

Instances

Predicate Succeed

Defined in Rerefined.Predicate.Succeed

Associated Types

type PredicateName d Succeed

Defined in Rerefined.Predicate.Succeed

type PredicateName d Succeed = "\8868"

Refine Succeed a

Defined in Rerefined.Predicate.Succeed

Methods

validate :: Proxy# Succeed -> a -> Maybe RefineFailure

type PredicateName d Succeed

Defined in Rerefined.Predicate.Succeed

type PredicateName d Succeed = "\8868"

data Fail

Always fails.

Instances

Predicate Fail

Defined in Rerefined.Predicate.Fail

Associated Types

type PredicateName d Fail

Defined in Rerefined.Predicate.Fail

type PredicateName d Fail = "\8869"

Refine Fail a

Defined in Rerefined.Predicate.Fail

Methods

validate :: Proxy# Fail -> a -> Maybe RefineFailure

type PredicateName d Fail

Defined in Rerefined.Predicate.Fail

type PredicateName d Fail = "\8869"

validateVia :: forall {k1} {k2} (pVia :: k1) (p :: k2) a. (Refine pVia a, Predicate p, KnownPredicateName p) => Proxy# p -> a -> Maybe RefineFailure

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)

Logical conjunction. Also AND logic gate.

Instances

(Predicate l, Predicate r) => Predicate (And l r :: Type)

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

Defined in Rerefined.Predicate.Logical.And

Methods

validate :: Proxy# (And l r) -> a -> Maybe RefineFailure

type PredicateName d (And l r :: Type)

Defined in Rerefined.Predicate.Logical.And

type PredicateName d (And l r :: Type) = PredicateNameBOp " \8743 " 3 d l r

data Iff (l :: k) (r :: k1)

Logical biconditional ("if and only if"). Also the XNOR logic gate, or equivalence (loosely).

Instances

(Predicate l, Predicate r) => Predicate (Iff l r :: Type)

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

Defined in Rerefined.Predicate.Logical.Iff

Methods

validate :: Proxy# (Iff l r) -> a -> Maybe RefineFailure

type PredicateName d (Iff l r :: Type)

Defined in Rerefined.Predicate.Logical.Iff

type PredicateName d (Iff l r :: Type) = PredicateNameBOp " \8596 " 4 d l r

data If (l :: k) (r :: k1)

Logical implication. "If l then r".

Instances

(Predicate l, Predicate r) => Predicate (If l r :: Type)

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

Defined in Rerefined.Predicate.Logical.If

Methods

validate :: Proxy# (If l r) -> a -> Maybe RefineFailure

type PredicateName d (If l r :: Type)

Defined in Rerefined.Predicate.Logical.If

type PredicateName d (If l r :: Type) = PredicateNameBOp " \8594 " 4 d l r

data Nand (l :: k) (r :: k1)

NAND logic gate. Also called the Sheffer stroke, or non-conjunction.

Instances

(Predicate l, Predicate r) => Predicate (Nand l r :: Type)

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

Defined in Rerefined.Predicate.Logical.Nand

Methods

validate :: Proxy# (Nand l r) -> a -> Maybe RefineFailure

type PredicateName d (Nand l r :: Type)

Defined in Rerefined.Predicate.Logical.Nand

type PredicateName d (Nand l r :: Type) = PredicateNameBOp " \8892 " 3 d l r

data Nor (l :: k) (r :: k1)

NOR logic gate. Also called non-disjunction, or joint denial.

Instances

(Predicate l, Predicate r) => Predicate (Nor l r :: Type)

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

Defined in Rerefined.Predicate.Logical.Nor

Methods

validate :: Proxy# (Nor l r) -> a -> Maybe RefineFailure

type PredicateName d (Nor l r :: Type)

Defined in Rerefined.Predicate.Logical.Nor

type PredicateName d (Nor l r :: Type) = PredicateNameBOp " \8893 " 2 d l r

data Not (p :: k)

Logical negation. Also NOT logic gate, or logical complement.

Instances

Predicate p => Predicate (Not p :: Type)

Precedence of 9 (one below function application).

Defined in Rerefined.Predicate.Logical.Not

(Refine p a, KnownPredicateName (Not p)) => Refine (Not p :: Type) a

Defined in Rerefined.Predicate.Logical.Not

Methods

validate :: Proxy# (Not p) -> a -> Maybe RefineFailure

type PredicateName d (Not p :: Type)

Defined in Rerefined.Predicate.Logical.Not

type PredicateName d (Not p :: Type) = ShowParen (d > 9) ("\172 " ++ PredicateName 10 p)

data Or (l :: k) (r :: k1)

Logical disjunction. Also OR logic gate.

Instances

ReifyRelOp GTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp GTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp GTE = ">="

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp LTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp LTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp LTE = "<="

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp NEQ

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp NEQ

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp NEQ = "/="

Methods

reifyRelOp :: Ord a => a -> a -> Bool

(Predicate l, Predicate r) => Predicate (Or l r :: Type)

Precedence of 2 (matching ||).

Defined in Rerefined.Predicate.Logical.Or

ReifyRelOp (Or 'EQ 'GT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'GT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'GT) = ShowRelOp GTE

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp (Or 'EQ 'LT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'LT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'LT) = ShowRelOp LTE

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp (Or 'GT 'LT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'GT 'LT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'GT 'LT) = ShowRelOp NEQ

Methods

reifyRelOp :: Ord a => a -> a -> Bool

(Refine l a, Refine r a, KnownPredicateName (Or l r)) => Refine (Or l r :: Type) a

Defined in Rerefined.Predicate.Logical.Or

Methods

validate :: Proxy# (Or l r) -> a -> Maybe RefineFailure

type ShowRelOp GTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp GTE = ">="

type ShowRelOp LTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp LTE = "<="

type ShowRelOp NEQ

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp NEQ = "/="

type PredicateName d (Or l r :: Type)

Defined in Rerefined.Predicate.Logical.Or

type PredicateName d (Or l r :: Type) = PredicateNameBOp " \8744 " 2 d l r

type ShowRelOp (Or 'EQ 'GT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'GT) = ShowRelOp GTE

type ShowRelOp (Or 'EQ 'LT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'LT) = ShowRelOp LTE

type ShowRelOp (Or 'GT 'LT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'GT 'LT) = ShowRelOp NEQ

data Xor (l :: k) (r :: k1)

Logical exclusive disjunction. Also XOR logic gate.

Instances

(Predicate l, Predicate r) => Predicate (Xor l r :: Type)

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

Defined in Rerefined.Predicate.Logical.Xor

Methods

validate :: Proxy# (Xor l r) -> a -> Maybe RefineFailure

type PredicateName d (Xor l r :: Type)

Defined in Rerefined.Predicate.Logical.Xor

type PredicateName d (Xor l r :: Type) = PredicateNameBOp " \8853 " 4 d l r

Relational

data CompareValue (op :: k) (sign :: Sign) (n :: Natural)

Compare value to a type-level Natural using the given RelOp.

Instances

Predicate (CompareValue op sign n :: Type)

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

Defined in Rerefined.Predicate.Relational.Value

Methods

validate :: Proxy# (CompareValue op sign n) -> a -> Maybe RefineFailure

type PredicateName d (CompareValue op sign n :: Type)

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 Sign

Constructors

Pos

Neg

data CompareLength (op :: k) (n :: Natural)

Compare length to a type-level Natural using the given RelOp.

Instances

(KnownNat n, Foldable f, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type)

Compare the length of a Foldable to a type-level Natural using the given RelOp.

Defined in Rerefined.Predicate.Relational.Length

Methods

validate1 :: Proxy# (CompareLength op n) -> f a -> Maybe RefineFailure

Predicate (CompareLength op n :: Type)

Precedence of 4 (matching base relational operators e.g. >=).

Defined in Rerefined.Predicate.Relational.Length

(KnownNat n, MonoFoldable a, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine (CompareLength op n :: Type) a

Compare the length of a MonoFoldable to a type-level Natural using the given RelOp.

Defined in Rerefined.Predicate.Relational.Length

Methods

validate :: Proxy# (CompareLength op n) -> a -> Maybe RefineFailure

type PredicateName d (CompareLength op n :: Type)

Defined in Rerefined.Predicate.Relational.Length

type PredicateName d (CompareLength op n :: Type) = ShowParen (d > 4) ((("Length " ++ ShowRelOp op) ++ ShowChar ' ') ++ ShowNatDec n)

type LTE = Or 'LT 'EQ

type GTE = Or 'GT 'EQ