Copyright	DFKI GmbH 2009
License	GPLv2 or higher, see LICENSE.txt
Maintainer	codruta.liliana@gmail.com
Stability	experimental
Portability	portable
Safe Haskell	Safe

ExtModal.AS_ExtModal

Description

Documentation

type EM_BASIC_SPEC = BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA Source #

data FrameForm Source #

Constructors

FrameForm
Fields frameVars :: [VAR_DECL] frameForms :: [Annoted (FORMULA EM_FORMULA)] frameFormRange :: Range

Instances

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

data ModDefn Source #

Constructors

ModDefn Bool Bool [Annoted Id] [Annoted FrameForm] Range

Instances

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

data EM_BASIC_ITEM Source #

Constructors

ModItem ModDefn
Nominal_decl [Annoted SIMPLE_ID] Range

Instances

Data EM_BASIC_ITEM Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_BASIC_ITEM -> c EM_BASIC_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_BASIC_ITEM toConstr :: EM_BASIC_ITEM -> Constr dataTypeOf :: EM_BASIC_ITEM -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c EM_BASIC_ITEM) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_BASIC_ITEM) gmapT :: (forall b. Data b => b -> b) -> EM_BASIC_ITEM -> EM_BASIC_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_BASIC_ITEM -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_BASIC_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> EM_BASIC_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> EM_BASIC_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM
Show EM_BASIC_ITEM Source #
Methods showsPrec :: Int -> EM_BASIC_ITEM -> ShowS show :: EM_BASIC_ITEM -> String showList :: [EM_BASIC_ITEM] -> ShowS
GetRange EM_BASIC_ITEM Source #
Methods getRange :: EM_BASIC_ITEM -> Range Source # rangeSpan :: EM_BASIC_ITEM -> [Pos] Source #
Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Methods parsersAndPrinters :: ExtModal -> Map String (PrefixMap -> AParser st EM_BASIC_SPEC, EM_BASIC_SPEC -> Doc) Source # parse_basic_spec :: ExtModal -> Maybe (PrefixMap -> AParser st EM_BASIC_SPEC) Source # parseSingleSymbItem :: ExtModal -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_items :: ExtModal -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_map_items :: ExtModal -> Maybe (AParser st SYMB_MAP_ITEMS) Source # toItem :: ExtModal -> EM_BASIC_SPEC -> Item Source # symb_items_name :: ExtModal -> SYMB_ITEMS -> [String] Source #
StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source #
Methods basic_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, GlobalAnnos) -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA])) Source # sen_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, ExtModalFORMULA) -> Result ExtModalFORMULA) Source # extBasicAnalysis :: ExtModal -> IRI -> LibName -> EM_BASIC_SPEC -> ExtModalSign -> GlobalAnnos -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA]) Source # stat_symb_map_items :: ExtModal -> ExtModalSign -> Maybe ExtModalSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: ExtModal -> ExtModalSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: ExtModal -> Maybe ((ExtModalSign, [Named ExtModalFORMULA]) -> EM_BASIC_SPEC) Source # ensures_amalgamability :: ExtModal -> ([CASLAmalgOpt], Gr ExtModalSign (Int, ExtModalMorph), [(Int, ExtModalMorph)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: ExtModal -> ExtModalMorph -> [Named ExtModalFORMULA] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # signature_colimit :: ExtModal -> Gr ExtModalSign (Int, ExtModalMorph) -> Result (ExtModalSign, Map Int ExtModalMorph) Source # qualify :: ExtModal -> SIMPLE_ID -> LibName -> ExtModalMorph -> ExtModalSign -> Result (ExtModalMorph, [Named ExtModalFORMULA]) Source # symbol_to_raw :: ExtModal -> Symbol -> RawSymbol Source # id_to_raw :: ExtModal -> Id -> RawSymbol Source # matches :: ExtModal -> Symbol -> RawSymbol -> Bool Source # empty_signature :: ExtModal -> ExtModalSign Source # add_symb_to_sign :: ExtModal -> ExtModalSign -> Symbol -> Result ExtModalSign Source # signature_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # signatureDiff :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # intersection :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # final_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # morphism_union :: ExtModal -> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph Source # is_subsig :: ExtModal -> ExtModalSign -> ExtModalSign -> Bool Source # subsig_inclusion :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalMorph Source # generated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source # cogenerated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source # induced_from_morphism :: ExtModal -> EndoMap RawSymbol -> ExtModalSign -> Result ExtModalMorph Source # induced_from_to_morphism :: ExtModal -> EndoMap RawSymbol -> ExtSign ExtModalSign Symbol -> ExtSign ExtModalSign Symbol -> Result ExtModalMorph Source # is_transportable :: ExtModal -> ExtModalMorph -> Bool Source # is_injective :: ExtModal -> ExtModalMorph -> Bool Source # theory_to_taxonomy :: ExtModal -> TaxoGraphKind -> MMiSSOntology -> ExtModalSign -> [Named ExtModalFORMULA] -> Result MMiSSOntology Source # corresp2th :: ExtModal -> String -> Bool -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ExtModalSign, [Named ExtModalFORMULA], ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: ExtModal -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ExtModalSign, ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: ExtModal -> [IRI] -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #
Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods parse_basic_sen :: ExtModal -> Maybe (EM_BASIC_SPEC -> AParser st ExtModalFORMULA) Source # stability :: ExtModal -> Stability Source # data_logic :: ExtModal -> Maybe AnyLogic Source # top_sublogic :: ExtModal -> ExtModalSL Source # all_sublogics :: ExtModal -> [ExtModalSL] Source # bottomSublogic :: ExtModal -> Maybe ExtModalSL Source # sublogicDimensions :: ExtModal -> [[ExtModalSL]] Source # parseSublogic :: ExtModal -> String -> Maybe ExtModalSL Source # proj_sublogic_epsilon :: ExtModal -> ExtModalSL -> ExtModalSign -> ExtModalMorph Source # provers :: ExtModal -> [Prover ExtModalSign ExtModalFORMULA ExtModalMorph ExtModalSL ()] Source # default_prover :: ExtModal -> String Source # cons_checkers :: ExtModal -> [ConsChecker ExtModalSign ExtModalFORMULA ExtModalSL ExtModalMorph ()] Source # conservativityCheck :: ExtModal -> [ConservativityChecker ExtModalSign ExtModalFORMULA ExtModalMorph] Source # empty_proof_tree :: ExtModal -> () Source # syntaxTable :: ExtModal -> ExtModalSign -> Maybe SyntaxTable Source # omdoc_metatheory :: ExtModal -> Maybe OMCD Source # export_symToOmdoc :: ExtModal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: ExtModal -> NameMap Symbol -> ExtModalFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: ExtModal -> SigMap Symbol -> ExtModalSign -> [Named ExtModalFORMULA] -> Result [TCElement] Source # omdocToSym :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ExtModalFORMULA)) Source # addOMadtToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [[OmdADT]] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # addOmdocToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [TCElement] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # sublogicOfTheo :: ExtModal -> (ExtModalSign, [ExtModalFORMULA]) -> ExtModalSL Source #
Comorphism CASL2ExtModal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2ExtModal -> CASL Source # sourceSublogic :: CASL2ExtModal -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2ExtModal -> CASL_Sublogics Source # minSourceTheory :: CASL2ExtModal -> Maybe (LibName, String) Source # targetLogic :: CASL2ExtModal -> ExtModal Source # mapSublogic :: CASL2ExtModal -> CASL_Sublogics -> Maybe ExtModalSL Source # map_theory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: CASL2ExtModal -> CASLMor -> Result ExtModalMorph Source # map_sentence :: CASL2ExtModal -> CASLSign -> CASLFORMULA -> Result ExtModalFORMULA Source # map_symbol :: CASL2ExtModal -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2ExtModal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2ExtModal -> Bool Source # has_model_expansion :: CASL2ExtModal -> Bool Source # is_weakly_amalgamable :: CASL2ExtModal -> Bool Source # constituents :: CASL2ExtModal -> [String] Source # isInclusionComorphism :: CASL2ExtModal -> Bool Source # rps :: CASL2ExtModal -> Bool Source # eps :: CASL2ExtModal -> Bool Source #
Comorphism ExtModal2CASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Methods sourceLogic :: ExtModal2CASL -> ExtModal Source # sourceSublogic :: ExtModal2CASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2CASL -> ExtModalSL Source # minSourceTheory :: ExtModal2CASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2CASL -> CASL Source # mapSublogic :: ExtModal2CASL -> ExtModalSL -> Maybe CASL_Sublogics Source # map_theory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: ExtModal2CASL -> ExtModalMorph -> Result CASLMor Source # map_sentence :: ExtModal2CASL -> ExtModalSign -> ExtModalFORMULA -> Result CASLFORMULA Source # map_symbol :: ExtModal2CASL -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2CASL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2CASL -> Bool Source # has_model_expansion :: ExtModal2CASL -> Bool Source # is_weakly_amalgamable :: ExtModal2CASL -> Bool Source # constituents :: ExtModal2CASL -> [String] Source # isInclusionComorphism :: ExtModal2CASL -> Bool Source # rps :: ExtModal2CASL -> Bool Source # eps :: ExtModal2CASL -> Bool Source #
Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalNoSubsorts -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # mapSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalNoSubsorts -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source # has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source # constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source # rps :: ExtModal2ExtModalNoSubsorts -> Bool Source # eps :: ExtModal2ExtModalNoSubsorts -> Bool Source #
Comorphism ExtModal2ExtModalTotal ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods sourceLogic :: ExtModal2ExtModalTotal -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalTotal -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalTotal -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalTotal -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalTotal -> ExtModal Source # mapSublogic :: ExtModal2ExtModalTotal -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalTotal -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalTotal -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalTotal -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalTotal -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalTotal -> Bool Source # has_model_expansion :: ExtModal2ExtModalTotal -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalTotal -> Bool Source # constituents :: ExtModal2ExtModalTotal -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalTotal -> Bool Source # rps :: ExtModal2ExtModalTotal -> Bool Source # eps :: ExtModal2ExtModalTotal -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source #
Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Methods sourceLogic :: ExtModal2OWL -> ExtModal Source # sourceSublogic :: ExtModal2OWL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2OWL -> ExtModalSL Source # minSourceTheory :: ExtModal2OWL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2OWL -> OWL2 Source # mapSublogic :: ExtModal2OWL -> ExtModalSL -> Maybe ProfSub Source # map_theory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: ExtModal2OWL -> ExtModalMorph -> Result OWLMorphism Source # map_sentence :: ExtModal2OWL -> ExtModalSign -> ExtModalFORMULA -> Result Axiom Source # map_symbol :: ExtModal2OWL -> ExtModalSign -> Symbol -> Set Entity Source # extractModel :: ExtModal2OWL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2OWL -> Bool Source # has_model_expansion :: ExtModal2OWL -> Bool Source # is_weakly_amalgamable :: ExtModal2OWL -> Bool Source # constituents :: ExtModal2OWL -> [String] Source # isInclusionComorphism :: ExtModal2OWL -> Bool Source # rps :: ExtModal2OWL -> Bool Source # eps :: ExtModal2OWL -> Bool Source #

