-----------------------------------------------------------------------------
-- 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)
--
-- Generalized rules, and inverse rules, for De Morgan and distributivity
--
-----------------------------------------------------------------------------
--  $Id: GeneralizedRules.hs 6548 2014-05-16 10:34:18Z bastiaan $

module Domain.Logic.GeneralizedRules
   ( generalRuleDeMorganOr, generalRuleDeMorganAnd
   , generalRuleAndOverOr, generalRuleOrOverAnd
   ) where

-- Note: the generalized rules do not take AC-unification into account,
-- and perhaps they should.
import Control.Monad
import Domain.Logic.Formula
import Domain.Logic.Utils
import Ideas.Common.Library

-----------------------------------------------------------------------------
-- Generalized rules

generalRuleDeMorganOr :: Rule SLogic
generalRuleDeMorganOr =
   siblingOf groupDeMorgan $ makeSimpleRule "GenDeMorganOr" f
 where
   f (Not e) = do
      let xs = disjunctions e
      guard (length xs > 2)
      return (ands (map Not xs))
   f _ = Nothing

generalRuleDeMorganAnd :: Rule SLogic
generalRuleDeMorganAnd =
   siblingOf groupDeMorgan $ makeSimpleRule "GenDeMorganAnd" f
 where
   f (Not e) = do
      let xs = conjunctions e
      guard (length xs > 2)
      return (ors (map Not xs))
   f _ = Nothing

generalRuleAndOverOr :: Rule SLogic
generalRuleAndOverOr =
   siblingOf groupDistribution $ makeSimpleRule "GenAndOverOr" f
 where
   f (x :&&: y) =
      case (disjunctions x, disjunctions y) of
         (xs, _) | length xs > 2 ->
            return (ors (map (:&&: y) xs))
         (_, ys) | length ys > 2 ->
            return (ors (map (x :&&:) ys))
         _ -> Nothing
   f _ = Nothing

generalRuleOrOverAnd :: Rule SLogic
generalRuleOrOverAnd =
   siblingOf groupDistribution $ makeSimpleRule "GenOrOverAnd" f
 where
   f (x :||: y) =
      case (conjunctions x, conjunctions y) of
         (xs, _) | length xs > 2 ->
            return (ands (map (:||: y) xs))
         (_, ys) | length ys > 2 ->
            return (ands (map (x :||:) ys))
         _ -> Nothing
   f _ = Nothing