Rerefined.Simplify.Relational

Relational predicate simplification.

These bits aren't mutually recursive with the main simplifier, so we can keep them separate for a bit of code hygiene.

Internal module. Exports may change without warning. Try not to use.

Documentation

type family SimplifyCompareLength (op :: RelOp) (n :: Natural) :: Maybe Type where ...

Equations

SimplifyCompareLength 'RelOpLT 0 = 'Just Fail

SimplifyCompareLength 'RelOpLTE 0 = 'Just (CompareLength 'RelOpEQ 0)

SimplifyCompareLength 'RelOpGTE 0 = 'Just Succeed

SimplifyCompareLength 'RelOpGT 0 = 'Just (CompareLength 'RelOpEQ 0)

SimplifyCompareLength op n = 'Nothing :: Maybe Type

type family SimplifyCompareLengthAnd (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) :: Maybe Type where ...

Equations

SimplifyCompareLengthAnd 'RelOpLT n 'RelOpGT m = OrdCond (CmpNat n m) ('Just Fail) ('Just Fail) ('Nothing :: Maybe Type)

SimplifyCompareLengthAnd 'RelOpGT m 'RelOpLT n = OrdCond (CmpNat n m) ('Just Fail) ('Just Fail) ('Nothing :: Maybe Type)

SimplifyCompareLengthAnd lop ln rop rn = 'Nothing :: Maybe Type

type family SimplifyCompareLengthOr (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) :: Maybe Type where ...

Equations

SimplifyCompareLengthOr 'RelOpLT n 'RelOpGT m = OrdCond (CmpNat n m) ('Nothing :: Maybe Type) ('Just (CompareLength 'RelOpNEQ n)) ('Just Succeed)

SimplifyCompareLengthOr 'RelOpGT m 'RelOpLT n = OrdCond (CmpNat n m) ('Nothing :: Maybe Type) ('Just (CompareLength 'RelOpNEQ n)) ('Just Succeed)

SimplifyCompareLengthOr lop ln rop rn = 'Nothing :: Maybe Type