Rerefined.Predicate.Relational

Documentation

data RelOp

Relational operator.

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

Note that these operators may be defined by combining Orderings in certain ways: for example LT OR EQ could be LTE, LT OR GT could be NEQ. This is convenient for user intuition, permitting the use of e.g. LT as a relational operator directly. However, it complicates type-level work, as now we can't restrict relational operators to a given kind, and we have to handle non-standard orderings like GT OR LT.

Constructors

RelOpEQ

== equal to

RelOpNEQ

/= less than or greater than (also not equal to)

RelOpLT

< less than

RelOpLTE

<= less than or equal to

RelOpGTE

>= equal to or greater than

RelOpGT

> greater than

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

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

Instances

Predicate (CompareValue op sign n :: Type)

Precedence of 4 (matching base relational operators e.g. >=).

Defined in Rerefined.Predicate.Relational.Value

(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

type PredicateName d (CompareValue op sign n :: Type)

Defined in Rerefined.Predicate.Relational.Value

type PredicateName d (CompareValue op sign n :: Type) = ShowParen (d > 4) (((("Value " ++ ShowRelOp op) ++ ShowChar ' ') ++ ShowSign sign) ++ ShowNatDec n)

data Sign

Constructors

Pos

Neg

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

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

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 :: Proxy# (CompareLength op n) -> f a -> Maybe RefineFailure

Predicate (CompareLength op n :: Type)

Precedence of 4 (matching base relational operators e.g. >=).

Defined in Rerefined.Predicate.Relational.Length

(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

type PredicateName d (CompareLength op n :: Type)

Defined in Rerefined.Predicate.Relational.Length

type PredicateName d (CompareLength op n :: Type) = ShowParen (d > 4) ((("Length " ++ ShowRelOp op) ++ ShowChar ' ') ++ ShowNatDec n)

type family WidenRelOp (op :: RelOp) (n :: Natural) (m :: Natural) :: Bool where ...

Can we widen the given RelOp on the given Natural from n to m?

Equations

WidenRelOp op n n = 'True

WidenRelOp 'RelOpLT n m = OrdCond (CmpNat n m) 'True 'True 'False

WidenRelOp 'RelOpLTE n m = OrdCond (CmpNat n m) 'True 'True 'False

WidenRelOp 'RelOpGTE n m = OrdCond (CmpNat n m) 'False 'True 'True

WidenRelOp 'RelOpGT n m = OrdCond (CmpNat n m) 'False 'True 'True

WidenRelOp op n m = 'False

type family FlipRelOp (op :: RelOp) :: RelOp where ...

Flip a RelOp to give the opposite comparison.

Equations

FlipRelOp 'RelOpEQ = 'RelOpNEQ

FlipRelOp 'RelOpNEQ = 'RelOpEQ

FlipRelOp 'RelOpLT = 'RelOpGTE

FlipRelOp 'RelOpLTE = 'RelOpGT

FlipRelOp 'RelOpGTE = 'RelOpLT

FlipRelOp 'RelOpGT = 'RelOpLTE