Consistency.hs revision d0642e0d269791a923f2bf86ea249f971f14addb
75da45714b471969a6eb41b469237d51d1ed92beMark CraigModule : $Header$
75da45714b471969a6eb41b469237d51d1ed92beMark CraigDescription : data types for consistency aka conservativity
75da45714b471969a6eb41b469237d51d1ed92beMark CraigCopyright : (c) Christian Maeder, DFKI GmbH 2008
75da45714b471969a6eb41b469237d51d1ed92beMark CraigLicense : GPLv2 or higher, see LICENSE.txt
75da45714b471969a6eb41b469237d51d1ed92beMark CraigMaintainer : Christian.Maeder@dfki.de
75da45714b471969a6eb41b469237d51d1ed92beMark CraigStability : provisional
75da45714b471969a6eb41b469237d51d1ed92beMark CraigPortability : portable
75da45714b471969a6eb41b469237d51d1ed92beMark CraigData types for conservativity
75da45714b471969a6eb41b469237d51d1ed92beMark Craig{- | Conservativity annotations. For compactness, only the greatest applicable
75da45714b471969a6eb41b469237d51d1ed92beMark Craig value is used in a DG. PCons stands for prooftheoretic conservativity as
75da45714b471969a6eb41b469237d51d1ed92beMark Craig required for extending imports (no confusion) in Maude -}
1c39f25b4e11ae0397f825f3d031bd01983b98f0Bruno Lavitdata Conservativity =
75da45714b471969a6eb41b469237d51d1ed92beMark Craig Inconsistent
75da45714b471969a6eb41b469237d51d1ed92beMark Craig | Unknown String
75da45714b471969a6eb41b469237d51d1ed92beMark Craig deriving (Show, Read, Eq, Ord)
75da45714b471969a6eb41b469237d51d1ed92beMark CraigshowConsistencyStatus :: Conservativity -> String
75da45714b471969a6eb41b469237d51d1ed92beMark CraigshowConsistencyStatus cs = case cs of
75da45714b471969a6eb41b469237d51d1ed92beMark Craig Inconsistent -> "not conservative"
75da45714b471969a6eb41b469237d51d1ed92beMark Craig Unknown str -> "unknown if being conservative. Cause is : " ++ str
75da45714b471969a6eb41b469237d51d1ed92beMark Craig None -> "unknown if being conservative"
75da45714b471969a6eb41b469237d51d1ed92beMark Craig Cons -> "conservative"
75da45714b471969a6eb41b469237d51d1ed92beMark Craig PCons -> "proof-theoretically conservative"
75da45714b471969a6eb41b469237d51d1ed92beMark Craig Mono -> "monomorphic"
75da45714b471969a6eb41b469237d51d1ed92beMark Craig Def -> "definitional"
75da45714b471969a6eb41b469237d51d1ed92beMark Craiginstance Pretty Conservativity where
75da45714b471969a6eb41b469237d51d1ed92beMark Craig pretty = text . showConsistencyStatus
75da45714b471969a6eb41b469237d51d1ed92beMark Craig{- | All target sentences must be implied by the source translated
75da45714b471969a6eb41b469237d51d1ed92beMark Craigalong the morphism. They are axioms only and not identical to any
75da45714b471969a6eb41b469237d51d1ed92beMark Craigtranslated sentence of the source. -}
75da45714b471969a6eb41b469237d51d1ed92beMark Craigdata ConservativityChecker sign sentence morphism = ConservativityChecker
75da45714b471969a6eb41b469237d51d1ed92beMark Craig { checkerId :: String
75da45714b471969a6eb41b469237d51d1ed92beMark Craig , checkConservativity
75da45714b471969a6eb41b469237d51d1ed92beMark Craig :: (sign, [Named sentence])
75da45714b471969a6eb41b469237d51d1ed92beMark Craig -> [Named sentence]
75da45714b471969a6eb41b469237d51d1ed92beMark Craig -> IO (Result (Conservativity, [sentence])) }