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

Instances details

Eq FrameForm Source #
Instance details Defined in ExtModal.AS_ExtModal Methods (==) :: FrameForm -> FrameForm -> Bool (/=) :: FrameForm -> FrameForm -> Bool
Data FrameForm Source #
Instance details Defined in ExtModal.AS_ExtModal 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 :: forall r r'. (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 #
Instance details Defined in ExtModal.AS_ExtModal 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 #
Instance details Defined in ExtModal.AS_ExtModal Methods showsPrec :: Int -> FrameForm -> ShowS show :: FrameForm -> String showList :: [FrameForm] -> ShowS
Generic FrameForm
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep FrameForm :: Type -> Type Methods from :: FrameForm -> Rep FrameForm x to :: Rep FrameForm x -> FrameForm
GetRange FrameForm Source #
Instance details Defined in ExtModal.AS_ExtModal Methods getRange :: FrameForm -> Range Source # rangeSpan :: FrameForm -> [Pos] Source #
FromJSON FrameForm
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser FrameForm parseJSONList :: Value -> Parser [FrameForm]
ToJSON FrameForm
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: FrameForm -> Value toEncoding :: FrameForm -> Encoding toJSONList :: [FrameForm] -> Value toEncodingList :: [FrameForm] -> Encoding
ShATermConvertible FrameForm
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> FrameForm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FrameForm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FrameForm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FrameForm])
Pretty FrameForm Source #
Instance details Defined in ExtModal.Print_AS Methods pretty :: FrameForm -> Doc Source # pretties :: [FrameForm] -> Doc Source #
type Rep FrameForm
Instance details Defined in ExtModal.ATC_ExtModal type Rep FrameForm = D1 ('MetaData "FrameForm" "ExtModal.AS_ExtModal" "main" 'False) (C1 ('MetaCons "FrameForm" 'PrefixI 'True) (S1 ('MetaSel ('Just "frameVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_DECL]) :: (S1 ('MetaSel ('Just "frameForms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (FORMULA EM_FORMULA)]) :: S1 ('MetaSel ('Just "frameFormRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data ModDefn Source #

Constructors

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

Instances

Instances details

Eq ModDefn Source #
Instance details Defined in ExtModal.AS_ExtModal Methods (==) :: ModDefn -> ModDefn -> Bool (/=) :: ModDefn -> ModDefn -> Bool
Data ModDefn Source #
Instance details Defined in ExtModal.AS_ExtModal 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 :: forall r r'. (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 #
Instance details Defined in ExtModal.AS_ExtModal 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 #
Instance details Defined in ExtModal.AS_ExtModal Methods showsPrec :: Int -> ModDefn -> ShowS show :: ModDefn -> String showList :: [ModDefn] -> ShowS
Generic ModDefn
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep ModDefn :: Type -> Type Methods from :: ModDefn -> Rep ModDefn x to :: Rep ModDefn x -> ModDefn
GetRange ModDefn Source #
Instance details Defined in ExtModal.AS_ExtModal Methods getRange :: ModDefn -> Range Source # rangeSpan :: ModDefn -> [Pos] Source #
FromJSON ModDefn
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser ModDefn parseJSONList :: Value -> Parser [ModDefn]
ToJSON ModDefn
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: ModDefn -> Value toEncoding :: ModDefn -> Encoding toJSONList :: [ModDefn] -> Value toEncodingList :: [ModDefn] -> Encoding
ShATermConvertible ModDefn
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> ModDefn -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ModDefn] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ModDefn) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ModDefn])
Pretty ModDefn Source #
Instance details Defined in ExtModal.Print_AS Methods pretty :: ModDefn -> Doc Source # pretties :: [ModDefn] -> Doc Source #
type Rep ModDefn
Instance details Defined in ExtModal.ATC_ExtModal type Rep ModDefn = D1 ('MetaData "ModDefn" "ExtModal.AS_ExtModal" "main" 'False) (C1 ('MetaCons "ModDefn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted Id]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted FrameForm]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))

data EM_BASIC_ITEM Source #

Constructors

ModItem ModDefn
Nominal_decl [Annoted SIMPLE_ID] Range

Instances

Instances details

Data EM_BASIC_ITEM Source #
Instance details Defined in ExtModal.AS_ExtModal 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 :: forall r r'. (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 #
Instance details Defined in ExtModal.AS_ExtModal Methods showsPrec :: Int -> EM_BASIC_ITEM -> ShowS show :: EM_BASIC_ITEM -> String showList :: [EM_BASIC_ITEM] -> ShowS
Generic EM_BASIC_ITEM
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep EM_BASIC_ITEM :: Type -> Type Methods from :: EM_BASIC_ITEM -> Rep EM_BASIC_ITEM x to :: Rep EM_BASIC_ITEM x -> EM_BASIC_ITEM
GetRange EM_BASIC_ITEM Source #
Instance details Defined in ExtModal.AS_ExtModal Methods getRange :: EM_BASIC_ITEM -> Range Source # rangeSpan :: EM_BASIC_ITEM -> [Pos] Source #
FromJSON EM_BASIC_ITEM
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser EM_BASIC_ITEM parseJSONList :: Value -> Parser [EM_BASIC_ITEM]
ToJSON EM_BASIC_ITEM
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: EM_BASIC_ITEM -> Value toEncoding :: EM_BASIC_ITEM -> Encoding toJSONList :: [EM_BASIC_ITEM] -> Value toEncodingList :: [EM_BASIC_ITEM] -> Encoding
ShATermConvertible EM_BASIC_ITEM
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> EM_BASIC_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [EM_BASIC_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, EM_BASIC_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [EM_BASIC_ITEM])
Pretty EM_BASIC_ITEM Source #
Instance details Defined in ExtModal.Print_AS Methods pretty :: EM_BASIC_ITEM -> Doc Source # pretties :: [EM_BASIC_ITEM] -> Doc Source #
AParsable EM_BASIC_ITEM Source #
Instance details Defined in ExtModal.Parse_AS Methods aparser :: AParser st EM_BASIC_ITEM Source #
MinSL Sublogic EM_BASIC_ITEM Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods minSL :: EM_BASIC_ITEM -> CASL_SL Sublogic 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 #
Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in ExtModal.Logic_ExtModal 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 (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: ExtModal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: ExtModal -> Maybe (PrefixMap -> 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 #
Instance details Defined in ExtModal.Logic_ExtModal 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 #
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 EM_BASIC_ITEM
Instance details Defined in ExtModal.ATC_ExtModal type Rep EM_BASIC_ITEM = D1 ('MetaData "EM_BASIC_ITEM" "ExtModal.AS_ExtModal" "main" 'False) (C1 ('MetaCons "ModItem" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModDefn)) :+: C1 ('MetaCons "Nominal_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted SIMPLE_ID]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data ModOp Source #

Constructors

Composition
Intersection
Union
OrElse

Instances

Instances details

Eq ModOp Source #
Instance details Defined in ExtModal.AS_ExtModal Methods (==) :: ModOp -> ModOp -> Bool (/=) :: ModOp -> ModOp -> Bool
Data ModOp Source #
Instance details Defined in ExtModal.AS_ExtModal 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 :: forall r r'. (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 #
Instance details Defined in ExtModal.AS_ExtModal 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 #
Instance details Defined in ExtModal.AS_ExtModal Methods showsPrec :: Int -> ModOp -> ShowS show :: ModOp -> String showList :: [ModOp] -> ShowS
Generic ModOp
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep ModOp :: Type -> Type Methods from :: ModOp -> Rep ModOp x to :: Rep ModOp x -> ModOp
GetRange ModOp Source #
Instance details Defined in ExtModal.AS_ExtModal Methods getRange :: ModOp -> Range Source # rangeSpan :: ModOp -> [Pos] Source #
FromJSON ModOp
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser ModOp parseJSONList :: Value -> Parser [ModOp]
ToJSON ModOp
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: ModOp -> Value toEncoding :: ModOp -> Encoding toJSONList :: [ModOp] -> Value toEncodingList :: [ModOp] -> Encoding
ShATermConvertible ModOp
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> ModOp -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ModOp] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ModOp) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ModOp])
type Rep ModOp
Instance details Defined in ExtModal.ATC_ExtModal type Rep ModOp = D1 ('MetaData "ModOp" "ExtModal.AS_ExtModal" "main" 'False) ((C1 ('MetaCons "Composition" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Intersection" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Union" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OrElse" 'PrefixI 'False) (U1 :: Type -> Type)))

data MODALITY Source #

Constructors

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

Instances

Instances details

Eq MODALITY Source #
Instance details Defined in ExtModal.AS_ExtModal Methods (==) :: MODALITY -> MODALITY -> Bool (/=) :: MODALITY -> MODALITY -> Bool
Data MODALITY Source #
Instance details Defined in ExtModal.AS_ExtModal 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 :: forall r r'. (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 #
Instance details Defined in ExtModal.AS_ExtModal 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 #
Instance details Defined in ExtModal.AS_ExtModal Methods showsPrec :: Int -> MODALITY -> ShowS show :: MODALITY -> String showList :: [MODALITY] -> ShowS
Generic MODALITY
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep MODALITY :: Type -> Type Methods from :: MODALITY -> Rep MODALITY x to :: Rep MODALITY x -> MODALITY
GetRange MODALITY Source #
Instance details Defined in ExtModal.AS_ExtModal Methods getRange :: MODALITY -> Range Source # rangeSpan :: MODALITY -> [Pos] Source #
FromJSON MODALITY
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser MODALITY parseJSONList :: Value -> Parser [MODALITY]
ToJSON MODALITY
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: MODALITY -> Value toEncoding :: MODALITY -> Encoding toJSONList :: [MODALITY] -> Value toEncodingList :: [MODALITY] -> Encoding
ShATermConvertible MODALITY
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> MODALITY -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [MODALITY] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, MODALITY) fromShATermList' :: Int -> ATermTable -> (ATermTable, [MODALITY])
Pretty MODALITY Source #
Instance details Defined in ExtModal.Print_AS Methods pretty :: MODALITY -> Doc Source # pretties :: [MODALITY] -> Doc Source #
type Rep MODALITY
Instance details Defined in ExtModal.ATC_ExtModal type Rep MODALITY = D1 ('MetaData "MODALITY" "ExtModal.AS_ExtModal" "main" 'False) ((C1 ('MetaCons "SimpleMod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SIMPLE_ID)) :+: C1 ('MetaCons "TermMod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM EM_FORMULA)))) :+: (C1 ('MetaCons "ModOp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModOp) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MODALITY) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MODALITY))) :+: (C1 ('MetaCons "TransClos" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MODALITY)) :+: C1 ('MetaCons "Guard" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA EM_FORMULA))))))

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

