Mon.hs revision d1767fe15b7c3960e36996cc02977c0480ab4b17
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann{- | Module : $Header$
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Description : Implementation of logic instance Mon
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Copyright : (c) Daniel Hausmann & Georgel Calin & Lutz Schroeder, DFKI Lab Bremen,
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Rob Myers & Dirk Pattinson, Department of Computing, ICL
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - License : Similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Maintainer : hausmann@dfki.de
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Stability : provisional
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Portability : portable
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Provides the implementation of the matching functions monotonic modal logic.
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--------------------------------------------------------------------------------
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- instance of feature for Monotonic logic
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--------------------------------------------------------------------------------
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmanndata Mon a = Mon [Formula a] deriving (Eq,Show)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- For any combination of a positive and a negative literal, there is a premise
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- containing only one sequent. This sequent contains only one formula over the
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- stripped positive literal and the negated stripped negative literal.
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- e.g. seq = [ (M Mon p), !(M Mon q), (M Mon !p), !(M Mon !r)]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- match seq = [ [[ p, !q]], [[p, r]], [[ !p, !q]], [[ !p, r]] ]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmanninstance (SigFeature b c d, Eq (b (c d)), Eq (c d)) => NonEmptyFeature Mon b c d where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefMatch flags seq = let stripnlits = [ Neg (head phi) | (Neg (Mod (Mon phi))) <- seq]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann striplits = [ (head phi) | (Mod (Mon phi)) <- seq]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann in if (flags!!1)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann [ [[(Sequent [(Neg (And (Neg neg) (Neg pos)))])]] | neg <- stripnlits, pos <- striplits]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann [ [[(Sequent [(Neg (And (Neg neg) (Neg pos)))])]] | neg <- stripnlits, pos <- striplits]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefPretty d = genfPretty d "[Mon]"
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefFeatureFromSignature sig = Mon
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefFeatureFromFormula phi = Mon
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefStripFeature (Mon phis) = phis
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--------------------------------------------------------------------------------
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- instance of sigFeature for Monotonic logic
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--------------------------------------------------------------------------------
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmanninstance (SigFeature b c d, Eq (c d), Eq (b (c d))) => NonEmptySigFeature Mon b c d where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann neGoOn sig flag = genericPGoOn sig flag