module Domain.Logic.InverseRules
( inverseDeMorganOr, inverseDeMorganAnd
, inverseAndOverOr, inverseOrOverAnd
, inverseIdempOr, inverseIdempAnd
, inverseRules
) where
import Control.Monad
import Domain.Logic.Formula
import Domain.Logic.Utils
import Ideas.Common.Library
inverseDeMorganOr :: Rule SLogic
inverseDeMorganOr = siblingOf groupDeMorgan $
makeListRule "InvDeMorganOr" $ \p -> do
(leftCtx, xs, rightCtx) <- split3 (conjunctions p)
guard (length xs > 1)
ys <- mapM isComplementM xs
return (ands (leftCtx ++ Not (ors ys) : rightCtx))
inverseDeMorganAnd :: Rule SLogic
inverseDeMorganAnd = siblingOf groupDeMorgan $
makeListRule "InvDeMorganAnd" $ \p -> do
(leftCtx, xs, rightCtx) <- split3 (disjunctions p)
guard (length xs > 1)
ys <- mapM isComplementM xs
return (ors (leftCtx ++ Not (ands ys) : rightCtx))
isComplementM :: Monad m => SLogic -> m SLogic
isComplementM = maybe (fail "not a complement") return . isComplement
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)
inverseIdempOr :: Rule SLogic
inverseIdempOr = siblingOf groupIdempotency $
makeListRule "InvIdempOr" $ \p -> do
(leftCtx, xs, rightCtx) <- split3 (disjunctions p)
return (ors (leftCtx ++ xs ++ xs ++ rightCtx))
inverseIdempAnd :: Rule SLogic
inverseIdempAnd = siblingOf groupIdempotency $
makeListRule "InvIdempAnd" $ \p -> do
(leftCtx, xs, rightCtx) <- split3 (conjunctions p)
return (ands (leftCtx ++ xs ++ xs ++ rightCtx))
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
split3 :: [a] -> [([a], [a], [a])]
split3 as =
[ (xs, ys1, ys2)
| (xs, ys) <- split as
, (ys1, ys2) <- split ys
]
split :: [a] -> [([a], [a])]
split xs = map (`splitAt` xs) [0 .. length xs]
inverseRules :: [Rule SLogic]
inverseRules =
[ invDefImpl, invDefEquiv, invDoubleNeg
, invTrueAnd, invNotTrue, invFalseOr, invNotFalse
]
invDefImpl :: Rule SLogic
invDefImpl = siblingOf groupImplication $ rewriteRule "DefImpl.inv" $
\x y -> Not x :||: y :~> x :->: y
invDefEquiv :: Rule SLogic
invDefEquiv = siblingOf groupEquivalence $ rewriteRule "DefEquiv.inv" $
\x y -> (x :&&: y) :||: (Not x :&&: Not y) :~> x :<->: y
invDoubleNeg :: Rule SLogic
invDoubleNeg = siblingOf groupDoubleNegation $ rewriteRule "NotNot.inv" $
\x -> x :~> Not (Not x)
invTrueAnd :: Rule SLogic
invTrueAnd = siblingOf groupTrueConjunction $ rewriteRules "TrueZeroAnd.inv"
[ \x -> x :~> T :&&: x
, \x -> x :~> x :&&: T
]
invNotTrue :: Rule SLogic
invNotTrue = siblingOf groupNotTrue $ rewriteRule "NotTrue.inv" $
F :~> Not T
invFalseOr :: Rule SLogic
invFalseOr = siblingOf groupFalseDisjunction $ rewriteRules "FalseZeroOr.inv"
[ \x -> x :~> F :||: x
, \x -> x :~> x :||: F
]
invNotFalse :: Rule SLogic
invNotFalse = siblingOf groupNotFalse $ rewriteRule "NotFalse.inv" $
T :~> Not F