Copyright	(c) Dominik Luecke 2008
License	GPLv2 or higher, see LICENSE.txt
Maintainer	luecke@informatik.uni-bremen.de
Stability	experimental
Portability	portable
Safe Haskell	Safe

CASL_DL.Sublogics

Description

Sublogic analysis for CASL_DL

This module provides the sublogic functions (as required by Logic.hs) for CASL_DL. The functions allow to compute the minimal sublogics needed by a given element, to check whether an item is part of a given sublogic, and to project an element into a given sublogic.

Documentation

data CASL_DL_SL Source #

Constructors

SROIQ

Instances

Instances details

Eq CASL_DL_SL Source #
Instance details Defined in CASL_DL.Sublogics Methods (==) :: CASL_DL_SL -> CASL_DL_SL -> Bool (/=) :: CASL_DL_SL -> CASL_DL_SL -> Bool
Data CASL_DL_SL Source #
Instance details Defined in CASL_DL.Sublogics Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CASL_DL_SL -> c CASL_DL_SL gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CASL_DL_SL toConstr :: CASL_DL_SL -> Constr dataTypeOf :: CASL_DL_SL -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CASL_DL_SL) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CASL_DL_SL) gmapT :: (forall b. Data b => b -> b) -> CASL_DL_SL -> CASL_DL_SL gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CASL_DL_SL -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CASL_DL_SL -> r gmapQ :: (forall d. Data d => d -> u) -> CASL_DL_SL -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CASL_DL_SL -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CASL_DL_SL -> m CASL_DL_SL gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CASL_DL_SL -> m CASL_DL_SL gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CASL_DL_SL -> m CASL_DL_SL
Ord CASL_DL_SL Source #
Instance details Defined in CASL_DL.Sublogics Methods compare :: CASL_DL_SL -> CASL_DL_SL -> Ordering (<) :: CASL_DL_SL -> CASL_DL_SL -> Bool (<=) :: CASL_DL_SL -> CASL_DL_SL -> Bool (>) :: CASL_DL_SL -> CASL_DL_SL -> Bool (>=) :: CASL_DL_SL -> CASL_DL_SL -> Bool max :: CASL_DL_SL -> CASL_DL_SL -> CASL_DL_SL min :: CASL_DL_SL -> CASL_DL_SL -> CASL_DL_SL
Show CASL_DL_SL Source #
Instance details Defined in CASL_DL.Sublogics Methods showsPrec :: Int -> CASL_DL_SL -> ShowS show :: CASL_DL_SL -> String showList :: [CASL_DL_SL] -> ShowS
Generic CASL_DL_SL
Instance details Defined in CASL_DL.ATC_CASL_DL Associated Types type Rep CASL_DL_SL :: Type -> Type Methods from :: CASL_DL_SL -> Rep CASL_DL_SL x to :: Rep CASL_DL_SL x -> CASL_DL_SL
FromJSON CASL_DL_SL
Instance details Defined in CASL_DL.ATC_CASL_DL Methods parseJSON :: Value -> Parser CASL_DL_SL parseJSONList :: Value -> Parser [CASL_DL_SL]
ToJSON CASL_DL_SL
Instance details Defined in CASL_DL.ATC_CASL_DL Methods toJSON :: CASL_DL_SL -> Value toEncoding :: CASL_DL_SL -> Encoding toJSONList :: [CASL_DL_SL] -> Value toEncodingList :: [CASL_DL_SL] -> Encoding
ShATermConvertible CASL_DL_SL
Instance details Defined in CASL_DL.ATC_CASL_DL Methods toShATermAux :: ATermTable -> CASL_DL_SL -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [CASL_DL_SL] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, CASL_DL_SL) fromShATermList' :: Int -> ATermTable -> (ATermTable, [CASL_DL_SL])
SublogicName CASL_DL_SL Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods sublogicName :: CASL_DL_SL -> String Source #
SemiLatticeWithTop CASL_DL_SL Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods lub :: CASL_DL_SL -> CASL_DL_SL -> CASL_DL_SL Source # top :: CASL_DL_SL Source #
ProjectSublogicM CASL_DL_SL SYMB_MAP_ITEMS Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods projectSublogicM :: CASL_DL_SL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS Source #
ProjectSublogicM CASL_DL_SL SYMB_ITEMS Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods projectSublogicM :: CASL_DL_SL -> SYMB_ITEMS -> Maybe SYMB_ITEMS Source #
ProjectSublogicM CASL_DL_SL Symbol Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods projectSublogicM :: CASL_DL_SL -> Symbol -> Maybe Symbol Source #
ProjectSublogic CASL_DL_SL DL_BASIC_SPEC Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods projectSublogic :: CASL_DL_SL -> DL_BASIC_SPEC -> DL_BASIC_SPEC Source #
ProjectSublogic CASL_DL_SL Symbol Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods projectSublogic :: CASL_DL_SL -> Symbol -> Symbol Source #
ProjectSublogic CASL_DL_SL DLSign Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods projectSublogic :: CASL_DL_SL -> DLSign -> DLSign Source #
ProjectSublogic CASL_DL_SL DLMor Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods projectSublogic :: CASL_DL_SL -> DLMor -> DLMor Source #
MinSublogic CASL_DL_SL SYMB_MAP_ITEMS Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods minSublogic :: SYMB_MAP_ITEMS -> CASL_DL_SL Source #
MinSublogic CASL_DL_SL SYMB_ITEMS Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods minSublogic :: SYMB_ITEMS -> CASL_DL_SL Source #
MinSublogic CASL_DL_SL DL_BASIC_SPEC Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods minSublogic :: DL_BASIC_SPEC -> CASL_DL_SL Source #
MinSublogic CASL_DL_SL Symbol Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods minSublogic :: Symbol -> CASL_DL_SL Source #
MinSublogic CASL_DL_SL DLSign Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods minSublogic :: DLSign -> CASL_DL_SL Source #
MinSublogic CASL_DL_SL DLFORMULA Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods minSublogic :: DLFORMULA -> CASL_DL_SL Source #
MinSublogic CASL_DL_SL DLMor Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods minSublogic :: DLMor -> CASL_DL_SL Source #
Logic CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods parse_basic_sen :: CASL_DL -> Maybe (DL_BASIC_SPEC -> AParser st DLFORMULA) Source # stability :: CASL_DL -> Stability Source # data_logic :: CASL_DL -> Maybe AnyLogic Source # top_sublogic :: CASL_DL -> CASL_DL_SL Source # all_sublogics :: CASL_DL -> [CASL_DL_SL] Source # bottomSublogic :: CASL_DL -> Maybe CASL_DL_SL Source # sublogicDimensions :: CASL_DL -> [[CASL_DL_SL]] Source # parseSublogic :: CASL_DL -> String -> Maybe CASL_DL_SL Source # proj_sublogic_epsilon :: CASL_DL -> CASL_DL_SL -> DLSign -> DLMor Source # provers :: CASL_DL -> [Prover DLSign DLFORMULA DLMor CASL_DL_SL ProofTree] Source # default_prover :: CASL_DL -> String Source # cons_checkers :: CASL_DL -> [ConsChecker DLSign DLFORMULA CASL_DL_SL DLMor ProofTree] Source # conservativityCheck :: CASL_DL -> [ConservativityChecker DLSign DLFORMULA DLMor] Source # empty_proof_tree :: CASL_DL -> ProofTree Source # syntaxTable :: CASL_DL -> DLSign -> Maybe SyntaxTable Source # omdoc_metatheory :: CASL_DL -> Maybe OMCD Source # export_symToOmdoc :: CASL_DL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CASL_DL -> NameMap Symbol -> DLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: CASL_DL -> SigMap Symbol -> DLSign -> [Named DLFORMULA] -> Result [TCElement] Source # omdocToSym :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named DLFORMULA)) Source # addOMadtToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [[OmdADT]] -> Result (DLSign, [Named DLFORMULA]) Source # addOmdocToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [TCElement] -> Result (DLSign, [Named DLFORMULA]) Source # sublogicOfTheo :: CASL_DL -> (DLSign, [DLFORMULA]) -> CASL_DL_SL Source #
Comorphism CASL_DL2CASL CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL_DL2CASL Methods sourceLogic :: CASL_DL2CASL -> CASL_DL Source # sourceSublogic :: CASL_DL2CASL -> CASL_DL_SL Source # sourceSublogicLossy :: CASL_DL2CASL -> CASL_DL_SL Source # minSourceTheory :: CASL_DL2CASL -> Maybe (LibName, String) Source # targetLogic :: CASL_DL2CASL -> CASL Source # mapSublogic :: CASL_DL2CASL -> CASL_DL_SL -> Maybe CASL_Sublogics Source # map_theory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL_DL2CASL -> DLMor -> Result CASLMor Source # map_sentence :: CASL_DL2CASL -> DLSign -> DLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL_DL2CASL -> DLSign -> Symbol -> Set Symbol Source # extractModel :: CASL_DL2CASL -> DLSign -> ProofTree -> Result (DLSign, [Named DLFORMULA]) Source # is_model_transportable :: CASL_DL2CASL -> Bool Source # has_model_expansion :: CASL_DL2CASL -> Bool Source # is_weakly_amalgamable :: CASL_DL2CASL -> Bool Source # constituents :: CASL_DL2CASL -> [String] Source # isInclusionComorphism :: CASL_DL2CASL -> Bool Source # rps :: CASL_DL2CASL -> Bool Source # eps :: CASL_DL2CASL -> Bool Source # isGTC :: CASL_DL2CASL -> Bool Source #
type Rep CASL_DL_SL
Instance details Defined in CASL_DL.ATC_CASL_DL type Rep CASL_DL_SL = D1 ('MetaData "CASL_DL_SL" "CASL_DL.Sublogics" "main" 'False) (C1 ('MetaCons "SROIQ" 'PrefixI 'False) (U1 :: Type -> Type))