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"

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