From 9c84c0609f9f2ff88506792b1e2bfff492bf5d5c Mon Sep 17 00:00:00 2001 From: Ben Orchard Date: Thu, 10 Oct 2024 22:15:00 +0100 Subject: [PATCH] add predicate simplifier --- TODO.md | 7 - rerefined.cabal | 3 +- src/Rerefined/Predicate/Logical/Normalize.hs | 10 - src/Rerefined/Predicate/Normalize.hs | 12 -- src/Rerefined/Simplify.hs | 190 +++++++++++++++++++ 5 files changed, 191 insertions(+), 31 deletions(-) delete mode 100644 src/Rerefined/Predicate/Logical/Normalize.hs delete mode 100644 src/Rerefined/Predicate/Normalize.hs create mode 100644 src/Rerefined/Simplify.hs diff --git a/TODO.md b/TODO.md index 258f2aa..a4a1715 100644 --- a/TODO.md +++ b/TODO.md @@ -15,13 +15,6 @@ ## Predicates * `All ps`, `And` a list of predicates? My errors work for it. Seems fun. -## Predicate normalization -I've got basic logical predicate normalization. It seems adding further -normalization will be more complicated. Relational normalization seems to -rely on inspecting logical predicates as well e.g. `(< n) && (> m) where n > m = -_|_`. I'm fairly certain we have to take a heuristic approach, and I'm fairly -happy with leaving this for a while. - ## Predicate names: fixity I do precedence, but not associativity. Not sure how to. `Show` doesn't help. See: http://intrologic.stanford.edu/dictionary/operator_precedence.html diff --git a/rerefined.cabal b/rerefined.cabal index efeb7d6..c4620f1 100644 --- a/rerefined.cabal +++ b/rerefined.cabal @@ -40,11 +40,9 @@ library Rerefined.Predicate.Logical.Iff Rerefined.Predicate.Logical.Nand Rerefined.Predicate.Logical.Nor - Rerefined.Predicate.Logical.Normalize Rerefined.Predicate.Logical.Not Rerefined.Predicate.Logical.Or Rerefined.Predicate.Logical.Xor - Rerefined.Predicate.Normalize Rerefined.Predicate.Relational Rerefined.Predicate.Relational.Internal Rerefined.Predicate.Relational.Length @@ -55,6 +53,7 @@ library Rerefined.Predicates.Operators Rerefined.Refine Rerefined.Refine.TH + Rerefined.Simplify other-modules: Paths_rerefined hs-source-dirs: diff --git a/src/Rerefined/Predicate/Logical/Normalize.hs b/src/Rerefined/Predicate/Logical/Normalize.hs deleted file mode 100644 index 445969b..0000000 --- a/src/Rerefined/Predicate/Logical/Normalize.hs +++ /dev/null @@ -1,10 +0,0 @@ -module Rerefined.Predicate.Logical.Normalize where - -import Rerefined.Predicate.Logical - -type family NormLogi p where - NormLogi (Not (Not p)) = Just p - NormLogi (Or l l) = Just l - NormLogi (And l l) = Just l - NormLogi (Nand l l) = Just (Not l) - NormLogi p = Nothing diff --git a/src/Rerefined/Predicate/Normalize.hs b/src/Rerefined/Predicate/Normalize.hs deleted file mode 100644 index d346d75..0000000 --- a/src/Rerefined/Predicate/Normalize.hs +++ /dev/null @@ -1,12 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - -module Rerefined.Predicate.Normalize where - -import Rerefined.Predicate.Logical.Normalize - -type family Norm p where - Norm p = Norm' p (NormLogi p) - -type family Norm' p mp where - Norm' p Nothing = p - Norm' p (Just p') = Norm p' diff --git a/src/Rerefined/Simplify.hs b/src/Rerefined/Simplify.hs new file mode 100644 index 0000000..587528e --- /dev/null +++ b/src/Rerefined/Simplify.hs @@ -0,0 +1,190 @@ +{-# LANGUAGE UndecidableInstances #-} + +{- | 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. + +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 +-} + +module Rerefined.Simplify + ( Simplify + , Simplify' + ) where + +import Rerefined.Predicate.Succeed +import Rerefined.Predicate.Fail + +import Rerefined.Predicate.Logical + +import Rerefined.Predicate.Relational +import GHC.TypeNats ( Natural, CmpNat ) +import Data.Type.Ord ( OrdCond ) + +-- | Simplify the given predicate. +-- +-- Returns the input predicate if we were unable to simplify. +type Simplify p = FromMaybe p (Simplify' p) + +-- | Promoted 'Data.Maybe.fromMaybe'. +type family FromMaybe a ma where + FromMaybe a Nothing = a + FromMaybe a (Just a') = a' + +-- | Try to simplify the given predicate. +-- +-- Returns 'Nothing' if we were unable to simplify. +type family Simplify' p where + Simplify' (And l r) = SimplifyAnd l r + Simplify' (Or l r) = SimplifyOr l r + Simplify' (Nand l r) = SimplifyNand l r + Simplify' (Not p) = SimplifyNot p + + Simplify' (CompareLength op n) = SimplifyCompareLength op n + + Simplify' 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 (Simplify' l) + (OrElseAndR l (Simplify' 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 + SimplifyOr (CompareLength lop ln) (CompareLength rop rn) = + SimplifyCompareLengthOr lop ln rop rn + + -- recurse + SimplifyOr l r = + (OrElseOrL r (Simplify' l) + (OrElseOrR l (Simplify' 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 SimplifyCompareLength (op :: RelOp) (n :: Natural) where + SimplifyCompareLength RelOpLT 0 = Just Fail + SimplifyCompareLength RelOpLTE 0 = Just (CompareLength RelOpEQ 0) + + -- TODO I think that's it for single relational predicates. + SimplifyCompareLength op n = Nothing + +type family SimplifyCompareLengthAnd + (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) where + -- @m@: @n<=m@ -> False + SimplifyCompareLengthAnd RelOpLT n RelOpGT m = + OrdCond (CmpNat n m) + (Just Fail) + (Just Fail) + Nothing + SimplifyCompareLengthAnd RelOpGT m RelOpLT n = + OrdCond (CmpNat n m) + (Just Fail) + (Just Fail) + Nothing + + SimplifyCompareLengthAnd lop ln rop rn = Nothing + +type family SimplifyCompareLengthOr + (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) where + -- @m@: @n==m@ -> NEQ; @n>m@ -> True (?) + SimplifyCompareLengthOr RelOpLT n RelOpGT m = + OrdCond (CmpNat n m) + Nothing + (Just (CompareLength RelOpNEQ n)) + (Just Succeed) + SimplifyCompareLengthOr RelOpGT m RelOpLT n = + OrdCond (CmpNat n m) + Nothing + (Just (CompareLength RelOpNEQ n)) + (Just Succeed) + + SimplifyCompareLengthOr lop ln rop rn = Nothing + +type family SimplifyNand l r where + -- TODO fill in rest + SimplifyNand p p = Just (Not p) + + -- recurse + SimplifyNand l r = + (OrElseNandL r (Simplify' l) + (OrElseNandR l (Simplify' 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 SimplifyNot p where + -- double negation + SimplifyNot (Not p) = Just p + + SimplifyNot Succeed = Just Fail + SimplifyNot Fail = Just Succeed + + -- TODO handle relational predicates! + + -- recurse + SimplifyNot p = OrElseNot (Simplify' p) Nothing + +type family OrElseNot mp cont where + OrElseNot Nothing cont = cont + OrElseNot (Just p') cont = Just (Not p')