Copyright	(c) Christian Maeder DFKI GmbH 2008
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

Common.Consistency

Description

Data types for conservativity

Synopsis

Documentation

data Conservativity Source #

Conservativity annotations. For compactness, only the greatest applicable value is used in a DG. PCons stands for prooftheoretic conservativity as required for extending imports (no confusion) in Maude

Constructors

Inconsistent
Unknown String
None
PCons
Cons
Mono
Def

Instances

Eq Conservativity Source #
Methods (==) :: Conservativity -> Conservativity -> Bool (/=) :: Conservativity -> Conservativity -> Bool
Data Conservativity Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Conservativity -> c Conservativity gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Conservativity toConstr :: Conservativity -> Constr dataTypeOf :: Conservativity -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Conservativity) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conservativity) gmapT :: (forall b. Data b => b -> b) -> Conservativity -> Conservativity gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conservativity -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conservativity -> r gmapQ :: (forall d. Data d => d -> u) -> Conservativity -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Conservativity -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity
Ord Conservativity Source #
Methods compare :: Conservativity -> Conservativity -> Ordering (<) :: Conservativity -> Conservativity -> Bool (<=) :: Conservativity -> Conservativity -> Bool (>) :: Conservativity -> Conservativity -> Bool (>=) :: Conservativity -> Conservativity -> Bool max :: Conservativity -> Conservativity -> Conservativity min :: Conservativity -> Conservativity -> Conservativity
Read Conservativity Source #
Methods readsPrec :: Int -> ReadS Conservativity readList :: ReadS [Conservativity] readPrec :: ReadPrec Conservativity readListPrec :: ReadPrec [Conservativity]
Show Conservativity Source #
Methods showsPrec :: Int -> Conservativity -> ShowS show :: Conservativity -> String showList :: [Conservativity] -> ShowS
Pretty Conservativity Source #
Methods pretty :: Conservativity -> Doc Source # pretties :: [Conservativity] -> Doc Source #

showConsistencyStatus :: Conservativity -> String Source #

data ConservativityChecker sign sentence morphism Source #

All target sentences must be implied by the source translated along the morphism. They are axioms only and not identical to any translated sentence of the source.

Constructors

ConservativityChecker
Fields checkerId :: String checkerUsable :: IO (Maybe String) checkConservativity :: (sign, [Named sentence]) -> morphism -> [Named sentence] -> IO (Result (Conservativity, [sentence]))