Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder Till Mossakowski and Uni Bremen 2002-2004
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (MPTC+FD)
Safe HaskellNone

CASL.Morphism

Description

Symbols and signature morphisms for the CASL logic

Synopsis

Documentation

data RawSymbol Source #

Instances

Eq RawSymbol Source # 

Methods

(==) :: RawSymbol -> RawSymbol -> Bool

(/=) :: RawSymbol -> RawSymbol -> Bool

Data RawSymbol Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RawSymbol -> c RawSymbol

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RawSymbol

toConstr :: RawSymbol -> Constr

dataTypeOf :: RawSymbol -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c RawSymbol)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol)

gmapT :: (forall b. Data b => b -> b) -> RawSymbol -> RawSymbol

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r

gmapQ :: (forall d. Data d => d -> u) -> RawSymbol -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> RawSymbol -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol

Ord RawSymbol Source # 

Methods

compare :: RawSymbol -> RawSymbol -> Ordering

(<) :: RawSymbol -> RawSymbol -> Bool

(<=) :: RawSymbol -> RawSymbol -> Bool

(>) :: RawSymbol -> RawSymbol -> Bool

(>=) :: RawSymbol -> RawSymbol -> Bool

max :: RawSymbol -> RawSymbol -> RawSymbol

min :: RawSymbol -> RawSymbol -> RawSymbol

Show RawSymbol Source # 

Methods

showsPrec :: Int -> RawSymbol -> ShowS

show :: RawSymbol -> String

showList :: [RawSymbol] -> ShowS

GetRange RawSymbol Source # 
Pretty RawSymbol Source # 
StaticAnalysis CASL CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol Source # 

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 CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol Source # 

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 COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source # 

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 CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # 

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 ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol Source # 

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 ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source # 

Methods

basic_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, GlobalAnnos) -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA])) Source #

sen_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, ExtModalFORMULA) -> Result ExtModalFORMULA) Source #

extBasicAnalysis :: ExtModal -> IRI -> LibName -> EM_BASIC_SPEC -> ExtModalSign -> GlobalAnnos -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA]) Source #

stat_symb_map_items :: ExtModal -> ExtModalSign -> Maybe ExtModalSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: ExtModal -> ExtModalSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: ExtModal -> Maybe ((ExtModalSign, [Named ExtModalFORMULA]) -> EM_BASIC_SPEC) Source #

ensures_amalgamability :: ExtModal -> ([CASLAmalgOpt], Gr ExtModalSign (Int, ExtModalMorph), [(Int, ExtModalMorph)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: ExtModal -> ExtModalMorph -> [Named ExtModalFORMULA] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

signature_colimit :: ExtModal -> Gr ExtModalSign (Int, ExtModalMorph) -> Result (ExtModalSign, Map Int ExtModalMorph) Source #

qualify :: ExtModal -> SIMPLE_ID -> LibName -> ExtModalMorph -> ExtModalSign -> Result (ExtModalMorph, [Named ExtModalFORMULA]) Source #

symbol_to_raw :: ExtModal -> Symbol -> RawSymbol Source #

id_to_raw :: ExtModal -> Id -> RawSymbol Source #

matches :: ExtModal -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: ExtModal -> ExtModalSign Source #

add_symb_to_sign :: ExtModal -> ExtModalSign -> Symbol -> Result ExtModalSign Source #

signature_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

signatureDiff :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

intersection :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

final_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

morphism_union :: ExtModal -> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph Source #

is_subsig :: ExtModal -> ExtModalSign -> ExtModalSign -> Bool Source #

subsig_inclusion :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalMorph Source #

generated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source #

cogenerated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source #

induced_from_morphism :: ExtModal -> EndoMap RawSymbol -> ExtModalSign -> Result ExtModalMorph Source #

induced_from_to_morphism :: ExtModal -> EndoMap RawSymbol -> ExtSign ExtModalSign Symbol -> ExtSign ExtModalSign Symbol -> Result ExtModalMorph Source #

is_transportable :: ExtModal -> ExtModalMorph -> Bool Source #

is_injective :: ExtModal -> ExtModalMorph -> Bool Source #

theory_to_taxonomy :: ExtModal -> TaxoGraphKind -> MMiSSOntology -> ExtModalSign -> [Named ExtModalFORMULA] -> Result MMiSSOntology Source #

corresp2th :: ExtModal -> String -> Bool -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ExtModalSign, [Named ExtModalFORMULA], ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: ExtModal -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ExtModalSign, ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: ExtModal -> [IRI] -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source # 

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 Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol Source # 

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 Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source # 

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 VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 

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 #

StaticAnalysis Hybridize Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol Source # 

Methods

basic_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, GlobalAnnos) -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])) Source #

