Hets - the Heterogeneous Tool Set

Copyright(c) Dominik Luecke 2008
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

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

Eq CASL_DL_SL Source # 

Methods

(==) :: CASL_DL_SL -> CASL_DL_SL -> Bool

(/=) :: CASL_DL_SL -> CASL_DL_SL -> Bool

Data CASL_DL_SL Source # 

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 :: (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 # 
Show CASL_DL_SL Source # 

Methods

showsPrec :: Int -> CASL_DL_SL -> ShowS

show :: CASL_DL_SL -> String

showList :: [CASL_DL_SL] -> ShowS

Logic CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree Source # 

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 #

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 #