{- |
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 :: FORMULA f -> Maybe (FORMULA f)
negateFormula f :: FORMULA f
f = case FORMULA f
f of
  Sort_gen_ax {} -> Maybe (FORMULA f)
forall a. Maybe a
Nothing
  _ -> FORMULA f -> Maybe (FORMULA f)
forall a. a -> Maybe a
Just (FORMULA f -> Maybe (FORMULA f)) -> FORMULA f -> Maybe (FORMULA f)
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
negateForm FORMULA f
f Range
nullRange

mkJunction :: Ord f => Junctor -> [FORMULA f] -> Range -> FORMULA f
mkJunction :: Junctor -> [FORMULA f] -> Range -> FORMULA f
mkJunction j :: Junctor
j fs :: [FORMULA f]
fs ps :: Range
ps = let
    (isTop :: FORMULA f -> Bool
isTop, top :: Bool
top, join :: [FORMULA f] -> Range -> FORMULA f
join) = case Junctor
j of
        Con -> (FORMULA f -> Bool
forall f. FORMULA f -> Bool
is_False_atom, Bool
False, [FORMULA f] -> Range -> FORMULA f
forall f. [FORMULA f] -> Range -> FORMULA f
conjunctRange)
        Dis -> (FORMULA f -> Bool
forall f. FORMULA f -> Bool
is_True_atom, Bool
True, [FORMULA f] -> Range -> FORMULA f
forall f. [FORMULA f] -> Range -> FORMULA f
disjunctRange)
    in case [FORMULA f] -> [FORMULA f]
forall a. Ord a => [a] -> [a]
nubOrd ([FORMULA f] -> [FORMULA f]) -> [FORMULA f] -> [FORMULA f]
forall a b. (a -> b) -> a -> b
$ (FORMULA f -> [FORMULA f]) -> [FORMULA f] -> [FORMULA f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ f :: FORMULA f
f -> case FORMULA f
f of
           Junction j2 :: Junctor
j2 ffs :: [FORMULA f]
ffs _ | Junctor
j Junctor -> Junctor -> Bool
forall a. Eq a => a -> a -> Bool
== Junctor
j2 -> [FORMULA f]
ffs
           Negation (Junction j2 :: Junctor
j2 ffs :: [FORMULA f]
ffs _) p :: Range
p | Junctor
j Junctor -> Junctor -> Bool
forall a. Eq a => a -> a -> Bool
/= Junctor
j2 ->
             (FORMULA f -> FORMULA f) -> [FORMULA f] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
`negateForm` Range
p) [FORMULA f]
ffs
           Atom b :: Bool
b _ | Bool
b Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
top -> []
           _ -> [FORMULA f
f]) [FORMULA f]
fs of
         flat :: [FORMULA f]
flat -> if (FORMULA f -> Bool) -> [FORMULA f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ f :: FORMULA f
f -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
isTop FORMULA f
f Bool -> Bool -> Bool
|| FORMULA f -> [FORMULA f] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
mkNeg FORMULA f
f) [FORMULA f]
flat) [FORMULA f]
flat
           then Bool -> Range -> FORMULA f
forall f. Bool -> Range -> FORMULA f
Atom Bool
top Range
ps else [FORMULA f] -> Range -> FORMULA f
forall f. [FORMULA f] -> Range -> FORMULA f
join [FORMULA f]
flat Range
ps

mkRelation :: Ord f => FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
mkRelation :: FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
mkRelation f1 :: FORMULA f
f1 c :: Relation
c f2 :: FORMULA f
f2 ps :: Range
ps =
    let nf1 :: FORMULA f
nf1 = FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
negateForm FORMULA f
f1 Range
ps
        tf :: FORMULA f
tf = Bool -> Range -> FORMULA f
forall f. Bool -> Range -> FORMULA f
Atom Bool
True Range
ps
        equiv :: Bool
equiv = Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
Equivalence
    in case FORMULA f
f1 of
      Atom b :: Bool
b _
        | Bool
b -> FORMULA f
f2
        | Bool
equiv -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
negateForm FORMULA f
f2 Range
ps
        | Bool
otherwise -> FORMULA f
forall f. FORMULA f
tf
      _ -> case FORMULA f
f2 of
           Atom b :: Bool
b _
             | Bool -> Bool
not Bool
b -> FORMULA f
nf1
             | Bool
equiv -> FORMULA f
f1
             | Bool
otherwise -> FORMULA f
forall f. FORMULA f
tf
           _ | FORMULA f
f1 FORMULA f -> FORMULA f -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA f
f2 -> FORMULA f
forall f. FORMULA f
tf
             | FORMULA f
