Rerefined.Simplify.Core

Core predicate simplification algorithm.

This is related to an NP-complete problem (see Boolean satisfiability problem). We focus on immediate, operation-reducing simplifications, and hope that the input is formed in such a way that our rules match.

In short, the simplifier is largely contextless. It inspects (usually) a single layer/depth at a time. So we can consistently simplify things like logical identities. But don't expect simplifications hard to spot with the naked eye.

Implementation pitfalls:

• not extensible: only works for built-in logical & relational predicates
• no protection against non-termination e.g. if a pair of transformations loop
• very tedious to write. that's life

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

Documentation

type family SimplifyStep p :: Maybe Type where ...

Try to perform a single simplification step on the given predicate.

Returns Nothing if we were unable to simplify.

Equations

SimplifyStep (Not p) = SimplifyNot p

SimplifyStep (And l r) = SimplifyAnd l r

SimplifyStep (Or l r) = SimplifyOr l r

SimplifyStep (Nand l r) = SimplifyNand l r

SimplifyStep (Nor l r) = SimplifyNor l r

SimplifyStep (Iff l r) = SimplifyIff l r

SimplifyStep (Xor l r) = SimplifyXor l r

SimplifyStep (If l r) = SimplifyIf l r

SimplifyStep (CompareLength op n) = SimplifyCompareLength op n

SimplifyStep p = 'Nothing :: Maybe Type

type family SimplifyAnd l r :: Maybe Type where ...

Equations

SimplifyAnd p Fail = 'Just Fail

SimplifyAnd Fail p = 'Just Fail

SimplifyAnd p Succeed = 'Just p

SimplifyAnd Succeed p = 'Just p

SimplifyAnd p p = 'Just p

SimplifyAnd (Or x y) (Or x z) = 'Just (Or x (And y z))

SimplifyAnd (CompareLength lop ln) (CompareLength rop rn) = SimplifyCompareLengthAnd lop ln rop rn