data ModOp Source #

Constructors

Composition
Intersection
Union
OrElse

Instances

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

data MODALITY Source #

Constructors

SimpleMod SIMPLE_ID
TermMod (TERM EM_FORMULA)
ModOp ModOp MODALITY MODALITY
TransClos MODALITY
Guard (FORMULA EM_FORMULA)

Instances

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

data EM_SIG_ITEM Source #

Constructors

Rigid_op_items Bool [Annoted (OP_ITEM EM_FORMULA)] Range
Rigid_pred_items Bool [Annoted (PRED_ITEM EM_FORMULA)] Range

Instances

Data EM_SIG_ITEM Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_SIG_ITEM -> c EM_SIG_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_SIG_ITEM toConstr :: EM_SIG_ITEM -> Constr dataTypeOf :: EM_SIG_ITEM -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c EM_SIG_ITEM) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_SIG_ITEM) gmapT :: (forall b. Data b => b -> b) -> EM_SIG_ITEM -> EM_SIG_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_SIG_ITEM -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_SIG_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> EM_SIG_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> EM_SIG_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM
Show EM_SIG_ITEM Source #
Methods showsPrec :: Int -> EM_SIG_ITEM -> ShowS show :: EM_SIG_ITEM -> String showList :: [EM_SIG_ITEM] -> ShowS
GetRange EM_SIG_ITEM Source #
Methods getRange :: EM_SIG_ITEM -> Range Source # rangeSpan :: EM_SIG_ITEM -> [Pos] Source #
Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Methods parsersAndPrinters :: ExtModal -> Map String (PrefixMap -> AParser st EM_BASIC_SPEC, EM_BASIC_SPEC -> Doc) Source # parse_basic_spec :: ExtModal -> Maybe (PrefixMap -> AParser st EM_BASIC_SPEC) Source # parseSingleSymbItem :: ExtModal -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_items :: ExtModal -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_map_items :: ExtModal -> Maybe (AParser st SYMB_MAP_ITEMS) Source # toItem :: ExtModal -> EM_BASIC_SPEC -> Item Source # symb_items_name :: ExtModal -> SYMB_ITEMS -> [String] Source #
StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source #
Methods basic_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, GlobalAnnos) -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA])) Source # sen_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, ExtModalFORMULA) -> Result ExtModalFORMULA) Source # extBasicAnalysis :: ExtModal -> IRI -> LibName -> EM_BASIC_SPEC -> ExtModalSign -> GlobalAnnos -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA]) Source # stat_symb_map_items :: ExtModal -> ExtModalSign -> Maybe ExtModalSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: ExtModal -> ExtModalSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: ExtModal -> Maybe ((ExtModalSign, [Named ExtModalFORMULA]) -> EM_BASIC_SPEC) Source # ensures_amalgamability :: ExtModal -> ([CASLAmalgOpt], Gr ExtModalSign (Int, ExtModalMorph), [(Int, ExtModalMorph)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: ExtModal -> ExtModalMorph -> [Named ExtModalFORMULA] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # signature_colimit :: ExtModal -> Gr ExtModalSign (Int, ExtModalMorph) -> Result (ExtModalSign, Map Int ExtModalMorph) Source # qualify :: ExtModal -> SIMPLE_ID -> LibName -> ExtModalMorph -> ExtModalSign -> Result (ExtModalMorph, [Named ExtModalFORMULA]) Source # symbol_to_raw :: ExtModal -> Symbol -> RawSymbol Source # id_to_raw :: ExtModal -> Id -> RawSymbol Source # matches :: ExtModal -> Symbol -> RawSymbol -> Bool Source # empty_signature :: ExtModal -> ExtModalSign Source # add_symb_to_sign :: ExtModal -> ExtModalSign -> Symbol -> Result ExtModalSign Source # signature_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # signatureDiff :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # intersection :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # final_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # morphism_union :: ExtModal -> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph Source # is_subsig :: ExtModal -> ExtModalSign -> ExtModalSign -> Bool Source # subsig_inclusion :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalMorph Source # generated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source # cogenerated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source # induced_from_morphism :: ExtModal -> EndoMap RawSymbol -> ExtModalSign -> Result ExtModalMorph Source # induced_from_to_morphism :: ExtModal -> EndoMap RawSymbol -> ExtSign ExtModalSign Symbol -> ExtSign ExtModalSign Symbol -> Result ExtModalMorph Source # is_transportable :: ExtModal -> ExtModalMorph -> Bool Source # is_injective :: ExtModal -> ExtModalMorph -> Bool Source # theory_to_taxonomy :: ExtModal -> TaxoGraphKind -> MMiSSOntology -> ExtModalSign -> [Named ExtModalFORMULA] -> Result MMiSSOntology Source # corresp2th :: ExtModal -> String -> Bool -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ExtModalSign, [Named ExtModalFORMULA], ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: ExtModal -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ExtModalSign, ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: ExtModal -> [IRI] -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #
Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods parse_basic_sen :: ExtModal -> Maybe (EM_BASIC_SPEC -> AParser st ExtModalFORMULA) Source # stability :: ExtModal -> Stability Source # data_logic :: ExtModal -> Maybe AnyLogic Source # top_sublogic :: ExtModal -> ExtModalSL Source # all_sublogics :: ExtModal -> [ExtModalSL] Source # bottomSublogic :: ExtModal -> Maybe ExtModalSL Source # sublogicDimensions :: ExtModal -> [[ExtModalSL]] Source # parseSublogic :: ExtModal -> String -> Maybe ExtModalSL Source # proj_sublogic_epsilon :: ExtModal -> ExtModalSL -> ExtModalSign -> ExtModalMorph Source # provers :: ExtModal -> [Prover ExtModalSign ExtModalFORMULA ExtModalMorph ExtModalSL ()] Source # default_prover :: ExtModal -> String Source # cons_checkers :: ExtModal -> [ConsChecker ExtModalSign ExtModalFORMULA ExtModalSL ExtModalMorph ()] Source # conservativityCheck :: ExtModal -> [ConservativityChecker ExtModalSign ExtModalFORMULA ExtModalMorph] Source # empty_proof_tree :: ExtModal -> () Source # syntaxTable :: ExtModal -> ExtModalSign -> Maybe SyntaxTable Source # omdoc_metatheory :: ExtModal -> Maybe OMCD Source # export_symToOmdoc :: ExtModal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: ExtModal -> NameMap Symbol -> ExtModalFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: ExtModal -> SigMap Symbol -> ExtModalSign -> [Named ExtModalFORMULA] -> Result [TCElement] Source # omdocToSym :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ExtModalFORMULA)) Source # addOMadtToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [[OmdADT]] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # addOmdocToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [TCElement] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # sublogicOfTheo :: ExtModal -> (ExtModalSign, [ExtModalFORMULA]) -> ExtModalSL Source #
Comorphism CASL2ExtModal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2ExtModal -> CASL Source # sourceSublogic :: CASL2ExtModal -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2ExtModal -> CASL_Sublogics Source # minSourceTheory :: CASL2ExtModal -> Maybe (LibName, String) Source # targetLogic :: CASL2ExtModal -> ExtModal Source # mapSublogic :: CASL2ExtModal -> CASL_Sublogics -> Maybe ExtModalSL Source # map_theory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: CASL2ExtModal -> CASLMor -> Result ExtModalMorph Source # map_sentence :: CASL2ExtModal -> CASLSign -> CASLFORMULA -> Result ExtModalFORMULA Source # map_symbol :: CASL2ExtModal -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2ExtModal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2ExtModal -> Bool Source # has_model_expansion :: CASL2ExtModal -> Bool Source # is_weakly_amalgamable :: CASL2ExtModal -> Bool Source # constituents :: CASL2ExtModal -> [String] Source # isInclusionComorphism :: CASL2ExtModal -> Bool Source # rps :: CASL2ExtModal -> Bool Source # eps :: CASL2ExtModal -> Bool Source #
Comorphism ExtModal2CASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Methods sourceLogic :: ExtModal2CASL -> ExtModal Source # sourceSublogic :: ExtModal2CASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2CASL -> ExtModalSL Source # minSourceTheory :: ExtModal2CASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2CASL -> CASL Source # mapSublogic :: ExtModal2CASL -> ExtModalSL -> Maybe CASL_Sublogics Source # map_theory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: ExtModal2CASL -> ExtModalMorph -> Result CASLMor Source # map_sentence :: ExtModal2CASL -> ExtModalSign -> ExtModalFORMULA -> Result CASLFORMULA Source # map_symbol :: ExtModal2CASL -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2CASL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2CASL -> Bool Source # has_model_expansion :: ExtModal2CASL -> Bool Source # is_weakly_amalgamable :: ExtModal2CASL -> Bool Source # constituents :: ExtModal2CASL -> [String] Source # isInclusionComorphism :: ExtModal2CASL -> Bool Source # rps :: ExtModal2CASL -> Bool Source # eps :: ExtModal2CASL -> Bool Source #
Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalNoSubsorts -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # mapSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalNoSubsorts -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source # has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source # constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source # rps :: ExtModal2ExtModalNoSubsorts -> Bool Source # eps :: ExtModal2ExtModalNoSubsorts -> Bool Source #
Comorphism ExtModal2ExtModalTotal ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods sourceLogic :: ExtModal2ExtModalTotal -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalTotal -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalTotal -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalTotal -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalTotal -> ExtModal Source # mapSublogic :: ExtModal2ExtModalTotal -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalTotal -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalTotal -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalTotal -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalTotal -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalTotal -> Bool Source # has_model_expansion :: ExtModal2ExtModalTotal -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalTotal -> Bool Source # constituents :: ExtModal2ExtModalTotal -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalTotal -> Bool Source # rps :: ExtModal2ExtModalTotal -> Bool Source # eps :: ExtModal2ExtModalTotal -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source #
Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Methods sourceLogic :: ExtModal2OWL -> ExtModal Source # sourceSublogic :: ExtModal2OWL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2OWL -> ExtModalSL Source # minSourceTheory :: ExtModal2OWL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2OWL -> OWL2 Source # mapSublogic :: ExtModal2OWL -> ExtModalSL -> Maybe ProfSub Source # map_theory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: ExtModal2OWL -> ExtModalMorph -> Result OWLMorphism Source # map_sentence :: ExtModal2OWL -> ExtModalSign -> ExtModalFORMULA -> Result Axiom Source # map_symbol :: ExtModal2OWL -> ExtModalSign -> Symbol -> Set Entity Source # extractModel :: ExtModal2OWL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2OWL -> Bool Source # has_model_expansion :: ExtModal2OWL -> Bool Source # is_weakly_amalgamable :: ExtModal2OWL -> Bool Source # constituents :: ExtModal2OWL -> [String] Source # isInclusionComorphism :: ExtModal2OWL -> Bool Source # rps :: ExtModal2OWL -> Bool Source # eps :: ExtModal2OWL -> Bool Source #

