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 type-level-show to build this. However, note that GHC cannot figure out KnownSymbol when there are type families in play, so you may need to put KnownSymbol constraints in instance contexts.

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)

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

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

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

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

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

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

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

Precendence 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

predicateName :: forall p. (Predicate p, KnownSymbol (PredicateName 0 p)) => String

Reify predicate name.