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-Inferred

Common.Consistency

Description

Data types for conservativity

Synopsis

Documentation

data Conservativity

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
Data Conservativity
Ord Conservativity
Read Conservativity
Show Conservativity
ShATermConvertible Conservativity
Pretty Conservativity
Typeable * Conservativity

showConsistencyStatus :: Conservativity -> String

data ConservativityChecker sign sentence morphism

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]))