{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./Common/Consistency.hs Description : data types for consistency aka conservativity Copyright : (c) Christian Maeder, DFKI GmbH 2008 License : GPLv2 or higher, see LICENSE.txt Maintainer : Christian.Maeder@dfki.de Stability : provisional Portability : portable Data types for conservativity -} module Common.Consistency where import Common.Doc import Common.DocUtils import Common.AS_Annotation import Common.Result import Data.Data {- | 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 -} data Conservativity = Inconsistent | Unknown String | None | PCons | Cons | Mono | Def deriving (Int -> Conservativity -> ShowS [Conservativity] -> ShowS Conservativity -> String (Int -> Conservativity -> ShowS) -> (Conservativity -> String) -> ([Conservativity] -> ShowS) -> Show Conservativity forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Conservativity] -> ShowS $cshowList :: [Conservativity] -> ShowS show :: Conservativity -> String $cshow :: Conservativity -> String showsPrec :: Int -> Conservativity -> ShowS $cshowsPrec :: Int -> Conservativity -> ShowS Show, ReadPrec [Conservativity] ReadPrec Conservativity Int -> ReadS Conservativity ReadS [Conservativity] (Int -> ReadS Conservativity) -> ReadS [Conservativity] -> ReadPrec Conservativity -> ReadPrec [Conservativity] -> Read Conservativity forall a. (Int -> ReadS a) -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a readListPrec :: ReadPrec [Conservativity] $creadListPrec :: ReadPrec [Conservativity] readPrec :: ReadPrec Conservativity $creadPrec :: ReadPrec Conservativity readList :: ReadS [Conservativity] $creadList :: ReadS [Conservativity] readsPrec :: Int -> ReadS Conservativity $creadsPrec :: Int -> ReadS Conservativity Read, Conservativity -> Conservativity -> Bool (Conservativity -> Conservativity -> Bool) -> (Conservativity -> Conservativity -> Bool) -> Eq Conservativity forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Conservativity -> Conservativity -> Bool $c/= :: Conservativity -> Conservativity -> Bool == :: Conservativity -> Conservativity -> Bool $c== :: Conservativity -> Conservativity -> Bool Eq, Eq Conservativity Eq Conservativity => (Conservativity -> Conservativity -> Ordering) -> (Conservativity -> Conservativity -> Bool) -> (Conservativity -> Conservativity -> Bool) -> (Conservativity -> Conservativity -> Bool) -> (Conservativity -> Conservativity -> Bool) -> (Conservativity -> Conservativity -> Conservativity) -> (Conservativity -> Conservativity -> Conservativity) -> Ord Conservativity Conservativity -> Conservativity -> Bool Conservativity -> Conservativity -> Ordering Conservativity -> Conservativity -> Conservativity forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Conservativity -> Conservativity -> Conservativity $cmin :: Conservativity -> Conservativity -> Conservativity max :: Conservativity -> Conservativity -> Conservativity $cmax :: Conservativity -> Conservativity -> Conservativity >= :: Conservativity -> Conservativity -> Bool $c>= :: Conservativity -> Conservativity -> Bool > :: Conservativity -> Conservativity -> Bool $c> :: Conservativity -> Conservativity -> Bool <= :: Conservativity -> Conservativity -> Bool $c<= :: Conservativity -> Conservativity -> Bool < :: Conservativity -> Conservativity -> Bool $c< :: Conservativity -> Conservativity -> Bool compare :: Conservativity -> Conservativity -> Ordering $ccompare :: Conservativity -> Conservativity -> Ordering $cp1Ord :: Eq Conservativity Ord, Typeable, Typeable Conservativity Constr DataType Typeable Conservativity => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Conservativity -> c Conservativity) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Conservativity) -> (Conservativity -> Constr) -> (Conservativity -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Conservativity)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conservativity)) -> ((forall b. Data b => b -> b) -> Conservativity -> Conservativity) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conservativity -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conservativity -> r) -> (forall u. (forall d. Data d => d -> u) -> Conservativity -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> Conservativity -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity) -> Data Conservativity Conservativity -> Constr Conservativity -> DataType (forall b. Data b => b -> b) -> Conservativity -> Conservativity (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Conservativity -> c Conservativity (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Conservativity forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> Conservativity -> u forall u. (forall d. Data d => d -> u) -> Conservativity -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conservativity -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conservativity -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Conservativity forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Conservativity -> c Conservativity forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Conservativity) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conservativity) $cDef :: Constr $cMono :: Constr $cCons :: Constr $cPCons :: Constr $cNone :: Constr $cUnknown :: Constr $cInconsistent :: Constr $tConservativity :: DataType gmapMo :: (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity gmapMp :: (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity gmapM :: (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Conservativity -> m Conservativity gmapQi :: Int -> (forall d. Data d => d -> u) -> Conservativity -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Conservativity -> u gmapQ :: (forall d. Data d => d -> u) -> Conservativity -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Conservativity -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conservativity -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conservativity -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conservativity -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conservativity -> r gmapT :: (forall b. Data b => b -> b) -> Conservativity -> Conservativity $cgmapT :: (forall b. Data b => b -> b) -> Conservativity -> Conservativity dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conservativity) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conservativity) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Conservativity) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Conservativity) dataTypeOf :: Conservativity -> DataType $cdataTypeOf :: Conservativity -> DataType toConstr :: Conservativity -> Constr $ctoConstr :: Conservativity -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Conservativity $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Conservativity gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Conservativity -> c Conservativity $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Conservativity -> c Conservativity $cp1Data :: Typeable Conservativity Data) showConsistencyStatus :: Conservativity -> String showConsistencyStatus :: Conservativity -> String showConsistencyStatus cs :: Conservativity cs = case Conservativity cs of Inconsistent -> "not conservative" Unknown str :: String str -> "unknown if being conservative. Cause is : " String -> ShowS forall a. [a] -> [a] -> [a] ++ String str None -> "unknown if being conservative" Cons -> "conservative" PCons -> "proof-theoretically conservative" Mono -> "monomorphic" Def -> "definitional" instance Pretty Conservativity where pretty :: Conservativity -> Doc pretty = String -> Doc text (String -> Doc) -> (Conservativity -> String) -> Conservativity -> Doc forall b c a. (b -> c) -> (a -> b) -> a -> c . Conservativity -> String showConsistencyStatus {- | 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. -} data ConservativityChecker sign sentence morphism = ConservativityChecker { ConservativityChecker sign sentence morphism -> String checkerId :: String , ConservativityChecker sign sentence morphism -> IO (Maybe String) checkerUsable :: IO (Maybe String) , ConservativityChecker sign sentence morphism -> (sign, [Named sentence]) -> morphism -> [Named sentence] -> IO (Result (Conservativity, [sentence])) checkConservativity :: (sign, [Named sentence]) -> morphism -> [Named sentence] -> IO (Result (Conservativity, [sentence])) }