rerefined-0.8.0: Refinement types, again
Safe HaskellNone
LanguageGHC2021

Rerefined.Simplify.Core

Description

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.

Synopsis

Documentation

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

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

Equations

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