rerefined-0.8.0: Refinement types, again
Safe HaskellNone
LanguageGHC2021

Rerefined.Predicate.Relational.Internal

Description

Relational operator definitions.

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

class ReifyRelOp (op :: RelOp) where Source #

Reify a RelOp.

Associated Types

type ShowRelOp (op :: RelOp) :: Symbol Source #

Pretty op.

Methods

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

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

Instances

Instances details
ReifyRelOp 'RelOpEQ Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpEQ 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpEQ = "=="

Methods

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

ReifyRelOp 'RelOpGT Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpGT 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpGT = ">"

Methods

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

ReifyRelOp 'RelOpGTE Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpGTE 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpGTE = ">="

Methods

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

ReifyRelOp 'RelOpLT Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpLT 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpLT = "<"

Methods

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

ReifyRelOp 'RelOpLTE Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpLTE 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpLTE = "<="

Methods

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

ReifyRelOp 'RelOpNEQ Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'RelOpNEQ 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp 'RelOpNEQ = "/="

Methods

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

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