diff --git a/rerefined.cabal b/rerefined.cabal index 61e52be..d49c3b6 100644 --- a/rerefined.cabal +++ b/rerefined.cabal @@ -54,6 +54,7 @@ library Rerefined.Refine Rerefined.Refine.TH Rerefined.Simplify + Rerefined.Simplify.Core Rerefined.Simplify.Relational other-modules: Paths_rerefined diff --git a/src/Rerefined/Simplify.hs b/src/Rerefined/Simplify.hs index ef34aa4..bc39e59 100644 --- a/src/Rerefined/Simplify.hs +++ b/src/Rerefined/Simplify.hs @@ -2,53 +2,26 @@ {- | 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 +See 'Rerefined.Simplify.Core' (internal module) for more details. -} module Rerefined.Simplify ( Simplify + , TrySimplify , SimplifyStep ) where -import Rerefined.Predicate.Succeed -import Rerefined.Predicate.Fail - -import Rerefined.Predicate.Logical - -import Rerefined.Predicate.Relational ( CompareLength, CompareValue, FlipRelOp ) -import Rerefined.Simplify.Relational - ( SimplifyCompareLength - , SimplifyCompareLengthAnd - , SimplifyCompareLengthOr - ) - -import Data.Kind ( Type ) - --- note that we can't modularize logical simplifications because they're --- mutually recursive with the main simplifier :( +import Rerefined.Simplify.Core ( SimplifyStep ) -- | Simplify the given predicate. -- -- Returns the input predicate if we were unable to simplify. -type Simplify :: Type -> Type type Simplify p = Simplify' p -- | Helper definition for reducing duplication. @@ -62,216 +35,15 @@ type family SimplifyLoop p mp where -- failed to simplify: give up, return the latest predicate SimplifyLoop p Nothing = p --- | Try to perform a single simplification step on the given predicate. +-- | Try to simplify the given predicate. -- -- Returns 'Nothing' if we were unable to simplify. -type family SimplifyStep p where - 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 - -- Don't think we can do anything for CompareValue. - - SimplifyStep p = Nothing - -type family SimplifyAnd l r where - -- identity laws - 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 - - -- distributivity - SimplifyAnd (Or x y) (Or x z) = Just (Or x (And y z)) - - -- special - SimplifyAnd (CompareLength lop ln) (CompareLength rop rn) = - SimplifyCompareLengthAnd lop ln rop rn - - -- recurse - SimplifyAnd l r = - (OrElseAndL r (SimplifyStep l) - (OrElseAndR l (SimplifyStep r) - Nothing)) - -type family OrElseAndL r mp cont where - OrElseAndL r Nothing cont = cont - OrElseAndL r (Just l') cont = Just (And l' r) - -type family OrElseAndR l mp cont where - OrElseAndR l Nothing cont = cont - OrElseAndR l (Just r') cont = Just (And l r') - -type family SimplifyOr l r where - -- identity laws - 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 - - -- distributivity - SimplifyOr (And x y) (And x z) = Just (And x (Or y z)) - - -- special relational - SimplifyOr (CompareLength lop ln) (CompareLength rop rn) = - SimplifyCompareLengthOr lop ln rop rn - - -- recurse - SimplifyOr l r = - (OrElseOrL r (SimplifyStep l) - (OrElseOrR l (SimplifyStep r) - Nothing)) - -type family OrElseOrL r mp cont where - OrElseOrL r Nothing cont = cont - OrElseOrL r (Just l') cont = Just (Or l' r) - -type family OrElseOrR l mp cont where - OrElseOrR l Nothing cont = cont - OrElseOrR l (Just r') cont = Just (Or l r') - -type family SimplifyNand l r where - -- identity laws - 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) - - -- recurse - SimplifyNand l r = - (OrElseNandL r (SimplifyStep l) - (OrElseNandR l (SimplifyStep r) - Nothing)) - -type family OrElseNandL r mp cont where - OrElseNandL r Nothing cont = cont - OrElseNandL r (Just l') cont = Just (Nand l' r) - -type family OrElseNandR l mp cont where - OrElseNandR l Nothing cont = cont - OrElseNandR l (Just r') cont = Just (Nand l r') - -type family SimplifyNor l r where - -- identity laws - 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) - - -- recurse - SimplifyNor l r = - (OrElseNorL r (SimplifyStep l) - (OrElseNorR l (SimplifyStep r) - Nothing)) - -type family OrElseNorL r mp cont where - OrElseNorL r Nothing cont = cont - OrElseNorL r (Just l') cont = Just (Nor l' r) - -type family OrElseNorR l mp cont where - OrElseNorR l Nothing cont = cont - OrElseNorR l (Just r') cont = Just (Nor l r') - -type family SimplifyXor l r where - -- identity laws - 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 - - -- recurse - SimplifyXor l r = - (OrElseXorL r (SimplifyStep l) - (OrElseXorR l (SimplifyStep r) - Nothing)) - -type family OrElseXorL r mp cont where - OrElseXorL r Nothing cont = cont - OrElseXorL r (Just l') cont = Just (Xor l' r) - -type family OrElseXorR l mp cont where - OrElseXorR l Nothing cont = cont - OrElseXorR l (Just r') cont = Just (Xor l r') - -type family SimplifyIf l r where - -- identity laws - 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 - - -- recurse - SimplifyIf l r = - (OrElseIfL r (SimplifyStep l) - (OrElseIfR l (SimplifyStep r) - Nothing)) - -type family OrElseIfL r mp cont where - OrElseIfL r Nothing cont = cont - OrElseIfL r (Just l') cont = Just (If l' r) - -type family OrElseIfR l mp cont where - OrElseIfR l Nothing cont = cont - OrElseIfR l (Just r') cont = Just (If l r') - -type family SimplifyIff l r where - -- identity laws - 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 - - -- recurse - SimplifyIff l r = - (OrElseIffL r (SimplifyStep l) - (OrElseIffR l (SimplifyStep r) - Nothing)) - -type family OrElseIffL r mp cont where - OrElseIffL r Nothing cont = cont - OrElseIffL r (Just l') cont = Just (Iff l' r) - -type family OrElseIffR l mp cont where - OrElseIffR l Nothing cont = cont - OrElseIffR l (Just r') cont = Just (Iff l r') - -type family SimplifyNot p where - -- double negation - SimplifyNot (Not p) = Just p - - SimplifyNot Succeed = Just Fail - SimplifyNot Fail = Just Succeed - - -- special relational - SimplifyNot (CompareLength op n) = - Just (CompareLength (FlipRelOp op) n) - SimplifyNot (CompareValue op sign n) = - Just (CompareValue (FlipRelOp op) sign n) +type TrySimplify p = TrySimplifyLoop p (SimplifyStep p) - -- recurse - SimplifyNot p = OrElseNot (SimplifyStep p) Nothing +-- | Simplification loop which returns 'Nothing' for 0 simplifications. +type family TrySimplifyLoop p mp where + -- got a simplification: continue with the regular simplifier + TrySimplifyLoop p (Just p') = Just (Simplify' p') -type family OrElseNot mp cont where - OrElseNot (Just p') cont = Just (Not p') - OrElseNot Nothing cont = cont + -- couldn't simplify + TrySimplifyLoop p Nothing = Nothing diff --git a/src/Rerefined/Simplify/Core.hs b/src/Rerefined/Simplify/Core.hs new file mode 100644 index 0000000..19414c4 --- /dev/null +++ b/src/Rerefined/Simplify/Core.hs @@ -0,0 +1,251 @@ +{-# LANGUAGE UndecidableInstances #-} + +{- | 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.__ +-} + +module Rerefined.Simplify.Core where + +import Rerefined.Predicate.Succeed +import Rerefined.Predicate.Fail + +import Rerefined.Predicate.Logical + +import Rerefined.Predicate.Relational ( CompareLength, CompareValue, FlipRelOp ) +import Rerefined.Simplify.Relational + ( SimplifyCompareLength + , SimplifyCompareLengthAnd + , SimplifyCompareLengthOr + ) + +-- note that we can't modularize logical simplifications because they're +-- mutually recursive with the main simplifier :( + +-- | Try to perform a single simplification step on the given predicate. +-- +-- Returns 'Nothing' if we were unable to simplify. +type family SimplifyStep p where + 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 + -- Don't think we can do anything for CompareValue. + + SimplifyStep p = Nothing + +type family SimplifyAnd l r where + -- identity laws + 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 + + -- distributivity + SimplifyAnd (Or x y) (Or x z) = Just (Or x (And y z)) + + -- special + SimplifyAnd (CompareLength lop ln) (CompareLength rop rn) = + SimplifyCompareLengthAnd lop ln rop rn + + -- recurse + SimplifyAnd l r = + (OrElseAndL r (SimplifyStep l) + (OrElseAndR l (SimplifyStep r) + Nothing)) + +type family OrElseAndL r mp cont where + OrElseAndL r Nothing cont = cont + OrElseAndL r (Just l') cont = Just (And l' r) + +type family OrElseAndR l mp cont where + OrElseAndR l Nothing cont = cont + OrElseAndR l (Just r') cont = Just (And l r') + +type family SimplifyOr l r where + -- identity laws + 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 + + -- distributivity + SimplifyOr (And x y) (And x z) = Just (And x (Or y z)) + + -- special relational + SimplifyOr (CompareLength lop ln) (CompareLength rop rn) = + SimplifyCompareLengthOr lop ln rop rn + + -- recurse + SimplifyOr l r = + (OrElseOrL r (SimplifyStep l) + (OrElseOrR l (SimplifyStep r) + Nothing)) + +type family OrElseOrL r mp cont where + OrElseOrL r Nothing cont = cont + OrElseOrL r (Just l') cont = Just (Or l' r) + +type family OrElseOrR l mp cont where + OrElseOrR l Nothing cont = cont + OrElseOrR l (Just r') cont = Just (Or l r') + +type family SimplifyNand l r where + -- identity laws + 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) + + -- recurse + SimplifyNand l r = + (OrElseNandL r (SimplifyStep l) + (OrElseNandR l (SimplifyStep r) + Nothing)) + +type family OrElseNandL r mp cont where + OrElseNandL r Nothing cont = cont + OrElseNandL r (Just l') cont = Just (Nand l' r) + +type family OrElseNandR l mp cont where + OrElseNandR l Nothing cont = cont + OrElseNandR l (Just r') cont = Just (Nand l r') + +type family SimplifyNor l r where + -- identity laws + 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) + + -- recurse + SimplifyNor l r = + (OrElseNorL r (SimplifyStep l) + (OrElseNorR l (SimplifyStep r) + Nothing)) + +type family OrElseNorL r mp cont where + OrElseNorL r Nothing cont = cont + OrElseNorL r (Just l') cont = Just (Nor l' r) + +type family OrElseNorR l mp cont where + OrElseNorR l Nothing cont = cont + OrElseNorR l (Just r') cont = Just (Nor l r') + +type family SimplifyXor l r where + -- identity laws + 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 + + -- recurse + SimplifyXor l r = + (OrElseXorL r (SimplifyStep l) + (OrElseXorR l (SimplifyStep r) + Nothing)) + +type family OrElseXorL r mp cont where + OrElseXorL r Nothing cont = cont + OrElseXorL r (Just l') cont = Just (Xor l' r) + +type family OrElseXorR l mp cont where + OrElseXorR l Nothing cont = cont + OrElseXorR l (Just r') cont = Just (Xor l r') + +type family SimplifyIf l r where + -- identity laws + 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 + + -- recurse + SimplifyIf l r = + (OrElseIfL r (SimplifyStep l) + (OrElseIfR l (SimplifyStep r) + Nothing)) + +type family OrElseIfL r mp cont where + OrElseIfL r Nothing cont = cont + OrElseIfL r (Just l') cont = Just (If l' r) + +type family OrElseIfR l mp cont where + OrElseIfR l Nothing cont = cont + OrElseIfR l (Just r') cont = Just (If l r') + +type family SimplifyIff l r where + -- identity laws + 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 + + -- recurse + SimplifyIff l r = + (OrElseIffL r (SimplifyStep l) + (OrElseIffR l (SimplifyStep r) + Nothing)) + +type family OrElseIffL r mp cont where + OrElseIffL r Nothing cont = cont + OrElseIffL r (Just l') cont = Just (Iff l' r) + +type family OrElseIffR l mp cont where + OrElseIffR l Nothing cont = cont + OrElseIffR l (Just r') cont = Just (Iff l r') + +type family SimplifyNot p where + -- double negation + SimplifyNot (Not p) = Just p + + SimplifyNot Succeed = Just Fail + SimplifyNot Fail = Just Succeed + + -- special relational + SimplifyNot (CompareLength op n) = + Just (CompareLength (FlipRelOp op) n) + SimplifyNot (CompareValue op sign n) = + Just (CompareValue (FlipRelOp op) sign n) + + -- recurse + SimplifyNot p = OrElseNot (SimplifyStep p) Nothing + +type family OrElseNot mp cont where + OrElseNot (Just p') cont = Just (Not p') + OrElseNot Nothing cont = cont diff --git a/src/Rerefined/Simplify/Relational.hs b/src/Rerefined/Simplify/Relational.hs index bee2cf2..aa433a5 100644 --- a/src/Rerefined/Simplify/Relational.hs +++ b/src/Rerefined/Simplify/Relational.hs @@ -1,5 +1,13 @@ {-# LANGUAGE UndecidableInstances #-} +{- | 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.__ +-} + module Rerefined.Simplify.Relational where import Rerefined.Predicate.Succeed