Rerefined.Predicate

Base definitions for refinement predicates.

Documentation

class Predicate p => Refine p a where

Refine a with predicate p.

Methods

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

Validate predicate p for the given a.

Nothing indicates success. Just contains a validation failure.

Instances

Refine Fail a

Defined in Rerefined.Predicate.Fail

Methods

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

Refine Succeed a

Defined in Rerefined.Predicate.Succeed

Methods

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

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

Defined in Rerefined.Predicate.Logical

Methods

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

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

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

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

class Predicate p => Refine1 p f where

Refine functor type f with functor predicate p.

By not making the contained type accessible, we ensure refinements apply forall a. f a. That is, refinements here apply only to the functor structure, and not the stored elements.

Methods

validate1 :: Proxy# p -> f a -> Maybe (RefineFailure String)

Validate predicate p for the given f a.

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)

data RefineFailure a

Predicate validation failure.

Polymorphic over the message type because I want to use Text, but want it doesn't have the convenient Show internals that String does.

Constructors

RefineFailure

Fields

• refineFailurePredicate :: a

  The predicate that failed.

• refineFailureDetail :: a

  Failure clarification.

• refineFailureInner :: [RefineFailure a]

  Any wrapped errors, for combinator predicates.

  What these are, and their order, should be noted in refineFailureDetail.

class Predicate p where

Types which define refinements on other types.

Methods

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

The predicate name, as a Show-like (for good bracketing).

Non-combinator predicates may derive this via Typeably. Combinator predicates must write a Show-like instance manually, in order to avoid incurring insidious Typeable contexts for the wrapped predicate(s). (TODO figure out some generics and/or TH to resolve that)

Instances

Predicate Fail

Defined in Rerefined.Predicate.Fail

Methods

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

Predicate Succeed

Defined in Rerefined.Predicate.Succeed

Methods

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

Typeable a => Predicate (Typeably a :: Type)

Fill out predicate metadata using its Typeable instance.

Do not use this for combinator predicates. Doing so will incur insidious Typeable contexts for the wrapped predicate(s).

Defined in Rerefined.Predicate

Methods

predicateName :: Proxy# (Typeably a) -> Int -> ShowS

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

Defined in Rerefined.Predicate.Logical

Methods

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

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

Defined in Rerefined.Predicate.Relational.Length

Methods

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

(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

(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