Hets - the Heterogeneous Tool Set

Copyright(c) Klaus Luettich Christian Maeder Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe

CASL.AS_Basic_CASL

Contents

Description

Abstract Syntax of CASL Basic_specs, Symb_items and Symb_map_items.

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

Synopsis

Documentation

data BASIC_SPEC b s f Source #

Constructors

Basic_spec [Annoted (BASIC_ITEMS b s f)] 

Instances

Syntax CASL CASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax CASL_DL DL_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax COL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax ConstraintCASL ConstraintCASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS 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 # 

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 #

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 # 
Show a => Syntax (GenCspCASL a) CspBasicSpec CspSymbol CspSymbItems CspSymbMapItems Source #

Syntax of CspCASL

Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol Source #

Static Analysis for CspCASL

Methods

basic_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])) Source #

sen_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, CspCASLSen) -> Result CspCASLSen) Source #

extBasicAnalysis :: GenCspCASL a -> IRI -> LibName -> CspBasicSpec -> CspCASLSign -> GlobalAnnos -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]) Source #

stat_symb_map_items :: GenCspCASL a -> CspCASLSign -> Maybe CspCASLSign -> [CspSymbMapItems] -> Result (EndoMap CspRawSymbol) Source #

stat_symb_items :: GenCspCASL a -> CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol] Source #

convertTheory :: GenCspCASL a -> Maybe ((CspCASLSign, [Named CspCASLSen]) -> CspBasicSpec) Source #