SimplifyAnd l r = OrElseAndL r (SimplifyStep l) (OrElseAndR l (SimplifyStep r) ('Nothing :: Maybe Type))

type family OrElseAndL (r :: k1) (mp :: Maybe k) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseAndL (r :: k1) ('Nothing :: Maybe k) cont = cont

OrElseAndL (r :: k1) ('Just l' :: Maybe k) cont = 'Just (And l' r)

type family OrElseAndR (l :: k) (mp :: Maybe k1) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseAndR (l :: k) ('Nothing :: Maybe k1) cont = cont

OrElseAndR (l :: k) ('Just r' :: Maybe k1) cont = 'Just (And l r')

type family SimplifyOr l r :: Maybe Type where ...

Equations

SimplifyOr Succeed p = 'Just Succeed

SimplifyOr p Succeed = 'Just Succeed

SimplifyOr Fail p = 'Just p

SimplifyOr p Fail = 'Just p

SimplifyOr p p = 'Just p

SimplifyOr (And x y) (And x z) = 'Just (And x (Or y z))

SimplifyOr (CompareLength lop ln) (CompareLength rop rn) = SimplifyCompareLengthOr lop ln rop rn

SimplifyOr l r = OrElseOrL r (SimplifyStep l) (OrElseOrR l (SimplifyStep r) ('Nothing :: Maybe Type))

type family OrElseOrL (r :: k1) (mp :: Maybe k) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseOrL (r :: k1) ('Nothing :: Maybe k) cont = cont

OrElseOrL (r :: k1) ('Just l' :: Maybe k) cont = 'Just (Or l' r)

type family OrElseOrR (l :: k) (mp :: Maybe k1) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseOrR (l :: k) ('Nothing :: Maybe k1) cont = cont

OrElseOrR (l :: k) ('Just r' :: Maybe k1) cont = 'Just (Or l r')

type family SimplifyNand l r :: Maybe Type where ...

Equations

SimplifyNand Fail p = 'Just Succeed

SimplifyNand p Fail = 'Just Succeed

SimplifyNand Succeed p = 'Just (Not p)

SimplifyNand p Succeed = 'Just (Not p)

SimplifyNand p p = 'Just (Not p)

SimplifyNand l r = OrElseNandL r (SimplifyStep l) (OrElseNandR l (SimplifyStep r) ('Nothing :: Maybe Type))

type family OrElseNandL (r :: k1) (mp :: Maybe k) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseNandL (r :: k1) ('Nothing :: Maybe k) cont = cont

OrElseNandL (r :: k1) ('Just l' :: Maybe k) cont = 'Just (Nand l' r)

type family OrElseNandR (l :: k) (mp :: Maybe k1) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseNandR (l :: k) ('Nothing :: Maybe k1) cont = cont

OrElseNandR (l :: k) ('Just r' :: Maybe k1) cont = 'Just (Nand l r')

type family SimplifyNor l r :: Maybe Type where ...

Equations

SimplifyNor Succeed p = 'Just Fail

SimplifyNor p Succeed = 'Just Fail

SimplifyNor Fail p = 'Just (Not p)

SimplifyNor p Fail = 'Just (Not p)

SimplifyNor p p = 'Just (Not p)

SimplifyNor l r = OrElseNorL r (SimplifyStep l) (OrElseNorR l (SimplifyStep r) ('Nothing :: Maybe Type))

type family OrElseNorL (r :: k1) (mp :: Maybe k) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseNorL (r :: k1) ('Nothing :: Maybe k) cont = cont

OrElseNorL (r :: k1) ('Just l' :: Maybe k) cont = 'Just (Nor l' r)

type family OrElseNorR (l :: k) (mp :: Maybe k1) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseNorR (l :: k) ('Nothing :: Maybe k1) cont = cont

OrElseNorR (l :: k) ('Just r' :: Maybe k1) cont = 'Just (Nor l r')

type family SimplifyXor l r :: Maybe Type where ...

Equations

SimplifyXor Fail p = 'Just p

SimplifyXor p Fail = 'Just p

SimplifyXor Succeed p = 'Just (Not p)

SimplifyXor p Succeed = 'Just (Not p)

SimplifyXor p p = 'Just Fail

SimplifyXor l r = OrElseXorL r (SimplifyStep l) (OrElseXorR l (SimplifyStep r) ('Nothing :: Maybe Type))

type family OrElseXorL (r :: k1) (mp :: Maybe k) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseXorL (r :: k1) ('Nothing :: Maybe k) cont = cont

OrElseXorL (r :: k1) ('Just l' :: Maybe k) cont = 'Just (Xor l' r)

type family OrElseXorR (l :: k) (mp :: Maybe k1) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseXorR (l :: k) ('Nothing :: Maybe k1) cont = cont

OrElseXorR (l :: k) ('Just r' :: Maybe k1) cont = 'Just (Xor l r')

type family SimplifyIf l r :: Maybe Type where ...

Equations

SimplifyIf Fail p = 'Just Succeed

SimplifyIf p Fail = 'Just Succeed

SimplifyIf Succeed p = 'Just p

SimplifyIf p Succeed = 'Just p

SimplifyIf p p = 'Just Succeed

SimplifyIf l r = OrElseIfL r (SimplifyStep l) (OrElseIfR l (SimplifyStep r) ('Nothing :: Maybe Type))

type family OrElseIfL (r :: k1) (mp :: Maybe k) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseIfL (r :: k1) ('Nothing :: Maybe k) cont = cont

OrElseIfL (r :: k1) ('Just l' :: Maybe k) cont = 'Just (If l' r)

type family OrElseIfR (l :: k) (mp :: Maybe k1) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseIfR (l :: k) ('Nothing :: Maybe k1) cont = cont

OrElseIfR (l :: k) ('Just r' :: Maybe k1) cont = 'Just (If l r')

type family SimplifyIff l r :: Maybe Type where ...

Equations

SimplifyIff Succeed p = 'Just p

SimplifyIff p Succeed = 'Just p

SimplifyIff Fail p = 'Just (Not p)

SimplifyIff p Fail = 'Just (Not p)

SimplifyIff p p = 'Just Succeed

SimplifyIff l r = OrElseIffL r (SimplifyStep l) (OrElseIffR l (SimplifyStep r) ('Nothing :: Maybe Type))

type family OrElseIffL (r :: k1) (mp :: Maybe k) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseIffL (r :: k1) ('Nothing :: Maybe k) cont = cont

OrElseIffL (r :: k1) ('Just l' :: Maybe k) cont = 'Just (Iff l' r)

type family OrElseIffR (l :: k) (mp :: Maybe k1) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseIffR (l :: k) ('Nothing :: Maybe k1) cont = cont

OrElseIffR (l :: k) ('Just r' :: Maybe k1) cont = 'Just (Iff l r')

type family SimplifyNot p :: Maybe Type where ...

Equations

SimplifyNot (Not p) = 'Just p

SimplifyNot Succeed = 'Just Fail

SimplifyNot Fail = 'Just Succeed

SimplifyNot (CompareLength op n) = 'Just (CompareLength (FlipRelOp op) n)

SimplifyNot (CompareValue op sign n) = 'Just (CompareValue (FlipRelOp op) sign n)

SimplifyNot p = OrElseNot (SimplifyStep p) ('Nothing :: Maybe Type)

type family OrElseNot (mp :: Maybe k) (cont :: Maybe Type) :: Maybe Type where ...

Equations

OrElseNot ('Just p' :: Maybe k) cont = 'Just (Not p')

OrElseNot ('Nothing :: Maybe k) cont = cont