Copyright	(c) DFKI 2012
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	None

ExtModal.Sublogic

Description

Sublogics for ExtModal Logic

Synopsis

data Frequency
- = None
- | One
- | Many
data Sublogic = Sublogic {
- hasModalities :: Frequency
- hasTermMods :: Bool
- hasTransClos :: Bool
- hasNominals :: Bool
- hasTimeMods :: Frequency
- hasFixPoints :: Bool
- hasFrameAxioms :: Bool
}
maxSublogic :: Sublogic
botSublogic :: Sublogic
foleml :: Sublogic
joinSublogic :: Sublogic -> Sublogic -> Sublogic
joinSublogics :: [Sublogic] -> Sublogic
type ExtModalSL = CASL_SL Sublogic
minSublogicOfForm :: FORMULA EM_FORMULA -> ExtModalSL
minSublogicOfTerm :: TERM EM_FORMULA -> ExtModalSL
minSublogicOfMod :: MODALITY -> ExtModalSL
minSublogicOfPrefix :: FormPrefix -> ExtModalSL
minSublogicOfEM :: EM_FORMULA -> ExtModalSL
minSublogicOfModDefn :: ModDefn -> ExtModalSL
minSublogicEMSign :: EModalSign -> ExtModalSL
minSublogicEMBasic :: EM_BASIC_ITEM -> ExtModalSL
minSLExtSigItem :: EM_SIG_ITEM -> [ExtModalSL]
setModalities :: [a] -> Sublogic -> Sublogic
setTermMods :: Bool -> Sublogic -> Sublogic
setTimeMods :: Bool -> [a] -> Sublogic -> Sublogic
minMod :: Bool -> Frequency -> Frequency
sublogicsDim :: [[Sublogic]]
sublogName :: Sublogic -> String
parseSublog :: String -> (Sublogic, String)

Documentation

data Frequency Source #

Constructors

None
One
Many

Instances

Instances details

