Skip to content

Commit

Permalink
Simplify: +TrySimplify; tweak modules
Browse files Browse the repository at this point in the history
  • Loading branch information
@raehik
raehik committed Oct 11, 2024
1 parent 5e52d21 commit b706e55
Show file tree
Hide file tree
Showing 4 changed files with 271 additions and 239 deletions.
1 change: 1 addition & 0 deletions rerefined.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ library
Rerefined.Refine
Rerefined.Refine.TH
Rerefined.Simplify
Rerefined.Simplify.Core
Rerefined.Simplify.Relational
other-modules:
Paths_rerefined
Expand Down
250 changes: 11 additions & 239 deletions src/Rerefined/Simplify.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
Loading

0 comments on commit b706e55

Please sign in to comment.