nf1 FORMULA f -> FORMULA f -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA f
f2 -> if Bool
equiv then Bool -> Range -> FORMULA f
forall f. Bool -> Range -> FORMULA f
Atom Bool
False Range
ps else FORMULA f
f1
           _ -> FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation FORMULA f
f1 Relation
c FORMULA f
f2 Range
ps

mkEquation :: Ord f => TERM f -> Equality -> TERM f -> Range -> FORMULA f
mkEquation :: TERM f -> Equality -> TERM f -> Range -> FORMULA f
mkEquation t1 :: TERM f
t1 e :: Equality
e t2 :: TERM f
t2 ps :: Range
ps =
  if Equality
e Equality -> Equality -> Bool
forall a. Eq a => a -> a -> Bool
== Equality
Strong Bool -> Bool -> Bool
&& TERM f
t1 TERM f -> TERM f -> Bool
forall a. Eq a => a -> a -> Bool
== TERM f
t2 then Bool -> Range -> FORMULA f
forall f. Bool -> Range -> FORMULA f
Atom Bool
True Range
ps else TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
t1 Equality
e TERM f
t2 Range
ps

simplifyRecord :: Ord f => (f -> f) -> Record f (FORMULA f) (TERM f)
simplifyRecord :: (f -> f) -> Record f (FORMULA f) (TERM f)
simplifyRecord mf :: f -> f
mf = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
mf)
    { foldConditional :: TERM f -> TERM f -> FORMULA f -> TERM f -> Range -> TERM f
foldConditional = \ _ t1 :: TERM f
t1 f :: FORMULA f
f t2 :: TERM f
t2 ps :: Range
ps -> case FORMULA f
f of
      Atom b :: Bool
b _ -> if Bool
b then TERM f
t1 else TERM f
t2
      _ -> TERM f -> FORMULA f -> TERM f -> Range -> TERM f
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional TERM f
t1 FORMULA f
f TERM f
t2 Range
ps
    , foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
foldQuantification = \ _ q :: QUANTIFIER
q vs :: [VAR_DECL]
vs qf :: FORMULA f
qf ps :: Range
ps ->
      let nf :: FORMULA f
nf = QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vs FORMULA f
qf Range
ps in
      case QUANTIFIER
q of
      Unique_existential -> FORMULA f
nf
      _ -> if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
vs then FORMULA f
qf else case (FORMULA f
qf, QUANTIFIER
q) of
           (Atom True _, Universal) -> FORMULA f
qf
           (Atom False _, Existential) -> FORMULA f
qf
           _ -> FORMULA f
nf
    , foldJunction :: FORMULA f -> Junctor -> [FORMULA f] -> Range -> FORMULA f
foldJunction = (Junctor -> [FORMULA f] -> Range -> FORMULA f)
-> FORMULA f -> Junctor -> [FORMULA f] -> Range -> FORMULA f
forall a b. a -> b -> a
const Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Ord f => Junctor -> [FORMULA f] -> Range -> FORMULA f
mkJunction
    , foldRelation :: FORMULA f
-> FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
foldRelation = (FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f)
-> FORMULA f
-> FORMULA f
-> Relation
-> FORMULA f
-> Range
-> FORMULA f
forall a b. a -> b -> a
const FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f.
Ord f =>
FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
mkRelation
    , foldNegation :: FORMULA f -> FORMULA f -> Range -> FORMULA f
foldNegation = (FORMULA f -> Range -> FORMULA f)
-> FORMULA f -> FORMULA f -> Range -> FORMULA f
forall a b. a -> b -> a
const FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
negateForm
    , foldEquation :: FORMULA f -> TERM f -> Equality -> TERM f -> Range -> FORMULA f
foldEquation = (TERM f -> Equality -> TERM f -> Range -> FORMULA f)
-> FORMULA f -> TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall a b. a -> b -> a
const TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f.
Ord f =>
TERM f -> Equality -> TERM f -> Range -> FORMULA f
mkEquation
    }

simplifyTerm :: Ord f => (f -> f) -> TERM f -> TERM f
simplifyTerm :: (f -> f) -> TERM f -> TERM f
simplifyTerm = Record f (FORMULA f) (TERM f) -> TERM f -> TERM f
forall f a b. Record f a b -> TERM f -> b
foldTerm (Record f (FORMULA f) (TERM f) -> TERM f -> TERM f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> TERM f
-> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> Record f (FORMULA f) (TERM f)
forall f. Ord f => (f -> f) -> Record f (FORMULA f) (TERM f)
simplifyRecord

simplifyFormula :: Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula :: (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> Record f (FORMULA f) (TERM f)
forall f. Ord f => (f -> f) -> Record f (FORMULA f) (TERM f)
simplifyRecord