Enum Frequency Source #
Instance details Defined in ExtModal.Sublogic Methods succ :: Frequency -> Frequency pred :: Frequency -> Frequency toEnum :: Int -> Frequency fromEnum :: Frequency -> Int enumFrom :: Frequency -> [Frequency] enumFromThen :: Frequency -> Frequency -> [Frequency] enumFromTo :: Frequency -> Frequency -> [Frequency] enumFromThenTo :: Frequency -> Frequency -> Frequency -> [Frequency]
Eq Frequency Source #
Instance details Defined in ExtModal.Sublogic Methods (==) :: Frequency -> Frequency -> Bool (/=) :: Frequency -> Frequency -> Bool
Data Frequency Source #
Instance details Defined in ExtModal.Sublogic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Frequency -> c Frequency gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Frequency toConstr :: Frequency -> Constr dataTypeOf :: Frequency -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Frequency) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Frequency) gmapT :: (forall b. Data b => b -> b) -> Frequency -> Frequency gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Frequency -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Frequency -> r gmapQ :: (forall d. Data d => d -> u) -> Frequency -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Frequency -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Frequency -> m Frequency gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Frequency -> m Frequency gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Frequency -> m Frequency
Ord Frequency Source #
Instance details Defined in ExtModal.Sublogic Methods compare :: Frequency -> Frequency -> Ordering (<) :: Frequency -> Frequency -> Bool (<=) :: Frequency -> Frequency -> Bool (>) :: Frequency -> Frequency -> Bool (>=) :: Frequency -> Frequency -> Bool max :: Frequency -> Frequency -> Frequency min :: Frequency -> Frequency -> Frequency
Show Frequency Source #
Instance details Defined in ExtModal.Sublogic Methods showsPrec :: Int -> Frequency -> ShowS show :: Frequency -> String showList :: [Frequency] -> ShowS
Generic Frequency
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep Frequency :: Type -> Type Methods from :: Frequency -> Rep Frequency x to :: Rep Frequency x -> Frequency
FromJSON Frequency
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser Frequency parseJSONList :: Value -> Parser [Frequency]
ToJSON Frequency
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: Frequency -> Value toEncoding :: Frequency -> Encoding toJSONList :: [Frequency] -> Value toEncodingList :: [Frequency] -> Encoding
ShATermConvertible Frequency
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> Frequency -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Frequency] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Frequency) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Frequency])
type Rep Frequency
Instance details Defined in ExtModal.ATC_ExtModal type Rep Frequency = D1 ('MetaData "Frequency" "ExtModal.Sublogic" "main" 'False) (C1 ('MetaCons "None" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "One" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Many" 'PrefixI 'False) (U1 :: Type -> Type)))

data Sublogic Source #

Constructors

Sublogic
Fields hasModalities :: Frequency hasTermMods :: Bool hasTransClos :: Bool hasNominals :: Bool hasTimeMods :: Frequency hasFixPoints :: Bool hasFrameAxioms :: Bool

Instances

Instances details

Eq Sublogic Source #
Instance details Defined in ExtModal.Sublogic Methods (==) :: Sublogic -> Sublogic -> Bool (/=) :: Sublogic -> Sublogic -> Bool
Data Sublogic Source #
Instance details Defined in ExtModal.Sublogic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sublogic -> c Sublogic gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sublogic toConstr :: Sublogic -> Constr dataTypeOf :: Sublogic -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sublogic) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sublogic) gmapT :: (forall b. Data b => b -> b) -> Sublogic -> Sublogic gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sublogic -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sublogic -> r gmapQ :: (forall d. Data d => d -> u) -> Sublogic -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Sublogic -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sublogic -> m Sublogic
Ord Sublogic Source #
Instance details Defined in ExtModal.Sublogic Methods compare :: Sublogic -> Sublogic -> Ordering (<) :: Sublogic -> Sublogic -> Bool (<=) :: Sublogic -> Sublogic -> Bool (>) :: Sublogic -> Sublogic -> Bool (>=) :: Sublogic -> Sublogic -> Bool max :: Sublogic -> Sublogic -> Sublogic min :: Sublogic -> Sublogic -> Sublogic
Show Sublogic Source #
Instance details Defined in ExtModal.Sublogic Methods showsPrec :: Int -> Sublogic -> ShowS show :: Sublogic -> String showList :: [Sublogic] -> ShowS
Generic Sublogic
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep Sublogic :: Type -> Type Methods from :: Sublogic -> Rep Sublogic x to :: Rep Sublogic x -> Sublogic
FromJSON Sublogic
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser Sublogic parseJSONList :: Value -> Parser [Sublogic]
ToJSON Sublogic
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: Sublogic -> Value toEncoding :: Sublogic -> Encoding toJSONList :: [Sublogic] -> Value toEncodingList :: [Sublogic] -> Encoding
ShATermConvertible Sublogic
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> Sublogic -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sublogic] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sublogic) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sublogic])
Lattice Sublogic Source #
Instance details Defined in ExtModal.Sublogic Methods cjoin :: Sublogic -> Sublogic -> Sublogic Source # ctop :: Sublogic Source # bot :: Sublogic Source #
NameSL Sublogic Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods nameSL :: Sublogic -> String Source #
ProjForm Sublogic EM_FORMULA Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods projForm :: CASL_SL Sublogic -> EM_FORMULA -> Maybe (FORMULA EM_FORMULA) Source #
MinSL Sublogic EM_FORMULA Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods minSL :: EM_FORMULA -> CASL_SL Sublogic Source #
MinSL Sublogic EM_SIG_ITEM Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods minSL :: EM_SIG_ITEM -> CASL_SL Sublogic Source #
MinSL Sublogic EM_BASIC_ITEM Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods minSL :: EM_BASIC_ITEM -> CASL_SL Sublogic Source #
MinSL Sublogic EModalSign Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods minSL :: EModalSign -> CASL_SL Sublogic Source #
ProjSigItem Sublogic EM_SIG_ITEM EM_FORMULA Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods projSigItems :: CASL_SL Sublogic -> EM_SIG_ITEM -> (Maybe (SIG_ITEMS EM_SIG_ITEM EM_FORMULA), [SORT]) Source #
ProjBasic Sublogic EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods projBasicItems :: CASL_SL Sublogic -> EM_BASIC_ITEM -> (Maybe (BASIC_ITEMS EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA), [SORT]) Source #
Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Instance details Defined in ExtModal.Logic_ExtModal 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 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 #
Instance details Defined in Comorphisms.ExtModal2OWL 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 # isGTC :: ExtModal2OWL -> 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 #
Instance details Defined in Comorphisms.ExtModal2CASL 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 # isGTC :: ExtModal2CASL -> 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 #
Instance details Defined in Comorphisms.ExtModal2ExtModalTotal 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 # isGTC :: ExtModal2ExtModalTotal -> 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 #
Instance details Defined in Comorphisms.ExtModal2ExtModalNoSubsorts 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 # isGTC :: ExtModal2ExtModalNoSubsorts -> 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 #
Instance details Defined in Comorphisms.ExtModal2HasCASL 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 -> Symbol0 -> 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 # isGTC :: ExtModal2HasCASL -> Bool 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 #
Instance details Defined in Comorphisms.CASL2ExtModal 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 # isGTC :: CASL2ExtModal -> Bool Source #
type Rep Sublogic
Instance details Defined in ExtModal.ATC_ExtModal type Rep Sublogic = D1 ('MetaData "Sublogic" "ExtModal.Sublogic" "main" 'False) (C1 ('MetaCons "Sublogic" 'PrefixI 'True) ((S1 ('MetaSel ('Just "hasModalities") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Frequency) :: (S1 ('MetaSel ('Just "hasTermMods") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "hasTransClos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: ((S1 ('MetaSel ('Just "hasNominals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "hasTimeMods") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Frequency)) :: (S1 ('MetaSel ('Just "hasFixPoints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "hasFrameAxioms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))