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

Methods

predicateName :: Proxy# Succeed -> Int -> ShowS

Refine Succeed a

Defined in Rerefined.Predicate.Succeed

Methods

validate :: Proxy# Succeed -> a -> Maybe (RefineFailure String)

data Fail

Always fails.

Instances

Predicate Fail

Defined in Rerefined.Predicate.Fail

Methods

predicateName :: Proxy# Fail -> Int -> ShowS

Refine Fail a

Defined in Rerefined.Predicate.Fail

Methods

validate :: Proxy# Fail -> a -> Maybe (RefineFailure String)

Logical

data Not p

Instances

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

Defined in Rerefined.Predicate.Logical

Methods

predicateName :: Proxy# (Not p) -> Int -> ShowS

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

Defined in Rerefined.Predicate.Logical

Methods

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

data Logical (op :: LogicOp) l r

A logical binary operation on two predicates.

Instances

(Predicate l, Predicate r, ReifyLogicOp op) => Predicate (Logical op l r :: Type)

Defined in Rerefined.Predicate.Logical

Methods

predicateName :: Proxy# (Logical op l r) -> Int -> ShowS

(Refine l a, Refine r a, ReifyLogicOp op) => Refine (Logical op l r :: Type) a

Defined in Rerefined.Predicate.Logical

Methods

validate :: Proxy# (Logical op l r) -> a -> Maybe (RefineFailure String)

Relational

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

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

Instances

(Typeable op, Typeable sign, KnownNat n) => Predicate (CompareValue op sign n :: Type)

Defined in Rerefined.Predicate.Relational.Value

Methods

predicateName :: Proxy# (CompareValue op sign n) -> Int -> ShowS

(KnownNat n, Num a, Ord a, ReifyRelOp op, ReifySignedNat sign n, ReifySign sign) => Refine (CompareValue op sign n :: Type) a

Defined in Rerefined.Predicate.Relational.Value

Methods

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

data Sign

Constructors

Pos

Neg

data RelOp

Relational operator.

There are three possible outcomes from compareing two terms, defined in Ordering. However, we may instead compare terms using relational operators such as >=, which are more specific comparisons that return a Bool.

Constructor order is arbitrary due to NEQ, which obstructs ordering in a meaningful way.

Constructors

LT'

< less than

LTE

<= less than or equal to

EQ'

== equal to

NEQ

/= less than or greater than

GTE

>= equal to or greater than

GT'

> greater than

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

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

Instances

(KnownNat n, Foldable f, ReifyRelOp op) => 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 String)

(Typeable op, KnownNat n) => Predicate (CompareLength op n :: Type)

Defined in Rerefined.Predicate.Relational.Length

Methods

predicateName :: Proxy# (CompareLength op n) -> Int -> ShowS

(KnownNat n, MonoFoldable a, ReifyRelOp op) => 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 String)