Methods

showsPrec :: Int -> CASL_DL -> ShowS

show :: CASL_DL -> String

showList :: [CASL_DL] -> ShowS

Methods

language_name :: CASL_DL -> String Source #

description :: CASL_DL -> String Source #

Methods

map_sen :: CASL_DL -> DLMor -> DLFORMULA -> Result DLFORMULA Source #

simplify_sen :: CASL_DL -> DLSign -> DLFORMULA -> DLFORMULA Source #

negation :: CASL_DL -> DLFORMULA -> Maybe DLFORMULA Source #

print_sign :: CASL_DL -> DLSign -> Doc Source #

print_named :: CASL_DL -> Named DLFORMULA -> Doc Source #

sym_of :: CASL_DL -> DLSign -> [Set Symbol] Source #

mostSymsOf :: CASL_DL -> DLSign -> [Symbol] Source #

symmap_of :: CASL_DL -> DLMor -> EndoMap Symbol Source #

sym_name :: CASL_DL -> Symbol -> Id Source #

sym_label :: CASL_DL -> Symbol -> Maybe String Source #

fullSymName :: CASL_DL -> Symbol -> String Source #

symKind :: CASL_DL -> Symbol -> String Source #

symsOfSen :: CASL_DL -> DLSign -> DLFORMULA -> [Symbol] Source #

pair_symbols :: CASL_DL -> Symbol -> Symbol -> Result Symbol Source #

Methods

parsersAndPrinters :: CASL_DL -> Map String (PrefixMap -> AParser st DL_BASIC_SPEC, DL_BASIC_SPEC -> Doc) Source #

parse_basic_spec :: CASL_DL -> Maybe (PrefixMap -> AParser st DL_BASIC_SPEC) Source #

parseSingleSymbItem :: CASL_DL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source #

parse_symb_items :: CASL_DL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source #

parse_symb_map_items :: CASL_DL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source #

toItem :: CASL_DL -> DL_BASIC_SPEC -> Item Source #

symb_items_name :: CASL_DL -> SYMB_ITEMS -> [String] Source #

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 #

Methods

parse_basic_sen :: CASL_DL -> Maybe (DL_BASIC_SPEC -> AParser st DLFORMULA) Source #

stability :: CASL_DL -> Stability Source #

data_logic :: CASL_DL -> Maybe AnyLogic Source #

top_sublogic :: CASL_DL -> CASL_DL_SL Source #

all_sublogics :: CASL_DL -> [CASL_DL_SL] Source #

bottomSublogic :: CASL_DL -> Maybe CASL_DL_SL Source #

sublogicDimensions :: CASL_DL -> [[CASL_DL_SL]] Source #

parseSublogic :: CASL_DL -> String -> Maybe CASL_DL_SL Source #

proj_sublogic_epsilon :: CASL_DL -> CASL_DL_SL -> DLSign -> DLMor Source #

provers :: CASL_DL -> [Prover DLSign DLFORMULA DLMor CASL_DL_SL ProofTree] Source #

default_prover :: CASL_DL -> String Source #

cons_checkers :: CASL_DL -> [ConsChecker DLSign DLFORMULA CASL_DL_SL DLMor ProofTree] Source #

conservativityCheck :: CASL_DL -> [ConservativityChecker DLSign DLFORMULA DLMor] Source #

empty_proof_tree :: CASL_DL -> ProofTree Source #

syntaxTable :: CASL_DL -> DLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CASL_DL -> Maybe OMCD Source #

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

export_senToOmdoc :: CASL_DL -> NameMap Symbol -> DLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CASL_DL -> SigMap Symbol -> DLSign -> [Named DLFORMULA] -> Result [TCElement] Source #

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

omdocToSen :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named DLFORMULA)) Source #

addOMadtToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [[OmdADT]] -> Result (DLSign, [Named DLFORMULA]) Source #

addOmdocToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [TCElement] -> Result (DLSign, [Named DLFORMULA]) Source #

sublogicOfTheo :: CASL_DL -> (DLSign, [DLFORMULA]) -> CASL_DL_SL Source #

Methods

sourceLogic :: CASL_DL2CASL -> CASL_DL Source #

sourceSublogic :: CASL_DL2CASL -> CASL_DL_SL Source #

sourceSublogicLossy :: CASL_DL2CASL -> CASL_DL_SL Source #

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

targetLogic :: CASL_DL2CASL -> CASL Source #

mapSublogic :: CASL_DL2CASL -> CASL_DL_SL -> Maybe CASL_Sublogics Source #

map_theory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL_DL2CASL -> DLMor -> Result CASLMor Source #

map_sentence :: CASL_DL2CASL -> DLSign -> DLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL_DL2CASL -> DLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL_DL2CASL -> DLSign -> ProofTree -> Result (DLSign, [Named DLFORMULA]) Source #

is_model_transportable :: CASL_DL2CASL -> Bool Source #

has_model_expansion :: CASL_DL2CASL -> Bool Source #

is_weakly_amalgamable :: CASL_DL2CASL -> Bool Source #

constituents :: CASL_DL2CASL -> [String] Source #

isInclusionComorphism :: CASL_DL2CASL -> Bool Source #

rps :: CASL_DL2CASL -> Bool Source #

eps :: CASL_DL2CASL -> Bool Source #

isGTC :: CASL_DL2CASL -> Bool Source #