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

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

Instances details
ProjectSublogic CASL_DL_SL DL_BASIC_SPEC Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

MinSublogic CASL_DL_SL DL_BASIC_SPEC Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Syntax CASL CASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Modal.Logic_Modal

Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Fpl.Logic_Fpl

Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Syntax ConstraintCASL ConstraintCASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Syntax COL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in COL.Logic_COL

Syntax CASL_DL DL_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in VSE.Logic_VSE

StaticAnalysis CASL CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

basic_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, GlobalAnnos) -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA])) Source #

sen_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, CASLFORMULA) -> Result CASLFORMULA) Source #

extBasicAnalysis :: CASL -> IRI -> LibName -> CASLBasicSpec -> CASLSign -> GlobalAnnos -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA]) Source #

stat_symb_map_items :: CASL -> CASLSign -> Maybe CASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CASL -> CASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CASL -> Maybe ((CASLSign, [Named CASLFORMULA]) -> CASLBasicSpec) Source #

ensures_amalgamability :: CASL -> ([CASLAmalgOpt], Gr CASLSign (Int, CASLMor), [(Int, CASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CASL -> CASLMor -> [Named CASLFORMULA] -> Result (CASLSign, [Named CASLFORMULA]) Source #

signature_colimit :: CASL -> Gr CASLSign (Int, CASLMor) -> Result (CASLSign, Map Int CASLMor) Source #

qualify :: CASL -> SIMPLE_ID -> LibName -> CASLMor -> CASLSign -> Result (CASLMor, [Named CASLFORMULA]) Source #

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

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

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

empty_signature :: CASL -> CASLSign Source #

add_symb_to_sign :: CASL -> CASLSign -> Symbol -> Result CASLSign Source #

signature_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

signatureDiff :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

intersection :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

final_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

morphism_union :: CASL -> CASLMor -> CASLMor -> Result CASLMor Source #

is_subsig :: CASL -> CASLSign -> CASLSign -> Bool Source #

subsig_inclusion :: CASL -> CASLSign -> CASLSign -> Result CASLMor Source #

generated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source #

cogenerated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source #

induced_from_morphism :: CASL -> EndoMap RawSymbol -> CASLSign -> Result CASLMor Source #

induced_from_to_morphism :: CASL -> EndoMap RawSymbol -> ExtSign CASLSign Symbol -> ExtSign CASLSign Symbol -> Result CASLMor Source #

is_transportable :: CASL -> CASLMor -> Bool Source #

is_injective :: CASL -> CASLMor -> Bool Source #

theory_to_taxonomy :: CASL -> TaxoGraphKind -> MMiSSOntology -> CASLSign -> [Named CASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CASL -> String -> Bool -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CASLSign, [Named CASLFORMULA], CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CASL -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CASLSign, CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CASL -> [IRI] -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source # 
Instance details

Defined in Modal.Logic_Modal

Methods

basic_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, GlobalAnnos) -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA])) Source #

sen_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, ModalFORMULA) -> Result ModalFORMULA) Source #

extBasicAnalysis :: Modal -> IRI -> LibName -> M_BASIC_SPEC -> MSign -> GlobalAnnos -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA]) Source #

stat_symb_map_items :: Modal -> MSign -> Maybe MSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Modal -> MSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Modal -> Maybe ((MSign, [Named ModalFORMULA]) -> M_BASIC_SPEC) Source #

ensures_amalgamability :: Modal -> ([CASLAmalgOpt], Gr MSign (Int, ModalMor), [(Int, ModalMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Modal -> ModalMor -> [Named ModalFORMULA] -> Result (MSign, [Named ModalFORMULA]) Source #

signature_colimit :: Modal -> Gr MSign (Int, ModalMor) -> Result (MSign, Map Int ModalMor) Source #

qualify :: Modal -> SIMPLE_ID -> LibName -> ModalMor -> MSign -> Result (ModalMor, [Named ModalFORMULA]) Source #

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

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

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

empty_signature :: Modal -> MSign Source #

add_symb_to_sign :: Modal -> MSign -> Symbol -> Result MSign Source #

signature_union :: Modal -> MSign -> MSign -> Result MSign Source #

signatureDiff :: Modal -> MSign -> MSign -> Result MSign Source #

intersection :: Modal -> MSign -> MSign -> Result MSign Source #

final_union :: Modal -> MSign -> MSign -> Result MSign Source #

morphism_union :: Modal -> ModalMor -> ModalMor -> Result ModalMor Source #

is_subsig :: Modal -> MSign -> MSign -> Bool Source #

subsig_inclusion :: Modal -> MSign -> MSign -> Result ModalMor Source #

generated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source #

cogenerated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source #

induced_from_morphism :: Modal -> EndoMap RawSymbol -> MSign -> Result ModalMor Source #

induced_from_to_morphism :: Modal -> EndoMap RawSymbol -> ExtSign MSign Symbol -> ExtSign MSign Symbol -> Result ModalMor Source #

is_transportable :: Modal -> ModalMor -> Bool Source #

is_injective :: Modal -> ModalMor -> Bool Source #

theory_to_taxonomy :: Modal -> TaxoGraphKind -> MMiSSOntology -> MSign -> [Named ModalFORMULA] -> Result MMiSSOntology Source #

corresp2th :: Modal -> String -> Bool -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (MSign, [Named ModalFORMULA], MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Modal -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (MSign, MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Modal -> [IRI] -> (MSign, [Named ModalFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #

StaticAnalysis Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Methods

basic_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, GlobalAnnos) -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA])) Source #

sen_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, HybridFORMULA) -> Result HybridFORMULA) Source #

extBasicAnalysis :: Hybrid -> IRI -> LibName -> H_BASIC_SPEC -> HSign -> GlobalAnnos -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA]) Source #

stat_symb_map_items :: Hybrid -> HSign -> Maybe HSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Hybrid -> HSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Hybrid -> Maybe ((HSign, [Named HybridFORMULA]) -> H_BASIC_SPEC) Source #

