Rerefined.Predicate.Relational.Internal

Relational operator definitions.

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

class ReifyRelOp (op :: RelOp) where

Reify a RelOp.

Associated Types

type ShowRelOp (op :: RelOp) :: Symbol

Pretty op.

Methods

reifyRelOp :: Ord a => a -> a -> Bool

The term-level relational operator that op :: RelOp describes.

Instances

ReifyRelOp 'RelOpEQ

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpEQ

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpEQ = "=="

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp 'RelOpGT

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpGT

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpGT = ">"

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp 'RelOpGTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpGTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpGTE = ">="

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp 'RelOpLT

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpLT

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpLT = "<"

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp 'RelOpLTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpLTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpLTE = "<="

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp 'RelOpNEQ

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpNEQ

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpNEQ = "/="

Methods

reifyRelOp :: Ord a => a -> a -> Bool

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