sen_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap) Source #

extBasicAnalysis :: Hybridize -> IRI -> LibName -> Spc_Wrap -> Sgn_Wrap -> GlobalAnnos -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]) Source #

stat_symb_map_items :: Hybridize -> Sgn_Wrap -> Maybe Sgn_Wrap -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Hybridize -> Sgn_Wrap -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Hybridize -> Maybe ((Sgn_Wrap, [Named Frm_Wrap]) -> Spc_Wrap) Source #

ensures_amalgamability :: Hybridize -> ([CASLAmalgOpt], Gr Sgn_Wrap (Int, Mor), [(Int, Mor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Hybridize -> Mor -> [Named Frm_Wrap] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #

signature_colimit :: Hybridize -> Gr Sgn_Wrap (Int, Mor) -> Result (Sgn_Wrap, Map Int Mor) Source #

qualify :: Hybridize -> SIMPLE_ID -> LibName -> Mor -> Sgn_Wrap -> Result (Mor, [Named Frm_Wrap]) Source #

symbol_to_raw :: Hybridize -> Symbol -> RawSymbol Source #

id_to_raw :: Hybridize -> Id -> RawSymbol Source #

matches :: Hybridize -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Hybridize -> Sgn_Wrap Source #

add_symb_to_sign :: Hybridize -> Sgn_Wrap -> Symbol -> Result Sgn_Wrap Source #

signature_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source #

signatureDiff :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source #

intersection :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source #

final_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source #

morphism_union :: Hybridize -> Mor -> Mor -> Result Mor Source #

is_subsig :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Bool Source #

subsig_inclusion :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Mor Source #

generated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source #

cogenerated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source #

induced_from_morphism :: Hybridize -> EndoMap RawSymbol -> Sgn_Wrap -> Result Mor Source #

induced_from_to_morphism :: Hybridize -> EndoMap RawSymbol -> ExtSign Sgn_Wrap Symbol -> ExtSign Sgn_Wrap Symbol -> Result Mor Source #

is_transportable :: Hybridize -> Mor -> Bool Source #

is_injective :: Hybridize -> Mor -> Bool Source #

theory_to_taxonomy :: Hybridize -> TaxoGraphKind -> MMiSSOntology -> Sgn_Wrap -> [Named Frm_Wrap] -> Result MMiSSOntology Source #

corresp2th :: Hybridize -> String -> Bool -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sgn_Wrap, [Named Frm_Wrap], Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sgn_Wrap, Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Hybridize -> [IRI] -> (Sgn_Wrap, [Named Frm_Wrap]) -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #

Logic CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 

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 #

Logic CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree Source # 

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 #

Logic COL () C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol () Source # 

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 #

Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 

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 #

Logic ConstraintCASL CASL_Sublogics ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol () Source # 

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 #

Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: ExtModal -> Maybe (EM_BASIC_SPEC -> AParser st ExtModalFORMULA) Source #

stability :: ExtModal -> Stability Source #

data_logic :: ExtModal -> Maybe AnyLogic Source #

top_sublogic :: ExtModal -> ExtModalSL Source #

all_sublogics :: ExtModal -> [ExtModalSL] Source #

bottomSublogic :: ExtModal -> Maybe ExtModalSL Source #

sublogicDimensions :: ExtModal -> [[ExtModalSL]] Source #

parseSublogic :: ExtModal -> String -> Maybe ExtModalSL Source #

proj_sublogic_epsilon :: ExtModal -> ExtModalSL -> ExtModalSign -> ExtModalMorph Source #

provers :: ExtModal -> [Prover ExtModalSign ExtModalFORMULA ExtModalMorph ExtModalSL ()] Source #

default_prover :: ExtModal -> String Source #

cons_checkers :: ExtModal -> [ConsChecker ExtModalSign ExtModalFORMULA ExtModalSL ExtModalMorph ()] Source #

conservativityCheck :: ExtModal -> [ConservativityChecker ExtModalSign ExtModalFORMULA ExtModalMorph] Source #

empty_proof_tree :: ExtModal -> () Source #

syntaxTable :: ExtModal -> ExtModalSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: ExtModal -> Maybe OMCD Source #

export_symToOmdoc :: ExtModal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: ExtModal -> NameMap Symbol -> ExtModalFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: ExtModal -> SigMap Symbol -> ExtModalSign -> [Named ExtModalFORMULA] -> Result [TCElement] Source #

omdocToSym :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ExtModalFORMULA)) Source #

addOMadtToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [[OmdADT]] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

addOmdocToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [TCElement] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

Logic Fpl () FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol () Source # 

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 #

Logic Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source # 

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 #

Logic Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 

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 #

Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 

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 #

Logic Hybridize () Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: Hybridize -> Maybe (Spc_Wrap -> AParser st Frm_Wrap) Source #

stability :: Hybridize -> Stability Source #

data_logic :: Hybridize -> Maybe AnyLogic Source #

top_sublogic :: Hybridize -> () Source #

all_sublogics :: Hybridize -> [()] Source #

bottomSublogic :: Hybridize -> Maybe () Source #

sublogicDimensions :: Hybridize -> [[()]] Source #

parseSublogic :: Hybridize -> String -> Maybe () Source #

proj_sublogic_epsilon :: Hybridize -> () -> Sgn_Wrap -> Mor Source #

provers :: Hybridize -> [Prover Sgn_Wrap Frm_Wrap Mor () ()] Source #

default_prover :: Hybridize -> String Source #

cons_checkers :: Hybridize -> [ConsChecker Sgn_Wrap Frm_Wrap () Mor ()] Source #

conservativityCheck :: Hybridize -> [ConservativityChecker Sgn_Wrap Frm_Wrap Mor] Source #

empty_proof_tree :: Hybridize -> () Source #

syntaxTable :: Hybridize -> Sgn_Wrap -> Maybe SyntaxTable Source #

omdoc_metatheory :: Hybridize -> Maybe OMCD Source #

export_symToOmdoc :: Hybridize -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Hybridize -> NameMap Symbol -> Frm_Wrap -> Result TCorOMElement Source #

export_theoryToOmdoc :: Hybridize -> SigMap Symbol -> Sgn_Wrap -> [Named Frm_Wrap] -> Result [TCElement] Source #

omdocToSym :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Frm_Wrap)) Source #

addOMadtToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [[OmdADT]] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #

addOmdocToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [TCElement] -> Result (Sgn_Wrap, [Named Frm_Wrap]) 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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree 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 # 
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 # 
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 # 
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 # 
Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 

Methods

sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source #

sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source #

minSourceTheory :: ExtModal2ExtModalNoSubsorts -> Maybe (LibName, String) Source #

targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source #

mapSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL -> Maybe ExtModalSL Source #

map_theory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

mapMarkedTheory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

map_morphism :: ExtModal2ExtModalNoSubsorts -> ExtModalMorph -> Result ExtModalMorph Source #

map_sentence :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source #

map_symbol :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> Symbol -> Set Symbol Source #

extractModel :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source #

has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source #

is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source #

constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source #

isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source #

rps :: ExtModal2ExtModalNoSubsorts -> Bool Source #

eps :: ExtModal2ExtModalNoSubsorts -> Bool Source #

Comorphism ExtModal2ExtModalTotal ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 
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 # 

data Morphism f e m Source #

Constructors

Morphism 

Instances

Sentences CASL CASLFORMULA CASLSign CASLMor Symbol Source # 
Sentences CASL_DL DLFORMULA DLSign DLMor Symbol Source # 
Sentences COL COLFORMULA CSign COLMor Symbol Source # 
Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol Source # 
Sentences ConstraintCASL ConstraintCASLFORMULA ConstraintCASLSign ConstraintCASLMor Symbol Source # 
Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol Source # 
Sentences Fpl FplForm FplSign FplMor Symbol Source # 
Sentences Hybrid HybridFORMULA HSign HybridMor Symbol Source # 
Sentences Modal ModalFORMULA MSign ModalMor Symbol Source # 
Sentences VSE Sentence VSESign VSEMor Symbol Source # 
StaticAnalysis CASL CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol Source # 

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 CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol Source # 

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 COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source # 

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 CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # 

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 ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol Source # 

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 ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source # 

Methods

basic_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, GlobalAnnos) -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA])) Source #

sen_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, ExtModalFORMULA) -> Result ExtModalFORMULA) Source #

extBasicAnalysis :: ExtModal -> IRI -> LibName -> EM_BASIC_SPEC -> ExtModalSign -> GlobalAnnos -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA]) Source #