ensures_amalgamability :: Hybrid -> ([CASLAmalgOpt], Gr HSign (Int, HybridMor), [(Int, HybridMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Hybrid -> HybridMor -> [Named HybridFORMULA] -> Result (HSign, [Named HybridFORMULA]) Source #

signature_colimit :: Hybrid -> Gr HSign (Int, HybridMor) -> Result (HSign, Map Int HybridMor) Source #

qualify :: Hybrid -> SIMPLE_ID -> LibName -> HybridMor -> HSign -> Result (HybridMor, [Named HybridFORMULA]) Source #

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

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

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

empty_signature :: Hybrid -> HSign Source #

add_symb_to_sign :: Hybrid -> HSign -> Symbol -> Result HSign Source #

signature_union :: Hybrid -> HSign -> HSign -> Result HSign Source #

signatureDiff :: Hybrid -> HSign -> HSign -> Result HSign Source #

intersection :: Hybrid -> HSign -> HSign -> Result HSign Source #

final_union :: Hybrid -> HSign -> HSign -> Result HSign Source #

morphism_union :: Hybrid -> HybridMor -> HybridMor -> Result HybridMor Source #

is_subsig :: Hybrid -> HSign -> HSign -> Bool Source #

subsig_inclusion :: Hybrid -> HSign -> HSign -> Result HybridMor Source #

generated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source #

cogenerated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source #

induced_from_morphism :: Hybrid -> EndoMap RawSymbol -> HSign -> Result HybridMor Source #

induced_from_to_morphism :: Hybrid -> EndoMap RawSymbol -> ExtSign HSign Symbol -> ExtSign HSign Symbol -> Result HybridMor Source #

is_transportable :: Hybrid -> HybridMor -> Bool Source #

is_injective :: Hybrid -> HybridMor -> Bool Source #

theory_to_taxonomy :: Hybrid -> TaxoGraphKind -> MMiSSOntology -> HSign -> [Named HybridFORMULA] -> Result MMiSSOntology Source #

corresp2th :: Hybrid -> String -> Bool -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (HSign, [Named HybridFORMULA], HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Hybrid -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (HSign, HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Hybrid -> [IRI] -> (HSign, [Named HybridFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source #

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

Defined in Fpl.Logic_Fpl

Methods

basic_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, GlobalAnnos) -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])) Source #

sen_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, FplForm) -> Result FplForm) Source #

extBasicAnalysis :: Fpl -> IRI -> LibName -> FplBasicSpec -> FplSign -> GlobalAnnos -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]) Source #

stat_symb_map_items :: Fpl -> FplSign -> Maybe FplSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Fpl -> FplSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Fpl -> Maybe ((FplSign, [Named FplForm]) -> FplBasicSpec) Source #

ensures_amalgamability :: Fpl -> ([CASLAmalgOpt], Gr FplSign (Int, FplMor), [(Int, FplMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Fpl -> FplMor -> [Named FplForm] -> Result (FplSign, [Named FplForm]) Source #

signature_colimit :: Fpl -> Gr FplSign (Int, FplMor) -> Result (FplSign, Map Int FplMor) Source #

qualify :: Fpl -> SIMPLE_ID -> LibName -> FplMor -> FplSign -> Result (FplMor, [Named FplForm]) Source #

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

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

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

empty_signature :: Fpl -> FplSign Source #

add_symb_to_sign :: Fpl -> FplSign -> Symbol -> Result FplSign Source #

signature_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

signatureDiff :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

intersection :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

final_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

morphism_union :: Fpl -> FplMor -> FplMor -> Result FplMor Source #

is_subsig :: Fpl -> FplSign -> FplSign -> Bool Source #

subsig_inclusion :: Fpl -> FplSign -> FplSign -> Result FplMor Source #

generated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

cogenerated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

induced_from_morphism :: Fpl -> EndoMap RawSymbol -> FplSign -> Result FplMor Source #

induced_from_to_morphism :: Fpl -> EndoMap RawSymbol -> ExtSign FplSign Symbol -> ExtSign FplSign Symbol -> Result FplMor Source #

is_transportable :: Fpl -> FplMor -> Bool Source #

is_injective :: Fpl -> FplMor -> Bool Source #

theory_to_taxonomy :: Fpl -> TaxoGraphKind -> MMiSSOntology -> FplSign -> [Named FplForm] -> Result MMiSSOntology Source #

corresp2th :: Fpl -> String -> Bool -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (FplSign, [Named FplForm], FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Fpl -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (FplSign, FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Fpl -> [IRI] -> (FplSign, [Named FplForm]) -> Result (FplSign, [Named FplForm]) Source #

StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

empty_signature :: ExtModal -> ExtModalSign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

StaticAnalysis ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Methods

basic_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos) -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA])) Source #

sen_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, ConstraintCASLFORMULA) -> Result ConstraintCASLFORMULA) Source #

extBasicAnalysis :: ConstraintCASL -> IRI -> LibName -> ConstraintCASLBasicSpec -> ConstraintCASLSign -> GlobalAnnos -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA]) Source #

