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

data Conservativity
- = Inconsistent
- | Unknown {
  - conservativityUnknownReason :: String
  }
- | None
- | PCons
- | Cons
- | Mono
- | Def
showConsistencyStatus :: Conservativity -> String
data ConservativityChecker sign sentence morphism = ConservativityChecker {
- checkerId :: String
- checkerUsable :: IO (Maybe String)
- checkConservativity :: (sign, [Named sentence]) -> morphism -> [Named sentence] -> IO (Result (Conservativity, [sentence]))
}

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
Fields conservativityUnknownReason :: String
None
PCons
Cons
Mono
Def

Instances

Instances details

Eq Conservativity Source #
Instance details Defined in Common.Consistency Methods (==) :: Conservativity -> Conservativity -> Bool (/=) :: Conservativity -> Conservativity -> Bool
Data Conservativity Source #
Instance details Defined in Common.Consistency 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 :: forall r r'. (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 #
Instance details Defined in Common.Consistency 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 #
Instance details Defined in Common.Consistency Methods readsPrec :: Int -> ReadS Conservativity readList :: ReadS [Conservativity] readPrec :: ReadPrec Conservativity readListPrec :: ReadPrec [Conservativity]
Show Conservativity Source #
Instance details Defined in Common.Consistency Methods showsPrec :: Int -> Conservativity -> ShowS show :: Conservativity -> String showList :: [Conservativity] -> ShowS
Generic Conservativity
Instance details Defined in ATC.Consistency Associated Types type Rep Conservativity :: Type -> Type Methods from :: Conservativity -> Rep Conservativity x to :: Rep Conservativity x -> Conservativity
FromJSON Conservativity
Instance details Defined in ATC.Consistency Methods parseJSON :: Value -> Parser Conservativity parseJSONList :: Value -> Parser [Conservativity]
ToJSON Conservativity
Instance details Defined in ATC.Consistency Methods toJSON :: Conservativity -> Value toEncoding :: Conservativity -> Encoding toJSONList :: [Conservativity] -> Value toEncodingList :: [Conservativity] -> Encoding
ShATermConvertible Conservativity
Instance details Defined in ATC.Consistency Methods toShATermAux :: ATermTable -> Conservativity -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Conservativity] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Conservativity) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Conservativity])
Pretty Conservativity Source #
Instance details Defined in Common.Consistency Methods pretty :: Conservativity -> Doc Source # pretties :: [Conservativity] -> Doc Source #
type Rep Conservativity
Instance details Defined in ATC.Consistency type Rep Conservativity = D1 ('MetaData "Conservativity" "Common.Consistency" "main" 'False) ((C1 ('MetaCons "Inconsistent" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Unknown" 'PrefixI 'True) (S1 ('MetaSel ('Just "conservativityUnknownReason") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "None" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PCons" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cons" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Mono" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Def" 'PrefixI 'False) (U1 :: Type -> Type))))

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