-----------------------------------------------------------------------------
-- 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: InverseRules.hs 6548 2014-05-16 10:34:18Z bastiaan $

module Domain.Logic.InverseRules
   ( inverseDeMorganOr, inverseDeMorganAnd
   , inverseAndOverOr, inverseOrOverAnd
   ) 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

-----------------------------------------------------------------------------
-- Inverse rules

-- generalized (works for multiple terms)
inverseDeMorganOr :: Rule SLogic
inverseDeMorganOr = siblingOf groupDeMorgan $
   makeSimpleRule "InvDeMorganOr" $ \p -> do
      let xs = conjunctions p
      guard (length xs > 1)
      ys <- mapM isComplement xs
      return (Not $ ors ys)

-- generalized (works for multiple terms)
inverseDeMorganAnd :: Rule SLogic
inverseDeMorganAnd = siblingOf groupDeMorgan $
   makeSimpleRule "InvDeMorganAnd" $ \p -> do
      let xs = disjunctions p
      guard (length xs > 1)
      ys <- mapM isComplement xs
      return (Not $ ands ys)

inverseAndOverOr :: Rule SLogic
inverseAndOverOr = siblingOf groupDistribution $
   makeSimpleRule "InvAndOverOr" $ \p -> do
      let xs = disjunctions p
      guard (length xs > 1)
      do pairs <- mapM isAndHead xs
         let (as, ys) = unzip pairs
         guard (allSame as)
         return (head as :&&: ors ys)
       `mplus` do
         pairs <- mapM isAndLast xs
         let (ys, as) = unzip pairs
         guard (allSame as)
         return (ors ys :&&: head as)

inverseOrOverAnd :: Rule SLogic
inverseOrOverAnd = siblingOf groupDistribution $
   makeSimpleRule "InvOrOverAnd" $ \p -> do
      let xs = conjunctions p
      guard (length xs > 1)
      do pairs <- mapM isOrHead xs
         let (as, ys) = unzip pairs
         guard (allSame as)
         return (head as :||: ands ys)
       `mplus` do
         pairs <- mapM isOrLast xs
         let (ys, as) = unzip pairs
         guard (allSame as)
         return (ands ys :||: head as)

isAndHead, isAndLast, isOrHead, isOrLast :: SLogic -> Maybe (SLogic, SLogic)
isAndHead = useHead (:&&:) . conjunctions
isAndLast = useLast (:&&:) . conjunctions
isOrHead  = useHead (:||:) . disjunctions
isOrLast  = useLast (:||:) . disjunctions

useHead, useLast :: (a -> a -> a) -> [a] -> Maybe (a, a)
useHead op (x:xs) | not (null xs) =
   Just (x, foldr1 op xs)
useHead _ _ = Nothing

useLast op = fmap (\(x, y) -> (y, x)) . useHead (flip op) . reverse

allSame :: Eq a => [a] -> Bool
allSame []     = True
allSame (x:xs) = all (==x) xs