Consistency.hs revision 1e39a4ee4e97d16c48003d49e4af3d181f25ad71
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederModule : $Header$
54ea981a0503c396c2923a1c06421c6235baf27fChristian MaederDescription : data types for consistency aka conservativity
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederMaintainer : Christian.Maeder@dfki.de
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederStability : provisional
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaederPortability : portable
54ea981a0503c396c2923a1c06421c6235baf27fChristian MaederData types for conservativity
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maederimport Data.Char (toLower)
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder{- | Conservativity annotations. For compactness, only the greatest applicable
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder value is used in a DG. PCons stands for prooftheoretic conservativity as
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder required for extending imports (no confusion) in Maude -}
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederdata Conservativity =
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder | Unknown String
a8713a56658d7d305753d673f3d30c8f78181dd9Christian Maeder deriving (Show, Read, Eq, Ord)
a3963596b8a24e870708767e064a9e24cfa7e5edChristian MaedershowConsistency :: Conservativity -> String
a3963596b8a24e870708767e064a9e24cfa7e5edChristian MaedershowConsistency c = case c of
a3963596b8a24e870708767e064a9e24cfa7e5edChristian Maeder Cons -> "Consistent"
a3963596b8a24e870708767e064a9e24cfa7e5edChristian Maeder Unknown str -> "unkown if being consistent. Cause is : " ++ str
54ea981a0503c396c2923a1c06421c6235baf27fChristian MaedershowConsistencyStatus :: Conservativity -> String
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaedershowConsistencyStatus cs = case cs of
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder Inconsistent -> "not conservative"
a3963596b8a24e870708767e064a9e24cfa7e5edChristian Maeder Unknown str -> "unkown if being conservative. Cause is : " ++ str
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder _ -> map toLower $ show cs
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederinstance Pretty Conservativity where
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder pretty = text . showConsistencyStatus
1e39a4ee4e97d16c48003d49e4af3d181f25ad71Christian Maeder{- | All target sentences must be implied by the source translated
1e39a4ee4e97d16c48003d49e4af3d181f25ad71Christian Maederalong the morphism. They are axioms only and not identical to any
1e39a4ee4e97d16c48003d49e4af3d181f25ad71Christian Maedertranslated sentence of the source. -}
f456529a89bfb620d39e5fd5b0a53b24643db96dDominik Lueckedata ConservativityChecker sign sentence morphism = ConservativityChecker
7ab2df3001654dd1b7a2cfc3da1ccef11c39a503Christian Maeder { checkerId :: String
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder , checkConservativity
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder :: (sign, [Named sentence])
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder -> [Named sentence]
7ab2df3001654dd1b7a2cfc3da1ccef11c39a503Christian Maeder -> IO (Result (Maybe (Conservativity, [sentence]))) }