ensures_amalgamability :: GenCspCASL a -> ([CASLAmalgOpt], Gr CspCASLSign (Int, CspCASLMorphism), [(Int, CspCASLMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: GenCspCASL a -> CspCASLMorphism -> [Named CspCASLSen] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

signature_colimit :: GenCspCASL a -> Gr CspCASLSign (Int, CspCASLMorphism) -> Result (CspCASLSign, Map Int CspCASLMorphism) Source #

qualify :: GenCspCASL a -> SIMPLE_ID -> LibName -> CspCASLMorphism -> CspCASLSign -> Result (CspCASLMorphism, [Named CspCASLSen]) Source #

symbol_to_raw :: GenCspCASL a -> CspSymbol -> CspRawSymbol Source #

id_to_raw :: GenCspCASL a -> Id -> CspRawSymbol Source #

matches :: GenCspCASL a -> CspSymbol -> CspRawSymbol -> Bool Source #

empty_signature :: GenCspCASL a -> CspCASLSign Source #

add_symb_to_sign :: GenCspCASL a -> CspCASLSign -> CspSymbol -> Result CspCASLSign Source #

signature_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

signatureDiff :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

intersection :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

final_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

morphism_union :: GenCspCASL a -> CspCASLMorphism -> CspCASLMorphism -> Result CspCASLMorphism Source #

is_subsig :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Bool Source #

subsig_inclusion :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism Source #

generated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

cogenerated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

induced_from_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

induced_from_to_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> ExtSign CspCASLSign CspSymbol -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism Source #

is_transportable :: GenCspCASL a -> CspCASLMorphism -> Bool Source #

is_injective :: GenCspCASL a -> CspCASLMorphism -> Bool Source #

theory_to_taxonomy :: GenCspCASL a -> TaxoGraphKind -> MMiSSOntology -> CspCASLSign -> [Named CspCASLSen] -> Result MMiSSOntology Source #

corresp2th :: GenCspCASL a -> String -> Bool -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> EndoMap CspSymbol -> EndoMap CspSymbol -> REL_REF -> Result (CspCASLSign, [Named CspCASLSen], CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source #

equiv2cospan :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> Result (CspCASLSign, CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source #

extract_module :: GenCspCASL a -> [IRI] -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #

CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #

Instance of Logic for CspCASL

Methods

parse_basic_sen :: GenCspCASL a -> Maybe (CspBasicSpec -> AParser st CspCASLSen) Source #

stability :: GenCspCASL a -> Stability Source #

data_logic :: GenCspCASL a -> Maybe AnyLogic Source #

top_sublogic :: GenCspCASL a -> () Source #

all_sublogics :: GenCspCASL a -> [()] Source #

bottomSublogic :: GenCspCASL a -> Maybe () Source #

sublogicDimensions :: GenCspCASL a -> [[()]] Source #

parseSublogic :: GenCspCASL a -> String -> Maybe () Source #

proj_sublogic_epsilon :: GenCspCASL a -> () -> CspCASLSign -> CspCASLMorphism Source #

provers :: GenCspCASL a -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()] Source #

default_prover :: GenCspCASL a -> String Source #

cons_checkers :: GenCspCASL a -> [ConsChecker CspCASLSign CspCASLSen () CspCASLMorphism ()] Source #

conservativityCheck :: GenCspCASL a -> [ConservativityChecker CspCASLSign CspCASLSen CspCASLMorphism] Source #

empty_proof_tree :: GenCspCASL a -> () Source #

syntaxTable :: GenCspCASL a -> CspCASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: GenCspCASL a -> Maybe OMCD Source #

export_symToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspCASLSen -> Result TCorOMElement Source #

export_theoryToOmdoc :: GenCspCASL a -> SigMap CspSymbol -> CspCASLSign -> [Named CspCASLSen] -> Result [TCElement] Source #

omdocToSym :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result CspSymbol Source #

omdocToSen :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result (Maybe (Named CspCASLSen)) Source #

addOMadtToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [[OmdADT]] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

addOmdocToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [TCElement] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

(CspCASLSemantics a, CspCASLSemantics b) => Comorphism (CspCASL2CspCASL a b) (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () (GenCspCASL b) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source # 
(Data f, Data s, Data b) => Data (BASIC_SPEC b s f) Source # 

Methods

gfoldl :: (forall d a. Data d => c (d -> a) -> d -> c a) -> (forall g. g -> c g) -> BASIC_SPEC b s f -> c (BASIC_SPEC b s f)

gunfold :: (forall a r. Data a => c (a -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (BASIC_SPEC b s f)

toConstr :: BASIC_SPEC b s f -> Constr

dataTypeOf :: BASIC_SPEC b s f -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (BASIC_SPEC b s f))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (BASIC_SPEC b s f))

gmapT :: (forall a. Data a => a -> a) -> BASIC_SPEC b s f -> BASIC_SPEC b s f

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC b s f -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC b s f -> r

gmapQ :: (forall d. Data d => d -> u) -> BASIC_SPEC b s f -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_SPEC b s f -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_SPEC b s f -> m (BASIC_SPEC b s f)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC b s f -> m (BASIC_SPEC b s f)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC b s f -> m (BASIC_SPEC b s f)

(Show s, Show f, Show b) => Show (BASIC_SPEC b s f) Source # 

Methods

showsPrec :: Int -> BASIC_SPEC b s f -> ShowS

show :: BASIC_SPEC b s f -> String

showList :: [BASIC_SPEC b s f] -> ShowS

(GetRange b, GetRange s, GetRange f) => GetRange (BASIC_SPEC b s f) Source # 

Methods

getRange :: BASIC_SPEC b s f -> Range Source #

rangeSpan :: BASIC_SPEC b s f -> [Pos] Source #

ATermConvertibleSML (BASIC_SPEC a b c) Source # 

Methods

from_sml_ShATerm :: ATermTable -> BASIC_SPEC a b c

from_sml_ShATermList :: ATermTable -> [BASIC_SPEC a b c]

data BASIC_ITEMS b s f Source #

Instances

(Data f, Data s, Data b) => Data (BASIC_ITEMS b s f) Source # 

Methods

gfoldl :: (forall d a. Data d => c (d -> a) -> d -> c a) -> (forall g. g -> c g) -> BASIC_ITEMS b s f -> c (BASIC_ITEMS b s f)

gunfold :: (forall a r. Data a => c (a -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (BASIC_ITEMS b s f)

toConstr :: BASIC_ITEMS b s f -> Constr

dataTypeOf :: BASIC_ITEMS b s f -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (BASIC_ITEMS b s f))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (BASIC_ITEMS b s f))

gmapT :: (forall a. Data a => a -> a) -> BASIC_ITEMS b s f -> BASIC_ITEMS b s f

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEMS b s f -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEMS b s f -> r

gmapQ :: (forall d. Data d => d -> u) -> BASIC_ITEMS b s f -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_ITEMS b s f -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_ITEMS b s f -> m (BASIC_ITEMS b s f)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEMS b s f -> m (BASIC_ITEMS b s f)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEMS b s f -> m (BASIC_ITEMS b s f)

(Show b, Show f, Show s) => Show (BASIC_ITEMS b s f) Source # 

Methods

showsPrec :: Int -> BASIC_ITEMS b s f -> ShowS

show :: BASIC_ITEMS b s f -> String

showList :: [BASIC_ITEMS b s f] -> ShowS

(GetRange b, GetRange s, GetRange f) => GetRange (BASIC_ITEMS b s f) Source # 

Methods

getRange :: BASIC_ITEMS b s f -> Range Source #

rangeSpan :: BASIC_ITEMS b s f -> [Pos] Source #

ATermConvertibleSML (BASIC_ITEMS a b c) Source # 

Methods

from_sml_ShATerm :: ATermTable -> BASIC_ITEMS a b c

from_sml_ShATermList :: ATermTable -> [BASIC_ITEMS a b c]

data SortsKind Source #

Instances

Data SortsKind Source # 

Methods

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

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

toConstr :: SortsKind -> Constr

dataTypeOf :: SortsKind -> DataType

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

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

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

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

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

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

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

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

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

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

Show SortsKind Source # 

Methods

showsPrec :: Int -> SortsKind -> ShowS

show :: SortsKind -> String

showList :: [SortsKind] -> ShowS

GetRange SortsKind Source # 

data SIG_ITEMS s f Source #

Instances

(Data f, Data s) => Data (SIG_ITEMS s f) Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SIG_ITEMS s f -> c (SIG_ITEMS s f)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SIG_ITEMS s f)

toConstr :: SIG_ITEMS s f -> Constr

dataTypeOf :: SIG_ITEMS s f -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> SIG_ITEMS s f -> SIG_ITEMS s f

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SIG_ITEMS s f -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SIG_ITEMS s f -> r

gmapQ :: (forall d. Data d => d -> u) -> SIG_ITEMS s f -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SIG_ITEMS s f -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SIG_ITEMS s f -> m (SIG_ITEMS s f)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SIG_ITEMS s f -> m (SIG_ITEMS s f)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SIG_ITEMS s f -> m (SIG_ITEMS s f)

(Show s, Show f) => Show (SIG_ITEMS s f) Source # 

Methods

showsPrec :: Int -> SIG_ITEMS s f -> ShowS

show :: SIG_ITEMS s f -> String

showList :: [SIG_ITEMS s f] -> ShowS

(GetRange s, GetRange f) => GetRange (SIG_ITEMS s f) Source # 
ATermConvertibleSML (SIG_ITEMS a b) Source # 

Methods

from_sml_ShATerm :: ATermTable -> SIG_ITEMS a b

from_sml_ShATermList :: ATermTable -> [SIG_ITEMS a b]

data SORT_ITEM f Source #

Instances

Data f => Data (SORT_ITEM f) Source # 

Methods

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

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

toConstr :: SORT_ITEM f -> Constr

dataTypeOf :: SORT_ITEM f -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> SORT_ITEM f -> SORT_ITEM f

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

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

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

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

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

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

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

Show f => Show (SORT_ITEM f) Source # 

Methods

showsPrec :: Int -> SORT_ITEM f -> ShowS

show :: SORT_ITEM f -> String

showList :: [SORT_ITEM f] -> ShowS

GetRange f => GetRange (SORT_ITEM f) Source # 
ListCheck (SORT_ITEM f) Source # 

Methods

innerList :: SORT_ITEM f -> [()] Source #

ATermConvertibleSML (SORT_ITEM a) Source # 

Methods

from_sml_ShATerm :: ATermTable -> SORT_ITEM a

from_sml_ShATermList :: ATermTable -> [SORT_ITEM a]

data OP_ITEM f Source #

Instances

Data f => Data (OP_ITEM f) Source # 

Methods

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

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

toConstr :: OP_ITEM f -> Constr

dataTypeOf :: OP_ITEM f -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> OP_ITEM f -> OP_ITEM f

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

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

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

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

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

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

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

Show f => Show (OP_ITEM f) Source # 

Methods

showsPrec :: Int -> OP_ITEM f -> ShowS

show :: OP_ITEM f -> String

showList :: [OP_ITEM f] -> ShowS

GetRange f => GetRange (OP_ITEM f) Source # 
ListCheck (OP_ITEM f) Source # 

Methods

innerList :: OP_ITEM f -> [()] Source #

ATermConvertibleSML (OP_ITEM a) Source # 

Methods

from_sml_ShATerm :: ATermTable -> OP_ITEM a

from_sml_ShATermList :: ATermTable -> [OP_ITEM a]

data OpKind Source #

Constructors

Total 
Partial 

Instances

Eq OpKind Source # 

Methods

(==) :: OpKind -> OpKind -> Bool

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

Data OpKind Source # 

Methods

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

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

toConstr :: OpKind -> Constr

dataTypeOf :: OpKind -> DataType

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

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

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

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

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

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

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

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

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

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

Ord OpKind Source # 

Methods

compare :: OpKind -> OpKind -> Ordering

(<) :: OpKind -> OpKind -> Bool

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

(>) :: OpKind -> OpKind -> Bool

(>=) :: OpKind -> OpKind -> Bool

max :: OpKind -> OpKind -> OpKind

min :: OpKind -> OpKind -> OpKind

Show OpKind Source # 

Methods

showsPrec :: Int -> OpKind -> ShowS

show :: OpKind -> String

showList :: [OpKind] -> ShowS

GetRange OpKind Source # 

data OP_TYPE Source #

Constructors

Op_type OpKind [SORT] SORT Range 

Instances

Eq OP_TYPE Source # 

Methods

(==) :: OP_TYPE -> OP_TYPE -> Bool

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

Data OP_TYPE Source # 

Methods

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

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

toConstr :: OP_TYPE -> Constr

dataTypeOf :: OP_TYPE -> DataType

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

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

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

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

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

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

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

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

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

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

Ord OP_TYPE Source # 

Methods

compare :: OP_TYPE -> OP_TYPE -> Ordering

(<) :: OP_TYPE -> OP_TYPE -> Bool

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

(>) :: OP_TYPE -> OP_TYPE -> Bool

(>=) :: OP_TYPE -> OP_TYPE -> Bool

max :: OP_TYPE -> OP_TYPE -> OP_TYPE

min :: OP_TYPE -> OP_TYPE -> OP_TYPE

Show OP_TYPE Source # 

Methods

showsPrec :: Int -> OP_TYPE -> ShowS

show :: OP_TYPE -> String

showList :: [OP_TYPE] -> ShowS

GetRange OP_TYPE Source # 
ATermConvertibleSML OP_TYPE Source # 

Methods

from_sml_ShATerm :: ATermTable -> OP_TYPE

from_sml_ShATermList :: ATermTable -> [OP_TYPE]

data OP_HEAD Source #

Constructors

Op_head OpKind [VAR_DECL] (Maybe SORT) Range 

Instances

Eq OP_HEAD Source # 

Methods

(==) :: OP_HEAD -> OP_HEAD -> Bool

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

Data OP_HEAD Source # 

Methods

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

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

toConstr :: OP_HEAD -> Constr

dataTypeOf :: OP_HEAD -> DataType

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

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

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

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

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

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

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

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

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

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

Ord OP_HEAD Source # 

Methods

compare :: OP_HEAD -> OP_HEAD -> Ordering

(<) :: OP_HEAD -> OP_HEAD -> Bool

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

(>) :: OP_HEAD -> OP_HEAD -> Bool

(>=) :: OP_HEAD -> OP_HEAD -> Bool

max :: OP_HEAD -> OP_HEAD -> OP_HEAD

min :: OP_HEAD -> OP_HEAD -> OP_HEAD

Show OP_HEAD Source # 

Methods

showsPrec :: Int -> OP_HEAD -> ShowS

show :: OP_HEAD -> String

showList :: [OP_HEAD] -> ShowS

GetRange OP_HEAD Source # 
ATermConvertibleSML OP_HEAD Source # 

Methods

from_sml_ShATerm :: ATermTable -> OP_HEAD

from_sml_ShATermList :: ATermTable -> [OP_HEAD]

data OP_ATTR f Source #

Instances

Eq f => Eq (OP_ATTR f) Source # 

Methods

(==) :: OP_ATTR f -> OP_ATTR f -> Bool

(/=) :: OP_ATTR f -> OP_ATTR f -> Bool

Data f => Data (OP_ATTR f) Source # 

Methods

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

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

toConstr :: OP_ATTR f -> Constr

dataTypeOf :: OP_ATTR f -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> OP_ATTR f -> OP_ATTR f

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

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

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

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

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

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

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

Ord f => Ord (OP_ATTR f) Source # 

Methods

compare :: OP_ATTR f -> OP_ATTR f -> Ordering

(<) :: OP_ATTR f -> OP_ATTR f -> Bool

(<=) :: OP_ATTR f -> OP_ATTR f -> Bool

(>) :: OP_ATTR f -> OP_ATTR f -> Bool

(>=) :: OP_ATTR f -> OP_ATTR f -> Bool

max :: OP_ATTR f -> OP_ATTR f -> OP_ATTR f

min :: OP_ATTR f -> OP_ATTR f -> OP_ATTR f

Show f => Show (OP_ATTR f) Source # 

Methods

showsPrec :: Int -> OP_ATTR f -> ShowS

show :: OP_ATTR f -> String

showList :: [OP_ATTR f] -> ShowS

GetRange f => GetRange (OP_ATTR f) Source # 
ATermConvertibleSML (OP_ATTR a) Source # 

Methods

from_sml_ShATerm :: ATermTable -> OP_ATTR a

from_sml_ShATermList :: ATermTable -> [OP_ATTR a]

data PRED_ITEM f Source #

Instances

Data f => Data (PRED_ITEM f) Source # 

Methods

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

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

toConstr :: PRED_ITEM f -> Constr

dataTypeOf :: PRED_ITEM f -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> PRED_ITEM f -> PRED_ITEM f

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

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

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

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

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

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

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

Show f => Show (PRED_ITEM f) Source # 

Methods

showsPrec :: Int -> PRED_ITEM f -> ShowS

show :: PRED_ITEM f -> String

showList :: [PRED_ITEM f] -> ShowS

GetRange f => GetRange (PRED_ITEM f) Source # 
ListCheck (PRED_ITEM f) Source # 

Methods

innerList :: PRED_ITEM f -> [()] Source #

ATermConvertibleSML (PRED_ITEM a) Source # 

Methods

from_sml_ShATerm :: ATermTable -> PRED_ITEM a

from_sml_ShATermList :: ATermTable -> [PRED_ITEM a]

data PRED_TYPE Source #

Constructors

Pred_type [SORT] Range 

Instances

Eq PRED_TYPE Source # 

Methods

(==) :: PRED_TYPE -> PRED_TYPE -> Bool

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

Data PRED_TYPE Source # 

Methods

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

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

toConstr :: PRED_TYPE -> Constr

dataTypeOf :: PRED_TYPE -> DataType

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

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

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

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

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

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

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

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

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

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

Ord PRED_TYPE Source # 

Methods

compare :: PRED_TYPE -> PRED_TYPE -> Ordering

(<) :: PRED_TYPE -> PRED_TYPE -> Bool

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

(>) :: PRED_TYPE -> PRED_TYPE -> Bool

(>=) :: PRED_TYPE -> PRED_TYPE -> Bool

max :: PRED_TYPE -> PRED_TYPE -> PRED_TYPE

min :: PRED_TYPE -> PRED_TYPE -> PRED_TYPE

Show PRED_TYPE Source # 

Methods

showsPrec :: Int -> PRED_TYPE -> ShowS

show :: PRED_TYPE -> String

showList :: [PRED_TYPE] -> ShowS

GetRange PRED_TYPE Source # 
ATermConvertibleSML PRED_TYPE Source # 

Methods

from_sml_ShATerm :: ATermTable -> PRED_TYPE

from_sml_ShATermList :: ATermTable -> [PRED_TYPE]

data PRED_HEAD Source #

Constructors

Pred_head [VAR_DECL] Range 

Instances

Data PRED_HEAD Source # 

Methods

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

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

toConstr :: PRED_HEAD -> Constr

dataTypeOf :: PRED_HEAD -> DataType

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

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

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

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

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

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

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

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

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

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

Show PRED_HEAD Source # 

Methods

showsPrec :: Int -> PRED_HEAD -> ShowS

show :: PRED_HEAD -> String

showList :: [PRED_HEAD] -> ShowS

GetRange PRED_HEAD Source # 
ATermConvertibleSML PRED_HEAD Source # 

Methods

from_sml_ShATerm :: ATermTable -> PRED_HEAD

from_sml_ShATermList :: ATermTable -> [PRED_HEAD]

data DATATYPE_DECL Source #

Instances

Data DATATYPE_DECL Source # 

Methods

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

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

toConstr :: DATATYPE_DECL -> Constr

dataTypeOf :: DATATYPE_DECL -> DataType

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

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

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

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

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

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

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

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

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

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

Show DATATYPE_DECL Source # 

Methods

showsPrec :: Int -> DATATYPE_DECL -> ShowS

show :: DATATYPE_DECL -> String

showList :: [DATATYPE_DECL] -> ShowS

GetRange DATATYPE_DECL Source # 
ATermConvertibleSML DATATYPE_DECL Source # 

Methods

from_sml_ShATerm :: ATermTable -> DATATYPE_DECL

from_sml_ShATermList :: ATermTable -> [DATATYPE_DECL]

data ALTERNATIVE Source #

Instances

Data ALTERNATIVE Source # 

Methods

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

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

toConstr :: ALTERNATIVE -> Constr

dataTypeOf :: ALTERNATIVE -> DataType

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

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

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

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

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

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

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

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

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

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

Show ALTERNATIVE Source # 

Methods

showsPrec :: Int -> ALTERNATIVE -> ShowS

show :: ALTERNATIVE -> String

showList :: [ALTERNATIVE] -> ShowS

GetRange ALTERNATIVE Source # 
ATermConvertibleSML ALTERNATIVE Source # 

Methods

from_sml_ShATerm :: ATermTable -> ALTERNATIVE

from_sml_ShATermList :: ATermTable -> [ALTERNATIVE]

data COMPONENTS Source #

Instances

Data COMPONENTS Source # 

Methods

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

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

toConstr :: COMPONENTS -> Constr

dataTypeOf :: COMPONENTS -> DataType

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

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

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

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

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

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

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

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

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

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

Show COMPONENTS Source # 

Methods

showsPrec :: Int -> COMPONENTS -> ShowS

show :: COMPONENTS -> String

showList :: [COMPONENTS] -> ShowS

GetRange COMPONENTS Source # 
ATermConvertibleSML COMPONENTS Source # 

Methods

from_sml_ShATerm :: ATermTable -> COMPONENTS

from_sml_ShATermList :: ATermTable -> [COMPONENTS]

data VAR_DECL Source #

Constructors

Var_decl [VAR] SORT Range 

Instances

Eq VAR_DECL Source # 

Methods

(==) :: VAR_DECL -> VAR_DECL -> Bool

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

Data VAR_DECL Source # 

Methods

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

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

toConstr :: VAR_DECL -> Constr

dataTypeOf :: VAR_DECL -> DataType

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

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

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

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

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

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

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

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

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

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

Ord VAR_DECL Source # 

Methods

compare :: VAR_DECL -> VAR_DECL -> Ordering

(<) :: VAR_DECL -> VAR_DECL -> Bool

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

(>) :: VAR_DECL -> VAR_DECL -> Bool

(>=) :: VAR_DECL -> VAR_DECL -> Bool

max :: VAR_DECL -> VAR_DECL -> VAR_DECL

min :: VAR_DECL -> VAR_DECL -> VAR_DECL

Show VAR_DECL Source # 

Methods

showsPrec :: Int -> VAR_DECL -> ShowS

show :: VAR_DECL -> String

showList :: [VAR_DECL] -> ShowS

GetRange VAR_DECL Source # 
ListCheck VAR_DECL Source # 

Methods

innerList :: VAR_DECL -> [()] Source #

ATermConvertibleSML VAR_DECL Source # 

Methods

from_sml_ShATerm :: ATermTable -> VAR_DECL

from_sml_ShATermList :: ATermTable -> [VAR_DECL]

data Junctor Source #

Constructors

Con 
Dis 

Instances

Eq Junctor Source # 

Methods

(==) :: Junctor -> Junctor -> Bool

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

Data Junctor Source # 

Methods

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

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

toConstr :: Junctor -> Constr

dataTypeOf :: Junctor -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Junctor Source # 

Methods

compare :: Junctor -> Junctor -> Ordering

(<) :: Junctor -> Junctor -> Bool

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

(>) :: Junctor -> Junctor -> Bool

(>=) :: Junctor -> Junctor -> Bool

max :: Junctor -> Junctor -> Junctor

min :: Junctor -> Junctor -> Junctor

Show Junctor Source # 

Methods

showsPrec :: Int -> Junctor -> ShowS

show :: Junctor -> String

showList :: [Junctor] -> ShowS

GetRange Junctor Source # 

data Relation Source #

Instances

Eq Relation Source # 

Methods

(==) :: Relation -> Relation -> Bool

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

Data Relation Source # 

Methods

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

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

toConstr :: Relation -> Constr

dataTypeOf :: Relation -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Relation Source # 

Methods

compare :: Relation -> Relation -> Ordering

(<) :: Relation -> Relation -> Bool

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

(>) :: Relation -> Relation -> Bool

(>=) :: Relation -> Relation -> Bool

max :: Relation -> Relation -> Relation

min :: Relation -> Relation -> Relation

Show Relation Source # 

Methods

showsPrec :: Int -> Relation -> ShowS

show :: Relation -> String

showList :: [Relation] -> ShowS

GetRange Relation Source # 

data Equality Source #

Constructors

Strong 
Existl 

Instances

Eq Equality Source # 

Methods

(==) :: Equality -> Equality -> Bool

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

Data Equality Source # 

Methods

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

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

toConstr :: Equality -> Constr

dataTypeOf :: Equality -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Equality Source # 

Methods

compare :: Equality -> Equality -> Ordering

(<) :: Equality -> Equality -> Bool

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

(>) :: Equality -> Equality -> Bool

(>=) :: Equality -> Equality -> Bool

max :: Equality -> Equality -> Equality

min :: Equality -> Equality -> Equality

Show Equality Source # 

Methods

showsPrec :: Int -> Equality -> ShowS

show :: Equality -> String

showList :: [Equality] -> ShowS

GetRange Equality Source # 

data FORMULA f Source #

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 #