Copyright	(c) T.Mossakowski W.Herding C.Maeder Uni Bremen 2004-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	till@informatik.uni-bremen.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

Modal.AS_Modal

Description

Abstract syntax for modal logic extension of CASL Only the added syntax is specified

Documentation

type M_BASIC_SPEC = BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA Source #

type AnModFORM = Annoted (FORMULA M_FORMULA) Source #

data M_BASIC_ITEM Source #

Constructors

Simple_mod_decl [Annoted SIMPLE_ID] [AnModFORM] Range
Term_mod_decl [Annoted SORT] [AnModFORM] Range

Instances

Instances details

Data M_BASIC_ITEM Source #
Instance details Defined in Modal.AS_Modal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> M_BASIC_ITEM -> c M_BASIC_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c M_BASIC_ITEM toConstr :: M_BASIC_ITEM -> Constr dataTypeOf :: M_BASIC_ITEM -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c M_BASIC_ITEM) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M_BASIC_ITEM) gmapT :: (forall b. Data b => b -> b) -> M_BASIC_ITEM -> M_BASIC_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M_BASIC_ITEM -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M_BASIC_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> M_BASIC_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> M_BASIC_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM
Show M_BASIC_ITEM Source #
Instance details Defined in Modal.AS_Modal Methods showsPrec :: Int -> M_BASIC_ITEM -> ShowS show :: M_BASIC_ITEM -> String showList :: [M_BASIC_ITEM] -> ShowS
Generic M_BASIC_ITEM
Instance details Defined in Modal.ATC_Modal Associated Types type Rep M_BASIC_ITEM :: Type -> Type Methods from :: M_BASIC_ITEM -> Rep M_BASIC_ITEM x to :: Rep M_BASIC_ITEM x -> M_BASIC_ITEM
GetRange M_BASIC_ITEM Source #
Instance details Defined in Modal.AS_Modal Methods getRange :: M_BASIC_ITEM -> Range Source # rangeSpan :: M_BASIC_ITEM -> [Pos] Source #
FromJSON M_BASIC_ITEM
Instance details Defined in Modal.ATC_Modal Methods parseJSON :: Value -> Parser M_BASIC_ITEM parseJSONList :: Value -> Parser [M_BASIC_ITEM]
ToJSON M_BASIC_ITEM
Instance details Defined in Modal.ATC_Modal Methods toJSON :: M_BASIC_ITEM -> Value toEncoding :: M_BASIC_ITEM -> Encoding toJSONList :: [M_BASIC_ITEM] -> Value toEncodingList :: [M_BASIC_ITEM] -> Encoding
ShATermConvertible M_BASIC_ITEM
Instance details Defined in Modal.ATC_Modal Methods toShATermAux :: ATermTable -> M_BASIC_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [M_BASIC_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, M_BASIC_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [M_BASIC_ITEM])
Pretty M_BASIC_ITEM Source #
Instance details Defined in Modal.Print_AS Methods pretty :: M_BASIC_ITEM -> Doc Source # pretties :: [M_BASIC_ITEM] -> Doc Source #
AParsable M_BASIC_ITEM Source #
Instance details Defined in Modal.Parse_AS Methods aparser :: AParser st M_BASIC_ITEM Source #
Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in Modal.Logic_Modal Methods parsersAndPrinters :: Modal -> Map String (PrefixMap -> AParser st M_BASIC_SPEC, M_BASIC_SPEC -> Doc) Source # parse_basic_spec :: Modal -> Maybe (PrefixMap -> AParser st M_BASIC_SPEC) Source # parseSingleSymbItem :: Modal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Modal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Modal -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Modal -> M_BASIC_SPEC -> Item Source # symb_items_name :: Modal -> SYMB_ITEMS -> [String] Source #
StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source #
Instance details Defined in Modal.Logic_Modal Methods basic_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, GlobalAnnos) -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA])) Source # sen_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, ModalFORMULA) -> Result ModalFORMULA) Source # extBasicAnalysis :: Modal -> IRI -> LibName -> M_BASIC_SPEC -> MSign -> GlobalAnnos -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA]) Source # stat_symb_map_items :: Modal -> MSign -> Maybe MSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Modal -> MSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Modal -> Maybe ((MSign, [Named ModalFORMULA]) -> M_BASIC_SPEC) Source # ensures_amalgamability :: Modal -> ([CASLAmalgOpt], Gr MSign (Int, ModalMor), [(Int, ModalMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Modal -> ModalMor -> [Named ModalFORMULA] -> Result (MSign, [Named ModalFORMULA]) Source # signature_colimit :: Modal -> Gr MSign (Int, ModalMor) -> Result (MSign, Map Int ModalMor) Source # qualify :: Modal -> SIMPLE_ID -> LibName -> ModalMor -> MSign -> Result (ModalMor, [Named ModalFORMULA]) Source # symbol_to_raw :: Modal -> Symbol -> RawSymbol Source # id_to_raw :: Modal -> Id -> RawSymbol Source # matches :: Modal -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Modal -> MSign Source # add_symb_to_sign :: Modal -> MSign -> Symbol -> Result MSign Source # signature_union :: Modal -> MSign -> MSign -> Result MSign Source # signatureDiff :: Modal -> MSign -> MSign -> Result MSign Source # intersection :: Modal -> MSign -> MSign -> Result MSign Source # final_union :: Modal -> MSign -> MSign -> Result MSign Source # morphism_union :: Modal -> ModalMor -> ModalMor -> Result ModalMor Source # is_subsig :: Modal -> MSign -> MSign -> Bool Source # subsig_inclusion :: Modal -> MSign -> MSign -> Result ModalMor Source # generated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source # cogenerated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source # induced_from_morphism :: Modal -> EndoMap RawSymbol -> MSign -> Result ModalMor Source # induced_from_to_morphism :: Modal -> EndoMap RawSymbol -> ExtSign MSign Symbol -> ExtSign MSign Symbol -> Result ModalMor Source # is_transportable :: Modal -> ModalMor -> Bool Source # is_injective :: Modal -> ModalMor -> Bool Source # theory_to_taxonomy :: Modal -> TaxoGraphKind -> MMiSSOntology -> MSign -> [Named ModalFORMULA] -> Result MMiSSOntology Source # corresp2th :: Modal -> String -> Bool -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (MSign, [Named ModalFORMULA], MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Modal -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (MSign, MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Modal -> [IRI] -> (MSign, [Named ModalFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #
Logic Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Modal.Logic_Modal Methods parse_basic_sen :: Modal -> Maybe (M_BASIC_SPEC -> AParser st ModalFORMULA) Source # stability :: Modal -> Stability Source # data_logic :: Modal -> Maybe AnyLogic Source # top_sublogic :: Modal -> () Source # all_sublogics :: Modal -> [()] Source # bottomSublogic :: Modal -> Maybe () Source # sublogicDimensions :: Modal -> [[()]] Source # parseSublogic :: Modal -> String -> Maybe () Source # proj_sublogic_epsilon :: Modal -> () -> MSign -> ModalMor Source # provers :: Modal -> [Prover MSign ModalFORMULA ModalMor () ()] Source # default_prover :: Modal -> String Source # cons_checkers :: Modal -> [ConsChecker MSign ModalFORMULA () ModalMor ()] Source # conservativityCheck :: Modal -> [ConservativityChecker MSign ModalFORMULA ModalMor] Source # empty_proof_tree :: Modal -> () Source # syntaxTable :: Modal -> MSign -> Maybe SyntaxTable Source # omdoc_metatheory :: Modal -> Maybe OMCD Source # export_symToOmdoc :: Modal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Modal -> NameMap Symbol -> ModalFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: Modal -> SigMap Symbol -> MSign -> [Named ModalFORMULA] -> Result [TCElement] Source # omdocToSym :: Modal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Modal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ModalFORMULA)) Source # addOMadtToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [[OmdADT]] -> Result (MSign, [Named ModalFORMULA]) Source # addOmdocToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [TCElement] -> Result (MSign, [Named ModalFORMULA]) Source # sublogicOfTheo :: Modal -> (MSign, [ModalFORMULA]) -> () Source #
Comorphism Modal2CASL Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Modal2CASL Methods sourceLogic :: Modal2CASL -> Modal Source # sourceSublogic :: Modal2CASL -> () Source # sourceSublogicLossy :: Modal2CASL -> () Source # minSourceTheory :: Modal2CASL -> Maybe (LibName, String) Source # targetLogic :: Modal2CASL -> CASL Source # mapSublogic :: Modal2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Modal2CASL -> ModalMor -> Result CASLMor Source # map_sentence :: Modal2CASL -> MSign -> ModalFORMULA -> Result CASLFORMULA Source # map_symbol :: Modal2CASL -> MSign -> Symbol -> Set Symbol Source # extractModel :: Modal2CASL -> MSign -> ProofTree -> Result (MSign, [Named ModalFORMULA]) Source # is_model_transportable :: Modal2CASL -> Bool Source # has_model_expansion :: Modal2CASL -> Bool Source # is_weakly_amalgamable :: Modal2CASL -> Bool Source # constituents :: Modal2CASL -> [String] Source # isInclusionComorphism :: Modal2CASL -> Bool Source # rps :: Modal2CASL -> Bool Source # eps :: Modal2CASL -> Bool Source # isGTC :: Modal2CASL -> Bool Source #
Comorphism CspCASL2Modal CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CspCASL2Modal Methods sourceLogic :: CspCASL2Modal -> CspCASL Source # sourceSublogic :: CspCASL2Modal -> () Source # sourceSublogicLossy :: CspCASL2Modal -> () Source # minSourceTheory :: CspCASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CspCASL2Modal -> Modal Source # mapSublogic :: CspCASL2Modal -> () -> Maybe () Source # map_theory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CspCASL2Modal -> CspCASLMorphism -> Result ModalMor Source # map_sentence :: CspCASL2Modal -> CspCASLSign -> CspCASLSen -> Result ModalFORMULA Source # map_symbol :: CspCASL2Modal -> CspCASLSign -> CspSymbol -> Set Symbol Source # extractModel :: CspCASL2Modal -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2Modal -> Bool Source # has_model_expansion :: CspCASL2Modal -> Bool Source # is_weakly_amalgamable :: CspCASL2Modal -> Bool Source # constituents :: CspCASL2Modal -> [String] Source # isInclusionComorphism :: CspCASL2Modal -> Bool Source # rps :: CspCASL2Modal -> Bool Source # eps :: CspCASL2Modal -> Bool Source # isGTC :: CspCASL2Modal -> Bool Source #
Comorphism CASL2Modal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2Modal Methods sourceLogic :: CASL2Modal -> CASL Source # sourceSublogic :: CASL2Modal -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Modal -> CASL_Sublogics Source # minSourceTheory :: CASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CASL2Modal -> Modal Source # mapSublogic :: CASL2Modal -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CASL2Modal -> CASLMor -> Result ModalMor Source # map_sentence :: CASL2Modal -> CASLSign -> CASLFORMULA -> Result ModalFORMULA Source # map_symbol :: CASL2Modal -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Modal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Modal -> Bool Source # has_model_expansion :: CASL2Modal -> Bool Source # is_weakly_amalgamable :: CASL2Modal -> Bool Source # constituents :: CASL2Modal -> [String] Source # isInclusionComorphism :: CASL2Modal -> Bool Source # rps :: CASL2Modal -> Bool Source # eps :: CASL2Modal -> Bool Source # isGTC :: CASL2Modal -> Bool Source #
type Rep M_BASIC_ITEM
Instance details Defined in Modal.ATC_Modal type Rep M_BASIC_ITEM = D1 ('MetaData "M_BASIC_ITEM" "Modal.AS_Modal" "main" 'False) (C1 ('MetaCons "Simple_mod_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted SIMPLE_ID]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AnModFORM]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Term_mod_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted SORT]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AnModFORM]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data RIGOR Source #

Constructors

Rigid
Flexible

Instances

Instances details

Data RIGOR Source #
Instance details Defined in Modal.AS_Modal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RIGOR -> c RIGOR gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RIGOR toConstr :: RIGOR -> Constr dataTypeOf :: RIGOR -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RIGOR) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RIGOR) gmapT :: (forall b. Data b => b -> b) -> RIGOR -> RIGOR gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RIGOR -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RIGOR -> r gmapQ :: (forall d. Data d => d -> u) -> RIGOR -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RIGOR -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RIGOR -> m RIGOR gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RIGOR -> m RIGOR gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RIGOR -> m RIGOR
Show RIGOR Source #
Instance details Defined in Modal.AS_Modal Methods showsPrec :: Int -> RIGOR -> ShowS show :: RIGOR -> String showList :: [RIGOR] -> ShowS
Generic RIGOR
Instance details Defined in Modal.ATC_Modal Associated Types type Rep RIGOR :: Type -> Type Methods from :: RIGOR -> Rep RIGOR x to :: Rep RIGOR x -> RIGOR
GetRange RIGOR Source #
Instance details Defined in Modal.AS_Modal Methods getRange :: RIGOR -> Range Source # rangeSpan :: RIGOR -> [Pos] Source #
FromJSON RIGOR
Instance details Defined in Modal.ATC_Modal Methods parseJSON :: Value -> Parser RIGOR parseJSONList :: Value -> Parser [RIGOR]
ToJSON RIGOR
Instance details Defined in Modal.ATC_Modal Methods toJSON :: RIGOR -> Value toEncoding :: RIGOR -> Encoding toJSONList :: [RIGOR] -> Value toEncodingList :: [RIGOR] -> Encoding
ShATermConvertible RIGOR
Instance details Defined in Modal.ATC_Modal Methods toShATermAux :: ATermTable -> RIGOR -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RIGOR] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RIGOR) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RIGOR])
Pretty RIGOR Source #
Instance details Defined in Modal.Print_AS Methods pretty :: RIGOR -> Doc Source # pretties :: [RIGOR] -> Doc Source #
type Rep RIGOR
Instance details Defined in Modal.ATC_Modal type Rep RIGOR = D1 ('MetaData "RIGOR" "Modal.AS_Modal" "main" 'False) (C1 ('MetaCons "Rigid" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Flexible" 'PrefixI 'False) (U1 :: Type -> Type))

data M_SIG_ITEM Source #

Constructors

Rigid_op_items RIGOR [Annoted (OP_ITEM M_FORMULA)] Range
Rigid_pred_items RIGOR [Annoted (PRED_ITEM M_FORMULA)] Range

Instances

Instances details

Data M_SIG_ITEM Source #
Instance details Defined in Modal.AS_Modal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> M_SIG_ITEM -> c M_SIG_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c M_SIG_ITEM toConstr :: M_SIG_ITEM -> Constr dataTypeOf :: M_SIG_ITEM -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c M_SIG_ITEM) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M_SIG_ITEM) gmapT :: (forall b. Data b => b -> b) -> M_SIG_ITEM -> M_SIG_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M_SIG_ITEM -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M_SIG_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> M_SIG_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> M_SIG_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM
Show M_SIG_ITEM Source #
Instance details Defined in Modal.AS_Modal Methods showsPrec :: Int -> M_SIG_ITEM -> ShowS show :: M_SIG_ITEM -> String showList :: [M_SIG_ITEM] -> ShowS
Generic M_SIG_ITEM
Instance details Defined in Modal.ATC_Modal Associated Types type Rep M_SIG_ITEM :: Type -> Type Methods from :: M_SIG_ITEM -> Rep M_SIG_ITEM x to :: Rep M_SIG_ITEM x -> M_SIG_ITEM
GetRange M_SIG_ITEM Source #
Instance details Defined in Modal.AS_Modal Methods getRange :: M_SIG_ITEM -> Range Source # rangeSpan :: M_SIG_ITEM -> [Pos] Source #
FromJSON M_SIG_ITEM
Instance details Defined in Modal.ATC_Modal Methods parseJSON :: Value -> Parser M_SIG_ITEM parseJSONList :: Value -> Parser [M_SIG_ITEM]
ToJSON M_SIG_ITEM
Instance details Defined in Modal.ATC_Modal Methods toJSON :: M_SIG_ITEM -> Value toEncoding :: M_SIG_ITEM -> Encoding toJSONList :: [M_SIG_ITEM] -> Value toEncodingList :: [M_SIG_ITEM] -> Encoding
ShATermConvertible M_SIG_ITEM
Instance details Defined in Modal.ATC_Modal Methods toShATermAux :: ATermTable -> M_SIG_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [M_SIG_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, M_SIG_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [M_SIG_ITEM])
Pretty M_SIG_ITEM Source #
Instance details Defined in Modal.Print_AS Methods pretty :: M_SIG_ITEM -> Doc Source # pretties :: [M_SIG_ITEM] -> Doc Source #
AParsable M_SIG_ITEM Source #
Instance details Defined in Modal.Parse_AS Methods aparser :: AParser st M_SIG_ITEM Source #
Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in Modal.Logic_Modal Methods parsersAndPrinters :: Modal -> Map String (PrefixMap -> AParser st M_BASIC_SPEC, M_BASIC_SPEC -> Doc) Source # parse_basic_spec :: Modal -> Maybe (PrefixMap -> AParser st M_BASIC_SPEC) Source # parseSingleSymbItem :: Modal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Modal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Modal -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Modal -> M_BASIC_SPEC -> Item Source # symb_items_name :: Modal -> SYMB_ITEMS -> [String] Source #
StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source #
Instance details Defined in Modal.Logic_Modal Methods basic_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, GlobalAnnos) -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA])) Source # sen_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, ModalFORMULA) -> Result ModalFORMULA) Source # extBasicAnalysis :: Modal -> IRI -> LibName -> M_BASIC_SPEC -> MSign -> GlobalAnnos -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA]) Source # stat_symb_map_items :: Modal -> MSign -> Maybe MSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Modal -> MSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Modal -> Maybe ((MSign, [Named ModalFORMULA]) -> M_BASIC_SPEC) Source # ensures_amalgamability :: Modal -> ([CASLAmalgOpt], Gr MSign (Int, ModalMor), [(Int, ModalMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Modal -> ModalMor -> [Named ModalFORMULA] -> Result (MSign, [Named ModalFORMULA]) Source # signature_colimit :: Modal -> Gr MSign (Int, ModalMor) -> Result (MSign, Map Int ModalMor) Source # qualify :: Modal -> SIMPLE_ID -> LibName -> ModalMor -> MSign -> Result (ModalMor, [Named ModalFORMULA]) Source # symbol_to_raw :: Modal -> Symbol -> RawSymbol Source # id_to_raw :: Modal -> Id -> RawSymbol Source # matches :: Modal -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Modal -> MSign Source # add_symb_to_sign :: Modal -> MSign -> Symbol -> Result MSign Source # signature_union :: Modal -> MSign -> MSign -> Result MSign Source # signatureDiff :: Modal -> MSign -> MSign -> Result MSign Source # intersection :: Modal -> MSign -> MSign -> Result MSign Source # final_union :: Modal -> MSign -> MSign -> Result MSign Source # morphism_union :: Modal -> ModalMor -> ModalMor -> Result ModalMor Source # is_subsig :: Modal -> MSign -> MSign -> Bool Source # subsig_inclusion :: Modal -> MSign -> MSign -> Result ModalMor Source # generated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source # cogenerated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source # induced_from_morphism :: Modal -> EndoMap RawSymbol -> MSign -> Result ModalMor Source # induced_from_to_morphism :: Modal -> EndoMap RawSymbol -> ExtSign MSign Symbol -> ExtSign MSign Symbol -> Result ModalMor Source # is_transportable :: Modal -> ModalMor -> Bool Source # is_injective :: Modal -> ModalMor -> Bool Source # theory_to_taxonomy :: Modal -> TaxoGraphKind -> MMiSSOntology -> MSign -> [Named ModalFORMULA] -> Result MMiSSOntology Source # corresp2th :: Modal -> String -> Bool -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (MSign, [Named ModalFORMULA], MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Modal -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (MSign, MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Modal -> [IRI] -> (MSign, [Named ModalFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #
Logic Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Modal.Logic_Modal Methods parse_basic_sen :: Modal -> Maybe (M_BASIC_SPEC -> AParser st ModalFORMULA) Source # stability :: Modal -> Stability Source # data_logic :: Modal -> Maybe AnyLogic Source # top_sublogic :: Modal -> () Source # all_sublogics :: Modal -> [()] Source # bottomSublogic :: Modal -> Maybe () Source # sublogicDimensions :: Modal -> [[()]] Source # parseSublogic :: Modal -> String -> Maybe () Source # proj_sublogic_epsilon :: Modal -> () -> MSign -> ModalMor Source # provers :: Modal -> [Prover MSign ModalFORMULA ModalMor () ()] Source # default_prover :: Modal -> String Source # cons_checkers :: Modal -> [ConsChecker MSign ModalFORMULA () ModalMor ()] Source # conservativityCheck :: Modal -> [ConservativityChecker MSign ModalFORMULA ModalMor] Source # empty_proof_tree :: Modal -> () Source # syntaxTable :: Modal -> MSign -> Maybe SyntaxTable Source # omdoc_metatheory :: Modal -> Maybe OMCD Source # export_symToOmdoc :: Modal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Modal -> NameMap Symbol -> ModalFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: Modal -> SigMap Symbol -> MSign -> [Named ModalFORMULA] -> Result [TCElement] Source # omdocToSym :: Modal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Modal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ModalFORMULA)) Source # addOMadtToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [[OmdADT]] -> Result (MSign, [Named ModalFORMULA]) Source # addOmdocToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [TCElement] -> Result (MSign, [Named ModalFORMULA]) Source # sublogicOfTheo :: Modal -> (MSign, [ModalFORMULA]) -> () Source #
Comorphism Modal2CASL Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Modal2CASL Methods sourceLogic :: Modal2CASL -> Modal Source # sourceSublogic :: Modal2CASL -> () Source # sourceSublogicLossy :: Modal2CASL -> () Source # minSourceTheory :: Modal2CASL -> Maybe (LibName, String) Source # targetLogic :: Modal2CASL -> CASL Source # mapSublogic :: Modal2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Modal2CASL -> ModalMor -> Result CASLMor Source # map_sentence :: Modal2CASL -> MSign -> ModalFORMULA -> Result CASLFORMULA Source # map_symbol :: Modal2CASL -> MSign -> Symbol -> Set Symbol Source # extractModel :: Modal2CASL -> MSign -> ProofTree -> Result (MSign, [Named ModalFORMULA]) Source # is_model_transportable :: Modal2CASL -> Bool Source # has_model_expansion :: Modal2CASL -> Bool Source # is_weakly_amalgamable :: Modal2CASL -> Bool Source # constituents :: Modal2CASL -> [String] Source # isInclusionComorphism :: Modal2CASL -> Bool Source # rps :: Modal2CASL -> Bool Source # eps :: Modal2CASL -> Bool Source # isGTC :: Modal2CASL -> Bool Source #
Comorphism CspCASL2Modal CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CspCASL2Modal Methods sourceLogic :: CspCASL2Modal -> CspCASL Source # sourceSublogic :: CspCASL2Modal -> () Source # sourceSublogicLossy :: CspCASL2Modal -> () Source # minSourceTheory :: CspCASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CspCASL2Modal -> Modal Source # mapSublogic :: CspCASL2Modal -> () -> Maybe () Source # map_theory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CspCASL2Modal -> CspCASLMorphism -> Result ModalMor Source # map_sentence :: CspCASL2Modal -> CspCASLSign -> CspCASLSen -> Result ModalFORMULA Source # map_symbol :: CspCASL2Modal -> CspCASLSign -> CspSymbol -> Set Symbol Source # extractModel :: CspCASL2Modal -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2Modal -> Bool Source # has_model_expansion :: CspCASL2Modal -> Bool Source # is_weakly_amalgamable :: CspCASL2Modal -> Bool Source # constituents :: CspCASL2Modal -> [String] Source # isInclusionComorphism :: CspCASL2Modal -> Bool Source # rps :: CspCASL2Modal -> Bool Source # eps :: CspCASL2Modal -> Bool Source # isGTC :: CspCASL2Modal -> Bool Source #
Comorphism CASL2Modal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2Modal Methods sourceLogic :: CASL2Modal -> CASL Source # sourceSublogic :: CASL2Modal -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Modal -> CASL_Sublogics Source # minSourceTheory :: CASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CASL2Modal -> Modal Source # mapSublogic :: CASL2Modal -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CASL2Modal -> CASLMor -> Result ModalMor Source # map_sentence :: CASL2Modal -> CASLSign -> CASLFORMULA -> Result ModalFORMULA Source # map_symbol :: CASL2Modal -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Modal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Modal -> Bool Source # has_model_expansion :: CASL2Modal -> Bool Source # is_weakly_amalgamable :: CASL2Modal -> Bool Source # constituents :: CASL2Modal -> [String] Source # isInclusionComorphism :: CASL2Modal -> Bool Source # rps :: CASL2Modal -> Bool Source # eps :: CASL2Modal -> Bool Source # isGTC :: CASL2Modal -> Bool Source #
type Rep M_SIG_ITEM
Instance details Defined in Modal.ATC_Modal type Rep M_SIG_ITEM = D1 ('MetaData "M_SIG_ITEM" "Modal.AS_Modal" "main" 'False) (C1 ('MetaCons "Rigid_op_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RIGOR) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (OP_ITEM M_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 RIGOR) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (PRED_ITEM M_FORMULA)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data MODALITY Source #

Constructors

Simple_mod SIMPLE_ID
Term_mod (TERM M_FORMULA)

Instances

Instances details

Eq MODALITY Source #
Instance details Defined in Modal.AS_Modal Methods (==) :: MODALITY -> MODALITY -> Bool (/=) :: MODALITY -> MODALITY -> Bool
Data MODALITY Source #
Instance details Defined in Modal.AS_Modal 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 Modal.AS_Modal 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 Modal.AS_Modal Methods showsPrec :: Int -> MODALITY -> ShowS show :: MODALITY -> String showList :: [MODALITY] -> ShowS
Generic MODALITY
Instance details Defined in Modal.ATC_Modal 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 Modal.AS_Modal Methods getRange :: MODALITY -> Range Source # rangeSpan :: MODALITY -> [Pos] Source #
FromJSON MODALITY
Instance details Defined in Modal.ATC_Modal Methods parseJSON :: Value -> Parser MODALITY parseJSONList :: Value -> Parser [MODALITY]
ToJSON MODALITY
Instance details Defined in Modal.ATC_Modal Methods toJSON :: MODALITY -> Value toEncoding :: MODALITY -> Encoding toJSONList :: [MODALITY] -> Value toEncodingList :: [MODALITY] -> Encoding
ShATermConvertible MODALITY
Instance details Defined in Modal.ATC_Modal 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 Modal.Print_AS Methods pretty :: MODALITY -> Doc Source # pretties :: [MODALITY] -> Doc Source #
type Rep MODALITY
Instance details Defined in Modal.ATC_Modal type Rep MODALITY = D1 ('MetaData "MODALITY" "Modal.AS_Modal" "main" 'False) (C1 ('MetaCons "Simple_mod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SIMPLE_ID)) :+: C1 ('MetaCons "Term_mod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM M_FORMULA))))

data M_FORMULA Source #

Constructors

BoxOrDiamond Bool MODALITY (FORMULA M_FORMULA) Range

Instances

Instances details

Eq M_FORMULA Source #
Instance details Defined in Modal.AS_Modal Methods (==) :: M_FORMULA -> M_FORMULA -> Bool (/=) :: M_FORMULA -> M_FORMULA -> Bool
Data M_FORMULA Source #
Instance details Defined in Modal.AS_Modal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> M_FORMULA -> c M_FORMULA gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c M_FORMULA toConstr :: M_FORMULA -> Constr dataTypeOf :: M_FORMULA -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c M_FORMULA) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M_FORMULA) gmapT :: (forall b. Data b => b -> b) -> M_FORMULA -> M_FORMULA gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M_FORMULA -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M_FORMULA -> r gmapQ :: (forall d. Data d => d -> u) -> M_FORMULA -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> M_FORMULA -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA
Ord M_FORMULA Source #
Instance details Defined in Modal.AS_Modal Methods compare :: M_FORMULA -> M_FORMULA -> Ordering (<) :: M_FORMULA -> M_FORMULA -> Bool (<=) :: M_FORMULA -> M_FORMULA -> Bool (>) :: M_FORMULA -> M_FORMULA -> Bool (>=) :: M_FORMULA -> M_FORMULA -> Bool max :: M_FORMULA -> M_FORMULA -> M_FORMULA min :: M_FORMULA -> M_FORMULA -> M_FORMULA
Show M_FORMULA Source #
Instance details Defined in Modal.AS_Modal Methods showsPrec :: Int -> M_FORMULA -> ShowS show :: M_FORMULA -> String showList :: [M_FORMULA] -> ShowS
Generic M_FORMULA
Instance details Defined in Modal.ATC_Modal Associated Types type Rep M_FORMULA :: Type -> Type Methods from :: M_FORMULA -> Rep M_FORMULA x to :: Rep M_FORMULA x -> M_FORMULA
GetRange M_FORMULA Source #
Instance details Defined in Modal.AS_Modal Methods getRange :: M_FORMULA -> Range Source # rangeSpan :: M_FORMULA -> [Pos] Source #
FromJSON M_FORMULA
Instance details Defined in Modal.ATC_Modal Methods parseJSON :: Value -> Parser M_FORMULA parseJSONList :: Value -> Parser [M_FORMULA]
ToJSON M_FORMULA
Instance details Defined in Modal.ATC_Modal Methods toJSON :: M_FORMULA -> Value toEncoding :: M_FORMULA -> Encoding toJSONList :: [M_FORMULA] -> Value toEncodingList :: [M_FORMULA] -> Encoding
ShATermConvertible M_FORMULA
Instance details Defined in Modal.ATC_Modal Methods toShATermAux :: ATermTable -> M_FORMULA -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [M_FORMULA] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, M_FORMULA) fromShATermList' :: Int -> ATermTable -> (ATermTable, [M_FORMULA])
Pretty M_FORMULA Source #
Instance details Defined in Modal.Print_AS Methods pretty :: M_FORMULA -> Doc Source # pretties :: [M_FORMULA] -> Doc Source #
FormExtension M_FORMULA Source #
Instance details Defined in Modal.Print_AS Methods isQuantifierLike :: M_FORMULA -> Bool Source # prefixExt :: M_FORMULA -> Doc -> Doc Source #
TermExtension M_FORMULA Source #
Instance details Defined in Modal.StatAna Methods freeVarsOfExt :: Sign M_FORMULA e -> M_FORMULA -> VarSet Source # optTermSort :: M_FORMULA -> Maybe SORT Source # sortOfTerm :: M_FORMULA -> SORT Source # termToFormula :: TERM M_FORMULA -> Result (FORMULA M_FORMULA) Source #
TermParser M_FORMULA Source #
Instance details Defined in Modal.Parse_AS Methods termParser :: Bool -> AParser st M_FORMULA Source #
Sentences Modal ModalFORMULA MSign ModalMor Symbol Source #
Instance details Defined in Modal.Logic_Modal Methods map_sen :: Modal -> ModalMor -> ModalFORMULA -> Result ModalFORMULA Source # simplify_sen :: Modal -> MSign -> ModalFORMULA -> ModalFORMULA Source # negation :: Modal -> ModalFORMULA -> Maybe ModalFORMULA Source # print_sign :: Modal -> MSign -> Doc Source # print_named :: Modal -> Named ModalFORMULA -> Doc Source # sym_of :: Modal -> MSign -> [Set Symbol] Source # mostSymsOf :: Modal -> MSign -> [Symbol] Source # symmap_of :: Modal -> ModalMor -> EndoMap Symbol Source # sym_name :: Modal -> Symbol -> Id Source # sym_label :: Modal -> Symbol -> Maybe String Source # fullSymName :: Modal -> Symbol -> String Source # symKind :: Modal -> Symbol -> String Source # symsOfSen :: Modal -> MSign -> ModalFORMULA -> [Symbol] Source # pair_symbols :: Modal -> Symbol -> Symbol -> Result Symbol Source #
Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in Modal.Logic_Modal Methods parsersAndPrinters :: Modal -> Map String (PrefixMap -> AParser st M_BASIC_SPEC, M_BASIC_SPEC -> Doc) Source # parse_basic_spec :: Modal -> Maybe (PrefixMap -> AParser st M_BASIC_SPEC) Source # parseSingleSymbItem :: Modal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Modal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Modal -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Modal -> M_BASIC_SPEC -> Item Source # symb_items_name :: Modal -> SYMB_ITEMS -> [String] Source #
StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source #
Instance details Defined in Modal.Logic_Modal Methods basic_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, GlobalAnnos) -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA])) Source # sen_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, ModalFORMULA) -> Result ModalFORMULA) Source # extBasicAnalysis :: Modal -> IRI -> LibName -> M_BASIC_SPEC -> MSign -> GlobalAnnos -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA]) Source # stat_symb_map_items :: Modal -> MSign -> Maybe MSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Modal -> MSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Modal -> Maybe ((MSign, [Named ModalFORMULA]) -> M_BASIC_SPEC) Source # ensures_amalgamability :: Modal -> ([CASLAmalgOpt], Gr MSign (Int, ModalMor), [(Int, ModalMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Modal -> ModalMor -> [Named ModalFORMULA] -> Result (MSign, [Named ModalFORMULA]) Source # signature_colimit :: Modal -> Gr MSign (Int, ModalMor) -> Result (MSign, Map Int ModalMor) Source # qualify :: Modal -> SIMPLE_ID -> LibName -> ModalMor -> MSign -> Result (ModalMor, [Named ModalFORMULA]) Source # symbol_to_raw :: Modal -> Symbol -> RawSymbol Source # id_to_raw :: Modal -> Id -> RawSymbol Source # matches :: Modal -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Modal -> MSign Source # add_symb_to_sign :: Modal -> MSign -> Symbol -> Result MSign Source # signature_union :: Modal -> MSign -> MSign -> Result MSign Source # signatureDiff :: Modal -> MSign -> MSign -> Result MSign Source # intersection :: Modal -> MSign -> MSign -> Result MSign Source # final_union :: Modal -> MSign -> MSign -> Result MSign Source # morphism_union :: Modal -> ModalMor -> ModalMor -> Result ModalMor Source # is_subsig :: Modal -> MSign -> MSign -> Bool Source # subsig_inclusion :: Modal -> MSign -> MSign -> Result ModalMor Source # generated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source # cogenerated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source # induced_from_morphism :: Modal -> EndoMap RawSymbol -> MSign -> Result ModalMor Source # induced_from_to_morphism :: Modal -> EndoMap RawSymbol -> ExtSign MSign Symbol -> ExtSign MSign Symbol -> Result ModalMor Source # is_transportable :: Modal -> ModalMor -> Bool Source # is_injective :: Modal -> ModalMor -> Bool Source # theory_to_taxonomy :: Modal -> TaxoGraphKind -> MMiSSOntology -> MSign -> [Named ModalFORMULA] -> Result MMiSSOntology Source # corresp2th :: Modal -> String -> Bool -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (MSign, [Named ModalFORMULA], MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Modal -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (MSign, MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Modal -> [IRI] -> (MSign, [Named ModalFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #
Logic Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Modal.Logic_Modal Methods parse_basic_sen :: Modal -> Maybe (M_BASIC_SPEC -> AParser st ModalFORMULA) Source # stability :: Modal -> Stability Source # data_logic :: Modal -> Maybe AnyLogic Source # top_sublogic :: Modal -> () Source # all_sublogics :: Modal -> [()] Source # bottomSublogic :: Modal -> Maybe () Source # sublogicDimensions :: Modal -> [[()]] Source # parseSublogic :: Modal -> String -> Maybe () Source # proj_sublogic_epsilon :: Modal -> () -> MSign -> ModalMor Source # provers :: Modal -> [Prover MSign ModalFORMULA ModalMor () ()] Source # default_prover :: Modal -> String Source # cons_checkers :: Modal -> [ConsChecker MSign ModalFORMULA () ModalMor ()] Source # conservativityCheck :: Modal -> [ConservativityChecker MSign ModalFORMULA ModalMor] Source # empty_proof_tree :: Modal -> () Source # syntaxTable :: Modal -> MSign -> Maybe SyntaxTable Source # omdoc_metatheory :: Modal -> Maybe OMCD Source # export_symToOmdoc :: Modal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Modal -> NameMap Symbol -> ModalFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: Modal -> SigMap Symbol -> MSign -> [Named ModalFORMULA] -> Result [TCElement] Source # omdocToSym :: Modal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Modal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ModalFORMULA)) Source # addOMadtToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [[OmdADT]] -> Result (MSign, [Named ModalFORMULA]) Source # addOmdocToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [TCElement] -> Result (MSign, [Named ModalFORMULA]) Source # sublogicOfTheo :: Modal -> (MSign, [ModalFORMULA]) -> () Source #
Comorphism Modal2CASL Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Modal2CASL Methods sourceLogic :: Modal2CASL -> Modal Source # sourceSublogic :: Modal2CASL -> () Source # sourceSublogicLossy :: Modal2CASL -> () Source # minSourceTheory :: Modal2CASL -> Maybe (LibName, String) Source # targetLogic :: Modal2CASL -> CASL Source # mapSublogic :: Modal2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Modal2CASL -> ModalMor -> Result CASLMor Source # map_sentence :: Modal2CASL -> MSign -> ModalFORMULA -> Result CASLFORMULA Source # map_symbol :: Modal2CASL -> MSign -> Symbol -> Set Symbol Source # extractModel :: Modal2CASL -> MSign -> ProofTree -> Result (MSign, [Named ModalFORMULA]) Source # is_model_transportable :: Modal2CASL -> Bool Source # has_model_expansion :: Modal2CASL -> Bool Source # is_weakly_amalgamable :: Modal2CASL -> Bool Source # constituents :: Modal2CASL -> [String] Source # isInclusionComorphism :: Modal2CASL -> Bool Source # rps :: Modal2CASL -> Bool Source # eps :: Modal2CASL -> Bool Source # isGTC :: Modal2CASL -> Bool Source #
Comorphism CspCASL2Modal CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CspCASL2Modal Methods sourceLogic :: CspCASL2Modal -> CspCASL Source # sourceSublogic :: CspCASL2Modal -> () Source # sourceSublogicLossy :: CspCASL2Modal -> () Source # minSourceTheory :: CspCASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CspCASL2Modal -> Modal Source # mapSublogic :: CspCASL2Modal -> () -> Maybe () Source # map_theory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CspCASL2Modal -> (CspCASLSign, [Named CspCASLSen]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CspCASL2Modal -> CspCASLMorphism -> Result ModalMor Source # map_sentence :: CspCASL2Modal -> CspCASLSign -> CspCASLSen -> Result ModalFORMULA Source # map_symbol :: CspCASL2Modal -> CspCASLSign -> CspSymbol -> Set Symbol Source # extractModel :: CspCASL2Modal -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2Modal -> Bool Source # has_model_expansion :: CspCASL2Modal -> Bool Source # is_weakly_amalgamable :: CspCASL2Modal -> Bool Source # constituents :: CspCASL2Modal -> [String] Source # isInclusionComorphism :: CspCASL2Modal -> Bool Source # rps :: CspCASL2Modal -> Bool Source # eps :: CspCASL2Modal -> Bool Source # isGTC :: CspCASL2Modal -> Bool Source #
Comorphism CASL2Modal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2Modal Methods sourceLogic :: CASL2Modal -> CASL Source # sourceSublogic :: CASL2Modal -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Modal -> CASL_Sublogics Source # minSourceTheory :: CASL2Modal -> Maybe (LibName, String) Source # targetLogic :: CASL2Modal -> Modal Source # mapSublogic :: CASL2Modal -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # mapMarkedTheory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source # map_morphism :: CASL2Modal -> CASLMor -> Result ModalMor Source # map_sentence :: CASL2Modal -> CASLSign -> CASLFORMULA -> Result ModalFORMULA Source # map_symbol :: CASL2Modal -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Modal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Modal -> Bool Source # has_model_expansion :: CASL2Modal -> Bool Source # is_weakly_amalgamable :: CASL2Modal -> Bool Source # constituents :: CASL2Modal -> [String] Source # isInclusionComorphism :: CASL2Modal -> Bool Source # rps :: CASL2Modal -> Bool Source # eps :: CASL2Modal -> Bool Source # isGTC :: CASL2Modal -> Bool Source #
type Rep M_FORMULA
Instance details Defined in Modal.ATC_Modal type Rep M_FORMULA = D1 ('MetaData "M_FORMULA" "Modal.AS_Modal" "main" 'False) (C1 ('MetaCons "BoxOrDiamond" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MODALITY)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA M_FORMULA)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))