stat_symb_map_items :: ExtModal -> ExtModalSign -> Maybe ExtModalSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: ExtModal -> ExtModalSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: ExtModal -> Maybe ((ExtModalSign, [Named ExtModalFORMULA]) -> EM_BASIC_SPEC) Source #

ensures_amalgamability :: ExtModal -> ([CASLAmalgOpt], Gr ExtModalSign (Int, ExtModalMorph), [(Int, ExtModalMorph)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: ExtModal -> ExtModalMorph -> [Named ExtModalFORMULA] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

signature_colimit :: ExtModal -> Gr ExtModalSign (Int, ExtModalMorph) -> Result (ExtModalSign, Map Int ExtModalMorph) Source #

qualify :: ExtModal -> SIMPLE_ID -> LibName -> ExtModalMorph -> ExtModalSign -> Result (ExtModalMorph, [Named ExtModalFORMULA]) Source #

symbol_to_raw :: ExtModal -> Symbol -> RawSymbol Source #

id_to_raw :: ExtModal -> Id -> RawSymbol Source #

matches :: ExtModal -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: ExtModal -> ExtModalSign Source #

add_symb_to_sign :: ExtModal -> ExtModalSign -> Symbol -> Result ExtModalSign Source #

signature_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

signatureDiff :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

intersection :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

final_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

morphism_union :: ExtModal -> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph Source #

is_subsig :: ExtModal -> ExtModalSign -> ExtModalSign -> Bool Source #

subsig_inclusion :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalMorph Source #

generated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source #

cogenerated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source #

induced_from_morphism :: ExtModal -> EndoMap RawSymbol -> ExtModalSign -> Result ExtModalMorph Source #

induced_from_to_morphism :: ExtModal -> EndoMap RawSymbol -> ExtSign ExtModalSign Symbol -> ExtSign ExtModalSign Symbol -> Result ExtModalMorph Source #

is_transportable :: ExtModal -> ExtModalMorph -> Bool Source #

is_injective :: ExtModal -> ExtModalMorph -> Bool Source #

theory_to_taxonomy :: ExtModal -> TaxoGraphKind -> MMiSSOntology -> ExtModalSign -> [Named ExtModalFORMULA] -> Result MMiSSOntology Source #

corresp2th :: ExtModal -> String -> Bool -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ExtModalSign, [Named ExtModalFORMULA], ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: ExtModal -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ExtModalSign, ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: ExtModal -> [IRI] -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source # 

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 Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol Source # 

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 Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source # 

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 VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 

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 # 

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 #

Logic CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree Source # 

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 #

Logic COL () C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol () Source # 

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 #

Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 

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 #

Logic ConstraintCASL CASL_Sublogics ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol () Source # 

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 #

Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: ExtModal -> Maybe (EM_BASIC_SPEC -> AParser st ExtModalFORMULA) Source #

stability :: ExtModal -> Stability Source #

data_logic :: ExtModal -> Maybe AnyLogic Source #

top_sublogic :: ExtModal -> ExtModalSL Source #

all_sublogics :: ExtModal -> [ExtModalSL] Source #

bottomSublogic :: ExtModal -> Maybe ExtModalSL Source #

sublogicDimensions :: ExtModal -> [[ExtModalSL]] Source #

parseSublogic :: ExtModal -> String -> Maybe ExtModalSL Source #

proj_sublogic_epsilon :: ExtModal -> ExtModalSL -> ExtModalSign -> ExtModalMorph Source #

provers :: ExtModal -> [Prover ExtModalSign ExtModalFORMULA ExtModalMorph ExtModalSL ()] Source #

default_prover :: ExtModal -> String Source #

cons_checkers :: ExtModal -> [ConsChecker ExtModalSign ExtModalFORMULA ExtModalSL ExtModalMorph ()] Source #

conservativityCheck :: ExtModal -> [ConservativityChecker ExtModalSign ExtModalFORMULA ExtModalMorph] Source #

empty_proof_tree :: ExtModal -> () Source #

syntaxTable :: ExtModal -> ExtModalSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: ExtModal -> Maybe OMCD Source #

export_symToOmdoc :: ExtModal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: ExtModal -> NameMap Symbol -> ExtModalFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: ExtModal -> SigMap Symbol -> ExtModalSign -> [Named ExtModalFORMULA] -> Result [TCElement] Source #

omdocToSym :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ExtModalFORMULA)) Source #

addOMadtToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [[OmdADT]] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

addOmdocToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [TCElement] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

Logic Fpl () FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol () Source #