rerefined-0.8.0: Refinement types, again
Safe HaskellNone
LanguageGHC2021

Rerefined.Predicate.Relational

Synopsis

Documentation

data RelOp Source #

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) Source #

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

Instances

Instances details
Predicate (CompareValue op sign n :: Type) Source #

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

Instance details

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 Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Value

Methods

validate :: Proxy# (CompareValue op sign n) -> a -> Maybe RefineFailure Source #

type PredicateName d (CompareValue op sign n :: Type) Source # 
Instance details

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 Source #

Constructors

Pos 
Neg 

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

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

Instances

Instances details
(KnownNat n, Foldable f, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type) Source #

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

Instance details

Defined in Rerefined.Predicate.Relational.Length

Methods

validate1 :: Proxy# (CompareLength op n) -> f a -> Maybe RefineFailure Source #

Predicate (CompareLength op n :: Type) Source #

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

Instance details

Defined in Rerefined.Predicate.Relational.Length

(KnownNat n, MonoFoldable a, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine (CompareLength op n :: Type) a Source #

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

Instance details

Defined in Rerefined.Predicate.Relational.Length

Methods

validate :: Proxy# (CompareLength op n) -> a -> Maybe RefineFailure Source #

type PredicateName d (CompareLength op n :: Type) Source # 
Instance details

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 ... Source #

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 ... Source #

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