-----------------------------------------------------------------------------
-- Copyright 2015, 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 7527 2015-04-08 07:58:06Z bastiaan $

module Domain.Logic.GeneralizedRules
   ( generalRuleDeMorganOr, generalRuleDeMorganAnd
   , generalRuleDistrAnd, generalRuleDistrOr
   ) 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 $ makeListRule "GenDeMorganOr" f
 where
   f (Not e) = do
      xs <- subDisjunctions e
      guard (length xs > 2)
      return (ands (map Not xs))
   f _ = []

generalRuleDeMorganAnd :: Rule SLogic
generalRuleDeMorganAnd =
   siblingOf groupDeMorgan $ makeListRule "GenDeMorganAnd" f
 where
   f (Not e) = do
      xs <- subConjunctions e
      guard (length xs > 2)
      return (ors (map Not xs))
   f _ = []

generalRuleDistrAnd :: Rule SLogic
generalRuleDistrAnd =
   siblingOf groupDistribution $ makeListRule "GenAndOverOr" f
 where
   f (x :&&: y) = do -- left distributive
      ys <- subDisjunctions y
      guard (length ys > 2)
      return (ors (map (x :&&:) ys))
    `mplus` do -- right distributive
      xs <- subDisjunctions x
      guard (length xs > 2)
      return (ors (map (:&&: y) xs))
   f _ = []

generalRuleDistrOr :: Rule SLogic
generalRuleDistrOr =
   siblingOf groupDistribution $ makeListRule "GenOrOverAnd" f
 where
   f (x :||: y) = do -- left distributive
      ys <- subConjunctions y
      guard (length ys > 2)
      return (ands (map (x :||:) ys))
    `mplus` do -- right distributive
       xs <- subConjunctions x
       guard (length xs > 2)
       return (ands (map (:||: y) xs))
   f _ = []

-------------------------------------------------------------------------
-- Helper functions

-- All combinations where some disjunctions are grouped, and others are not
subDisjunctions :: SLogic -> [[SLogic]]
subDisjunctions = subformulas (:||:) . disjunctions

subConjunctions :: SLogic -> [[SLogic]]
subConjunctions = subformulas (:&&:) . conjunctions

subformulas :: (a -> a -> a) -> [a] -> [[a]]
subformulas _  []     = []
subformulas _  [x]    = [[x]]
subformulas op (x:xs) = map (x:) yss ++ [ op x y : ys| y:ys <- yss ]
 where
   yss = subformulas op xs