{-# 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])) }