{- |
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)