data BoxOp Source #

Constructors

Box
Diamond
EBox

Instances

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

data FormPrefix Source #

Constructors

BoxOrDiamond BoxOp MODALITY Bool Int
Hybrid Bool SIMPLE_ID
PathQuantification Bool
NextY Bool
StateQuantification Bool Bool
FixedPoint Bool VAR

Instances

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

data EM_FORMULA Source #

Constructors

PrefixForm FormPrefix (FORMULA EM_FORMULA) Range
UntilSince Bool (FORMULA EM_FORMULA) (FORMULA EM_FORMULA) Range
ModForm ModDefn

Instances

Eq EM_FORMULA Source #
Methods (==) :: EM_FORMULA -> EM_FORMULA -> Bool (/=) :: EM_FORMULA -> EM_FORMULA -> Bool
Data EM_FORMULA Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_FORMULA -> c EM_FORMULA gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_FORMULA toConstr :: EM_FORMULA -> Constr dataTypeOf :: EM_FORMULA -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c EM_FORMULA) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_FORMULA) gmapT :: (forall b. Data b => b -> b) -> EM_FORMULA -> EM_FORMULA gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_FORMULA -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_FORMULA -> r gmapQ :: (forall d. Data d => d -> u) -> EM_FORMULA -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> EM_FORMULA -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA
Ord EM_FORMULA Source #
Methods compare :: EM_FORMULA -> EM_FORMULA -> Ordering (<) :: EM_FORMULA -> EM_FORMULA -> Bool (<=) :: EM_FORMULA -> EM_FORMULA -> Bool (>) :: EM_FORMULA -> EM_FORMULA -> Bool (>=) :: EM_FORMULA -> EM_FORMULA -> Bool max :: EM_FORMULA -> EM_FORMULA -> EM_FORMULA min :: EM_FORMULA -> EM_FORMULA -> EM_FORMULA
Show EM_FORMULA Source #
Methods showsPrec :: Int -> EM_FORMULA -> ShowS show :: EM_FORMULA -> String showList :: [EM_FORMULA] -> ShowS
GetRange EM_FORMULA Source #
Methods getRange :: EM_FORMULA -> Range Source # rangeSpan :: EM_FORMULA -> [Pos] Source #
Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol Source #
Methods map_sen :: ExtModal -> ExtModalMorph -> ExtModalFORMULA -> Result ExtModalFORMULA Source # simplify_sen :: ExtModal -> ExtModalSign -> ExtModalFORMULA -> ExtModalFORMULA Source # negation :: ExtModal -> ExtModalFORMULA -> Maybe ExtModalFORMULA Source # print_sign :: ExtModal -> ExtModalSign -> Doc Source # print_named :: ExtModal -> Named ExtModalFORMULA -> Doc Source # sym_of :: ExtModal -> ExtModalSign -> [Set Symbol] Source # mostSymsOf :: ExtModal -> ExtModalSign -> [Symbol] Source # symmap_of :: ExtModal -> ExtModalMorph -> EndoMap Symbol Source # sym_name :: ExtModal -> Symbol -> Id Source # sym_label :: ExtModal -> Symbol -> Maybe String Source # fullSymName :: ExtModal -> Symbol -> String Source # symKind :: ExtModal -> Symbol -> String Source # symsOfSen :: ExtModal -> ExtModalSign -> ExtModalFORMULA -> [Symbol] Source # pair_symbols :: ExtModal -> Symbol -> Symbol -> Result Symbol Source #
Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Methods parsersAndPrinters :: ExtModal -> Map String (PrefixMap -> AParser st EM_BASIC_SPEC, EM_BASIC_SPEC -> Doc) Source # parse_basic_spec :: ExtModal -> Maybe (PrefixMap -> AParser st EM_BASIC_SPEC) Source # parseSingleSymbItem :: ExtModal -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_items :: ExtModal -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_map_items :: ExtModal -> Maybe (AParser st SYMB_MAP_ITEMS) Source # toItem :: ExtModal -> EM_BASIC_SPEC -> Item Source # symb_items_name :: ExtModal -> SYMB_ITEMS -> [String] Source #
StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source #
Methods basic_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, GlobalAnnos) -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA])) Source # sen_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, ExtModalFORMULA) -> Result ExtModalFORMULA) Source # extBasicAnalysis :: ExtModal -> IRI -> LibName -> EM_BASIC_SPEC -> ExtModalSign -> GlobalAnnos -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA]) Source # stat_symb_map_items :: ExtModal -> ExtModalSign -> Maybe ExtModalSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: ExtModal -> ExtModalSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: ExtModal -> Maybe ((ExtModalSign, [Named ExtModalFORMULA]) -> EM_BASIC_SPEC) Source # ensures_amalgamability :: ExtModal -> ([CASLAmalgOpt], Gr ExtModalSign (Int, ExtModalMorph), [(Int, ExtModalMorph)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: ExtModal -> ExtModalMorph -> [Named ExtModalFORMULA] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # signature_colimit :: ExtModal -> Gr ExtModalSign (Int, ExtModalMorph) -> Result (ExtModalSign, Map Int ExtModalMorph) Source # qualify :: ExtModal -> SIMPLE_ID -> LibName -> ExtModalMorph -> ExtModalSign -> Result (ExtModalMorph, [Named ExtModalFORMULA]) Source # symbol_to_raw :: ExtModal -> Symbol -> RawSymbol Source # id_to_raw :: ExtModal -> Id -> RawSymbol Source # matches :: ExtModal -> Symbol -> RawSymbol -> Bool Source # empty_signature :: ExtModal -> ExtModalSign Source # add_symb_to_sign :: ExtModal -> ExtModalSign -> Symbol -> Result ExtModalSign Source # signature_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # signatureDiff :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # intersection :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # final_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source # morphism_union :: ExtModal -> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph Source # is_subsig :: ExtModal -> ExtModalSign -> ExtModalSign -> Bool Source # subsig_inclusion :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalMorph Source # generated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source # cogenerated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source # induced_from_morphism :: ExtModal -> EndoMap RawSymbol -> ExtModalSign -> Result ExtModalMorph Source # induced_from_to_morphism :: ExtModal -> EndoMap RawSymbol -> ExtSign ExtModalSign Symbol -> ExtSign ExtModalSign Symbol -> Result ExtModalMorph Source # is_transportable :: ExtModal -> ExtModalMorph -> Bool Source # is_injective :: ExtModal -> ExtModalMorph -> Bool Source # theory_to_taxonomy :: ExtModal -> TaxoGraphKind -> MMiSSOntology -> ExtModalSign -> [Named ExtModalFORMULA] -> Result MMiSSOntology Source # corresp2th :: ExtModal -> String -> Bool -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ExtModalSign, [Named ExtModalFORMULA], ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: ExtModal -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ExtModalSign, ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: ExtModal -> [IRI] -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #
Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods parse_basic_sen :: ExtModal -> Maybe (EM_BASIC_SPEC -> AParser st ExtModalFORMULA) Source # stability :: ExtModal -> Stability Source # data_logic :: ExtModal -> Maybe AnyLogic Source # top_sublogic :: ExtModal -> ExtModalSL Source # all_sublogics :: ExtModal -> [ExtModalSL] Source # bottomSublogic :: ExtModal -> Maybe ExtModalSL Source # sublogicDimensions :: ExtModal -> [[ExtModalSL]] Source # parseSublogic :: ExtModal -> String -> Maybe ExtModalSL Source # proj_sublogic_epsilon :: ExtModal -> ExtModalSL -> ExtModalSign -> ExtModalMorph Source # provers :: ExtModal -> [Prover ExtModalSign ExtModalFORMULA ExtModalMorph ExtModalSL ()] Source # default_prover :: ExtModal -> String Source # cons_checkers :: ExtModal -> [ConsChecker ExtModalSign ExtModalFORMULA ExtModalSL ExtModalMorph ()] Source # conservativityCheck :: ExtModal -> [ConservativityChecker ExtModalSign ExtModalFORMULA ExtModalMorph] Source # empty_proof_tree :: ExtModal -> () Source # syntaxTable :: ExtModal -> ExtModalSign -> Maybe SyntaxTable Source # omdoc_metatheory :: ExtModal -> Maybe OMCD Source # export_symToOmdoc :: ExtModal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: ExtModal -> NameMap Symbol -> ExtModalFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: ExtModal -> SigMap Symbol -> ExtModalSign -> [Named ExtModalFORMULA] -> Result [TCElement] Source # omdocToSym :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ExtModalFORMULA)) Source # addOMadtToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [[OmdADT]] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # addOmdocToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [TCElement] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # sublogicOfTheo :: ExtModal -> (ExtModalSign, [ExtModalFORMULA]) -> ExtModalSL Source #
Comorphism CASL2ExtModal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2ExtModal -> CASL Source # sourceSublogic :: CASL2ExtModal -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2ExtModal -> CASL_Sublogics Source # minSourceTheory :: CASL2ExtModal -> Maybe (LibName, String) Source # targetLogic :: CASL2ExtModal -> ExtModal Source # mapSublogic :: CASL2ExtModal -> CASL_Sublogics -> Maybe ExtModalSL Source # map_theory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: CASL2ExtModal -> CASLMor -> Result ExtModalMorph Source # map_sentence :: CASL2ExtModal -> CASLSign -> CASLFORMULA -> Result ExtModalFORMULA Source # map_symbol :: CASL2ExtModal -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2ExtModal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2ExtModal -> Bool Source # has_model_expansion :: CASL2ExtModal -> Bool Source # is_weakly_amalgamable :: CASL2ExtModal -> Bool Source # constituents :: CASL2ExtModal -> [String] Source # isInclusionComorphism :: CASL2ExtModal -> Bool Source # rps :: CASL2ExtModal -> Bool Source # eps :: CASL2ExtModal -> Bool Source #
Comorphism ExtModal2CASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Methods sourceLogic :: ExtModal2CASL -> ExtModal Source # sourceSublogic :: ExtModal2CASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2CASL -> ExtModalSL Source # minSourceTheory :: ExtModal2CASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2CASL -> CASL Source # mapSublogic :: ExtModal2CASL -> ExtModalSL -> Maybe CASL_Sublogics Source # map_theory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: ExtModal2CASL -> ExtModalMorph -> Result CASLMor Source # map_sentence :: ExtModal2CASL -> ExtModalSign -> ExtModalFORMULA -> Result CASLFORMULA Source # map_symbol :: ExtModal2CASL -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2CASL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2CASL -> Bool Source # has_model_expansion :: ExtModal2CASL -> Bool Source # is_weakly_amalgamable :: ExtModal2CASL -> Bool Source # constituents :: ExtModal2CASL -> [String] Source # isInclusionComorphism :: ExtModal2CASL -> Bool Source # rps :: ExtModal2CASL -> Bool Source # eps :: ExtModal2CASL -> Bool Source #
Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalNoSubsorts -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # mapSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalNoSubsorts -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source # has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source # constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source # rps :: ExtModal2ExtModalNoSubsorts -> Bool Source # eps :: ExtModal2ExtModalNoSubsorts -> Bool Source #
Comorphism ExtModal2ExtModalTotal ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Methods sourceLogic :: ExtModal2ExtModalTotal -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalTotal -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalTotal -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalTotal -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalTotal -> ExtModal Source # mapSublogic :: ExtModal2ExtModalTotal -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalTotal -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalTotal -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalTotal -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalTotal -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalTotal -> Bool Source # has_model_expansion :: ExtModal2ExtModalTotal -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalTotal -> Bool Source # constituents :: ExtModal2ExtModalTotal -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalTotal -> Bool Source # rps :: ExtModal2ExtModalTotal -> Bool Source # eps :: ExtModal2ExtModalTotal -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source #
Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Methods sourceLogic :: ExtModal2OWL -> ExtModal Source # sourceSublogic :: ExtModal2OWL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2OWL -> ExtModalSL Source # minSourceTheory :: ExtModal2OWL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2OWL -> OWL2 Source # mapSublogic :: ExtModal2OWL -> ExtModalSL -> Maybe ProfSub Source # map_theory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: ExtModal2OWL -> ExtModalMorph -> Result OWLMorphism Source # map_sentence :: ExtModal2OWL -> ExtModalSign -> ExtModalFORMULA -> Result Axiom Source # map_symbol :: ExtModal2OWL -> ExtModalSign -> Symbol -> Set Entity Source # extractModel :: ExtModal2OWL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2OWL -> Bool Source # has_model_expansion :: ExtModal2OWL -> Bool Source # is_weakly_amalgamable :: ExtModal2OWL -> Bool Source # constituents :: ExtModal2OWL -> [String] Source # isInclusionComorphism :: ExtModal2OWL -> Bool Source # rps :: ExtModal2OWL -> Bool Source # eps :: ExtModal2OWL -> Bool Source #