Copyright	(c) Klaus Luettich Christian Maeder Uni Bremen 2002-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

CASL.AS_Basic_CASL

Contents

short cuts for terms and formulas
type synonyms

Description

Abstract Syntax of CASL Basic_specs, Symb_items and Symb_map_items.

Follows Sect. II:2.2 of the CASL Reference Manual.

Synopsis

data BASIC_SPEC b s f = Basic_spec [Annoted (BASIC_ITEMS b s f)]
data BASIC_ITEMS b s f
- = Sig_items (SIG_ITEMS s f)
- | Free_datatype SortsKind [Annoted DATATYPE_DECL] Range
- | Sort_gen [Annoted (SIG_ITEMS s f)] Range
- | Var_items [VAR_DECL] Range
- | Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] Range
- | Axiom_items [Annoted (FORMULA f)] Range
- | Ext_BASIC_ITEMS b
data SortsKind
- = NonEmptySorts
- | PossiblyEmptySorts
data SIG_ITEMS s f
- = Sort_items SortsKind [Annoted (SORT_ITEM f)] Range
- | Op_items [Annoted (OP_ITEM f)] Range
- | Pred_items [Annoted (PRED_ITEM f)] Range
- | Datatype_items SortsKind [Annoted DATATYPE_DECL] Range
- | Ext_SIG_ITEMS s
data SORT_ITEM f
- = Sort_decl [SORT] Range
- | Subsort_decl [SORT] SORT Range
- | Subsort_defn SORT VAR SORT (Annoted (FORMULA f)) Range
- | Iso_decl [SORT] Range
data OP_ITEM f
- = Op_decl [OP_NAME] OP_TYPE [OP_ATTR f] Range
- | Op_defn OP_NAME OP_HEAD (Annoted (TERM f)) Range
data OpKind
- = Total
- | Partial
data OP_TYPE = Op_type OpKind [SORT] SORT Range
args_OP_TYPE :: OP_TYPE -> [SORT]
res_OP_TYPE :: OP_TYPE -> SORT
data OP_HEAD = Op_head OpKind [VAR_DECL] (Maybe SORT) Range
data OP_ATTR f
- = Assoc_op_attr
- | Comm_op_attr
- | Idem_op_attr
- | Unit_op_attr (TERM f)
data PRED_ITEM f
- = Pred_decl [PRED_NAME] PRED_TYPE Range
- | Pred_defn PRED_NAME PRED_HEAD (Annoted (FORMULA f)) Range
data PRED_TYPE = Pred_type [SORT] Range
data PRED_HEAD = Pred_head [VAR_DECL] Range
data DATATYPE_DECL = Datatype_decl SORT [Annoted ALTERNATIVE] Range
data ALTERNATIVE
- = Alt_construct OpKind OP_NAME [COMPONENTS] Range
- | Subsorts [SORT] Range
data COMPONENTS
- = Cons_select OpKind [OP_NAME] SORT Range
- | Sort SORT
data VAR_DECL = Var_decl [VAR] SORT Range
varDeclRange :: VAR_DECL -> [Pos]
data Junctor
- = Con
- | Dis
dualJunctor :: Junctor -> Junctor
data Relation
- = Implication
- | RevImpl
- | Equivalence
data Equality
- = Strong
- | Existl
data FORMULA f
- = Quantification QUANTIFIER [VAR_DECL] (FORMULA f) Range
- | Junction Junctor [FORMULA f] Range
- | Relation (FORMULA f) Relation (FORMULA f) Range
- | Negation (FORMULA f) Range
- | Atom Bool Range
- | Predication PRED_SYMB [TERM f] Range
- | Definedness (TERM f) Range
- | Equation (TERM f) Equality (TERM f) Range
- | Membership (TERM f) SORT Range
- | Mixfix_formula (TERM f)
- | Unparsed_formula String Range
- | Sort_gen_ax [Constraint] Bool
- | QuantOp OP_NAME OP_TYPE (FORMULA f)
- | QuantPred PRED_NAME PRED_TYPE (FORMULA f)
- | ExtFORMULA f
mkSort_gen_ax :: [Constraint] -> Bool -> FORMULA f
is_True_atom :: FORMULA f -> Bool
is_False_atom :: FORMULA f -> Bool
boolForm :: Bool -> FORMULA f
trueForm :: FORMULA f
falseForm :: FORMULA f
data Constraint = Constraint {
- newSort :: SORT
- opSymbs :: [(OP_SYMB, [Int])]
- origSort :: SORT
}
sortConstraints :: [Constraint] -> [Constraint]
isInjectiveList :: Ord a => [a] -> Bool
recover_Sort_gen_ax :: [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)])
recoverSortGen :: [Constraint] -> [(SORT, [OP_SYMB])]
recover_free_Sort_gen_ax :: [Constraint] -> Maybe [(SORT, [OP_SYMB])]
isSortGen :: FORMULA f -> Bool
data QUANTIFIER
- = Universal
- | Existential
- | Unique_existential
data PRED_SYMB
- = Pred_name PRED_NAME
- | Qual_pred_name PRED_NAME PRED_TYPE Range
predSymbName :: PRED_SYMB -> PRED_NAME
data TERM f
- = Qual_var VAR SORT Range
- | Application OP_SYMB [TERM f] Range
- | Sorted_term (TERM f) SORT Range
- | Cast (TERM f) SORT Range
- | Conditional (TERM f) (FORMULA f) (TERM f) Range
- | Unparsed_term String Range
- | Mixfix_qual_pred PRED_SYMB
- | Mixfix_term [TERM f]
- | Mixfix_token Token
- | Mixfix_sorted_term SORT Range
- | Mixfix_cast SORT Range
- | Mixfix_parenthesized [TERM f] Range
- | Mixfix_bracketed [TERM f] Range
- | Mixfix_braced [TERM f] Range
- | ExtTERM f
varOrConst :: Token -> TERM f
data OP_SYMB
- = Op_name OP_NAME
- | Qual_op_name OP_NAME OP_TYPE Range
opSymbName :: OP_SYMB -> OP_NAME
mkForallRange :: [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForall :: [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist :: [VAR_DECL] -> FORMULA f -> FORMULA f
toQualVar :: VAR_DECL -> TERM f
mkRel :: Relation -> FORMULA f -> FORMULA f -> FORMULA f
mkImpl :: FORMULA f -> FORMULA f -> FORMULA f
mkAnyEq :: Equality -> TERM f -> TERM f -> FORMULA f
mkExEq :: TERM f -> TERM f -> FORMULA f
mkStEq :: TERM f -> TERM f -> FORMULA f
mkEqv :: FORMULA f -> FORMULA f -> FORMULA f
mkAppl :: OP_SYMB -> [TERM f] -> TERM f
mkPredication :: PRED_SYMB -> [TERM f] -> FORMULA f
mkVarDecl :: VAR -> SORT -> VAR_DECL
mkVarTerm :: VAR -> SORT -> TERM f
conjunctRange :: [FORMULA f] -> Range -> FORMULA f
conjunct :: [FORMULA f] -> FORMULA f
disjunctRange :: [FORMULA f] -> Range -> FORMULA f
disjunct :: [FORMULA f] -> FORMULA f
mkQualOp :: OP_NAME -> OP_TYPE -> OP_SYMB
mkQualPred :: PRED_NAME -> PRED_TYPE -> PRED_SYMB
negateForm :: FORMULA f -> Range -> FORMULA f
mkNeg :: FORMULA f -> FORMULA f
mkVarDeclStr :: String -> SORT -> VAR_DECL
type CASLFORMULA = FORMULA ()
type CASLTERM = TERM ()
type OP_NAME = Id
type PRED_NAME = Id
type SORT = Id
type VAR = Token
data SYMB_ITEMS = Symb_items SYMB_KIND [SYMB] Range
symbItemsName :: SYMB_ITEMS -> [String]
data SYMB_MAP_ITEMS = Symb_map_items SYMB_KIND [SYMB_OR_MAP] Range
data SYMB_KIND
- = Implicit
- | Sorts_kind
- | Ops_kind
- | Preds_kind
data SYMB
- = Symb_id Id
- | Qual_id Id TYPE Range
data TYPE
- = O_type OP_TYPE
- | P_type PRED_TYPE
- | A_type SORT
data SYMB_OR_MAP
- = Symb SYMB
- | Symb_map SYMB SYMB Range

Documentation

data BASIC_SPEC b s f Source #

Constructors

Basic_spec [Annoted (BASIC_ITEMS b s f)]

Instances

Instances details

ProjectSublogic CASL_DL_SL DL_BASIC_SPEC Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods projectSublogic :: CASL_DL_SL -> DL_BASIC_SPEC -> DL_BASIC_SPEC Source #
MinSublogic CASL_DL_SL DL_BASIC_SPEC Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods minSublogic :: DL_BASIC_SPEC -> CASL_DL_SL Source #
Syntax CASL CASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in CASL.Logic_CASL Methods parsersAndPrinters :: CASL -> Map String (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc) Source # parse_basic_spec :: CASL -> Maybe (PrefixMap -> AParser st CASLBasicSpec) Source # parseSingleSymbItem :: CASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: CASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CASL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: CASL -> CASLBasicSpec -> Item Source # symb_items_name :: CASL -> SYMB_ITEMS -> [String] 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 #
Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in Hybrid.Logic_Hybrid Methods parsersAndPrinters :: Hybrid -> Map String (PrefixMap -> AParser st H_BASIC_SPEC, H_BASIC_SPEC -> Doc) Source # parse_basic_spec :: Hybrid -> Maybe (PrefixMap -> AParser st H_BASIC_SPEC) Source # parseSingleSymbItem :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Hybrid -> H_BASIC_SPEC -> Item Source # symb_items_name :: Hybrid -> SYMB_ITEMS -> [String] Source #
Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in Fpl.Logic_Fpl Methods parsersAndPrinters :: Fpl -> Map String (PrefixMap -> AParser st FplBasicSpec, FplBasicSpec -> Doc) Source # parse_basic_spec :: Fpl -> Maybe (PrefixMap -> AParser st FplBasicSpec) Source # parseSingleSymbItem :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Fpl -> FplBasicSpec -> Item Source # symb_items_name :: Fpl -> SYMB_ITEMS -> [String] 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 #
Syntax ConstraintCASL ConstraintCASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in ConstraintCASL.Logic_ConstraintCASL Methods parsersAndPrinters :: ConstraintCASL -> Map String (PrefixMap -> AParser st ConstraintCASLBasicSpec, ConstraintCASLBasicSpec -> Doc) Source # parse_basic_spec :: ConstraintCASL -> Maybe (PrefixMap -> AParser st ConstraintCASLBasicSpec) Source # parseSingleSymbItem :: ConstraintCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: ConstraintCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: ConstraintCASL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: ConstraintCASL -> ConstraintCASLBasicSpec -> Item Source # symb_items_name :: ConstraintCASL -> SYMB_ITEMS -> [String] Source #
Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods parsersAndPrinters :: CoCASL -> Map String (PrefixMap -> AParser st C_BASIC_SPEC, C_BASIC_SPEC -> Doc) Source # parse_basic_spec :: CoCASL -> Maybe (PrefixMap -> AParser st C_BASIC_SPEC) Source # parseSingleSymbItem :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: CoCASL -> C_BASIC_SPEC -> Item Source # symb_items_name :: CoCASL -> SYMB_ITEMS -> [String] Source #
Syntax COL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in COL.Logic_COL Methods parsersAndPrinters :: COL -> Map String (PrefixMap -> AParser st C_BASIC_SPEC, C_BASIC_SPEC -> Doc) Source # parse_basic_spec :: COL -> Maybe (PrefixMap -> AParser st C_BASIC_SPEC) Source # parseSingleSymbItem :: COL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: COL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: COL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: COL -> C_BASIC_SPEC -> Item Source # symb_items_name :: COL -> SYMB_ITEMS -> [String] Source #
Syntax CASL_DL DL_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods parsersAndPrinters :: CASL_DL -> Map String (PrefixMap -> AParser st DL_BASIC_SPEC, DL_BASIC_SPEC -> Doc) Source # parse_basic_spec :: CASL_DL -> Maybe (PrefixMap -> AParser st DL_BASIC_SPEC) Source # parseSingleSymbItem :: CASL_DL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: CASL_DL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CASL_DL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: CASL_DL -> DL_BASIC_SPEC -> Item Source # symb_items_name :: CASL_DL -> SYMB_ITEMS -> [String] Source #
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in VSE.Logic_VSE Methods parsersAndPrinters :: VSE -> Map String (PrefixMap -> AParser st VSEBasicSpec, VSEBasicSpec -> Doc) Source # parse_basic_spec :: VSE -> Maybe (PrefixMap -> AParser st VSEBasicSpec) Source # parseSingleSymbItem :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: VSE -> VSEBasicSpec -> Item Source # symb_items_name :: VSE -> SYMB_ITEMS -> [String] Source #
StaticAnalysis CASL CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol Source #
Instance details Defined in CASL.Logic_CASL Methods basic_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, GlobalAnnos) -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA])) Source # sen_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, CASLFORMULA) -> Result CASLFORMULA) Source # extBasicAnalysis :: CASL -> IRI -> LibName -> CASLBasicSpec -> CASLSign -> GlobalAnnos -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA]) Source # stat_symb_map_items :: CASL -> CASLSign -> Maybe CASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: CASL -> CASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: CASL -> Maybe ((CASLSign, [Named CASLFORMULA]) -> CASLBasicSpec) Source # ensures_amalgamability :: CASL -> ([CASLAmalgOpt], Gr CASLSign (Int, CASLMor), [(Int, CASLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CASL -> CASLMor -> [Named CASLFORMULA] -> Result (CASLSign, [Named CASLFORMULA]) Source # signature_colimit :: CASL -> Gr CASLSign (Int, CASLMor) -> Result (CASLSign, Map Int CASLMor) Source # qualify :: CASL -> SIMPLE_ID -> LibName -> CASLMor -> CASLSign -> Result (CASLMor, [Named CASLFORMULA]) Source # symbol_to_raw :: CASL -> Symbol -> RawSymbol Source # id_to_raw :: CASL -> Id -> RawSymbol Source # matches :: CASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: CASL -> CASLSign Source # add_symb_to_sign :: CASL -> CASLSign -> Symbol -> Result CASLSign Source # signature_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source # signatureDiff :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source # intersection :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source # final_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source # morphism_union :: CASL -> CASLMor -> CASLMor -> Result CASLMor Source # is_subsig :: CASL -> CASLSign -> CASLSign -> Bool Source # subsig_inclusion :: CASL -> CASLSign -> CASLSign -> Result CASLMor Source # generated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source # cogenerated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source # induced_from_morphism :: CASL -> EndoMap RawSymbol -> CASLSign -> Result CASLMor Source # induced_from_to_morphism :: CASL -> EndoMap RawSymbol -> ExtSign CASLSign Symbol -> ExtSign CASLSign Symbol -> Result CASLMor Source # is_transportable :: CASL -> CASLMor -> Bool Source # is_injective :: CASL -> CASLMor -> Bool Source # theory_to_taxonomy :: CASL -> TaxoGraphKind -> MMiSSOntology -> CASLSign -> [Named CASLFORMULA] -> Result MMiSSOntology Source # corresp2th :: CASL -> String -> Bool -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CASLSign, [Named CASLFORMULA], CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CASL -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CASLSign, CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CASL -> [IRI] -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) 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 #
StaticAnalysis Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol Source #
Instance details Defined in Hybrid.Logic_Hybrid Methods basic_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, GlobalAnnos) -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA])) Source # sen_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, HybridFORMULA) -> Result HybridFORMULA) Source # extBasicAnalysis :: Hybrid -> IRI -> LibName -> H_BASIC_SPEC -> HSign -> GlobalAnnos -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA]) Source # stat_symb_map_items :: Hybrid -> HSign -> Maybe HSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Hybrid -> HSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Hybrid -> Maybe ((HSign, [Named HybridFORMULA]) -> H_BASIC_SPEC) Source # ensures_amalgamability :: Hybrid -> ([CASLAmalgOpt], Gr HSign (Int, HybridMor), [(Int, HybridMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Hybrid -> HybridMor -> [Named HybridFORMULA] -> Result (HSign, [Named HybridFORMULA]) Source # signature_colimit :: Hybrid -> Gr HSign (Int, HybridMor) -> Result (HSign, Map Int HybridMor) Source # qualify :: Hybrid -> SIMPLE_ID -> LibName -> HybridMor -> HSign -> Result (HybridMor, [Named HybridFORMULA]) Source # symbol_to_raw :: Hybrid -> Symbol -> RawSymbol Source # id_to_raw :: Hybrid -> Id -> RawSymbol Source # matches :: Hybrid -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Hybrid -> HSign Source # add_symb_to_sign :: Hybrid -> HSign -> Symbol -> Result HSign Source # signature_union :: Hybrid -> HSign -> HSign -> Result HSign Source # signatureDiff :: Hybrid -> HSign -> HSign -> Result HSign Source # intersection :: Hybrid -> HSign -> HSign -> Result HSign Source # final_union :: Hybrid -> HSign -> HSign -> Result HSign Source # morphism_union :: Hybrid -> HybridMor -> HybridMor -> Result HybridMor Source # is_subsig :: Hybrid -> HSign -> HSign -> Bool Source # subsig_inclusion :: Hybrid -> HSign -> HSign -> Result HybridMor Source # generated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source # cogenerated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source # induced_from_morphism :: Hybrid -> EndoMap RawSymbol -> HSign -> Result HybridMor Source # induced_from_to_morphism :: Hybrid -> EndoMap RawSymbol -> ExtSign HSign Symbol -> ExtSign HSign Symbol -> Result HybridMor Source # is_transportable :: Hybrid -> HybridMor -> Bool Source # is_injective :: Hybrid -> HybridMor -> Bool Source # theory_to_taxonomy :: Hybrid -> TaxoGraphKind -> MMiSSOntology -> HSign -> [Named HybridFORMULA] -> Result MMiSSOntology Source # corresp2th :: Hybrid -> String -> Bool -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (HSign, [Named HybridFORMULA], HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Hybrid -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (HSign, HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Hybrid -> [IRI] -> (HSign, [Named HybridFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source #
StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source #
Instance details Defined in Fpl.Logic_Fpl Methods basic_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, GlobalAnnos) -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])) Source # sen_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, FplForm) -> Result FplForm) Source # extBasicAnalysis :: Fpl -> IRI -> LibName -> FplBasicSpec -> FplSign -> GlobalAnnos -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]) Source # stat_symb_map_items :: Fpl -> FplSign -> Maybe FplSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Fpl -> FplSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Fpl -> Maybe ((FplSign, [Named FplForm]) -> FplBasicSpec) Source # ensures_amalgamability :: Fpl -> ([CASLAmalgOpt], Gr FplSign (Int, FplMor), [(Int, FplMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Fpl -> FplMor -> [Named FplForm] -> Result (FplSign, [Named FplForm]) Source # signature_colimit :: Fpl -> Gr FplSign (Int, FplMor) -> Result (FplSign, Map Int FplMor) Source # qualify :: Fpl -> SIMPLE_ID -> LibName -> FplMor -> FplSign -> Result (FplMor, [Named FplForm]) Source # symbol_to_raw :: Fpl -> Symbol -> RawSymbol Source # id_to_raw :: Fpl -> Id -> RawSymbol Source # matches :: Fpl -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Fpl -> FplSign Source # add_symb_to_sign :: Fpl -> FplSign -> Symbol -> Result FplSign Source # signature_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source # signatureDiff :: Fpl -> FplSign -> FplSign -> Result FplSign Source # intersection :: Fpl -> FplSign -> FplSign -> Result FplSign Source # final_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source # morphism_union :: Fpl -> FplMor -> FplMor -> Result FplMor Source # is_subsig :: Fpl -> FplSign -> FplSign -> Bool Source # subsig_inclusion :: Fpl -> FplSign -> FplSign -> Result FplMor Source # generated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source # cogenerated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source # induced_from_morphism :: Fpl -> EndoMap RawSymbol -> FplSign -> Result FplMor Source # induced_from_to_morphism :: Fpl -> EndoMap RawSymbol -> ExtSign FplSign Symbol -> ExtSign FplSign Symbol -> Result FplMor Source # is_transportable :: Fpl -> FplMor -> Bool Source # is_injective :: Fpl -> FplMor -> Bool Source # theory_to_taxonomy :: Fpl -> TaxoGraphKind -> MMiSSOntology -> FplSign -> [Named FplForm] -> Result MMiSSOntology Source # corresp2th :: Fpl -> String -> Bool -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (FplSign, [Named FplForm], FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Fpl -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (FplSign, FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Fpl -> [IRI] -> (FplSign, [Named FplForm]) -> Result (FplSign, [Named FplForm]) 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 #
StaticAnalysis ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol Source #
Instance details Defined in ConstraintCASL.Logic_ConstraintCASL Methods basic_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos) -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA])) Source # sen_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, ConstraintCASLFORMULA) -> Result ConstraintCASLFORMULA) Source # extBasicAnalysis :: ConstraintCASL -> IRI -> LibName -> ConstraintCASLBasicSpec -> ConstraintCASLSign -> GlobalAnnos -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA]) Source # stat_symb_map_items :: ConstraintCASL -> ConstraintCASLSign -> Maybe ConstraintCASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: ConstraintCASL -> ConstraintCASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: ConstraintCASL -> Maybe ((ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> ConstraintCASLBasicSpec) Source # ensures_amalgamability :: ConstraintCASL -> ([CASLAmalgOpt], Gr ConstraintCASLSign (Int, ConstraintCASLMor), [(Int, ConstraintCASLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: ConstraintCASL -> ConstraintCASLMor -> [Named ConstraintCASLFORMULA] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source # signature_colimit :: ConstraintCASL -> Gr ConstraintCASLSign (Int, ConstraintCASLMor) -> Result (ConstraintCASLSign, Map Int ConstraintCASLMor) Source # qualify :: ConstraintCASL -> SIMPLE_ID -> LibName -> ConstraintCASLMor -> ConstraintCASLSign -> Result (ConstraintCASLMor, [Named ConstraintCASLFORMULA]) Source # symbol_to_raw :: ConstraintCASL -> Symbol -> RawSymbol Source # id_to_raw :: ConstraintCASL -> Id -> RawSymbol Source # matches :: ConstraintCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: ConstraintCASL -> ConstraintCASLSign Source # add_symb_to_sign :: ConstraintCASL -> ConstraintCASLSign -> Symbol -> Result ConstraintCASLSign Source # signature_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source # signatureDiff :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source # intersection :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source # final_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source # morphism_union :: ConstraintCASL -> ConstraintCASLMor -> ConstraintCASLMor -> Result ConstraintCASLMor Source # is_subsig :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Bool Source # subsig_inclusion :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLMor Source # generated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source # cogenerated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source # induced_from_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source # induced_from_to_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ExtSign ConstraintCASLSign Symbol -> ExtSign ConstraintCASLSign Symbol -> Result ConstraintCASLMor Source # is_transportable :: ConstraintCASL -> ConstraintCASLMor -> Bool Source # is_injective :: ConstraintCASL -> ConstraintCASLMor -> Bool Source # theory_to_taxonomy :: ConstraintCASL -> TaxoGraphKind -> MMiSSOntology -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result MMiSSOntology Source # corresp2th :: ConstraintCASL -> String -> Bool -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA], ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ConstraintCASLSign, ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: ConstraintCASL -> [IRI] -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #
StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods basic_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA])) Source # sen_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, CoCASLFORMULA) -> Result CoCASLFORMULA) Source # extBasicAnalysis :: CoCASL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA]) Source # stat_symb_map_items :: CoCASL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: CoCASL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: CoCASL -> Maybe ((CSign, [Named CoCASLFORMULA]) -> C_BASIC_SPEC) Source # ensures_amalgamability :: CoCASL -> ([CASLAmalgOpt], Gr CSign (Int, CoCASLMor), [(Int, CoCASLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CoCASL -> CoCASLMor -> [Named CoCASLFORMULA] -> Result (CSign, [Named CoCASLFORMULA]) Source # signature_colimit :: CoCASL -> Gr CSign (Int, CoCASLMor) -> Result (CSign, Map Int CoCASLMor) Source # qualify :: CoCASL -> SIMPLE_ID -> LibName -> CoCASLMor -> CSign -> Result (CoCASLMor, [Named CoCASLFORMULA]) Source # symbol_to_raw :: CoCASL -> Symbol -> RawSymbol Source # id_to_raw :: CoCASL -> Id -> RawSymbol Source # matches :: CoCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: CoCASL -> CSign Source # add_symb_to_sign :: CoCASL -> CSign -> Symbol -> Result CSign Source # signature_union :: CoCASL -> CSign -> CSign -> Result CSign Source # signatureDiff :: CoCASL -> CSign -> CSign -> Result CSign Source # intersection :: CoCASL -> CSign -> CSign -> Result CSign Source # final_union :: CoCASL -> CSign -> CSign -> Result CSign Source # morphism_union :: CoCASL -> CoCASLMor -> CoCASLMor -> Result CoCASLMor Source # is_subsig :: CoCASL -> CSign -> CSign -> Bool Source # subsig_inclusion :: CoCASL -> CSign -> CSign -> Result CoCASLMor Source # generated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source # cogenerated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source # induced_from_morphism :: CoCASL -> EndoMap RawSymbol -> CSign -> Result CoCASLMor Source # induced_from_to_morphism :: CoCASL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result CoCASLMor Source # is_transportable :: CoCASL -> CoCASLMor -> Bool Source # is_injective :: CoCASL -> CoCASLMor -> Bool Source # theory_to_taxonomy :: CoCASL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named CoCASLFORMULA] -> Result MMiSSOntology Source # corresp2th :: CoCASL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named CoCASLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CoCASL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CoCASL -> [IRI] -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #
StaticAnalysis COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source #
Instance details Defined in COL.Logic_COL Methods basic_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA])) Source # sen_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, COLFORMULA) -> Result COLFORMULA) Source # extBasicAnalysis :: COL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]) Source # stat_symb_map_items :: COL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: COL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: COL -> Maybe ((CSign, [Named COLFORMULA]) -> C_BASIC_SPEC) Source # ensures_amalgamability :: COL -> ([CASLAmalgOpt], Gr CSign (Int, COLMor), [(Int, COLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: COL -> COLMor -> [Named COLFORMULA] -> Result (CSign, [Named COLFORMULA]) Source # signature_colimit :: COL -> Gr CSign (Int, COLMor) -> Result (CSign, Map Int COLMor) Source # qualify :: COL -> SIMPLE_ID -> LibName -> COLMor -> CSign -> Result (COLMor, [Named COLFORMULA]) Source # symbol_to_raw :: COL -> Symbol -> RawSymbol Source # id_to_raw :: COL -> Id -> RawSymbol Source # matches :: COL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: COL -> CSign Source # add_symb_to_sign :: COL -> CSign -> Symbol -> Result CSign Source # signature_union :: COL -> CSign -> CSign -> Result CSign Source # signatureDiff :: COL -> CSign -> CSign -> Result CSign Source # intersection :: COL -> CSign -> CSign -> Result CSign Source # final_union :: COL -> CSign -> CSign -> Result CSign Source # morphism_union :: COL -> COLMor -> COLMor -> Result COLMor Source # is_subsig :: COL -> CSign -> CSign -> Bool Source # subsig_inclusion :: COL -> CSign -> CSign -> Result COLMor Source # generated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source # cogenerated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source # induced_from_morphism :: COL -> EndoMap RawSymbol -> CSign -> Result COLMor Source # induced_from_to_morphism :: COL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result COLMor Source # is_transportable :: COL -> COLMor -> Bool Source # is_injective :: COL -> COLMor -> Bool Source # theory_to_taxonomy :: COL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named COLFORMULA] -> Result MMiSSOntology Source # corresp2th :: COL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named COLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: COL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: COL -> [IRI] -> (CSign, [Named COLFORMULA]) -> Result (CSign, [Named COLFORMULA]) Source #
StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods basic_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, GlobalAnnos) -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA])) Source # sen_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, DLFORMULA) -> Result DLFORMULA) Source # extBasicAnalysis :: CASL_DL -> IRI -> LibName -> DL_BASIC_SPEC -> DLSign -> GlobalAnnos -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA]) Source # stat_symb_map_items :: CASL_DL -> DLSign -> Maybe DLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: CASL_DL -> DLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: CASL_DL -> Maybe ((DLSign, [Named DLFORMULA]) -> DL_BASIC_SPEC) Source # ensures_amalgamability :: CASL_DL -> ([CASLAmalgOpt], Gr DLSign (Int, DLMor), [(Int, DLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CASL_DL -> DLMor -> [Named DLFORMULA] -> Result (DLSign, [Named DLFORMULA]) Source # signature_colimit :: CASL_DL -> Gr DLSign (Int, DLMor) -> Result (DLSign, Map Int DLMor) Source # qualify :: CASL_DL -> SIMPLE_ID -> LibName -> DLMor -> DLSign -> Result (DLMor, [Named DLFORMULA]) Source # symbol_to_raw :: CASL_DL -> Symbol -> RawSymbol Source # id_to_raw :: CASL_DL -> Id -> RawSymbol Source # matches :: CASL_DL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: CASL_DL -> DLSign Source # add_symb_to_sign :: CASL_DL -> DLSign -> Symbol -> Result DLSign Source # signature_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # signatureDiff :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # intersection :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # final_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source # morphism_union :: CASL_DL -> DLMor -> DLMor -> Result DLMor Source # is_subsig :: CASL_DL -> DLSign -> DLSign -> Bool Source # subsig_inclusion :: CASL_DL -> DLSign -> DLSign -> Result DLMor Source # generated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source # cogenerated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source # induced_from_morphism :: CASL_DL -> EndoMap RawSymbol -> DLSign -> Result DLMor Source # induced_from_to_morphism :: CASL_DL -> EndoMap RawSymbol -> ExtSign DLSign Symbol -> ExtSign DLSign Symbol -> Result DLMor Source # is_transportable :: CASL_DL -> DLMor -> Bool Source # is_injective :: CASL_DL -> DLMor -> Bool Source # theory_to_taxonomy :: CASL_DL -> TaxoGraphKind -> MMiSSOntology -> DLSign -> [Named DLFORMULA] -> Result MMiSSOntology Source # corresp2th :: CASL_DL -> String -> Bool -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (DLSign, [Named DLFORMULA], DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CASL_DL -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (DLSign, DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CASL_DL -> [IRI] -> (DLSign, [Named DLFORMULA]) -> Result (DLSign, [Named DLFORMULA]) Source #
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source #
Instance details Defined in VSE.Logic_VSE Methods basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source # sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source # stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source # ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source # signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source # qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source # symbol_to_raw :: VSE -> Symbol -> RawSymbol Source # id_to_raw :: VSE -> Id -> RawSymbol Source # matches :: VSE -> Symbol -> RawSymbol -> Bool Source # empty_signature :: VSE -> VSESign Source # add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source # signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source # intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source # final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source # is_subsig :: VSE -> VSESign -> VSESign -> Bool Source # subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source # generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source # induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source # is_transportable :: VSE -> VSEMor -> Bool Source # is_injective :: VSE -> VSEMor -> Bool Source # theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #
Logic CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in CASL.Logic_CASL Methods parse_basic_sen :: CASL -> Maybe (CASLBasicSpec -> AParser st CASLFORMULA) Source # stability :: CASL -> Stability Source # data_logic :: CASL -> Maybe AnyLogic Source # top_sublogic :: CASL -> CASL_Sublogics Source # all_sublogics :: CASL -> [CASL_Sublogics] Source # bottomSublogic :: CASL -> Maybe CASL_Sublogics Source # sublogicDimensions :: CASL -> [[CASL_Sublogics]] Source # parseSublogic :: CASL -> String -> Maybe CASL_Sublogics Source # proj_sublogic_epsilon :: CASL -> CASL_Sublogics -> CASLSign -> CASLMor Source # provers :: CASL -> [Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree] Source # default_prover :: CASL -> String Source # cons_checkers :: CASL -> [ConsChecker CASLSign CASLFORMULA CASL_Sublogics CASLMor ProofTree] Source # conservativityCheck :: CASL -> [ConservativityChecker CASLSign CASLFORMULA CASLMor] Source # empty_proof_tree :: CASL -> ProofTree Source # syntaxTable :: CASL -> CASLSign -> Maybe SyntaxTable Source # omdoc_metatheory :: CASL -> Maybe OMCD Source # export_symToOmdoc :: CASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CASL -> NameMap Symbol -> CASLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: CASL -> SigMap Symbol -> CASLSign -> [Named CASLFORMULA] -> Result [TCElement] Source # omdocToSym :: CASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CASLFORMULA)) Source # addOMadtToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [[OmdADT]] -> Result (CASLSign, [Named CASLFORMULA]) Source # addOmdocToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [TCElement] -> Result (CASLSign, [Named CASLFORMULA]) Source # sublogicOfTheo :: CASL -> (CASLSign, [CASLFORMULA]) -> CASL_Sublogics 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 #
Logic Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source #
Instance details Defined in Hybrid.Logic_Hybrid Methods parse_basic_sen :: Hybrid -> Maybe (H_BASIC_SPEC -> AParser st HybridFORMULA) Source # stability :: Hybrid -> Stability Source # data_logic :: Hybrid -> Maybe AnyLogic Source # top_sublogic :: Hybrid -> () Source # all_sublogics :: Hybrid -> [()] Source # bottomSublogic :: Hybrid -> Maybe () Source # sublogicDimensions :: Hybrid -> [[()]] Source # parseSublogic :: Hybrid -> String -> Maybe () Source # proj_sublogic_epsilon :: Hybrid -> () -> HSign -> HybridMor Source # provers :: Hybrid -> [Prover HSign HybridFORMULA HybridMor () ()] Source # default_prover :: Hybrid -> String Source # cons_checkers :: Hybrid -> [ConsChecker HSign HybridFORMULA () HybridMor ()] Source # conservativityCheck :: Hybrid -> [ConservativityChecker HSign HybridFORMULA HybridMor] Source # empty_proof_tree :: Hybrid -> () Source # syntaxTable :: Hybrid -> HSign -> Maybe SyntaxTable Source # omdoc_metatheory :: Hybrid -> Maybe OMCD Source # export_symToOmdoc :: Hybrid -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Hybrid -> NameMap Symbol -> HybridFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: Hybrid -> SigMap Symbol -> HSign -> [Named HybridFORMULA] -> Result [TCElement] Source # omdocToSym :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named HybridFORMULA)) Source # addOMadtToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [[OmdADT]] -> Result (HSign, [Named HybridFORMULA]) Source # addOmdocToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [TCElement] -> Result (HSign, [Named HybridFORMULA]) Source # sublogicOfTheo :: Hybrid -> (HSign, [HybridFORMULA]) -> () Source #
Logic Fpl () FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol () Source #
Instance details Defined in Fpl.Logic_Fpl Methods parse_basic_sen :: Fpl -> Maybe (FplBasicSpec -> AParser st FplForm) Source # stability :: Fpl -> Stability Source # data_logic :: Fpl -> Maybe AnyLogic Source # top_sublogic :: Fpl -> () Source # all_sublogics :: Fpl -> [()] Source # bottomSublogic :: Fpl -> Maybe () Source # sublogicDimensions :: Fpl -> [[()]] Source # parseSublogic :: Fpl -> String -> Maybe () Source # proj_sublogic_epsilon :: Fpl -> () -> FplSign -> FplMor Source # provers :: Fpl -> [Prover FplSign FplForm FplMor () ()] Source # default_prover :: Fpl -> String Source # cons_checkers :: Fpl -> [ConsChecker FplSign FplForm () FplMor ()] Source # conservativityCheck :: Fpl -> [ConservativityChecker FplSign FplForm FplMor] Source # empty_proof_tree :: Fpl -> () Source # syntaxTable :: Fpl -> FplSign -> Maybe SyntaxTable Source # omdoc_metatheory :: Fpl -> Maybe OMCD Source # export_symToOmdoc :: Fpl -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Fpl -> NameMap Symbol -> FplForm -> Result TCorOMElement Source # export_theoryToOmdoc :: Fpl -> SigMap Symbol -> FplSign -> [Named FplForm] -> Result [TCElement] Source # omdocToSym :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FplForm)) Source # addOMadtToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [[OmdADT]] -> Result (FplSign, [Named FplForm]) Source # addOmdocToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [TCElement] -> Result (FplSign, [Named FplForm]) Source # sublogicOfTheo :: Fpl -> (FplSign, [FplForm]) -> () 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 #
Logic ConstraintCASL CASL_Sublogics ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol () Source #
Instance details Defined in ConstraintCASL.Logic_ConstraintCASL Methods parse_basic_sen :: ConstraintCASL -> Maybe (ConstraintCASLBasicSpec -> AParser st ConstraintCASLFORMULA) Source # stability :: ConstraintCASL -> Stability Source # data_logic :: ConstraintCASL -> Maybe AnyLogic Source # top_sublogic :: ConstraintCASL -> CASL_Sublogics Source # all_sublogics :: ConstraintCASL -> [CASL_Sublogics] Source # bottomSublogic :: ConstraintCASL -> Maybe CASL_Sublogics Source # sublogicDimensions :: ConstraintCASL -> [[CASL_Sublogics]] Source # parseSublogic :: ConstraintCASL -> String -> Maybe CASL_Sublogics Source # proj_sublogic_epsilon :: ConstraintCASL -> CASL_Sublogics -> ConstraintCASLSign -> ConstraintCASLMor Source # provers :: ConstraintCASL -> [Prover ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor CASL_Sublogics ()] Source # default_prover :: ConstraintCASL -> String Source # cons_checkers :: ConstraintCASL -> [ConsChecker ConstraintCASLSign ConstraintCASLFORMULA CASL_Sublogics ConstraintCASLMor ()] Source # conservativityCheck :: ConstraintCASL -> [ConservativityChecker ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor] Source # empty_proof_tree :: ConstraintCASL -> () Source # syntaxTable :: ConstraintCASL -> ConstraintCASLSign -> Maybe SyntaxTable Source # omdoc_metatheory :: ConstraintCASL -> Maybe OMCD Source # export_symToOmdoc :: ConstraintCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: ConstraintCASL -> NameMap Symbol -> ConstraintCASLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: ConstraintCASL -> SigMap Symbol -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result [TCElement] Source # omdocToSym :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ConstraintCASLFORMULA)) Source # addOMadtToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [[OmdADT]] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source # addOmdocToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [TCElement] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source # sublogicOfTheo :: ConstraintCASL -> (ConstraintCASLSign, [ConstraintCASLFORMULA]) -> CASL_Sublogics Source #
Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in CoCASL.Logic_CoCASL Methods parse_basic_sen :: CoCASL -> Maybe (C_BASIC_SPEC -> AParser st CoCASLFORMULA) Source # stability :: CoCASL -> Stability Source # data_logic :: CoCASL -> Maybe AnyLogic Source # top_sublogic :: CoCASL -> CoCASL_Sublogics Source # all_sublogics :: CoCASL -> [CoCASL_Sublogics] Source # bottomSublogic :: CoCASL -> Maybe CoCASL_Sublogics Source # sublogicDimensions :: CoCASL -> [[CoCASL_Sublogics]] Source # parseSublogic :: CoCASL -> String -> Maybe CoCASL_Sublogics Source # proj_sublogic_epsilon :: CoCASL -> CoCASL_Sublogics -> CSign -> CoCASLMor Source # provers :: CoCASL -> [Prover CSign CoCASLFORMULA CoCASLMor CoCASL_Sublogics ()] Source # default_prover :: CoCASL -> String Source # cons_checkers :: CoCASL -> [ConsChecker CSign CoCASLFORMULA CoCASL_Sublogics CoCASLMor ()] Source # conservativityCheck :: CoCASL -> [ConservativityChecker CSign CoCASLFORMULA CoCASLMor] Source # empty_proof_tree :: CoCASL -> () Source # syntaxTable :: CoCASL -> CSign -> Maybe SyntaxTable Source # omdoc_metatheory :: CoCASL -> Maybe OMCD Source # export_symToOmdoc :: CoCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CoCASL -> NameMap Symbol -> CoCASLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: CoCASL -> SigMap Symbol -> CSign -> [Named CoCASLFORMULA] -> Result [TCElement] Source # omdocToSym :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CoCASLFORMULA)) Source # addOMadtToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named CoCASLFORMULA]) Source # addOmdocToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [TCElement] -> Result (CSign, [Named CoCASLFORMULA]) Source # sublogicOfTheo :: CoCASL -> (CSign, [CoCASLFORMULA]) -> CoCASL_Sublogics Source #
Logic COL () C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol () Source #
Instance details Defined in COL.Logic_COL Methods parse_basic_sen :: COL -> Maybe (C_BASIC_SPEC -> AParser st COLFORMULA) Source # stability :: COL -> Stability Source # data_logic :: COL -> Maybe AnyLogic Source # top_sublogic :: COL -> () Source # all_sublogics :: COL -> [()] Source # bottomSublogic :: COL -> Maybe () Source # sublogicDimensions :: COL -> [[()]] Source # parseSublogic :: COL -> String -> Maybe () Source # proj_sublogic_epsilon :: COL -> () -> CSign -> COLMor Source # provers :: COL -> [Prover CSign COLFORMULA COLMor () ()] Source # default_prover :: COL -> String Source # cons_checkers :: COL -> [ConsChecker CSign COLFORMULA () COLMor ()] Source # conservativityCheck :: COL -> [ConservativityChecker CSign COLFORMULA COLMor] Source # empty_proof_tree :: COL -> () Source # syntaxTable :: COL -> CSign -> Maybe SyntaxTable Source # omdoc_metatheory :: COL -> Maybe OMCD Source # export_symToOmdoc :: COL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: COL -> NameMap Symbol -> COLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: COL -> SigMap Symbol -> CSign -> [Named COLFORMULA] -> Result [TCElement] Source # omdocToSym :: COL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: COL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named COLFORMULA)) Source # addOMadtToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named COLFORMULA]) Source # addOmdocToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [TCElement] -> Result (CSign, [Named COLFORMULA]) Source # sublogicOfTheo :: COL -> (CSign, [COLFORMULA]) -> () Source #
Logic CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in CASL_DL.Logic_CASL_DL Methods parse_basic_sen :: CASL_DL -> Maybe (DL_BASIC_SPEC -> AParser st DLFORMULA) Source # stability :: CASL_DL -> Stability Source # data_logic :: CASL_DL -> Maybe AnyLogic Source # top_sublogic :: CASL_DL -> CASL_DL_SL Source # all_sublogics :: CASL_DL -> [CASL_DL_SL] Source # bottomSublogic :: CASL_DL -> Maybe CASL_DL_SL Source # sublogicDimensions :: CASL_DL -> [[CASL_DL_SL]] Source # parseSublogic :: CASL_DL -> String -> Maybe CASL_DL_SL Source # proj_sublogic_epsilon :: CASL_DL -> CASL_DL_SL -> DLSign -> DLMor Source # provers :: CASL_DL -> [Prover DLSign DLFORMULA DLMor CASL_DL_SL ProofTree] Source # default_prover :: CASL_DL -> String Source # cons_checkers :: CASL_DL -> [ConsChecker DLSign DLFORMULA CASL_DL_SL DLMor ProofTree] Source # conservativityCheck :: CASL_DL -> [ConservativityChecker DLSign DLFORMULA DLMor] Source # empty_proof_tree :: CASL_DL -> ProofTree Source # syntaxTable :: CASL_DL -> DLSign -> Maybe SyntaxTable Source # omdoc_metatheory :: CASL_DL -> Maybe OMCD Source # export_symToOmdoc :: CASL_DL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CASL_DL -> NameMap Symbol -> DLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: CASL_DL -> SigMap Symbol -> DLSign -> [Named DLFORMULA] -> Result [TCElement] Source # omdocToSym :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named DLFORMULA)) Source # addOMadtToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [[OmdADT]] -> Result (DLSign, [Named DLFORMULA]) Source # addOmdocToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [TCElement] -> Result (DLSign, [Named DLFORMULA]) Source # sublogicOfTheo :: CASL_DL -> (DLSign, [DLFORMULA]) -> CASL_DL_SL Source #
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in VSE.Logic_VSE Methods parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source # stability :: VSE -> Stability Source # data_logic :: VSE -> Maybe AnyLogic Source # top_sublogic :: VSE -> () Source # all_sublogics :: VSE -> [()] Source # bottomSublogic :: VSE -> Maybe () Source # sublogicDimensions :: VSE -> [[()]] Source # parseSublogic :: VSE -> String -> Maybe () Source # proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source # provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source # default_prover :: VSE -> String Source # cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source # conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source # empty_proof_tree :: VSE -> () Source # syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source # omdoc_metatheory :: VSE -> Maybe OMCD Source # export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source # addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source # sublogicOfTheo :: VSE -> (VSESign, [Sentence]) -> () Source #
Comorphism OWL22CASL OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in OWL2.OWL22CASL Methods sourceLogic :: OWL22CASL -> OWL2 Source # sourceSublogic :: OWL22CASL -> ProfSub Source # sourceSublogicLossy :: OWL22CASL -> ProfSub Source # minSourceTheory :: OWL22CASL -> Maybe (LibName, String) Source # targetLogic :: OWL22CASL -> CASL Source # mapSublogic :: OWL22CASL -> ProfSub -> Maybe CASL_Sublogics Source # map_theory :: OWL22CASL -> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: OWL22CASL -> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: OWL22CASL -> OWLMorphism -> Result CASLMor Source # map_sentence :: OWL22CASL -> Sign -> Axiom -> Result CASLFORMULA Source # map_symbol :: OWL22CASL -> Sign -> Entity -> Set Symbol Source # extractModel :: OWL22CASL -> Sign -> ProofTree -> Result (Sign, [Named Axiom]) Source # is_model_transportable :: OWL22CASL -> Bool Source # has_model_expansion :: OWL22CASL -> Bool Source # is_weakly_amalgamable :: OWL22CASL -> Bool Source # constituents :: OWL22CASL -> [String] Source # isInclusionComorphism :: OWL22CASL -> Bool Source # rps :: OWL22CASL -> Bool Source # eps :: OWL22CASL -> Bool Source # isGTC :: OWL22CASL -> Bool Source #
Comorphism CASL2OWL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
Instance details Defined in OWL2.CASL2OWL Methods sourceLogic :: CASL2OWL -> CASL Source # sourceSublogic :: CASL2OWL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2OWL -> CASL_Sublogics Source # minSourceTheory :: CASL2OWL -> Maybe (LibName, String) Source # targetLogic :: CASL2OWL -> OWL2 Source # mapSublogic :: CASL2OWL -> CASL_Sublogics -> Maybe ProfSub Source # map_theory :: CASL2OWL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom]) Source # mapMarkedTheory :: CASL2OWL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom]) Source # map_morphism :: CASL2OWL -> CASLMor -> Result OWLMorphism Source # map_sentence :: CASL2OWL -> CASLSign -> CASLFORMULA -> Result Axiom Source # map_symbol :: CASL2OWL -> CASLSign -> Symbol -> Set Entity Source # extractModel :: CASL2OWL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2OWL -> Bool Source # has_model_expansion :: CASL2OWL -> Bool Source # is_weakly_amalgamable :: CASL2OWL -> Bool Source # constituents :: CASL2OWL -> [String] Source # isInclusionComorphism :: CASL2OWL -> Bool Source # rps :: CASL2OWL -> Bool Source # eps :: CASL2OWL -> Bool Source # isGTC :: CASL2OWL -> Bool Source #
Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source #
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 RelScheme2CASL RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.RelScheme2CASL Methods sourceLogic :: RelScheme2CASL -> RelScheme Source # sourceSublogic :: RelScheme2CASL -> () Source # sourceSublogicLossy :: RelScheme2CASL -> () Source # minSourceTheory :: RelScheme2CASL -> Maybe (LibName, String) Source # targetLogic :: RelScheme2CASL -> CASL Source # mapSublogic :: RelScheme2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: RelScheme2CASL -> RSMorphism -> Result CASLMor Source # map_sentence :: RelScheme2CASL -> Sign -> Sentence -> Result CASLFORMULA Source # map_symbol :: RelScheme2CASL -> Sign -> RSSymbol -> Set Symbol Source # extractModel :: RelScheme2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: RelScheme2CASL -> Bool Source # has_model_expansion :: RelScheme2CASL -> Bool Source # is_weakly_amalgamable :: RelScheme2CASL -> Bool Source # constituents :: RelScheme2CASL -> [String] Source # isInclusionComorphism :: RelScheme2CASL -> Bool Source # rps :: RelScheme2CASL -> Bool Source # eps :: RelScheme2CASL -> Bool Source # isGTC :: RelScheme2CASL -> Bool Source #
Comorphism Prop2CASL Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Prop2CASL Methods sourceLogic :: Prop2CASL -> Propositional Source # sourceSublogic :: Prop2CASL -> PropSL Source # sourceSublogicLossy :: Prop2CASL -> PropSL Source # minSourceTheory :: Prop2CASL -> Maybe (LibName, String) Source # targetLogic :: Prop2CASL -> CASL Source # mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics Source # map_theory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Prop2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Prop2CASL -> Sign -> FORMULA -> Result CASLFORMULA Source # map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Prop2CASL -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: Prop2CASL -> Bool Source # has_model_expansion :: Prop2CASL -> Bool Source # is_weakly_amalgamable :: Prop2CASL -> Bool Source # constituents :: Prop2CASL -> [String] Source # isInclusionComorphism :: Prop2CASL -> Bool Source # rps :: Prop2CASL -> Bool Source # eps :: Prop2CASL -> Bool Source # isGTC :: Prop2CASL -> Bool 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 Maude2CASL Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Maude2CASL Methods sourceLogic :: Maude2CASL -> Maude Source # sourceSublogic :: Maude2CASL -> () Source # sourceSublogicLossy :: Maude2CASL -> () Source # minSourceTheory :: Maude2CASL -> Maybe (LibName, String) Source # targetLogic :: Maude2CASL -> CASL Source # mapSublogic :: Maude2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Maude2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Maude2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Maude2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Maude2CASL -> Sign -> Sentence -> Result CASLFORMULA Source # map_symbol :: Maude2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Maude2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: Maude2CASL -> Bool Source # has_model_expansion :: Maude2CASL -> Bool Source # is_weakly_amalgamable :: Maude2CASL -> Bool Source # constituents :: Maude2CASL -> [String] Source # isInclusionComorphism :: Maude2CASL -> Bool Source # rps :: Maude2CASL -> Bool Source # eps :: Maude2CASL -> Bool Source # isGTC :: Maude2CASL -> 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 DFOL2CASL DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.DFOL2CASL Methods sourceLogic :: DFOL2CASL -> DFOL Source # sourceSublogic :: DFOL2CASL -> () Source # sourceSublogicLossy :: DFOL2CASL -> () Source # minSourceTheory :: DFOL2CASL -> Maybe (LibName, String) Source # targetLogic :: DFOL2CASL -> CASL Source # mapSublogic :: DFOL2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: DFOL2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: DFOL2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: DFOL2CASL -> Morphism -> Result CASLMor Source # map_sentence :: DFOL2CASL -> Sign -> FORMULA -> Result CASLFORMULA Source # map_symbol :: DFOL2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: DFOL2CASL -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: DFOL2CASL -> Bool Source # has_model_expansion :: DFOL2CASL -> Bool Source # is_weakly_amalgamable :: DFOL2CASL -> Bool Source # constituents :: DFOL2CASL -> [String] Source # isInclusionComorphism :: DFOL2CASL -> Bool Source # rps :: DFOL2CASL -> Bool Source # eps :: DFOL2CASL -> Bool Source # isGTC :: DFOL2CASL -> Bool Source #
Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CommonLogic2CASL Methods sourceLogic :: CL2CFOL -> CommonLogic Source # sourceSublogic :: CL2CFOL -> CommonLogicSL Source # sourceSublogicLossy :: CL2CFOL -> CommonLogicSL Source # minSourceTheory :: CL2CFOL -> Maybe (LibName, String) Source # targetLogic :: CL2CFOL -> CASL Source # mapSublogic :: CL2CFOL -> CommonLogicSL -> Maybe CASL_Sublogics Source # map_theory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CL2CFOL -> Morphism -> Result CASLMor Source # map_sentence :: CL2CFOL -> Sign -> TEXT_META -> Result CASLFORMULA Source # map_symbol :: CL2CFOL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: CL2CFOL -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source # is_model_transportable :: CL2CFOL -> Bool Source # has_model_expansion :: CL2CFOL -> Bool Source # is_weakly_amalgamable :: CL2CFOL -> Bool Source # constituents :: CL2CFOL -> [String] Source # isInclusionComorphism :: CL2CFOL -> Bool Source # rps :: CL2CFOL -> Bool Source # eps :: CL2CFOL -> Bool Source # isGTC :: CL2CFOL -> Bool Source #
Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CSMOF2CASL Methods sourceLogic :: CSMOF2CASL -> CSMOF Source # sourceSublogic :: CSMOF2CASL -> () Source # sourceSublogicLossy :: CSMOF2CASL -> () Source # minSourceTheory :: CSMOF2CASL -> Maybe (LibName, String) Source # targetLogic :: CSMOF2CASL -> CASL Source # mapSublogic :: CSMOF2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: CSMOF2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CSMOF2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CSMOF2CASL -> Morphism -> Result CASLMor Source # map_sentence :: CSMOF2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: CSMOF2CASL -> Sign -> () -> Set Symbol Source # extractModel :: CSMOF2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: CSMOF2CASL -> Bool Source # has_model_expansion :: CSMOF2CASL -> Bool Source # is_weakly_amalgamable :: CSMOF2CASL -> Bool Source # constituents :: CSMOF2CASL -> [String] Source # isInclusionComorphism :: CSMOF2CASL -> Bool Source # rps :: CSMOF2CASL -> Bool Source # eps :: CSMOF2CASL -> Bool Source # isGTC :: CSMOF2CASL -> Bool Source #
Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.QVTR2CASL Methods sourceLogic :: QVTR2CASL -> QVTR Source # sourceSublogic :: QVTR2CASL -> () Source # sourceSublogicLossy :: QVTR2CASL -> () Source # minSourceTheory :: QVTR2CASL -> Maybe (LibName, String) Source # targetLogic :: QVTR2CASL -> CASL Source # mapSublogic :: QVTR2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: QVTR2CASL -> Morphism -> Result CASLMor Source # map_sentence :: QVTR2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: QVTR2CASL -> Sign -> () -> Set Symbol Source # extractModel :: QVTR2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: QVTR2CASL -> Bool Source # has_model_expansion :: QVTR2CASL -> Bool Source # is_weakly_amalgamable :: QVTR2CASL -> Bool Source # constituents :: QVTR2CASL -> [String] Source # isInclusionComorphism :: QVTR2CASL -> Bool Source # rps :: QVTR2CASL -> Bool Source # eps :: QVTR2CASL -> Bool Source # isGTC :: QVTR2CASL -> Bool Source #
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CFOL2IsabelleHOL Methods sourceLogic :: CFOL2IsabelleHOL -> CASL Source # sourceSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics Source # sourceSublogicLossy :: CFOL2IsabelleHOL -> CASL_Sublogics Source # minSourceTheory :: CFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics -> Maybe () Source # map_theory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CFOL2IsabelleHOL -> CASLMor -> Result IsabelleMorphism Source # map_sentence :: CFOL2IsabelleHOL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CFOL2IsabelleHOL -> CASLSign -> Symbol -> Set () Source # extractModel :: CFOL2IsabelleHOL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CFOL2IsabelleHOL -> Bool Source # constituents :: CFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CFOL2IsabelleHOL -> Bool Source # rps :: CFOL2IsabelleHOL -> Bool Source # eps :: CFOL2IsabelleHOL -> Bool Source # isGTC :: CFOL2IsabelleHOL -> Bool Source #
Comorphism CASL2TopSort CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2TopSort Methods sourceLogic :: CASL2TopSort -> CASL Source # sourceSublogic :: CASL2TopSort -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2TopSort -> CASL_Sublogics Source # minSourceTheory :: CASL2TopSort -> Maybe (LibName, String) Source # targetLogic :: CASL2TopSort -> CASL Source # mapSublogic :: CASL2TopSort -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2TopSort -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2TopSort -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2TopSort -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2TopSort -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2TopSort -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2TopSort -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2TopSort -> Bool Source # has_model_expansion :: CASL2TopSort -> Bool Source # is_weakly_amalgamable :: CASL2TopSort -> Bool Source # constituents :: CASL2TopSort -> [String] Source # isInclusionComorphism :: CASL2TopSort -> Bool Source # rps :: CASL2TopSort -> Bool Source # eps :: CASL2TopSort -> Bool Source # isGTC :: CASL2TopSort -> Bool Source #
Comorphism CASL2SubCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2SubCFOL Methods sourceLogic :: CASL2SubCFOL -> CASL Source # sourceSublogic :: CASL2SubCFOL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2SubCFOL -> CASL_Sublogics Source # minSourceTheory :: CASL2SubCFOL -> Maybe (LibName, String) Source # targetLogic :: CASL2SubCFOL -> CASL Source # mapSublogic :: CASL2SubCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2SubCFOL -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2SubCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2SubCFOL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2SubCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2SubCFOL -> Bool Source # has_model_expansion :: CASL2SubCFOL -> Bool Source # is_weakly_amalgamable :: CASL2SubCFOL -> Bool Source # constituents :: CASL2SubCFOL -> [String] Source # isInclusionComorphism :: CASL2SubCFOL -> Bool Source # rps :: CASL2SubCFOL -> Bool Source # eps :: CASL2SubCFOL -> Bool Source # isGTC :: CASL2SubCFOL -> 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 CASL2Skolem CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2Skolem Methods sourceLogic :: CASL2Skolem -> CASL Source # sourceSublogic :: CASL2Skolem -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Skolem -> CASL_Sublogics Source # minSourceTheory :: CASL2Skolem -> Maybe (LibName, String) Source # targetLogic :: CASL2Skolem -> CASL Source # mapSublogic :: CASL2Skolem -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2Skolem -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2Skolem -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2Skolem -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2Skolem -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2Skolem -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Skolem -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Skolem -> Bool Source # has_model_expansion :: CASL2Skolem -> Bool Source # is_weakly_amalgamable :: CASL2Skolem -> Bool Source # constituents :: CASL2Skolem -> [String] Source # isInclusionComorphism :: CASL2Skolem -> Bool Source # rps :: CASL2Skolem -> Bool Source # eps :: CASL2Skolem -> Bool Source # isGTC :: CASL2Skolem -> Bool Source #
Comorphism CASL2Prop CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2Prop Methods sourceLogic :: CASL2Prop -> CASL Source # sourceSublogic :: CASL2Prop -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Prop -> CASL_Sublogics Source # minSourceTheory :: CASL2Prop -> Maybe (LibName, String) Source # targetLogic :: CASL2Prop -> Propositional Source # mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL Source # map_theory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source # mapMarkedTheory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: CASL2Prop -> CASLMor -> Result Morphism Source # map_sentence :: CASL2Prop -> CASLSign -> CASLFORMULA -> Result FORMULA Source # map_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2Prop -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Prop -> Bool Source # has_model_expansion :: CASL2Prop -> Bool Source # is_weakly_amalgamable :: CASL2Prop -> Bool Source # constituents :: CASL2Prop -> [String] Source # isInclusionComorphism :: CASL2Prop -> Bool Source # rps :: CASL2Prop -> Bool Source # eps :: CASL2Prop -> Bool Source # isGTC :: CASL2Prop -> Bool Source #
Comorphism CASL2Prenex CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2Prenex Methods sourceLogic :: CASL2Prenex -> CASL Source # sourceSublogic :: CASL2Prenex -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Prenex -> CASL_Sublogics Source # minSourceTheory :: CASL2Prenex -> Maybe (LibName, String) Source # targetLogic :: CASL2Prenex -> CASL Source # mapSublogic :: CASL2Prenex -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2Prenex -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2Prenex -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2Prenex -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2Prenex -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2Prenex -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Prenex -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Prenex -> Bool Source # has_model_expansion :: CASL2Prenex -> Bool Source # is_weakly_amalgamable :: CASL2Prenex -> Bool Source # constituents :: CASL2Prenex -> [String] Source # isInclusionComorphism :: CASL2Prenex -> Bool Source # rps :: CASL2Prenex -> Bool Source # eps :: CASL2Prenex -> Bool Source # isGTC :: CASL2Prenex -> Bool Source #
Comorphism CASL2PCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2PCFOL Methods sourceLogic :: CASL2PCFOL -> CASL Source # sourceSublogic :: CASL2PCFOL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2PCFOL -> CASL_Sublogics Source # minSourceTheory :: CASL2PCFOL -> Maybe (LibName, String) Source # targetLogic :: CASL2PCFOL -> CASL Source # mapSublogic :: CASL2PCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2PCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2PCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2PCFOL -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2PCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2PCFOL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2PCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2PCFOL -> Bool Source # has_model_expansion :: CASL2PCFOL -> Bool Source # is_weakly_amalgamable :: CASL2PCFOL -> Bool Source # constituents :: CASL2PCFOL -> [String] Source # isInclusionComorphism :: CASL2PCFOL -> Bool Source # rps :: CASL2PCFOL -> Bool Source # eps :: CASL2PCFOL -> Bool Source # isGTC :: CASL2PCFOL -> 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 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 CASL2NNF CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2NNF Methods sourceLogic :: CASL2NNF -> CASL Source # sourceSublogic :: CASL2NNF -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2NNF -> CASL_Sublogics Source # minSourceTheory :: CASL2NNF -> Maybe (LibName, String) Source # targetLogic :: CASL2NNF -> CASL Source # mapSublogic :: CASL2NNF -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2NNF -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2NNF -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2NNF -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2NNF -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2NNF -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2NNF -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2NNF -> Bool Source # has_model_expansion :: CASL2NNF -> Bool Source # is_weakly_amalgamable :: CASL2NNF -> Bool Source # constituents :: CASL2NNF -> [String] Source # isInclusionComorphism :: CASL2NNF -> Bool Source # rps :: CASL2NNF -> Bool Source # eps :: CASL2NNF -> Bool Source # isGTC :: CASL2NNF -> 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 #
Comorphism CASL2Hybrid CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2Hybrid Methods sourceLogic :: CASL2Hybrid -> CASL Source # sourceSublogic :: CASL2Hybrid -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Hybrid -> CASL_Sublogics Source # minSourceTheory :: CASL2Hybrid -> Maybe (LibName, String) Source # targetLogic :: CASL2Hybrid -> Hybrid Source # mapSublogic :: CASL2Hybrid -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source # mapMarkedTheory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source # map_morphism :: CASL2Hybrid -> CASLMor -> Result HybridMor Source # map_sentence :: CASL2Hybrid -> CASLSign -> CASLFORMULA -> Result HybridFORMULA Source # map_symbol :: CASL2Hybrid -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Hybrid -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Hybrid -> Bool Source # has_model_expansion :: CASL2Hybrid -> Bool Source # is_weakly_amalgamable :: CASL2Hybrid -> Bool Source # constituents :: CASL2Hybrid -> [String] Source # isInclusionComorphism :: CASL2Hybrid -> Bool Source # rps :: CASL2Hybrid -> Bool Source # eps :: CASL2Hybrid -> Bool Source # isGTC :: CASL2Hybrid -> Bool Source #
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods sourceLogic :: CASL2HasCASL -> CASL Source # sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2HasCASL -> HasCASL Source # mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source # map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source # map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2HasCASL -> Bool Source # has_model_expansion :: CASL2HasCASL -> Bool Source # is_weakly_amalgamable :: CASL2HasCASL -> Bool Source # constituents :: CASL2HasCASL -> [String] Source # isInclusionComorphism :: CASL2HasCASL -> Bool Source # rps :: CASL2HasCASL -> Bool Source # eps :: CASL2HasCASL -> Bool Source # isGTC :: CASL2HasCASL -> 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 #
Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #
Instance details Defined in Comorphisms.CASL2CspCASL Methods sourceLogic :: CASL2CspCASL -> CASL Source # sourceSublogic :: CASL2CspCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CspCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CspCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CspCASL -> CspCASL Source # mapSublogic :: CASL2CspCASL -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CASL2CspCASL -> CASLMor -> Result CspCASLMorphism Source # map_sentence :: CASL2CspCASL -> CASLSign -> CASLFORMULA -> Result CspCASLSen Source # map_symbol :: CASL2CspCASL -> CASLSign -> Symbol -> Set CspSymbol Source # extractModel :: CASL2CspCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CspCASL -> Bool Source # has_model_expansion :: CASL2CspCASL -> Bool Source # is_weakly_amalgamable :: CASL2CspCASL -> Bool Source # constituents :: CASL2CspCASL -> [String] Source # isInclusionComorphism :: CASL2CspCASL -> Bool Source # rps :: CASL2CspCASL -> Bool Source # eps :: CASL2CspCASL -> Bool Source # isGTC :: CASL2CspCASL -> Bool Source #
Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Adl2CASL Methods sourceLogic :: Adl2CASL -> Adl Source # sourceSublogic :: Adl2CASL -> () Source # sourceSublogicLossy :: Adl2CASL -> () Source # minSourceTheory :: Adl2CASL -> Maybe (LibName, String) Source # targetLogic :: Adl2CASL -> CASL Source # mapSublogic :: Adl2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Adl2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Adl2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: Adl2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Adl2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: Adl2CASL -> Bool Source # has_model_expansion :: Adl2CASL -> Bool Source # is_weakly_amalgamable :: Adl2CASL -> Bool Source # constituents :: Adl2CASL -> [String] Source # isInclusionComorphism :: Adl2CASL -> Bool Source # rps :: Adl2CASL -> Bool Source # eps :: Adl2CASL -> Bool Source # isGTC :: Adl2CASL -> Bool Source #
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods sourceLogic :: CoCFOL2IsabelleHOL -> CoCASL Source # sourceSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CoCFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics -> Maybe () Source # map_theory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CoCFOL2IsabelleHOL -> CoCASLMor -> Result IsabelleMorphism Source # map_sentence :: CoCFOL2IsabelleHOL -> CSign -> CoCASLFORMULA -> Result Sentence Source # map_symbol :: CoCFOL2IsabelleHOL -> CSign -> Symbol -> Set () Source # extractModel :: CoCFOL2IsabelleHOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CoCFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CoCFOL2IsabelleHOL -> Bool Source # constituents :: CoCFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CoCFOL2IsabelleHOL -> Bool Source # rps :: CoCFOL2IsabelleHOL -> Bool Source # eps :: CoCFOL2IsabelleHOL -> Bool Source # isGTC :: CoCFOL2IsabelleHOL -> Bool Source #
Comorphism CoCASL2CoSubCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoSubCFOL Methods sourceLogic :: CoCASL2CoSubCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoSubCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoSubCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoSubCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoSubCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoSubCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoSubCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoSubCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoSubCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoSubCFOL -> Bool Source # has_model_expansion :: CoCASL2CoSubCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoSubCFOL -> Bool Source # constituents :: CoCASL2CoSubCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoSubCFOL -> Bool Source # rps :: CoCASL2CoSubCFOL -> Bool Source # eps :: CoCASL2CoSubCFOL -> Bool Source # isGTC :: CoCASL2CoSubCFOL -> Bool Source #
Comorphism CoCASL2CoPCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CoCASL2CoPCFOL Methods sourceLogic :: CoCASL2CoPCFOL -> CoCASL Source # sourceSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCASL2CoPCFOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCASL2CoPCFOL -> Maybe (LibName, String) Source # targetLogic :: CoCASL2CoPCFOL -> CoCASL Source # mapSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CoCASL2CoPCFOL -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CoCASL2CoPCFOL -> CoCASLMor -> Result CoCASLMor Source # map_sentence :: CoCASL2CoPCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CoCASL2CoPCFOL -> CSign -> Symbol -> Set Symbol Source # extractModel :: CoCASL2CoPCFOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCASL2CoPCFOL -> Bool Source # has_model_expansion :: CoCASL2CoPCFOL -> Bool Source # is_weakly_amalgamable :: CoCASL2CoPCFOL -> Bool Source # constituents :: CoCASL2CoPCFOL -> [String] Source # isInclusionComorphism :: CoCASL2CoPCFOL -> Bool Source # rps :: CoCASL2CoPCFOL -> Bool Source # eps :: CoCASL2CoPCFOL -> Bool Source # isGTC :: CoCASL2CoPCFOL -> Bool Source #
Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2CoCASL Methods sourceLogic :: CASL2CoCASL -> CASL Source # sourceSublogic :: CASL2CoCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2CoCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2CoCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2CoCASL -> CoCASL Source # mapSublogic :: CASL2CoCASL -> CASL_Sublogics -> Maybe CoCASL_Sublogics Source # map_theory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # mapMarkedTheory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source # map_morphism :: CASL2CoCASL -> CASLMor -> Result CoCASLMor Source # map_sentence :: CASL2CoCASL -> CASLSign -> CASLFORMULA -> Result CoCASLFORMULA Source # map_symbol :: CASL2CoCASL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2CoCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2CoCASL -> Bool Source # has_model_expansion :: CASL2CoCASL -> Bool Source # is_weakly_amalgamable :: CASL2CoCASL -> Bool Source # constituents :: CASL2CoCASL -> [String] Source # isInclusionComorphism :: CASL2CoCASL -> Bool Source # rps :: CASL2CoCASL -> Bool Source # eps :: CASL2CoCASL -> Bool Source # isGTC :: CASL2CoCASL -> Bool Source #
Comorphism CASL_DL2CASL CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL_DL2CASL Methods sourceLogic :: CASL_DL2CASL -> CASL_DL Source # sourceSublogic :: CASL_DL2CASL -> CASL_DL_SL Source # sourceSublogicLossy :: CASL_DL2CASL -> CASL_DL_SL Source # minSourceTheory :: CASL_DL2CASL -> Maybe (LibName, String) Source # targetLogic :: CASL_DL2CASL -> CASL Source # mapSublogic :: CASL_DL2CASL -> CASL_DL_SL -> Maybe CASL_Sublogics Source # map_theory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL_DL2CASL -> DLMor -> Result CASLMor Source # map_sentence :: CASL_DL2CASL -> DLSign -> DLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL_DL2CASL -> DLSign -> Symbol -> Set Symbol Source # extractModel :: CASL_DL2CASL -> DLSign -> ProofTree -> Result (DLSign, [Named DLFORMULA]) Source # is_model_transportable :: CASL_DL2CASL -> Bool Source # has_model_expansion :: CASL_DL2CASL -> Bool Source # is_weakly_amalgamable :: CASL_DL2CASL -> Bool Source # constituents :: CASL_DL2CASL -> [String] Source # isInclusionComorphism :: CASL_DL2CASL -> Bool Source # rps :: CASL_DL2CASL -> Bool Source # eps :: CASL_DL2CASL -> Bool Source # isGTC :: CASL_DL2CASL -> Bool Source #
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSERefine Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source # isGTC :: CASL2VSERefine -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSEImport Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source # isGTC :: CASL2VSEImport -> Bool Source #
Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSE Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source # isGTC :: CASL2VSE -> Bool Source #
Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics) (CompComorphism CASL2Modal Modal2CASL) CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Modifications.ModalEmbedding Methods tauSigma :: MODAL_EMBEDDING -> CASLSign -> Result CASLMor Source # sourceComorphism :: MODAL_EMBEDDING -> InclComorphism CASL CASL_Sublogics Source # targetComorphism :: MODAL_EMBEDDING -> CompComorphism CASL2Modal Modal2CASL Source #
Show a => Syntax (GenCspCASL a) CspBasicSpec CspSymbol CspSymbItems CspSymbMapItems Source #	Syntax of CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods parsersAndPrinters :: GenCspCASL a -> Map String (PrefixMap -> AParser st CspBasicSpec, CspBasicSpec -> Doc) Source # parse_basic_spec :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspBasicSpec) Source # parseSingleSymbItem :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbItems) Source # parse_symb_items :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbItems) Source # parse_symb_map_items :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbMapItems) Source # toItem :: GenCspCASL a -> CspBasicSpec -> Item Source # symb_items_name :: GenCspCASL a -> CspSymbItems -> [String] Source #
Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol Source #	Static Analysis for CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods basic_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])) Source # sen_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, CspCASLSen) -> Result CspCASLSen) Source # extBasicAnalysis :: GenCspCASL a -> IRI -> LibName -> CspBasicSpec -> CspCASLSign -> GlobalAnnos -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]) Source # stat_symb_map_items :: GenCspCASL a -> CspCASLSign -> Maybe CspCASLSign -> [CspSymbMapItems] -> Result (EndoMap CspRawSymbol) Source # stat_symb_items :: GenCspCASL a -> CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol] Source # convertTheory :: GenCspCASL a -> Maybe ((CspCASLSign, [Named CspCASLSen]) -> CspBasicSpec) Source # ensures_amalgamability :: GenCspCASL a -> ([CASLAmalgOpt], Gr CspCASLSign (Int, CspCASLMorphism), [(Int, CspCASLMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: GenCspCASL a -> CspCASLMorphism -> [Named CspCASLSen] -> Result (CspCASLSign, [Named CspCASLSen]) Source # signature_colimit :: GenCspCASL a -> Gr CspCASLSign (Int, CspCASLMorphism) -> Result (CspCASLSign, Map Int CspCASLMorphism) Source # qualify :: GenCspCASL a -> SIMPLE_ID -> LibName -> CspCASLMorphism -> CspCASLSign -> Result (CspCASLMorphism, [Named CspCASLSen]) Source # symbol_to_raw :: GenCspCASL a -> CspSymbol -> CspRawSymbol Source # id_to_raw :: GenCspCASL a -> Id -> CspRawSymbol Source # matches :: GenCspCASL a -> CspSymbol -> CspRawSymbol -> Bool Source # empty_signature :: GenCspCASL a -> CspCASLSign Source # add_symb_to_sign :: GenCspCASL a -> CspCASLSign -> CspSymbol -> Result CspCASLSign Source # signature_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # signatureDiff :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # intersection :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # final_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source # morphism_union :: GenCspCASL a -> CspCASLMorphism -> CspCASLMorphism -> Result CspCASLMorphism Source # is_subsig :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Bool Source # subsig_inclusion :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism Source # generated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source # cogenerated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source # induced_from_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> CspCASLSign -> Result CspCASLMorphism Source # induced_from_to_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> ExtSign CspCASLSign CspSymbol -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism Source # is_transportable :: GenCspCASL a -> CspCASLMorphism -> Bool Source # is_injective :: GenCspCASL a -> CspCASLMorphism -> Bool Source # theory_to_taxonomy :: GenCspCASL a -> TaxoGraphKind -> MMiSSOntology -> CspCASLSign -> [Named CspCASLSen] -> Result MMiSSOntology Source # corresp2th :: GenCspCASL a -> String -> Bool -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> EndoMap CspSymbol -> EndoMap CspSymbol -> REL_REF -> Result (CspCASLSign, [Named CspCASLSen], CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source # equiv2cospan :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> Result (CspCASLSign, CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source # extract_module :: GenCspCASL a -> [IRI] -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #
CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #	Instance of Logic for CspCASL
Instance details Defined in CspCASL.Logic_CspCASL Methods parse_basic_sen :: GenCspCASL a -> Maybe (CspBasicSpec -> AParser st CspCASLSen) Source # stability :: GenCspCASL a -> Stability Source # data_logic :: GenCspCASL a -> Maybe AnyLogic Source # top_sublogic :: GenCspCASL a -> () Source # all_sublogics :: GenCspCASL a -> [()] Source # bottomSublogic :: GenCspCASL a -> Maybe () Source # sublogicDimensions :: GenCspCASL a -> [[()]] Source # parseSublogic :: GenCspCASL a -> String -> Maybe () Source # proj_sublogic_epsilon :: GenCspCASL a -> () -> CspCASLSign -> CspCASLMorphism Source # provers :: GenCspCASL a -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()] Source # default_prover :: GenCspCASL a -> String Source # cons_checkers :: GenCspCASL a -> [ConsChecker CspCASLSign CspCASLSen () CspCASLMorphism ()] Source # conservativityCheck :: GenCspCASL a -> [ConservativityChecker CspCASLSign CspCASLSen CspCASLMorphism] Source # empty_proof_tree :: GenCspCASL a -> () Source # syntaxTable :: GenCspCASL a -> CspCASLSign -> Maybe SyntaxTable Source # omdoc_metatheory :: GenCspCASL a -> Maybe OMCD Source # export_symToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspSymbol -> String -> Result TCElement Source # export_senToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspCASLSen -> Result TCorOMElement Source # export_theoryToOmdoc :: GenCspCASL a -> SigMap CspSymbol -> CspCASLSign -> [Named CspCASLSen] -> Result [TCElement] Source # omdocToSym :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result CspSymbol Source # omdocToSen :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result (Maybe (Named CspCASLSen)) Source # addOMadtToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [[OmdADT]] -> Result (CspCASLSign, [Named CspCASLSen]) Source # addOmdocToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [TCElement] -> Result (CspCASLSign, [Named CspCASLSen]) Source # sublogicOfTheo :: GenCspCASL a -> (CspCASLSign, [CspCASLSen]) -> () Source #
(MinSL a f, MinSL a s, MinSL a b, ProjForm a f, ProjSigItem a s f, ProjBasic a b s f) => ProjectSublogic (CASL_SL a) (BASIC_SPEC b s f) Source #
Instance details Defined in CASL.Logic_CASL Methods projectSublogic :: CASL_SL a -> BASIC_SPEC b s f -> BASIC_SPEC b s f Source #
(MinSL a f, MinSL a s, MinSL a b) => MinSublogic (CASL_SL a) (BASIC_SPEC b s f) Source #
Instance details Defined in CASL.Logic_CASL Methods minSublogic :: BASIC_SPEC b s f -> CASL_SL a Source #
(CspCASLSemantics a, CspCASLSemantics b) => Comorphism (CspCASL2CspCASL a b) (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () (GenCspCASL b) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #
Instance details Defined in CspCASL.Comorphisms Methods sourceLogic :: CspCASL2CspCASL a b -> GenCspCASL a Source # sourceSublogic :: CspCASL2CspCASL a b -> () Source # sourceSublogicLossy :: CspCASL2CspCASL a b -> () Source # minSourceTheory :: CspCASL2CspCASL a b -> Maybe (LibName, String) Source # targetLogic :: CspCASL2CspCASL a b -> GenCspCASL b Source # mapSublogic :: CspCASL2CspCASL a b -> () -> Maybe () Source # map_theory :: CspCASL2CspCASL a b -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # mapMarkedTheory :: CspCASL2CspCASL a b -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source # map_morphism :: CspCASL2CspCASL a b -> CspCASLMorphism -> Result CspCASLMorphism Source # map_sentence :: CspCASL2CspCASL a b -> CspCASLSign -> CspCASLSen -> Result CspCASLSen Source # map_symbol :: CspCASL2CspCASL a b -> CspCASLSign -> CspSymbol -> Set CspSymbol Source # extractModel :: CspCASL2CspCASL a b -> CspCASLSign -> () -> Result (CspCASLSign, [Named CspCASLSen]) Source # is_model_transportable :: CspCASL2CspCASL a b -> Bool Source # has_model_expansion :: CspCASL2CspCASL a b -> Bool Source # is_weakly_amalgamable :: CspCASL2CspCASL a b -> Bool Source # constituents :: CspCASL2CspCASL a b -> [String] Source # isInclusionComorphism :: CspCASL2CspCASL a b -> Bool Source # rps :: CspCASL2CspCASL a b -> Bool Source # eps :: CspCASL2CspCASL a b -> Bool Source # isGTC :: CspCASL2CspCASL a b -> Bool Source #
(Data b, Data s, Data f) => Data (BASIC_SPEC b s f) Source #
Instance details Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> BASIC_SPEC b s f -> c (BASIC_SPEC b s f) gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (BASIC_SPEC b s f) toConstr :: BASIC_SPEC b s f -> Constr dataTypeOf :: BASIC_SPEC b s f -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (BASIC_SPEC b s f)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (BASIC_SPEC b s f)) gmapT :: (forall b0. Data b0 => b0 -> b0) -> BASIC_SPEC b s f -> BASIC_SPEC b s f gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC b s f -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC b s f -> r gmapQ :: (forall d. Data d => d -> u) -> BASIC_SPEC b s f -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_SPEC b s f -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_SPEC b s f -> m (BASIC_SPEC b s f) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC b s f -> m (BASIC_SPEC b s f) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC b s f -> m (BASIC_SPEC b s f)
(Show s, Show f, Show b) => Show (BASIC_SPEC b s f) Source #
Instance details Defined in CASL.AS_Basic_CASL Methods showsPrec :: Int -> BASIC_SPEC b s f -> ShowS show :: BASIC_SPEC b s f -> String showList :: [BASIC_SPEC b s f] -> ShowS
Generic (BASIC_SPEC b s f)
Instance details Defined in CASL.ATC_CASL Associated Types type Rep (BASIC_SPEC b s f) :: Type -> Type Methods from :: BASIC_SPEC b s f -> Rep (BASIC_SPEC b s f) x to :: Rep (BASIC_SPEC b s f) x -> BASIC_SPEC b s f
Semigroup (BASIC_SPEC b s f)
Instance details Defined in CASL.Logic_CASL Methods (<>) :: BASIC_SPEC b s f -> BASIC_SPEC b s f -> BASIC_SPEC b s f # sconcat :: NonEmpty (BASIC_SPEC b s f) -> BASIC_SPEC b s f stimes :: Integral b0 => b0 -> BASIC_SPEC b s f -> BASIC_SPEC b s f
Monoid (BASIC_SPEC b s f)
Instance details Defined in CASL.Logic_CASL Methods mempty :: BASIC_SPEC b s f mappend :: BASIC_SPEC b s f -> BASIC_SPEC b s f -> BASIC_SPEC b s f mconcat :: [BASIC_SPEC b s f] -> BASIC_SPEC b s f
(GetRange b, GetRange s, GetRange f) => GetRange (BASIC_SPEC b s f) Source #
Instance details Defined in CASL.AS_Basic_CASL Methods getRange :: BASIC_SPEC b s f -> Range Source # rangeSpan :: BASIC_SPEC b s f -> [Pos] Source #
(FromJSON b, FromJSON s, FromJSON f) => FromJSON (BASIC_SPEC b s f)
Instance details Defined in CASL.ATC_CASL Methods parseJSON :: Value -> Parser (BASIC_SPEC b s f) parseJSONList :: Value -> Parser [BASIC_SPEC b s f]
(ToJSON b, ToJSON s, ToJSON f) => ToJSON (BASIC_SPEC b s f)
Instance details Defined in CASL.ATC_CASL Methods toJSON :: BASIC_SPEC b s f -> Value toEncoding :: BASIC_SPEC b s f -> Encoding toJSONList :: [BASIC_SPEC b s f] -> Value toEncodingList :: [BASIC_SPEC b s f] -> Encoding
(ShATermConvertible b, ShATermConvertible s, ShATermConvertible f) => ShATermConvertible (BASIC_SPEC b s f)
Instance details Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> BASIC_SPEC b s f -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BASIC_SPEC b s f] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC b s f) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_SPEC b s f])
(Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_SPEC b s f) Source #
Instance details Defined in CASL.ToDoc Methods pretty :: BASIC_SPEC b s f -> Doc Source # pretties :: [BASIC_SPEC b s f] -> Doc Source #
ATermConvertibleSML (BASIC_SPEC a b c) Source #
Instance details Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> BASIC_SPEC a b c from_sml_ShATermList :: ATermTable -> [BASIC_SPEC a b c]
type Rep (BASIC_SPEC b s f)
Instance details Defined in CASL.ATC_CASL type Rep (BASIC_SPEC b s f) = D1 ('MetaData "BASIC_SPEC" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Basic_spec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (BASIC_ITEMS b s f)])))

data BASIC_ITEMS b s f Source #

Constructors

Sig_items (SIG_ITEMS s f)
Free_datatype SortsKind [Annoted DATATYPE_DECL] Range
Sort_gen [Annoted (SIG_ITEMS s f)] Range
Var_items [VAR_DECL] Range
Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] Range
Axiom_items [Annoted (FORMULA f)] Range
Ext_BASIC_ITEMS b