stat_symb_map_items :: ConstraintCASL -> ConstraintCASLSign -> Maybe ConstraintCASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: ConstraintCASL -> ConstraintCASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: ConstraintCASL -> Maybe ((ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> ConstraintCASLBasicSpec) Source #

ensures_amalgamability :: ConstraintCASL -> ([CASLAmalgOpt], Gr ConstraintCASLSign (Int, ConstraintCASLMor), [(Int, ConstraintCASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: ConstraintCASL -> ConstraintCASLMor -> [Named ConstraintCASLFORMULA] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

signature_colimit :: ConstraintCASL -> Gr ConstraintCASLSign (Int, ConstraintCASLMor) -> Result (ConstraintCASLSign, Map Int ConstraintCASLMor) Source #

qualify :: ConstraintCASL -> SIMPLE_ID -> LibName -> ConstraintCASLMor -> ConstraintCASLSign -> Result (ConstraintCASLMor, [Named ConstraintCASLFORMULA]) Source #

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

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

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

empty_signature :: ConstraintCASL -> ConstraintCASLSign Source #

add_symb_to_sign :: ConstraintCASL -> ConstraintCASLSign -> Symbol -> Result ConstraintCASLSign Source #

signature_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

signatureDiff :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

intersection :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

final_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

morphism_union :: ConstraintCASL -> ConstraintCASLMor -> ConstraintCASLMor -> Result ConstraintCASLMor Source #

is_subsig :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Bool Source #

subsig_inclusion :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

generated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

cogenerated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

induced_from_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

induced_from_to_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ExtSign ConstraintCASLSign Symbol -> ExtSign ConstraintCASLSign Symbol -> Result ConstraintCASLMor Source #

is_transportable :: ConstraintCASL -> ConstraintCASLMor -> Bool Source #

is_injective :: ConstraintCASL -> ConstraintCASLMor -> Bool Source #

theory_to_taxonomy :: ConstraintCASL -> TaxoGraphKind -> MMiSSOntology -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: ConstraintCASL -> String -> Bool -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA], ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ConstraintCASLSign, ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: ConstraintCASL -> [IRI] -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

basic_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA])) Source #

sen_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, CoCASLFORMULA) -> Result CoCASLFORMULA) Source #

extBasicAnalysis :: CoCASL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA]) Source #

stat_symb_map_items :: CoCASL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CoCASL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CoCASL -> Maybe ((CSign, [Named CoCASLFORMULA]) -> C_BASIC_SPEC) Source #

ensures_amalgamability :: CoCASL -> ([CASLAmalgOpt], Gr CSign (Int, CoCASLMor), [(Int, CoCASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CoCASL -> CoCASLMor -> [Named CoCASLFORMULA] -> Result (CSign, [Named CoCASLFORMULA]) Source #

signature_colimit :: CoCASL -> Gr CSign (Int, CoCASLMor) -> Result (CSign, Map Int CoCASLMor) Source #

qualify :: CoCASL -> SIMPLE_ID -> LibName -> CoCASLMor -> CSign -> Result (CoCASLMor, [Named CoCASLFORMULA]) Source #

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

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

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

empty_signature :: CoCASL -> CSign Source #

add_symb_to_sign :: CoCASL -> CSign -> Symbol -> Result CSign Source #

signature_union :: CoCASL -> CSign -> CSign -> Result CSign Source #

signatureDiff :: CoCASL -> CSign -> CSign -> Result CSign Source #

intersection :: CoCASL -> CSign -> CSign -> Result CSign Source #

final_union :: CoCASL -> CSign -> CSign -> Result CSign Source #

morphism_union :: CoCASL -> CoCASLMor -> CoCASLMor -> Result CoCASLMor Source #

is_subsig :: CoCASL -> CSign -> CSign -> Bool Source #

subsig_inclusion :: CoCASL -> CSign -> CSign -> Result CoCASLMor Source #

generated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source #

cogenerated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source #

induced_from_morphism :: CoCASL -> EndoMap RawSymbol -> CSign -> Result CoCASLMor Source #

induced_from_to_morphism :: CoCASL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result CoCASLMor Source #

is_transportable :: CoCASL -> CoCASLMor -> Bool Source #

is_injective :: CoCASL -> CoCASLMor -> Bool Source #

theory_to_taxonomy :: CoCASL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named CoCASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CoCASL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named CoCASLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CoCASL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CoCASL -> [IRI] -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #

StaticAnalysis COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source # 
Instance details

Defined in COL.Logic_COL

Methods

basic_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA])) Source #

sen_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, COLFORMULA) -> Result COLFORMULA) Source #

extBasicAnalysis :: COL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]) Source #

stat_symb_map_items :: COL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: COL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: COL -> Maybe ((CSign, [Named COLFORMULA]) -> C_BASIC_SPEC) Source #

ensures_amalgamability :: COL -> ([CASLAmalgOpt], Gr CSign (Int, COLMor), [(Int, COLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: COL -> COLMor -> [Named COLFORMULA] -> Result (CSign, [Named COLFORMULA]) Source #

signature_colimit :: COL -> Gr CSign (Int, COLMor) -> Result (CSign, Map Int COLMor) Source #

qualify :: COL -> SIMPLE_ID -> LibName -> COLMor -> CSign -> Result (COLMor, [Named COLFORMULA]) Source #

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

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

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

empty_signature :: COL -> CSign Source #

add_symb_to_sign :: COL -> CSign -> Symbol -> Result CSign Source #

signature_union :: COL -> CSign -> CSign -> Result CSign Source #

signatureDiff :: COL -> CSign -> CSign -> Result CSign Source #

intersection :: COL -> CSign -> CSign -> Result CSign Source #

final_union :: COL -> CSign -> CSign -> Result CSign Source #

morphism_union :: COL -> COLMor -> COLMor -> Result COLMor Source #

is_subsig :: COL -> CSign -> CSign -> Bool Source #

subsig_inclusion :: COL -> CSign -> CSign -> Result COLMor Source #

generated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source #

cogenerated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source #

induced_from_morphism :: COL -> EndoMap RawSymbol -> CSign -> Result COLMor Source #

induced_from_to_morphism :: COL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result COLMor Source #

is_transportable :: COL -> COLMor -> Bool Source #

is_injective :: COL -> COLMor -> Bool Source #

theory_to_taxonomy :: COL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named COLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: COL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named COLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: COL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: COL -> [IRI] -> (CSign, [Named COLFORMULA]) -> Result (CSign, [Named COLFORMULA]) Source #

StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Methods

basic_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, GlobalAnnos) -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA])) Source #

sen_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, DLFORMULA) -> Result DLFORMULA) Source #

extBasicAnalysis :: CASL_DL -> IRI -> LibName -> DL_BASIC_SPEC -> DLSign -> GlobalAnnos -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA]) Source #

stat_symb_map_items :: CASL_DL -> DLSign -> Maybe DLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CASL_DL -> DLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CASL_DL -> Maybe ((DLSign, [Named DLFORMULA]) -> DL_BASIC_SPEC) Source #

