content: {- |
  Module      :  ./CASL/Simplify.hs
  Description :  resolve empty conjunctions and other trivial cases
  Copyright   :  (c) Christian Maeder, Uni Bremen 2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  Resolve empty conjunctions and other trivial cases
  -}
  
  module CASL.Simplify where
  
  import CASL.AS_Basic_CASL
  import CASL.Fold
  
  import Common.Id
  import Common.Utils (nubOrd)
  
  negateFormula :: FORMULA f -> Maybe (FORMULA f)
  negateFormula f = case f of
    Sort_gen_ax {} -> Nothing
    _ -> Just $ negateForm f nullRange
  
  mkJunction :: Ord f => Junctor -> [FORMULA f] -> Range -> FORMULA f
  mkJunction j fs ps = let
      (isTop, top, join) = case j of
          Con -> (is_False_atom, False, conjunctRange)
          Dis -> (is_True_atom, True, disjunctRange)
      in case nubOrd $ concatMap (\ f -> case f of
             Junction j2 ffs _ | j == j2 -> ffs
             Negation (Junction j2 ffs _) p | j /= j2 ->
               map (`negateForm` p) ffs
             Atom b _ | b /= top -> []
             _ -> [f]) fs of
           flat -> if any (\ f -> isTop f || elem (mkNeg f) flat) flat
             then Atom top ps else join flat ps
  
  mkRelation :: Ord f => FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
  mkRelation f1 c f2 ps =
      let nf1 = negateForm f1 ps
          tf = Atom True ps
          equiv = c == Equivalence
      in case f1 of
        Atom b _
          | b -> f2
          | equiv -> negateForm f2 ps
          | otherwise -> tf
        _ -> case f2 of
             Atom b _
               | not b -> nf1
               | equiv -> f1
               | otherwise -> tf
             _ | f1 == f2 -> tf
               | nf1 == f2 -> if equiv then Atom False ps else f1
             _ -> Relation f1 c f2 ps
  
  mkEquation :: Ord f => TERM f -> Equality -> TERM f -> Range -> FORMULA f
  mkEquation t1 e t2 ps =
    if e == Strong && t1 == t2 then Atom True ps else Equation t1 e t2 ps
  
  simplifyRecord :: Ord f => (f -> f) -> Record f (FORMULA f) (TERM f)
  simplifyRecord mf = (mapRecord mf)
      { foldConditional = \ _ t1 f t2 ps -> case f of
        Atom b _ -> if b then t1 else t2
        _ -> Conditional t1 f t2 ps
      , foldQuantification = \ _ q vs qf ps ->
        let nf = Quantification q vs qf ps in
        case q of
        Unique_existential -> nf
        _ -> if null vs then qf else case (qf, q) of
             (Atom True _, Universal) -> qf
             (Atom False _, Existential) -> qf
             _ -> nf
      , foldJunction = const mkJunction
      , foldRelation = const mkRelation
      , foldNegation = const negateForm
      , foldEquation = const mkEquation
      }
  
  simplifyTerm :: Ord f => (f -> f) -> TERM f -> TERM f
  simplifyTerm = foldTerm . simplifyRecord
  
  simplifyFormula :: Ord f => (f -> f) -> FORMULA f -> FORMULA f
  simplifyFormula = foldFormula . simplifyRecord
  