Strategies.hs

-----------------------------------------------------------------------------
-- Copyright 2014, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-----------------------------------------------------------------------------
--  $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $

module Domain.Logic.Strategies
   ( dnfStrategyDWA, somewhereOr
   , cnfStrategyDWA
   ) where

import Domain.Logic.Formula
import Domain.Logic.GeneralizedRules
import Domain.Logic.Rules
import Ideas.Common.Library

-----------------------------------------------------------------------------
-- To DNF, with priorities (the "DWA" approach)

dnfStrategyDWA :: LabeledStrategy (Context SLogic)
dnfStrategyDWA =  label "Bring to dnf (DWA)" $
   repeatS $ toplevel <|> somewhereOr
      (  label "Simplify"                            simpl
      |> label "Eliminate implications/equivalences" eliminateImplEquiv
      |> label "Eliminate nots"                      eliminateNots
      |> label "Move ors to top"                     orToTop
      )
 where
    toplevel = useRules
       [ ruleFalseZeroOr, ruleTrueZeroOr, ruleIdempOr
       , ruleAbsorpOr, ruleComplOr
       ]
    simpl = somewhere $ useRules
       [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd
       , ruleFalseZeroAnd, ruleNotTrue, ruleNotFalse
       , ruleNotNot, ruleIdempOr, ruleIdempAnd, ruleAbsorpOr, ruleAbsorpAnd
       , ruleComplOr, ruleComplAnd
       ]
    eliminateImplEquiv = somewhere $ useRules
       [ ruleDefImpl, ruleDefEquiv
       ]
    eliminateNots = somewhere $ useRules
       [ generalRuleDeMorganAnd, generalRuleDeMorganOr
       , ruleDeMorganAnd, ruleDeMorganOr
       ]
    orToTop = somewhere $ useRules
       [ generalRuleAndOverOr, ruleAndOverOr ]

-- A specialized variant of the somewhere traversal combinator. Apply
-- the strategy only at (top-level) disjuncts
somewhereOr :: IsStrategy g => g (Context SLogic) -> Strategy (Context SLogic)
somewhereOr s =
   let curIsOr a = case currentInContext a of
                      Just (_ :||: _) -> True
                      _               -> False
   in fix $ \this -> check (Prelude.not . curIsOr) <*> s
                 <|> check curIsOr <*> layer [] this

--check1, check2 :: (a -> Bool) -> Rule a
--check1 p = minorRule $ makeSimpleRule "check1" $ \a -> if p a then Just a else Nothing
--check2 p = minorRule $ makeSimpleRule "check2" $ \a -> if p a then Just a else Nothing

-----------------------------------------------------------------------------
-- To DNF, in four steps
{-
dnfStrategy :: LabeledStrategy (Context SLogic)
dnfStrategy =  label "Bring to dnf"
      $  label "Eliminate constants"                 eliminateConstants
     <*> label "Eliminate implications/equivalences" eliminateImplEquiv
     <*> label "Eliminate nots"                      eliminateNots
     <*> label "Move ors to top"                     orToTop
 where
   eliminateConstants = repeatS $ oncetd $ useRules
      [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd
      , ruleFalseZeroAnd, ruleNotTrue, ruleNotFalse
      -- , ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl
      ]
   eliminateImplEquiv = repeatS $ oncebu $ useRules
      [ ruleDefImpl, ruleDefEquiv
      ]
   eliminateNots = repeatS $ oncetd $
      useRules
         [ generalRuleDeMorganAnd, generalRuleDeMorganOr ]
      |> useRules
         [ ruleDeMorganAnd, ruleDeMorganOr
         , ruleNotNot
         ]
   orToTop = repeatS $ somewhere $
      liftToContext generalRuleAndOverOr |>
      liftToContext ruleAndOverOr -}

-- local helper function
useRules :: [Rule SLogic] -> Strategy (Context SLogic)
useRules = alternatives . map liftToContext

-----------------------------------------------------------------
-- Conjunctive normal form

cnfStrategyDWA :: LabeledStrategy (Context SLogic)
cnfStrategyDWA =  label "Bring to cnf (DWA)" $
   repeatS $ toplevel <|> somewhereAnd -- CHANGED
      (  label "Simplify"                            simpl
      |> label "Eliminate implications/equivalences" eliminateImplEquiv
      |> label "Eliminate nots"                      eliminateNots
      |> label "Move ands to top"                    andToTop -- CHANGED
      )
 where
    toplevel = useRules -- CHANGED
       [ ruleFalseZeroAnd, ruleTrueZeroAnd, ruleIdempAnd
       , ruleAbsorpAnd, ruleComplAnd
       ]
    simpl = somewhere $ useRules
       [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd
       , ruleFalseZeroAnd, ruleNotTrue, ruleNotFalse
       , ruleNotNot, ruleIdempOr, ruleIdempAnd, ruleAbsorpOr, ruleAbsorpAnd
       , ruleComplOr, ruleComplAnd
       ]
    eliminateImplEquiv = somewhere $ useRules
       [ ruleDefImpl, ruleDefEquiv
       ]
    eliminateNots = somewhere $ useRules
       [ generalRuleDeMorganAnd, generalRuleDeMorganOr
       , ruleDeMorganAnd, ruleDeMorganOr
       ]
    andToTop = somewhere $ useRules
       [ generalRuleOrOverAnd, ruleOrOverAnd ]

-- Copied from somewhereAnd (and changed)
somewhereAnd :: IsStrategy g => g (Context SLogic) -> Strategy (Context SLogic)
somewhereAnd s =
   let curIsAnd a = case currentInContext a of
                       Just (_ :&&: _) -> True
                       _               -> False
   in fix $ \this -> check (Prelude.not . curIsAnd) <*> s
                 <|> check curIsAnd <*> layer [] this