ensures_amalgamability :: CASL_DL -> ([CASLAmalgOpt], Gr DLSign (Int, DLMor), [(Int, DLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CASL_DL -> DLMor -> [Named DLFORMULA] -> Result (DLSign, [Named DLFORMULA]) Source #

signature_colimit :: CASL_DL -> Gr DLSign (Int, DLMor) -> Result (DLSign, Map Int DLMor) Source #

qualify :: CASL_DL -> SIMPLE_ID -> LibName -> DLMor -> DLSign -> Result (DLMor, [Named DLFORMULA]) Source #

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

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

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

empty_signature :: CASL_DL -> DLSign Source #

add_symb_to_sign :: CASL_DL -> DLSign -> Symbol -> Result DLSign Source #

signature_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

signatureDiff :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

intersection :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

final_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

morphism_union :: CASL_DL -> DLMor -> DLMor -> Result DLMor Source #

is_subsig :: CASL_DL -> DLSign -> DLSign -> Bool Source #

subsig_inclusion :: CASL_DL -> DLSign -> DLSign -> Result DLMor Source #

generated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source #

cogenerated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source #

induced_from_morphism :: CASL_DL -> EndoMap RawSymbol -> DLSign -> Result DLMor Source #

induced_from_to_morphism :: CASL_DL -> EndoMap RawSymbol -> ExtSign DLSign Symbol -> ExtSign DLSign Symbol -> Result DLMor Source #

is_transportable :: CASL_DL -> DLMor -> Bool Source #

is_injective :: CASL_DL -> DLMor -> Bool Source #

theory_to_taxonomy :: CASL_DL -> TaxoGraphKind -> MMiSSOntology -> DLSign -> [Named DLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CASL_DL -> String -> Bool -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (DLSign, [Named DLFORMULA], DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CASL_DL -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (DLSign, DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CASL_DL -> [IRI] -> (DLSign, [Named DLFORMULA]) -> Result (DLSign, [Named DLFORMULA]) Source #

StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 
Instance details

Defined in VSE.Logic_VSE

Methods

basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source #

sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source #

ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source #

signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source #

qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source #

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

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

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

empty_signature :: VSE -> VSESign Source #

add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source #

signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source #

intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source #

final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source #

is_subsig :: VSE -> VSESign -> VSESign -> Bool Source #

subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source #

generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source #

induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source #

is_transportable :: VSE -> VSEMor -> Bool Source #

is_injective :: VSE -> VSEMor -> Bool Source #

theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #

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

Defined in CASL.Logic_CASL

Methods

parse_basic_sen :: CASL -> Maybe (CASLBasicSpec -> AParser st CASLFORMULA) Source #

stability :: CASL -> Stability Source #

data_logic :: CASL -> Maybe AnyLogic Source #

top_sublogic :: CASL -> CASL_Sublogics Source #

all_sublogics :: CASL -> [CASL_Sublogics] Source #

bottomSublogic :: CASL -> Maybe CASL_Sublogics Source #

sublogicDimensions :: CASL -> [[CASL_Sublogics]] Source #

parseSublogic :: CASL -> String -> Maybe CASL_Sublogics Source #

proj_sublogic_epsilon :: CASL -> CASL_Sublogics -> CASLSign -> CASLMor Source #

provers :: CASL -> [Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree] Source #

default_prover :: CASL -> String Source #

cons_checkers :: CASL -> [ConsChecker CASLSign CASLFORMULA CASL_Sublogics CASLMor ProofTree] Source #

conservativityCheck :: CASL -> [ConservativityChecker CASLSign CASLFORMULA CASLMor] Source #

empty_proof_tree :: CASL -> ProofTree Source #

syntaxTable :: CASL -> CASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CASL -> Maybe OMCD Source #

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

export_senToOmdoc :: CASL -> NameMap Symbol -> CASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CASL -> SigMap Symbol -> CASLSign -> [Named CASLFORMULA] -> Result [TCElement] Source #

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

omdocToSen :: CASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CASLFORMULA)) Source #

addOMadtToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [[OmdADT]] -> Result (CASLSign, [Named CASLFORMULA]) Source #

addOmdocToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [TCElement] -> Result (CASLSign, [Named CASLFORMULA]) Source #

sublogicOfTheo :: CASL -> (CASLSign, [CASLFORMULA]) -> CASL_Sublogics Source #

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

Defined in Modal.Logic_Modal

Methods

parse_basic_sen :: Modal -> Maybe (M_BASIC_SPEC -> AParser st ModalFORMULA) Source #

stability :: Modal -> Stability Source #

data_logic :: Modal -> Maybe AnyLogic Source #

top_sublogic :: Modal -> () Source #

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

bottomSublogic :: Modal -> Maybe () Source #

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

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

proj_sublogic_epsilon :: Modal -> () -> MSign -> ModalMor Source #

provers :: Modal -> [Prover MSign ModalFORMULA ModalMor () ()] Source #

default_prover :: Modal -> String Source #

cons_checkers :: Modal -> [ConsChecker MSign ModalFORMULA () ModalMor ()] Source #

conservativityCheck :: Modal -> [ConservativityChecker MSign ModalFORMULA ModalMor] Source #

empty_proof_tree :: Modal -> () Source #

syntaxTable :: Modal -> MSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Modal -> Maybe OMCD Source #

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

export_senToOmdoc :: Modal -> NameMap Symbol -> ModalFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Modal -> SigMap Symbol -> MSign -> [Named ModalFORMULA] -> Result [TCElement] Source #

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

omdocToSen :: Modal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ModalFORMULA)) Source #

addOMadtToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [[OmdADT]] -> Result (MSign, [Named ModalFORMULA]) Source #

addOmdocToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [TCElement] -> Result (MSign, [Named ModalFORMULA]) Source #

sublogicOfTheo :: Modal -> (MSign, [ModalFORMULA]) -> () Source #

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

Defined in Hybrid.Logic_Hybrid

Methods

parse_basic_sen :: Hybrid -> Maybe (H_BASIC_SPEC -> AParser st HybridFORMULA) Source #

stability :: Hybrid -> Stability Source #

data_logic :: Hybrid -> Maybe AnyLogic Source #

top_sublogic :: Hybrid -> () Source #

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

bottomSublogic :: Hybrid -> Maybe () Source #

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

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

proj_sublogic_epsilon :: Hybrid -> () -> HSign -> HybridMor Source #

provers :: Hybrid -> [Prover HSign HybridFORMULA HybridMor () ()] Source #

default_prover :: Hybrid -> String Source #

cons_checkers :: Hybrid -> [ConsChecker HSign HybridFORMULA () HybridMor ()] Source #

conservativityCheck :: Hybrid -> [ConservativityChecker HSign HybridFORMULA HybridMor] Source #

empty_proof_tree :: Hybrid -> () Source #

syntaxTable :: Hybrid -> HSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Hybrid -> Maybe OMCD Source #

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

export_senToOmdoc :: Hybrid -> NameMap Symbol -> HybridFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Hybrid -> SigMap Symbol -> HSign -> [Named HybridFORMULA] -> Result [TCElement] Source #

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

omdocToSen :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named HybridFORMULA)) Source #

addOMadtToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [[OmdADT]] -> Result (HSign, [Named HybridFORMULA]) Source #

addOmdocToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [TCElement] -> Result (HSign, [Named HybridFORMULA]) Source #

sublogicOfTheo :: Hybrid -> (HSign, [HybridFORMULA]) -> () Source #

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

Defined in Fpl.Logic_Fpl

Methods

parse_basic_sen :: Fpl -> Maybe (FplBasicSpec -> AParser st FplForm) Source #

stability :: Fpl -> Stability Source #

data_logic :: Fpl -> Maybe AnyLogic Source #

top_sublogic :: Fpl -> () Source #

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

bottomSublogic :: Fpl -> Maybe () Source #

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

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

proj_sublogic_epsilon :: Fpl -> () -> FplSign -> FplMor Source #

provers :: Fpl -> [Prover FplSign FplForm FplMor () ()] Source #

default_prover :: Fpl -> String Source #

cons_checkers :: Fpl -> [ConsChecker FplSign FplForm () FplMor ()] Source #

conservativityCheck :: Fpl -> [ConservativityChecker FplSign FplForm FplMor] Source #

empty_proof_tree :: Fpl -> () Source #

syntaxTable :: Fpl -> FplSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Fpl -> Maybe OMCD Source #

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

export_senToOmdoc :: Fpl -> NameMap Symbol -> FplForm -> Result TCorOMElement Source #

export_theoryToOmdoc :: Fpl -> SigMap Symbol -> FplSign -> [Named FplForm] -> Result [TCElement] Source #

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

omdocToSen :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FplForm)) Source #

addOMadtToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [[OmdADT]] -> Result (FplSign, [Named FplForm]) Source #

addOmdocToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [TCElement] -> Result (FplSign, [Named FplForm]) Source #

sublogicOfTheo :: Fpl -> (FplSign, [FplForm]) -> () Source #

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

Defined in ExtModal.Logic_ExtModal

Methods

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

stability :: ExtModal -> Stability Source #

data_logic :: ExtModal -> Maybe AnyLogic Source #

top_sublogic :: ExtModal -> ExtModalSL Source #

all_sublogics :: ExtModal -> [ExtModalSL] Source #

bottomSublogic :: ExtModal -> Maybe ExtModalSL Source #

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

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

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

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

default_prover :: ExtModal -> String Source #

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

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

empty_proof_tree :: ExtModal -> () Source #

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

omdoc_metatheory :: ExtModal -> Maybe OMCD Source #

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

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

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

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

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

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

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

sublogicOfTheo :: ExtModal -> (ExtModalSign, [ExtModalFORMULA]) -> ExtModalSL Source #

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

Defined in ConstraintCASL.Logic_ConstraintCASL

Methods

parse_basic_sen :: ConstraintCASL -> Maybe (ConstraintCASLBasicSpec -> AParser st ConstraintCASLFORMULA) Source #

stability :: ConstraintCASL -> Stability Source #

data_logic :: ConstraintCASL -> Maybe AnyLogic Source #

top_sublogic :: ConstraintCASL -> CASL_Sublogics Source #

all_sublogics :: ConstraintCASL -> [CASL_Sublogics] Source #

bottomSublogic :: ConstraintCASL -> Maybe CASL_Sublogics Source #

sublogicDimensions :: ConstraintCASL -> [[CASL_Sublogics]] Source #

parseSublogic :: ConstraintCASL -> String -> Maybe CASL_Sublogics Source #

proj_sublogic_epsilon :: ConstraintCASL -> CASL_Sublogics -> ConstraintCASLSign -> ConstraintCASLMor Source #

provers :: ConstraintCASL -> [Prover ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor CASL_Sublogics ()] Source #

default_prover :: ConstraintCASL -> String Source #

cons_checkers :: ConstraintCASL -> [ConsChecker ConstraintCASLSign ConstraintCASLFORMULA CASL_Sublogics ConstraintCASLMor ()] Source #

conservativityCheck :: ConstraintCASL -> [ConservativityChecker ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor] Source #

empty_proof_tree :: ConstraintCASL -> () Source #

syntaxTable :: ConstraintCASL -> ConstraintCASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: ConstraintCASL -> Maybe OMCD Source #

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

export_senToOmdoc :: ConstraintCASL -> NameMap Symbol -> ConstraintCASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: ConstraintCASL -> SigMap Symbol -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result [TCElement] Source #

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

omdocToSen :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ConstraintCASLFORMULA)) Source #

addOMadtToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [[OmdADT]] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

addOmdocToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [TCElement] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

sublogicOfTheo :: ConstraintCASL -> (ConstraintCASLSign, [ConstraintCASLFORMULA]) -> CASL_Sublogics Source #

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

Defined in CoCASL.Logic_CoCASL

Methods

parse_basic_sen :: CoCASL -> Maybe (C_BASIC_SPEC -> AParser st CoCASLFORMULA) Source #

