Rerefined

Documentation

module Rerefined.Refine

class Predicate p

Types which define refinements on other types.

Minimal complete definition

predicateName

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

class Predicate p => Refine p a

Refine a with predicate p.

Minimal complete definition

validate

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

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.

Minimal complete definition

validate1

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)