Rerefined.Simplify

Primitive predicate simplifier.

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.

The simplifier may not be expectected to consistently implement any transformations whatsoever. The only guarantees are

• the output has the same or fewer operations
• the output meaning is identical to the input

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

Documentation

type Simplify p = Simplify' p

Simplify the given predicate.

Returns the input predicate if we were unable to simplify.

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