Instances details

Data EM_SIG_ITEM Source #
Instance details Defined in ExtModal.AS_ExtModal 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 :: forall r r'. (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 #
Instance details Defined in ExtModal.AS_ExtModal Methods showsPrec :: Int -> EM_SIG_ITEM -> ShowS show :: EM_SIG_ITEM -> String showList :: [EM_SIG_ITEM] -> ShowS
Generic EM_SIG_ITEM
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep EM_SIG_ITEM :: Type -> Type Methods from :: EM_SIG_ITEM -> Rep EM_SIG_ITEM x to :: Rep EM_SIG_ITEM x -> EM_SIG_ITEM
GetRange EM_SIG_ITEM Source #
Instance details Defined in ExtModal.AS_ExtModal Methods getRange :: EM_SIG_ITEM -> Range Source # rangeSpan :: EM_SIG_ITEM -> [Pos] Source #
FromJSON EM_SIG_ITEM
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser EM_SIG_ITEM parseJSONList :: Value -> Parser [EM_SIG_ITEM]
ToJSON EM_SIG_ITEM
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: EM_SIG_ITEM -> Value toEncoding :: EM_SIG_ITEM -> Encoding toJSONList :: [EM_SIG_ITEM] -> Value toEncodingList :: [EM_SIG_ITEM] -> Encoding
ShATermConvertible EM_SIG_ITEM
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> EM_SIG_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [EM_SIG_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, EM_SIG_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [EM_SIG_ITEM])
Pretty EM_SIG_ITEM Source #
Instance details Defined in ExtModal.Print_AS Methods pretty :: EM_SIG_ITEM -> Doc Source # pretties :: [EM_SIG_ITEM] -> Doc Source #
AParsable EM_SIG_ITEM Source #
Instance details Defined in ExtModal.Parse_AS Methods aparser :: AParser st EM_SIG_ITEM Source #
MinSL Sublogic EM_SIG_ITEM Source #
Instance details Defined in ExtModal.Logic_ExtModal Methods minSL :: EM_SIG_ITEM -> 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 #
Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in ExtModal.Logic_ExtModal 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 (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: ExtModal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: ExtModal -> Maybe (PrefixMap -> 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 #
Instance details Defined in ExtModal.Logic_ExtModal 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 #
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 EM_SIG_ITEM
Instance details Defined in ExtModal.ATC_ExtModal type Rep EM_SIG_ITEM = D1 ('MetaData "EM_SIG_ITEM" "ExtModal.AS_ExtModal" "main" 'False) (C1 ('MetaCons "Rigid_op_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (OP_ITEM EM_FORMULA)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Rigid_pred_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (PRED_ITEM EM_FORMULA)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data BoxOp Source #

Constructors

Box
Diamond
EBox

Instances

Instances details

Eq BoxOp Source #
Instance details Defined in ExtModal.AS_ExtModal Methods (==) :: BoxOp -> BoxOp -> Bool (/=) :: BoxOp -> BoxOp -> Bool
Data BoxOp Source #
Instance details Defined in ExtModal.AS_ExtModal 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 :: forall r r'. (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 #
Instance details Defined in ExtModal.AS_ExtModal 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 #
Instance details Defined in ExtModal.AS_ExtModal Methods showsPrec :: Int -> BoxOp -> ShowS show :: BoxOp -> String showList :: [BoxOp] -> ShowS
Generic BoxOp
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep BoxOp :: Type -> Type Methods from :: BoxOp -> Rep BoxOp x to :: Rep BoxOp x -> BoxOp
GetRange BoxOp Source #
Instance details Defined in ExtModal.AS_ExtModal Methods getRange :: BoxOp -> Range Source # rangeSpan :: BoxOp -> [Pos] Source #
FromJSON BoxOp
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser BoxOp parseJSONList :: Value -> Parser [BoxOp]
ToJSON BoxOp
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: BoxOp -> Value toEncoding :: BoxOp -> Encoding toJSONList :: [BoxOp] -> Value toEncodingList :: [BoxOp] -> Encoding
ShATermConvertible BoxOp
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> BoxOp -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BoxOp] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BoxOp) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BoxOp])
type Rep BoxOp
Instance details Defined in ExtModal.ATC_ExtModal type Rep BoxOp = D1 ('MetaData "BoxOp" "ExtModal.AS_ExtModal" "main" 'False) (C1 ('MetaCons "Box" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Diamond" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EBox" 'PrefixI 'False) (U1 :: Type -> Type)))

data FormPrefix Source #

Constructors

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

Instances

Instances details

Eq FormPrefix Source #
Instance details Defined in ExtModal.AS_ExtModal Methods (==) :: FormPrefix -> FormPrefix -> Bool (/=) :: FormPrefix -> FormPrefix -> Bool
Data FormPrefix Source #
Instance details Defined in ExtModal.AS_ExtModal 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 :: forall r r'. (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 #
Instance details Defined in ExtModal.AS_ExtModal 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 #
Instance details Defined in ExtModal.AS_ExtModal Methods showsPrec :: Int -> FormPrefix -> ShowS show :: FormPrefix -> String showList :: [FormPrefix] -> ShowS
Generic FormPrefix
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep FormPrefix :: Type -> Type Methods from :: FormPrefix -> Rep FormPrefix x to :: Rep FormPrefix x -> FormPrefix
GetRange FormPrefix Source #
Instance details Defined in ExtModal.AS_ExtModal Methods getRange :: FormPrefix -> Range Source # rangeSpan :: FormPrefix -> [Pos] Source #
FromJSON FormPrefix
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser FormPrefix parseJSONList :: Value -> Parser [FormPrefix]
ToJSON FormPrefix
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: FormPrefix -> Value toEncoding :: FormPrefix -> Encoding toJSONList :: [FormPrefix] -> Value toEncodingList :: [FormPrefix] -> Encoding
ShATermConvertible FormPrefix
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> FormPrefix -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FormPrefix] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FormPrefix) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FormPrefix])
Pretty FormPrefix Source #
Instance details Defined in ExtModal.Print_AS Methods pretty :: FormPrefix -> Doc Source # pretties :: [FormPrefix] -> Doc Source #
type Rep FormPrefix
Instance details Defined in ExtModal.ATC_ExtModal type Rep FormPrefix = D1 ('MetaData "FormPrefix" "ExtModal.AS_ExtModal" "main" 'False) ((C1 ('MetaCons "BoxOrDiamond" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BoxOp) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MODALITY)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: (C1 ('MetaCons "Hybrid" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SIMPLE_ID)) :+: C1 ('MetaCons "PathQuantification" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: (C1 ('MetaCons "NextY" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: (C1 ('MetaCons "StateQuantification" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "FixedPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VAR)))))

data EM_FORMULA Source #

Constructors

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

Instances

Instances details

Eq EM_FORMULA Source #
Instance details Defined in ExtModal.AS_ExtModal Methods (==) :: EM_FORMULA -> EM_FORMULA -> Bool (/=) :: EM_FORMULA -> EM_FORMULA -> Bool
Data EM_FORMULA Source #
Instance details Defined in ExtModal.AS_ExtModal 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 :: forall r r'. (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 #
Instance details Defined in ExtModal.AS_ExtModal 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 #
Instance details Defined in ExtModal.AS_ExtModal Methods showsPrec :: Int -> EM_FORMULA -> ShowS show :: EM_FORMULA -> String showList :: [EM_FORMULA] -> ShowS
Generic EM_FORMULA
Instance details Defined in ExtModal.ATC_ExtModal Associated Types type Rep EM_FORMULA :: Type -> Type Methods from :: EM_FORMULA -> Rep EM_FORMULA x to :: Rep EM_FORMULA x -> EM_FORMULA
GetRange EM_FORMULA Source #
Instance details Defined in ExtModal.AS_ExtModal Methods getRange :: EM_FORMULA -> Range Source # rangeSpan :: EM_FORMULA -> [Pos] Source #
FromJSON EM_FORMULA
Instance details Defined in ExtModal.ATC_ExtModal Methods parseJSON :: Value -> Parser EM_FORMULA parseJSONList :: Value -> Parser [EM_FORMULA]
ToJSON EM_FORMULA
Instance details Defined in ExtModal.ATC_ExtModal Methods toJSON :: EM_FORMULA -> Value toEncoding :: EM_FORMULA -> Encoding toJSONList :: [EM_FORMULA] -> Value toEncodingList :: [EM_FORMULA] -> Encoding
ShATermConvertible EM_FORMULA
Instance details Defined in ExtModal.ATC_ExtModal Methods toShATermAux :: ATermTable -> EM_FORMULA -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [EM_FORMULA] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, EM_FORMULA) fromShATermList' :: Int -> ATermTable -> (ATermTable, [EM_FORMULA])
Pretty EM_FORMULA Source #
Instance details Defined in ExtModal.Print_AS Methods pretty :: EM_FORMULA -> Doc Source # pretties :: [EM_FORMULA] -> Doc Source #
FormExtension EM_FORMULA Source #
Instance details Defined in ExtModal.Print_AS Methods isQuantifierLike :: EM_FORMULA -> Bool Source # prefixExt :: EM_FORMULA -> Doc -> Doc Source #
TermExtension EM_FORMULA Source #
Instance details Defined in ExtModal.StatAna Methods freeVarsOfExt :: Sign EM_FORMULA e -> EM_FORMULA -> VarSet Source # optTermSort :: EM_FORMULA -> Maybe SORT Source # sortOfTerm :: EM_FORMULA -> SORT Source # termToFormula :: TERM EM_FORMULA -> Result (FORMULA EM_FORMULA) Source #
TermParser EM_FORMULA Source #
Instance details Defined in ExtModal.Parse_AS Methods termParser :: Bool -> AParser st EM_FORMULA 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 #
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 #
Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol Source #
Instance details Defined in ExtModal.Logic_ExtModal 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 #
Instance details Defined in ExtModal.Logic_ExtModal 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 (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: ExtModal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: ExtModal -> Maybe (PrefixMap -> 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 #
Instance details Defined in ExtModal.Logic_ExtModal 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 #
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 EM_FORMULA
Instance details Defined in ExtModal.ATC_ExtModal type Rep EM_FORMULA = D1 ('MetaData "EM_FORMULA" "ExtModal.AS_ExtModal" "main" 'False) (C1 ('MetaCons "PrefixForm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FormPrefix) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA EM_FORMULA)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "UntilSince" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA EM_FORMULA))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA EM_FORMULA)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "ModForm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModDefn))))