Instances

Instances details

(Data b, Data s, Data f) => Data (BASIC_ITEMS b s f) Source #
Instance details Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> BASIC_ITEMS b s f -> c (BASIC_ITEMS b s f) gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (BASIC_ITEMS b s f) toConstr :: BASIC_ITEMS b s f -> Constr dataTypeOf :: BASIC_ITEMS b s f -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (BASIC_ITEMS b s f)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (BASIC_ITEMS b s f)) gmapT :: (forall b0. Data b0 => b0 -> b0) -> BASIC_ITEMS b s f -> BASIC_ITEMS b s f gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEMS b s f -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEMS b s f -> r gmapQ :: (forall d. Data d => d -> u) -> BASIC_ITEMS b s f -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_ITEMS b s f -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_ITEMS b s f -> m (BASIC_ITEMS b s f) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEMS b s f -> m (BASIC_ITEMS b s f) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEMS b s f -> m (BASIC_ITEMS b s f)
(Show s, Show f, Show b) => Show (BASIC_ITEMS b s f) Source #
Instance details Defined in CASL.AS_Basic_CASL Methods showsPrec :: Int -> BASIC_ITEMS b s f -> ShowS show :: BASIC_ITEMS b s f -> String showList :: [BASIC_ITEMS b s f] -> ShowS
Generic (BASIC_ITEMS b s f)
Instance details Defined in CASL.ATC_CASL Associated Types type Rep (BASIC_ITEMS b s f) :: Type -> Type Methods from :: BASIC_ITEMS b s f -> Rep (BASIC_ITEMS b s f) x to :: Rep (BASIC_ITEMS b s f) x -> BASIC_ITEMS b s f
(GetRange b, GetRange s, GetRange f) => GetRange (BASIC_ITEMS b s f) Source #
Instance details Defined in CASL.AS_Basic_CASL Methods getRange :: BASIC_ITEMS b s f -> Range Source # rangeSpan :: BASIC_ITEMS b s f -> [Pos] Source #
(FromJSON b, FromJSON s, FromJSON f) => FromJSON (BASIC_ITEMS b s f)
Instance details Defined in CASL.ATC_CASL Methods parseJSON :: Value -> Parser (BASIC_ITEMS b s f) parseJSONList :: Value -> Parser [BASIC_ITEMS b s f]
(ToJSON b, ToJSON s, ToJSON f) => ToJSON (BASIC_ITEMS b s f)
Instance details Defined in CASL.ATC_CASL Methods toJSON :: BASIC_ITEMS b s f -> Value toEncoding :: BASIC_ITEMS b s f -> Encoding toJSONList :: [BASIC_ITEMS b s f] -> Value toEncodingList :: [BASIC_ITEMS b s f] -> Encoding
(ShATermConvertible b, ShATermConvertible s, ShATermConvertible f) => ShATermConvertible (BASIC_ITEMS b s f)
Instance details Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> BASIC_ITEMS b s f -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BASIC_ITEMS b s f] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_ITEMS b s f) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_ITEMS b s f])
(Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_ITEMS b s f) Source #
Instance details Defined in CASL.ToDoc Methods pretty :: BASIC_ITEMS b s f -> Doc Source # pretties :: [BASIC_ITEMS b s f] -> Doc Source #
ATermConvertibleSML (BASIC_ITEMS a b c) Source #
Instance details Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> BASIC_ITEMS a b c from_sml_ShATermList :: ATermTable -> [BASIC_ITEMS a b c]
type Rep (BASIC_ITEMS b s f)
Instance details Defined in CASL.ATC_CASL type Rep (BASIC_ITEMS b s f) = D1 ('MetaData "BASIC_ITEMS" "CASL.AS_Basic_CASL" "main" 'False) ((C1 ('MetaCons "Sig_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SIG_ITEMS s f))) :+: (C1 ('MetaCons "Free_datatype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SortsKind) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted DATATYPE_DECL]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Sort_gen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (SIG_ITEMS s f)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "Var_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_DECL]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Local_var_axioms" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_DECL]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (FORMULA f)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "Axiom_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (FORMULA f)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Ext_BASIC_ITEMS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)))))

data SortsKind Source #

Constructors

NonEmptySorts
PossiblyEmptySorts

Instances

Instances details

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

data SIG_ITEMS s f Source #

Constructors

Sort_items SortsKind [Annoted (SORT_ITEM f)] Range
Op_items [Annoted (OP_ITEM f)] Range
Pred_items [Annoted (PRED_ITEM f)] Range
Datatype_items SortsKind [Annoted DATATYPE_DECL] Range
Ext_SIG_ITEMS s

Instances

Instances details