Simplify.hs

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

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
-}

module Rerefined.Simplify
  ( Simplify
  , 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 :(

-- | 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.
type Simplify' p = SimplifyLoop p (SimplifyStep p)

-- | Simplification loop.
type family SimplifyLoop p mp where
    -- simplification step succeeded: try again on the simplified predicate
    SimplifyLoop p (Just p') = Simplify' p'

    -- failed to simplify: give up, return the latest predicate
    SimplifyLoop p Nothing   = p

-- | 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