stability :: CoCASL -> Stability Source #

data_logic :: CoCASL -> Maybe AnyLogic Source #

top_sublogic :: CoCASL -> CoCASL_Sublogics Source #

all_sublogics :: CoCASL -> [CoCASL_Sublogics] Source #

bottomSublogic :: CoCASL -> Maybe CoCASL_Sublogics Source #

sublogicDimensions :: CoCASL -> [[CoCASL_Sublogics]] Source #

parseSublogic :: CoCASL -> String -> Maybe CoCASL_Sublogics Source #

proj_sublogic_epsilon :: CoCASL -> CoCASL_Sublogics -> CSign -> CoCASLMor Source #

provers :: CoCASL -> [Prover CSign CoCASLFORMULA CoCASLMor CoCASL_Sublogics ()] Source #

default_prover :: CoCASL -> String Source #

cons_checkers :: CoCASL -> [ConsChecker CSign CoCASLFORMULA CoCASL_Sublogics CoCASLMor ()] Source #

conservativityCheck :: CoCASL -> [ConservativityChecker CSign CoCASLFORMULA CoCASLMor] Source #

empty_proof_tree :: CoCASL -> () Source #

syntaxTable :: CoCASL -> CSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CoCASL -> Maybe OMCD Source #

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

export_senToOmdoc :: CoCASL -> NameMap Symbol -> CoCASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CoCASL -> SigMap Symbol -> CSign -> [Named CoCASLFORMULA] -> Result [TCElement] Source #

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

omdocToSen :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CoCASLFORMULA)) Source #

addOMadtToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named CoCASLFORMULA]) Source #

addOmdocToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [TCElement] -> Result (CSign, [Named CoCASLFORMULA]) Source #

sublogicOfTheo :: CoCASL -> (CSign, [CoCASLFORMULA]) -> CoCASL_Sublogics Source #

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

Defined in COL.Logic_COL

Methods

parse_basic_sen :: COL -> Maybe (C_BASIC_SPEC -> AParser st COLFORMULA) Source #

stability :: COL -> Stability Source #

data_logic :: COL -> Maybe AnyLogic Source #

top_sublogic :: COL -> () Source #

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

bottomSublogic :: COL -> Maybe () Source #

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

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

proj_sublogic_epsilon :: COL -> () -> CSign -> COLMor Source #

provers :: COL -> [Prover CSign COLFORMULA COLMor () ()] Source #

default_prover :: COL -> String Source #

cons_checkers :: COL -> [ConsChecker CSign COLFORMULA () COLMor ()] Source #

conservativityCheck :: COL -> [ConservativityChecker CSign COLFORMULA COLMor] Source #

empty_proof_tree :: COL -> () Source #

syntaxTable :: COL -> CSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: COL -> Maybe OMCD Source #

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

export_senToOmdoc :: COL -> NameMap Symbol -> COLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: COL -> SigMap Symbol -> CSign -> [Named COLFORMULA] -> Result [TCElement] Source #

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

omdocToSen :: COL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named COLFORMULA)) Source #

addOMadtToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named COLFORMULA]) Source #

addOmdocToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [TCElement] -> Result (CSign, [Named COLFORMULA]) Source #

sublogicOfTheo :: COL -> (CSign, [COLFORMULA]) -> () Source #

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

Defined in CASL_DL.Logic_CASL_DL

Methods

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

stability :: CASL_DL -> Stability Source #

data_logic :: CASL_DL -> Maybe AnyLogic Source #

top_sublogic :: CASL_DL -> CASL_DL_SL Source #

all_sublogics :: CASL_DL -> [CASL_DL_SL] Source #

bottomSublogic :: CASL_DL -> Maybe CASL_DL_SL Source #

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

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

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

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

default_prover :: CASL_DL -> String Source #

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

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

empty_proof_tree :: CASL_DL -> ProofTree Source #

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

omdoc_metatheory :: CASL_DL -> Maybe OMCD Source #

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

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

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

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

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

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

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

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

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

Defined in VSE.Logic_VSE

Methods

parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source #

stability :: VSE -> Stability Source #

data_logic :: VSE -> Maybe AnyLogic Source #

top_sublogic :: VSE -> () Source #

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

bottomSublogic :: VSE -> Maybe () Source #

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

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

proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source #

provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source #

default_prover :: VSE -> String Source #

cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source #

conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source #

empty_proof_tree :: VSE -> () Source #

syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source #

omdoc_metatheory :: VSE -> Maybe OMCD Source #

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

export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source #

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

omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source #

addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #

sublogicOfTheo :: VSE -> (VSESign, [Sentence]) -> () Source #

Comorphism OWL22CASL OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in OWL2.OWL22CASL

Comorphism CASL2OWL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Instance details

Defined in OWL2.CASL2OWL

Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Instance details

Defined in Comorphisms.ExtModal2OWL

Comorphism RelScheme2CASL RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.RelScheme2CASL

Comorphism Prop2CASL Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Prop2CASL

Comorphism Modal2CASL Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Modal2CASL

Comorphism Maude2CASL Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Maude2CASL

Comorphism ExtModal2CASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.ExtModal2CASL

Comorphism DFOL2CASL DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.DFOL2CASL

Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CommonLogic2CASL

Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CSMOF2CASL

Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.QVTR2CASL

Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.CFOL2IsabelleHOL

Comorphism CASL2TopSort CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2TopSort

Comorphism CASL2SubCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2SubCFOL

Comorphism ExtModal2ExtModalTotal ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.ExtModal2ExtModalTotal

Methods

sourceLogic :: ExtModal2ExtModalTotal -> ExtModal Source #

sourceSublogic :: ExtModal2ExtModalTotal -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2ExtModalTotal -> ExtModalSL Source #

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

targetLogic :: ExtModal2ExtModalTotal -> ExtModal Source #

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

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

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

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

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

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

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

is_model_transportable :: ExtModal2ExtModalTotal -> Bool Source #

has_model_expansion :: ExtModal2ExtModalTotal -> Bool Source #

