content: {- |
  Module      :  ./Propositional/Fold.hs
  Description :  folding function for propositional formulas
  Copyright   :  (c) Christian Maeder, DFKI GmbH 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  folding and simplification of propositional formulas
  
  -}
  
  module Propositional.Fold where
  
  import Common.Id
  import Propositional.AS_BASIC_Propositional
  
  import qualified Data.Set as Set
  
  data FoldRecord a = FoldRecord
    { foldNegation :: a -> Range -> a
    , foldConjunction :: [a] -> Range -> a
    , foldDisjunction :: [a] -> Range -> a
    , foldImplication :: a -> a -> Range -> a
    , foldEquivalence :: a -> a -> Range -> a
    , foldTrue_atom :: Range -> a
    , foldFalse_atom :: Range -> a
    , foldPredication :: Token -> a }
  
  foldFormula :: FoldRecord a -> FORMULA -> a
  foldFormula r frm = case frm of
     Negation f n -> foldNegation r (foldFormula r f) n
     Conjunction xs n -> foldConjunction r (map (foldFormula r) xs) n
     Disjunction xs n -> foldDisjunction r (map (foldFormula r) xs) n
     Implication x y n -> foldImplication r (foldFormula r x) (foldFormula r y) n
     Equivalence x y n -> foldEquivalence r (foldFormula r x) (foldFormula r y) n
     True_atom n -> foldTrue_atom r n
     False_atom n -> foldFalse_atom r n
     Predication x -> foldPredication r x
  
  mapRecord :: FoldRecord FORMULA
  mapRecord = FoldRecord
    { foldNegation = Negation
    , foldConjunction = Conjunction
    , foldDisjunction = Disjunction
    , foldImplication = Implication
    , foldEquivalence = Equivalence
    , foldTrue_atom = True_atom
    , foldFalse_atom = False_atom
    , foldPredication = Predication }
  
  isNeg :: FORMULA -> Bool
  isNeg f = case f of
    Negation _ _ -> True
    _ -> False
  
  getLits :: Set.Set FORMULA -> Set.Set FORMULA
  getLits = Set.fold (\ f -> case f of
    Negation x _ -> Set.insert x
    _ -> Set.insert f) Set.empty
  
  bothLits :: Set.Set FORMULA -> Bool
  bothLits fs = let
    (ns, ps) = Set.partition isNeg fs
    in not $ Set.null $ Set.intersection (getLits ns) (getLits ps)
  
  getConj :: FORMULA -> [FORMULA]
  getConj f = case f of
    Conjunction xs _ -> xs
    True_atom _ -> []
    _ -> [f]
  
  getDisj :: FORMULA -> [FORMULA]
  getDisj f = case f of
    Disjunction xs _ -> xs
    False_atom _ -> []
    _ -> [f]
  
  flatConj :: [FORMULA] -> Set.Set FORMULA
  flatConj = Set.fromList
    . concatMap (\ f -> case f of
        True_atom _ -> []
        Conjunction fs _ -> fs
        _ -> [f])
  
  mkConj :: [FORMULA] -> Range -> FORMULA
  mkConj fs n = let s = flatConj fs in
    if Set.member (False_atom nullRange) s || bothLits s then False_atom n else
    case Set.toList s of
      [] -> True_atom n
      [x] -> x
      ls -> Conjunction (map (flip mkDisj n . Set.toList)
        $ foldr ((\ l ll ->
          if any (`Set.isSubsetOf` l) ll then ll else
            l : filter (not . Set.isSubsetOf l) ll)
            . Set.fromList . getDisj) [] ls) n
  
  flatDisj :: [FORMULA] -> Set.Set FORMULA
  flatDisj = Set.fromList
    . concatMap (\ f -> case f of
        False_atom _ -> []
        Disjunction fs _ -> fs
        _ -> [f])
  
  mkDisj :: [FORMULA] -> Range -> FORMULA
  mkDisj fs n = let s = flatDisj fs in
    if Set.member (True_atom nullRange) s || bothLits s then True_atom n else
    case Set.toList s of
      [] -> False_atom n
      [x] -> x
      ls -> Disjunction (map (flip mkConj n . Set.toList)
        $ foldr ((\ l ll ->
          if any (`Set.isSubsetOf` l) ll then ll else
            l : filter (not . Set.isSubsetOf l) ll)
            . Set.fromList . getConj) [] ls) n
  
  simplify :: FORMULA -> FORMULA
  simplify = foldFormula mapRecord
    { foldNegation = \ f n -> case f of
      True_atom p -> False_atom p
      False_atom p -> True_atom p
      Negation g _ -> g
      s -> Negation s n
    , foldConjunction = mkConj
    , foldDisjunction = mkDisj
    , foldImplication = \ x y n -> case x of
      False_atom p -> True_atom p
      _ -> if x == y then True_atom n else case x of
             True_atom _ -> y
             False_atom _ -> True_atom n
             Negation z _ | z == y -> x
             _ -> case y of
               Negation z _ | z == x -> x
               _ -> Implication x y n
    , foldEquivalence = \ x y n -> case compare x y of
      LT -> case y of
        Negation z _ | x == z -> False_atom n
        _ -> Equivalence x y n
      EQ -> True_atom n
      GT -> case x of
        Negation z _ | z == y -> False_atom n
        _ -> Equivalence y x n }
  
  elimEquiv :: FORMULA -> FORMULA
  elimEquiv = foldFormula mapRecord
    { foldEquivalence = \ x y n ->
      Conjunction [Implication x y n, Implication y x n] n }
  
  elimImpl :: FORMULA -> FORMULA
  elimImpl = foldFormula mapRecord
    { foldImplication = \ x y n ->
      Disjunction [Negation x n, y] n }
  
  negForm :: Range -> FORMULA -> FORMULA
  negForm r frm = case frm of
    Negation f _ -> case f of
      Negation nf _ -> negForm r nf
      _ -> f
    Conjunction xs n -> Disjunction (map (negForm r) xs) n
    Disjunction xs n -> Conjunction (map (negForm r) xs) n
    True_atom n -> False_atom n
    False_atom n -> True_atom n
    _ -> Negation frm r
  
  moveNegIn :: FORMULA -> FORMULA
  moveNegIn frm = case frm of
    Negation f n -> negForm n f
    Conjunction xs n -> Conjunction (map moveNegIn xs) n
    Disjunction xs n -> Disjunction (map moveNegIn xs) n
    _ -> frm
  
  distributeAndOverOr :: FORMULA -> FORMULA
  distributeAndOverOr f = case f of
    Conjunction xs n -> mkConj (map distributeAndOverOr xs) n
    Disjunction xs n -> if all isPrimForm xs then mkDisj xs n else
      distributeAndOverOr
      $ mkConj (map (`mkDisj` n) . combine $ map getConj xs) n
    _ -> f
  
  cnf :: FORMULA -> FORMULA
  cnf = flipLiterals . distributeAndOverOr . moveNegIn . elimImpl . elimEquiv
  
  flipLiterals :: FORMULA -> FORMULA
  flipLiterals f = case f of
    Negation p@(Predication _) _ -> p
    Predication t -> Negation f $ tokPos t
    Conjunction xs n -> Conjunction (map flipLiterals xs) n
    Disjunction xs n -> Disjunction (map flipLiterals xs) n
    _ -> f
  
  distributeOrOverAnd :: FORMULA -> FORMULA
  distributeOrOverAnd f = case f of
    Disjunction xs n -> mkDisj (map distributeOrOverAnd xs) n
    Conjunction xs n -> if all isPrimForm xs then mkConj xs n else
      distributeOrOverAnd
      $ mkDisj (map (`mkConj` n) . combine $ map getDisj xs) n
    _ -> f
  
  dnf :: FORMULA -> FORMULA
  dnf = distributeOrOverAnd . moveNegIn . elimImpl . elimEquiv
  
  combine :: [[a]] -> [[a]]
  combine l = case l of
    [] -> [[]]
    h : t -> concatMap (flip map h . flip (:)) (combine t)
  