module Data.Logic.Normal.Implicative
( LiteralMapT
, NormalT
, runNormal
, runNormalT
, ImplicativeForm(INF, neg, pos)
, makeINF'
, implicativeNormalForm
, prettyINF
, prettyProof
) where
import Control.Monad.Identity (Identity(runIdentity))
import Control.Monad.State (StateT(runStateT), MonadPlus, msum)
import Data.Generics (Data, Typeable, listify)
import Data.List (intersperse)
import Data.Logic.Classes.Atom (Atom)
import Data.Logic.Classes.Constants (true, ifElse)
import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))
import Data.Logic.Classes.Propositional (PropositionalFormula)
import Data.Logic.Classes.Skolem (Skolem(isSkolem))
import Data.Logic.Classes.Literal (Literal(..))
import Data.Logic.Classes.Negate (Negatable(..))
import Data.Logic.Classes.Term (Term)
import Data.Logic.Harrison.Skolem (SkolemT, runSkolemT)
import Data.Logic.Normal.Clause (clauseNormalForm)
import qualified Data.Set.Extra as Set
import qualified Data.Map as Map
import Text.PrettyPrint (Doc, cat, text, hsep)
type NormalT formula v term m a = SkolemT v term (LiteralMapT formula m) a
runNormalT :: Monad m => NormalT formula v term m a -> m a
runNormalT action = runLiteralMapM (runSkolemT action)
runNormal :: NormalT formula v term Identity a -> a
runNormal = runIdentity . runNormalT
type LiteralMapT f = StateT (Int, Map.Map f Int)
runLiteralMapM :: Monad m => LiteralMapT f m a -> m a
runLiteralMapM action = (runStateT action) (1, Map.empty) >>= return . fst
data ImplicativeForm lit =
INF {neg :: Set.Set lit, pos :: Set.Set lit}
deriving (Eq, Ord, Data, Typeable, Show)
makeINF' :: (Negatable lit, Ord lit) => [lit] -> [lit] -> ImplicativeForm lit
makeINF' n p = INF (Set.fromList n) (Set.fromList p)
prettyINF :: (Negatable lit, Ord lit) => (lit -> Doc) -> ImplicativeForm lit -> Doc
prettyINF lit x = cat $ [text "(", hsep (map lit (Set.toList (neg x))),
text ") => (", hsep (map lit (Set.toList (pos x))), text ")"]
prettyProof :: (Negatable lit, Ord lit) => (lit -> Doc) -> Set.Set (ImplicativeForm lit) -> Doc
prettyProof lit p = cat $ [text "["] ++ intersperse (text ", ") (map (prettyINF lit) (Set.toList p)) ++ [text "]"]
implicativeNormalForm :: forall m formula atom term v f lit.
(Monad m,
FirstOrderFormula formula atom v,
PropositionalFormula formula atom,
Atom atom term v,
Literal lit atom,
Term term v f,
Data formula, Ord formula, Ord lit, Data lit, Skolem f v) =>
formula -> SkolemT v term m (Set.Set (ImplicativeForm lit))
implicativeNormalForm formula =
do cnf <- clauseNormalForm formula
let pairs = Set.map (Set.fold collect (Set.empty, Set.empty)) cnf :: Set.Set (Set.Set lit, Set.Set lit)
pairs' = Set.flatten (Set.map split pairs) :: Set.Set (Set.Set lit, Set.Set lit)
return (Set.map (\ (n,p) -> INF n p) pairs')
where
collect :: lit -> (Set.Set lit, Set.Set lit) -> (Set.Set lit, Set.Set lit)
collect f (n, p) =
foldLiteral (\ f' -> (Set.insert f' n, p))
(ifElse (n, Set.insert true p) (Set.insert true n, p))
(\ _ -> (n, Set.insert f p))
f
split :: (Set.Set lit, Set.Set lit) -> Set.Set (Set.Set lit, Set.Set lit)
split (lhs, rhs) =
if any isSkolem (gFind rhs :: [f])
then Set.map (\ x -> (lhs, Set.singleton x)) rhs
else Set.singleton (lhs, rhs)
gFind :: (MonadPlus m, Data a, Typeable b) => a -> m b
gFind = msum . map return . listify (const True)