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 :: Symbol

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 :: Symbol

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"

data Via pVia p

Predicate p is implemented via predicate 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.

Via assists in doing this. Implement your Predicate instance as normal, then implement Refine with:

validate = validateVia @pVia

Now when this predicate fails, it will print the pVia failure with a wrapper stating the name of the original predicate.

Note that you may not use DerivingVia because it only works on the last parameter of a multi-parameter type class, and I don't want to switch the order of the Refine parameters. Even if I did, DerivingVia isn't much different to or easier than this.

Instances

(Predicate p, Predicate pVia) => Predicate (Via pVia p :: Type)

Defined in Rerefined.Predicate.Via

Associated Types

type PredicateName d (Via pVia p) :: Symbol

(Refine pVia a, Predicate p, KnownPredicateName p) => Refine (Via pVia p :: Type) a

Defined in Rerefined.Predicate.Via

Methods

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

type PredicateName d (Via pVia p :: Type)

Defined in Rerefined.Predicate.Via

type PredicateName d (Via pVia p :: Type) = ShowParen (d > 9) ((("Via " ++ PredicateName 10 p) ++ " ") ++ PredicateName 10 pVia)

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

Logical

data And l r

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

Associated Types

type PredicateName d (And l r) :: Symbol

(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 r

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

Associated Types

type PredicateName d (Iff l r) :: Symbol

(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 r

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

Associated Types

type PredicateName d (If l r) :: Symbol

(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 r

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

Associated Types

type PredicateName d (Nand l r) :: Symbol

(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 r

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

Associated Types

type PredicateName d (Nor l r) :: Symbol

(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

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

Associated Types

type PredicateName d (Not p) :: Symbol

(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 r

Logical disjunction. Also OR logic gate.

Instances

ReifyRelOp GTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp GTE :: Symbol

Methods

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

ReifyRelOp LTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp LTE :: Symbol

Methods

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

ReifyRelOp NEQ

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp NEQ :: Symbol

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

Associated Types

type PredicateName d (Or l r) :: Symbol

ReifyRelOp (Or 'EQ 'GT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'GT) :: Symbol

Methods

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

ReifyRelOp (Or 'EQ 'LT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'LT) :: Symbol

Methods

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

ReifyRelOp (Or 'GT 'LT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'GT 'LT) :: Symbol

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 r

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

Associated Types

type PredicateName d (Xor l r) :: Symbol

(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 (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

Associated Types

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

(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 (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 :: forall (a :: k1). 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

Associated Types

type PredicateName d (CompareLength op n) :: Symbol

(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 = LT `Or` EQ

type GTE = GT `Or` EQ