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

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

Refine Succeed a

Defined in Rerefined.Predicate.Succeed

Methods

validate :: Proxy# Succeed -> a -> Maybe RefineFailure

(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

(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

(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

(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

(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

(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

(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

(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

(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

(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

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

Validate predicate p for the given f a.

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

data RefineFailure

Predicate validation failure.

Constructors

RefineFailure

Fields

• refineFailurePredicate :: Builder

  The name of the predicate that failed.

  Obtained via predicateName.

• refineFailureDetail :: Builder

  Precise failure detail e.g. which of the inner predicates of an And combinator predicate failed.

• refineFailureInner :: [RefineFailure]

  Any wrapped errors, for combinator predicates.

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

Instances

Show RefineFailure

Defined in Rerefined.Predicate

Methods

showsPrec :: Int -> RefineFailure -> ShowS

show :: RefineFailure -> String

showList :: [RefineFailure] -> ShowS

class Predicate p

Types which define refinements on other types.

Associated Types

type PredicateName (d :: Natural) p :: Symbol

Predicate name.

Predicate names should aim to communicate the meaning of the predicate as clearly and concisely as possible.

Consider using the package type-level-show to build this.

Instances

Predicate Fail

Defined in Rerefined.Predicate.Fail

Associated Types

type PredicateName d Fail :: Symbol

Predicate Succeed

Defined in Rerefined.Predicate.Succeed

Associated Types

type PredicateName d Succeed :: Symbol

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

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

(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

(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

(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

(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

(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

(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

(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

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

type KnownPredicateName p = KnownSymbol (PredicateName 0 p)

Constraint for reifying a predicate name.

predicateName :: forall p. KnownPredicateName p => String

Reify predicate name to a String.

Using this regrettably necessitates UndecidableInstances, due to the type family in the constraint. It sucks, but that's life.