is_weakly_amalgamable :: ExtModal2ExtModalTotal -> Bool Source #

constituents :: ExtModal2ExtModalTotal -> [String] Source #

isInclusionComorphism :: ExtModal2ExtModalTotal -> Bool Source #

rps :: ExtModal2ExtModalTotal -> Bool Source #

eps :: ExtModal2ExtModalTotal -> Bool Source #

isGTC :: ExtModal2ExtModalTotal -> Bool Source #

Comorphism CASL2Skolem CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2Skolem

Comorphism CASL2Prop CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2Prop

Comorphism CASL2Prenex CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2Prenex

Comorphism CASL2PCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2PCFOL

Comorphism CspCASL2Modal CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CspCASL2Modal

Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.ExtModal2ExtModalNoSubsorts

Methods

sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source #

sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source #

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

targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source #

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

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

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

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

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

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

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

is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source #

has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source #

is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source #

constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source #

isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source #

rps :: ExtModal2ExtModalNoSubsorts -> Bool Source #

eps :: ExtModal2ExtModalNoSubsorts -> Bool Source #

isGTC :: ExtModal2ExtModalNoSubsorts -> Bool Source #

Comorphism CASL2NNF CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2NNF

Comorphism CASL2Modal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2Modal

Comorphism CASL2Hybrid CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2Hybrid

Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2HasCASL

Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.ExtModal2HasCASL

Comorphism CASL2ExtModal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2ExtModal

Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2CspCASL

Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Adl2CASL

Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.CoCFOL2IsabelleHOL

Comorphism CoCASL2CoSubCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CoCASL2CoSubCFOL

Comorphism CoCASL2CoPCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CoCASL2CoPCFOL

Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2CoCASL

Comorphism CASL_DL2CASL CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL_DL2CASL

Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2VSERefine

Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2VSEImport

Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2VSE

Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics) (CompComorphism CASL2Modal Modal2CASL) CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Modifications.ModalEmbedding

Show a => Syntax (GenCspCASL a) CspBasicSpec CspSymbol CspSymbItems CspSymbMapItems Source #

Syntax of CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

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

Static Analysis for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

empty_signature :: GenCspCASL a -> CspCASLSign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Instance of Logic for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Methods

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

stability :: GenCspCASL a -> Stability Source #

data_logic :: GenCspCASL a -> Maybe AnyLogic Source #

top_sublogic :: GenCspCASL a -> () Source #

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

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

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

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

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

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

default_prover :: GenCspCASL a -> String Source #

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

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

empty_proof_tree :: GenCspCASL a -> () Source #

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

omdoc_metatheory :: GenCspCASL a -> Maybe OMCD Source #

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

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

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

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

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

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

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

sublogicOfTheo :: GenCspCASL a -> (CspCASLSign, [CspCASLSen]) -> () Source #

(MinSL a f, MinSL a s, MinSL a b, ProjForm a f, ProjSigItem a s f, ProjBasic a b s f) => ProjectSublogic (CASL_SL a) (BASIC_SPEC b s f) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

projectSublogic :: CASL_SL a -> BASIC_SPEC b s f -> BASIC_SPEC b s f Source #

(MinSL a f, MinSL a s, MinSL a b) => MinSublogic (CASL_SL a) (BASIC_SPEC b s f) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

minSublogic :: BASIC_SPEC b s f -> CASL_SL a Source #

(CspCASLSemantics a, CspCASLSemantics b) => Comorphism (CspCASL2CspCASL a b) (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () (GenCspCASL b) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source # 
Instance details

Defined in CspCASL.Comorphisms

(Data b, Data s, Data f) => Data (BASIC_SPEC b s f) Source # 
Instance details

Defined in CASL.AS_Basic_CASL

Methods

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

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

toConstr :: BASIC_SPEC b s f -> Constr

dataTypeOf :: BASIC_SPEC b s f -> DataType

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

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

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

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

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

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

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

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

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

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

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

Defined in CASL.AS_Basic_CASL

Methods

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

show :: BASIC_SPEC b s f -> String

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

Generic (BASIC_SPEC b s f) 
Instance details

Defined in CASL.ATC_CASL

Associated Types

type Rep (BASIC_SPEC b s f) :: Type -> Type

Methods

from :: BASIC_SPEC b s f -> Rep (BASIC_SPEC b s f) x

to :: Rep (BASIC_SPEC b s f) x -> BASIC_SPEC b s f

Semigroup (BASIC_SPEC b s f) 
Instance details

Defined in CASL.Logic_CASL

Methods

(<>) :: BASIC_SPEC b s f -> BASIC_SPEC b s f -> BASIC_SPEC b s f #

sconcat :: NonEmpty (BASIC_SPEC b s f) -> BASIC_SPEC b s f

stimes :: Integral b0 => b0 -> BASIC_SPEC b s f -> BASIC_SPEC b s f

Monoid (BASIC_SPEC b s f) 
Instance details

Defined in CASL.Logic_CASL

Methods

mempty :: BASIC_SPEC b s f

mappend :: BASIC_SPEC b s f -> BASIC_SPEC b s f -> BASIC_SPEC b s f

mconcat :: [BASIC_SPEC b s f] -> BASIC_SPEC b s f

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

Defined in CASL.AS_Basic_CASL

Methods

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

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

(FromJSON b, FromJSON s, FromJSON f) => FromJSON (BASIC_SPEC b s f) 
Instance details

Defined in CASL.ATC_CASL

Methods

parseJSON :: Value -> Parser (BASIC_SPEC b s f)

parseJSONList :: Value -> Parser [BASIC_SPEC b s f]

(ToJSON b, ToJSON s, ToJSON f) => ToJSON (BASIC_SPEC b s f) 
Instance details

Defined in CASL.ATC_CASL

Methods

toJSON :: BASIC_SPEC b s f -> Value

toEncoding :: BASIC_SPEC b s f -> Encoding

toJSONList :: [BASIC_SPEC b s f] -> Value

toEncodingList :: [BASIC_SPEC b s f] -> Encoding

(ShATermConvertible b, ShATermConvertible s, ShATermConvertible f) => ShATermConvertible (BASIC_SPEC b s f) 
Instance details

Defined in CASL.ATC_CASL

Methods

toShATermAux :: ATermTable -> BASIC_SPEC b s f -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [BASIC_SPEC b s f] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC b s f)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_SPEC b s f])

(Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_SPEC b s f) Source # 
Instance details

Defined in CASL.ToDoc

Methods

pretty :: BASIC_SPEC b s f -> Doc Source #

pretties :: [BASIC_SPEC b s f] -> Doc Source #

ATermConvertibleSML (BASIC_SPEC a b c) Source # 
Instance details

Defined in ATC.Sml_cats

Methods

from_sml_ShATerm :: ATermTable -> BASIC_SPEC a b c

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

type Rep (BASIC_SPEC b s f) 
Instance details

Defined in CASL.ATC_CASL

type Rep (BASIC_SPEC b s f) = D1 ('MetaData "BASIC_SPEC" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Basic_spec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (BASIC_ITEMS b s f)])))

data BASIC_ITEMS b s f Source #

Instances

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

Defined in CASL.AS_Basic_CASL

Methods

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

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

toConstr :: BASIC_ITEMS b s f -> Constr

dataTypeOf :: BASIC_ITEMS b s f -> DataType

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

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

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

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

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

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

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

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

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

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

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

Defined in CASL.AS_Basic_CASL

Methods

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

show :: BASIC_ITEMS b s f -> String

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

Generic (BASIC_ITEMS b s f) 
Instance details

Defined in CASL.ATC_CASL

Associated Types

type Rep (BASIC_ITEMS b s f) :: Type -> Type

Methods

from :: BASIC_ITEMS b s f -> Rep (BASIC_ITEMS b s f) x

to :: Rep (BASIC_ITEMS b s f) x -> BASIC_ITEMS b s f

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

Defined in CASL.AS_Basic_CASL

Methods

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

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

(FromJSON b, FromJSON s, FromJSON f) => FromJSON (BASIC_ITEMS b s f) 
Instance details

Defined in CASL.ATC_CASL

Methods

parseJSON :: Value -> Parser (BASIC_ITEMS b s f)

parseJSONList :: Value -> Parser [BASIC_ITEMS b s f]

(ToJSON b, ToJSON s, ToJSON f) => ToJSON (BASIC_ITEMS b s f) 
Instance details

Defined in CASL.ATC_CASL

Methods

toJSON :: BASIC_ITEMS b s f -> Value

toEncoding :: BASIC_ITEMS b s f -> Encoding

toJSONList :: [BASIC_ITEMS b s f] -> Value

toEncodingList :: [BASIC_ITEMS b s f] -> Encoding

(ShATermConvertible b, ShATermConvertible s, ShATermConvertible f) => ShATermConvertible (BASIC_ITEMS b s f) 
Instance details

Defined in CASL.ATC_CASL

Methods

toShATermAux :: ATermTable -> BASIC_ITEMS b s f -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [BASIC_ITEMS b s f] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_ITEMS b s f)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_ITEMS b s f])

(Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_ITEMS b s f) Source # 
Instance details

Defined in CASL.ToDoc

Methods

pretty :: BASIC_ITEMS b s f -> Doc Source #

pretties :: [BASIC_ITEMS b s f] -> Doc Source #

ATermConvertibleSML (BASIC_ITEMS a b c) Source # 
Instance details

Defined in ATC.Sml_cats

Methods

from_sml_ShATerm :: ATermTable -> BASIC_ITEMS a b c

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

type Rep (BASIC_ITEMS b s f) 
Instance details

Defined in CASL.ATC_CASL

type Rep (BASIC_ITEMS b s f) = D1 ('MetaData "BASIC_ITEMS" "CASL.AS_Basic_CASL" "main" 'False) ((C1 ('MetaCons "Sig_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SIG_ITEMS s f))) :+: (C1 ('MetaCons "Free_datatype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SortsKind) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted DATATYPE_DECL]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Sort_gen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (SIG_ITEMS s f)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "Var_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_DECL]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Local_var_axioms" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_DECL]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (FORMULA f)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "Axiom_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (FORMULA f)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Ext_BASIC_ITEMS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)))))

data SortsKind Source #

Instances

Instances details
Data SortsKind Source # 
Instance details

Defined in CASL.AS_Basic_CASL

Methods

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

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

toConstr :: SortsKind -> Constr

dataTypeOf :: SortsKind -> DataType

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

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

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

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

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

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

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

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

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

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

Show SortsKind Source # 
Instance details

Defined in CASL.AS_Basic_CASL

Methods

showsPrec :: Int -> SortsKind -> ShowS

show :: SortsKind -> String

showList :: [SortsKind] -> ShowS

Generic SortsKind 
Instance details

Defined in CASL.ATC_CASL

Associated Types

type Rep SortsKind :: Type -> Type

Methods

from :: SortsKind -> Rep SortsKind x

to :: Rep SortsKind x -> SortsKind

GetRange SortsKind Source # 
Instance details

Defined in CASL.AS_Basic_CASL

FromJSON SortsKind 
Instance details

Defined in CASL.ATC_CASL

Methods

parseJSON :: Value -> Parser SortsKind

parseJSONList :: Value -> Parser [SortsKind]

ToJSON SortsKind 
Instance details

Defined in CASL.ATC_CASL

Methods

toJSON :: SortsKind -> Value

toEncoding :: SortsKind -> Encoding

toJSONList :: [SortsKind] -> Value

toEncodingList :: [SortsKind] -> Encoding

ShATermConvertible SortsKind 
Instance details

Defined in CASL.ATC_CASL

Methods

toShATermAux :: ATermTable -> SortsKind -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [SortsKind] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, SortsKind)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [SortsKind])

type Rep SortsKind 
Instance details

Defined in CASL.ATC_CASL

type Rep SortsKind = D1 ('MetaData "SortsKind" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "NonEmptySorts" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PossiblyEmptySorts" 'PrefixI 'False) (U1 :: Type -> Type))