1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
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
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
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Read, Eq, Ord, Typeable, Data)
54ea981a0503c396c2923a1c06421c6235baf27fChristian MaedershowConsistencyStatus :: Conservativity -> String
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian MaedershowConsistencyStatus cs = case cs of
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder Inconsistent -> "not conservative"
6f08518fe3561930fef290b8e01384a6f1c90598Till Mossakowski Unknown str -> "unknown if being conservative. Cause is : " ++ str
6f08518fe3561930fef290b8e01384a6f1c90598Till Mossakowski None -> "unknown if being conservative"
6f08518fe3561930fef290b8e01384a6f1c90598Till Mossakowski Cons -> "conservative"
6f08518fe3561930fef290b8e01384a6f1c90598Till Mossakowski PCons -> "proof-theoretically conservative"
6f08518fe3561930fef290b8e01384a6f1c90598Till Mossakowski Mono -> "monomorphic"
6f08518fe3561930fef290b8e01384a6f1c90598Till Mossakowski Def -> "definitional"
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
0a65899b09e78455a94af9128455f6613441ab71cmaeder , checkerUsable :: IO (Maybe String)
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder , checkConservativity
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder :: (sign, [Named sentence])
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder -> [Named sentence]
d0642e0d269791a923f2bf86ea249f971f14addbChristian Maeder -> IO (Result (Conservativity, [sentence])) }