Copyright	(c) Klaus Luettich Uni Bremen 2004
License	GPLv2 or higher, see LICENSE.txt
Maintainer	luecke@informatik.uni-bremen.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

CASL_DL.Sign

Description

Signatures for DL logics, as extension of CASL signatures.

Documentation

data CASL_DLSign Source #

Constructors

CASL_DLSign
Fields annoProperties :: Map SIMPLE_ID PropertyType annoPropertySens :: [AnnoAppl]

Instances

Eq CASL_DLSign Source #
Methods (==) :: CASL_DLSign -> CASL_DLSign -> Bool (/=) :: CASL_DLSign -> CASL_DLSign -> Bool
Data CASL_DLSign Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CASL_DLSign -> c CASL_DLSign gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CASL_DLSign toConstr :: CASL_DLSign -> Constr dataTypeOf :: CASL_DLSign -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c CASL_DLSign) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CASL_DLSign) gmapT :: (forall b. Data b => b -> b) -> CASL_DLSign -> CASL_DLSign gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CASL_DLSign -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CASL_DLSign -> r gmapQ :: (forall d. Data d => d -> u) -> CASL_DLSign -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CASL_DLSign -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CASL_DLSign -> m CASL_DLSign gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CASL_DLSign -> m CASL_DLSign gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CASL_DLSign -> m CASL_DLSign
Ord CASL_DLSign Source #
Methods compare :: CASL_DLSign -> CASL_DLSign -> Ordering (<) :: CASL_DLSign -> CASL_DLSign -> Bool (<=) :: CASL_DLSign -> CASL_DLSign -> Bool (>) :: CASL_DLSign -> CASL_DLSign -> Bool (>=) :: CASL_DLSign -> CASL_DLSign -> Bool max :: CASL_DLSign -> CASL_DLSign -> CASL_DLSign min :: CASL_DLSign -> CASL_DLSign -> CASL_DLSign
Show CASL_DLSign Source #
Methods showsPrec :: Int -> CASL_DLSign -> ShowS show :: CASL_DLSign -> String showList :: [CASL_DLSign] -> ShowS
Pretty CASL_DLSign Source #
Methods pretty :: CASL_DLSign -> Doc Source # pretties :: [CASL_DLSign] -> Doc Source #
Sentences CASL_DL DLFORMULA DLSign DLMor Symbol Source #
Methods map_sen :: CASL_DL -> DLMor -> DLFORMULA -> Result DLFORMULA Source # simplify_sen :: CASL_DL -> DLSign -> DLFORMULA -> DLFORMULA Source # negation :: CASL_DL -> DLFORMULA -> Maybe DLFORMULA Source # print_sign :: CASL_DL -> DLSign -> Doc Source # print_named :: CASL_DL -> Named DLFORMULA -> Doc Source # sym_of :: CASL_DL -> DLSign -> [Set Symbol] Source # mostSymsOf :: CASL_DL -> DLSign -> [Symbol] Source # symmap_of :: CASL_DL -> DLMor -> EndoMap Symbol Source # sym_name :: CASL_DL -> Symbol -> Id Source # sym_label :: CASL_DL -> Symbol -> Maybe String Source # fullSymName :: CASL_DL -> Symbol -> String Source # symKind :: CASL_DL -> Symbol -> String Source # symsOfSen :: CASL_DL -> DLSign -> DLFORMULA -> [Symbol] Source # pair_symbols :: CASL_DL -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol Source #
Methods basic_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, GlobalAnnos) -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA])) Source # sen_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, DLFORMULA) -> Result DLFORMULA) Source # extBasicAnalysis :: CASL_DL -> IRI -> LibName -> DL_BASIC_SPEC -> DLSign -> GlobalAnnos -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA]) Source # stat_symb_map_items :: CASL_DL -> DLSign -> Maybe DLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: CASL_DL -> DLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: CASL_DL -> Maybe ((DLSign, [Named DLFORMULA]) -> DL_BASIC_SPEC) Source # ensures_amalgamability :: CASL_DL -> ([CASLAmalgOpt], Gr DLSign (Int, DLMor), [(Int, DLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CASL_DL -> DLMor -> [Named DLFORMULA] -> Result (DLSign, [Named DLFORMULA]) Source # signature_colimit :: CASL_DL -> Gr DLSign (Int, DLMor) -> Result (DLSign, Map Int DLMor) Source # qualify :: CASL_DL -> SIMPLE_ID -> LibName -> DLMor -> DLSign -> Result (DLMor, [Named DLFORMULA]) Source # symbol_to_raw :: CASL_DL -> Symbol -> RawSymbol Source # id_to_raw :: CASL_DL -> Id -> RawSymbol Source # matches :: CASL_DL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: CASL_DL -> DLSign Source # add_symb_to_sign :: CASL_DL -> DLSign -> Symbol -> Result DLSign Source # signature_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # signatureDiff :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # intersection :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # final_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # morphism_union :: CASL_DL -> DLMor -> DLMor -> Result DLMor Source # is_subsig :: CASL_DL -> DLSign -> DLSign -> Bool Source # subsig_inclusion :: CASL_DL -> DLSign -> DLSign -> Result DLMor Source # generated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source # cogenerated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source # induced_from_morphism :: CASL_DL -> EndoMap RawSymbol -> DLSign -> Result DLMor Source # induced_from_to_morphism :: CASL_DL -> EndoMap RawSymbol -> ExtSign DLSign Symbol -> ExtSign DLSign Symbol -> Result DLMor Source # is_transportable :: CASL_DL -> DLMor -> Bool Source # is_injective :: CASL_DL -> DLMor -> Bool Source # theory_to_taxonomy :: CASL_DL -> TaxoGraphKind -> MMiSSOntology -> DLSign -> [Named DLFORMULA] -> Result MMiSSOntology Source # corresp2th :: CASL_DL -> String -> Bool -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (DLSign, [Named DLFORMULA], DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CASL_DL -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (DLSign, DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CASL_DL -> [IRI] -> (DLSign, [Named DLFORMULA]) -> Result (DLSign, [Named DLFORMULA]) Source #
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 #
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 #

data PropertyType Source #

Constructors

AnnoProperty
OntoProperty

Instances

Eq PropertyType Source #
Methods (==) :: PropertyType -> PropertyType -> Bool (/=) :: PropertyType -> PropertyType -> Bool
Data PropertyType Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PropertyType -> c PropertyType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PropertyType toConstr :: PropertyType -> Constr dataTypeOf :: PropertyType -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c PropertyType) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropertyType) gmapT :: (forall b. Data b => b -> b) -> PropertyType -> PropertyType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PropertyType -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PropertyType -> r gmapQ :: (forall d. Data d => d -> u) -> PropertyType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PropertyType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PropertyType -> m PropertyType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PropertyType -> m PropertyType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PropertyType -> m PropertyType
Ord PropertyType Source #
Methods compare :: PropertyType -> PropertyType -> Ordering (<) :: PropertyType -> PropertyType -> Bool (<=) :: PropertyType -> PropertyType -> Bool (>) :: PropertyType -> PropertyType -> Bool (>=) :: PropertyType -> PropertyType -> Bool max :: PropertyType -> PropertyType -> PropertyType min :: PropertyType -> PropertyType -> PropertyType
Show PropertyType Source #
Methods showsPrec :: Int -> PropertyType -> ShowS show :: PropertyType -> String showList :: [PropertyType] -> ShowS

data AnnoAppl Source #

Constructors

AnnoAppl SIMPLE_ID Id AnnoLiteral

Instances

Eq AnnoAppl Source #
Methods (==) :: AnnoAppl -> AnnoAppl -> Bool (/=) :: AnnoAppl -> AnnoAppl -> Bool
Data AnnoAppl Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AnnoAppl -> c AnnoAppl gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AnnoAppl toConstr :: AnnoAppl -> Constr dataTypeOf :: AnnoAppl -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c AnnoAppl) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AnnoAppl) gmapT :: (forall b. Data b => b -> b) -> AnnoAppl -> AnnoAppl gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AnnoAppl -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AnnoAppl -> r gmapQ :: (forall d. Data d => d -> u) -> AnnoAppl -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> AnnoAppl -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> AnnoAppl -> m AnnoAppl gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnoAppl -> m AnnoAppl gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnoAppl -> m AnnoAppl
Ord AnnoAppl Source #
Methods compare :: AnnoAppl -> AnnoAppl -> Ordering (<) :: AnnoAppl -> AnnoAppl -> Bool (<=) :: AnnoAppl -> AnnoAppl -> Bool (>) :: AnnoAppl -> AnnoAppl -> Bool (>=) :: AnnoAppl -> AnnoAppl -> Bool max :: AnnoAppl -> AnnoAppl -> AnnoAppl min :: AnnoAppl -> AnnoAppl -> AnnoAppl
Show AnnoAppl Source #
Methods showsPrec :: Int -> AnnoAppl -> ShowS show :: AnnoAppl -> String showList :: [AnnoAppl] -> ShowS
Pretty AnnoAppl Source #
Methods pretty :: AnnoAppl -> Doc Source # pretties :: [AnnoAppl] -> Doc Source #

data AnnoLiteral Source #

Constructors

AL_Term (TERM DL_FORMULA)
AL_Id Id

Instances

Eq AnnoLiteral Source #
Methods (==) :: AnnoLiteral -> AnnoLiteral -> Bool (/=) :: AnnoLiteral -> AnnoLiteral -> Bool
Data AnnoLiteral Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AnnoLiteral -> c AnnoLiteral gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AnnoLiteral toConstr :: AnnoLiteral -> Constr dataTypeOf :: AnnoLiteral -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c AnnoLiteral) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AnnoLiteral) gmapT :: (forall b. Data b => b -> b) -> AnnoLiteral -> AnnoLiteral gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AnnoLiteral -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AnnoLiteral -> r gmapQ :: (forall d. Data d => d -> u) -> AnnoLiteral -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> AnnoLiteral -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral
Ord AnnoLiteral Source #
Methods compare :: AnnoLiteral -> AnnoLiteral -> Ordering (<) :: AnnoLiteral -> AnnoLiteral -> Bool (<=) :: AnnoLiteral -> AnnoLiteral -> Bool (>) :: AnnoLiteral -> AnnoLiteral -> Bool (>=) :: AnnoLiteral -> AnnoLiteral -> Bool max :: AnnoLiteral -> AnnoLiteral -> AnnoLiteral min :: AnnoLiteral -> AnnoLiteral -> AnnoLiteral
Show AnnoLiteral Source #
Methods showsPrec :: Int -> AnnoLiteral -> ShowS show :: AnnoLiteral -> String showList :: [AnnoLiteral] -> ShowS
Pretty AnnoLiteral Source #
Methods pretty :: AnnoLiteral -> Doc Source # pretties :: [AnnoLiteral] -> Doc Source #

emptyCASL_DLSign :: CASL_DLSign Source #

addCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> CASL_DLSign Source #

throwAnnoError :: String -> SIMPLE_ID -> PropertyType -> PropertyType -> PropertyType Source #

diffCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> CASL_DLSign Source #

isSubCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> Bool Source #

isSublistOf :: Eq a => [a] -> [a] -> Bool Source #