Hets - the Heterogeneous Tool Set
Copyright(c) Klaus Luettich Uni Bremen 2002-2005
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

CASL.Logic_CASL

Description

Instance of class Logic for the CASL logic Also the instances for Syntax and Category.

Documentation

data CASL Source #

Constructors

CASL 

Instances

Instances details
Show CASL Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

showsPrec :: Int -> CASL -> ShowS

show :: CASL -> String

showList :: [CASL] -> ShowS

Language CASL Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

language_name :: CASL -> String Source #

description :: CASL -> String Source #

Sentences CASL CASLFORMULA CASLSign CASLMor Symbol Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

map_sen :: CASL -> CASLMor -> CASLFORMULA -> Result CASLFORMULA Source #

simplify_sen :: CASL -> CASLSign -> CASLFORMULA -> CASLFORMULA Source #

negation :: CASL -> CASLFORMULA -> Maybe CASLFORMULA Source #

print_sign :: CASL -> CASLSign -> Doc Source #

print_named :: CASL -> Named CASLFORMULA -> Doc Source #

sym_of :: CASL -> CASLSign -> [Set Symbol] Source #

mostSymsOf :: CASL -> CASLSign -> [Symbol] Source #

symmap_of :: CASL -> CASLMor -> EndoMap Symbol Source #

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

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

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

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

symsOfSen :: CASL -> CASLSign -> CASLFORMULA -> [Symbol] Source #

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

Syntax CASL CASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

parsersAndPrinters :: CASL -> Map String (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc) Source #

parse_basic_spec :: CASL -> Maybe (PrefixMap -> AParser st CASLBasicSpec) Source #

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

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

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

toItem :: CASL -> CASLBasicSpec -> Item Source #

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

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 #

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 #

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

Defined in OWL2.OWL22CASL

Methods

sourceLogic :: OWL22CASL -> OWL2 Source #

sourceSublogic :: OWL22CASL -> ProfSub Source #

sourceSublogicLossy :: OWL22CASL -> ProfSub Source #

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

targetLogic :: OWL22CASL -> CASL Source #

mapSublogic :: OWL22CASL -> ProfSub -> Maybe CASL_Sublogics Source #

map_theory :: OWL22CASL -> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: OWL22CASL -> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: OWL22CASL -> OWLMorphism -> Result CASLMor Source #

map_sentence :: OWL22CASL -> Sign -> Axiom -> Result CASLFORMULA Source #

map_symbol :: OWL22CASL -> Sign -> Entity -> Set Symbol Source #

extractModel :: OWL22CASL -> Sign -> ProofTree -> Result (Sign, [Named Axiom]) Source #

is_model_transportable :: OWL22CASL -> Bool Source #

has_model_expansion :: OWL22CASL -> Bool Source #

is_weakly_amalgamable :: OWL22CASL -> Bool Source #

constituents :: OWL22CASL -> [String] Source #

isInclusionComorphism :: OWL22CASL -> Bool Source #

rps :: OWL22CASL -> Bool Source #

eps :: OWL22CASL -> Bool Source #

isGTC :: OWL22CASL -> Bool Source #

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

Defined in OWL2.CASL2OWL

Methods

sourceLogic :: CASL2OWL -> CASL Source #

sourceSublogic :: CASL2OWL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2OWL -> CASL_Sublogics Source #

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

targetLogic :: CASL2OWL -> OWL2 Source #

mapSublogic :: CASL2OWL -> CASL_Sublogics -> Maybe ProfSub Source #

map_theory :: CASL2OWL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom]) Source #

mapMarkedTheory :: CASL2OWL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom]) Source #

map_morphism :: CASL2OWL -> CASLMor -> Result OWLMorphism Source #

map_sentence :: CASL2OWL -> CASLSign -> CASLFORMULA -> Result Axiom Source #

map_symbol :: CASL2OWL -> CASLSign -> Symbol -> Set Entity Source #

extractModel :: CASL2OWL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2OWL -> Bool Source #

has_model_expansion :: CASL2OWL -> Bool Source #

is_weakly_amalgamable :: CASL2OWL -> Bool Source #

constituents :: CASL2OWL -> [String] Source #

isInclusionComorphism :: CASL2OWL -> Bool Source #

rps :: CASL2OWL -> Bool Source #

eps :: CASL2OWL -> Bool Source #

isGTC :: CASL2OWL -> Bool Source #

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

Defined in Comorphisms.RelScheme2CASL

Methods

sourceLogic :: RelScheme2CASL -> RelScheme Source #

sourceSublogic :: RelScheme2CASL -> () Source #

sourceSublogicLossy :: RelScheme2CASL -> () Source #

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

targetLogic :: RelScheme2CASL -> CASL Source #

mapSublogic :: RelScheme2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: RelScheme2CASL -> RSMorphism -> Result CASLMor Source #

map_sentence :: RelScheme2CASL -> Sign -> Sentence -> Result CASLFORMULA Source #

map_symbol :: RelScheme2CASL -> Sign -> RSSymbol -> Set Symbol Source #

extractModel :: RelScheme2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source #

is_model_transportable :: RelScheme2CASL -> Bool Source #

has_model_expansion :: RelScheme2CASL -> Bool Source #

is_weakly_amalgamable :: RelScheme2CASL -> Bool Source #

constituents :: RelScheme2CASL -> [String] Source #

isInclusionComorphism :: RelScheme2CASL -> Bool Source #

rps :: RelScheme2CASL -> Bool Source #

eps :: RelScheme2CASL -> Bool Source #

isGTC :: RelScheme2CASL -> Bool Source #

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

Defined in Comorphisms.Prop2CASL

Methods

sourceLogic :: Prop2CASL -> Propositional Source #

sourceSublogic :: Prop2CASL -> PropSL Source #

sourceSublogicLossy :: Prop2CASL -> PropSL Source #

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

targetLogic :: Prop2CASL -> CASL Source #

mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics Source #

map_theory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: Prop2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: Prop2CASL -> Sign -> FORMULA -> Result CASLFORMULA Source #

map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: Prop2CASL -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source #

is_model_transportable :: Prop2CASL -> Bool Source #

has_model_expansion :: Prop2CASL -> Bool Source #

is_weakly_amalgamable :: Prop2CASL -> Bool Source #

constituents :: Prop2CASL -> [String] Source #

isInclusionComorphism :: Prop2CASL -> Bool Source #

rps :: Prop2CASL -> Bool Source #

eps :: Prop2CASL -> Bool Source #

isGTC :: Prop2CASL -> Bool Source #

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

Defined in Comorphisms.Modal2CASL

Methods

sourceLogic :: Modal2CASL -> Modal Source #

sourceSublogic :: Modal2CASL -> () Source #

sourceSublogicLossy :: Modal2CASL -> () Source #

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

targetLogic :: Modal2CASL -> CASL Source #

mapSublogic :: Modal2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: Modal2CASL -> ModalMor -> Result CASLMor Source #

map_sentence :: Modal2CASL -> MSign -> ModalFORMULA -> Result CASLFORMULA Source #

map_symbol :: Modal2CASL -> MSign -> Symbol -> Set Symbol Source #

extractModel :: Modal2CASL -> MSign -> ProofTree -> Result (MSign, [Named ModalFORMULA]) Source #

is_model_transportable :: Modal2CASL -> Bool Source #

has_model_expansion :: Modal2CASL -> Bool Source #

is_weakly_amalgamable :: Modal2CASL -> Bool Source #

constituents :: Modal2CASL -> [String] Source #

isInclusionComorphism :: Modal2CASL -> Bool Source #

rps :: Modal2CASL -> Bool Source #

eps :: Modal2CASL -> Bool Source #

isGTC :: Modal2CASL -> Bool Source #

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

Defined in Comorphisms.Maude2CASL

Methods

sourceLogic :: Maude2CASL -> Maude Source #

sourceSublogic :: Maude2CASL -> () Source #

sourceSublogicLossy :: Maude2CASL -> () Source #

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

targetLogic :: Maude2CASL -> CASL Source #

mapSublogic :: Maude2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: Maude2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: Maude2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: Maude2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: Maude2CASL -> Sign -> Sentence -> Result CASLFORMULA Source #

map_symbol :: Maude2CASL -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: Maude2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source #

is_model_transportable :: Maude2CASL -> Bool Source #

has_model_expansion :: Maude2CASL -> Bool Source #

is_weakly_amalgamable :: Maude2CASL -> Bool Source #

constituents :: Maude2CASL -> [String] Source #

isInclusionComorphism :: Maude2CASL -> Bool Source #

rps :: Maude2CASL -> Bool Source #

eps :: Maude2CASL -> Bool Source #

isGTC :: Maude2CASL -> Bool Source #

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

Defined in Comorphisms.ExtModal2CASL

Methods

sourceLogic :: ExtModal2CASL -> ExtModal Source #

sourceSublogic :: ExtModal2CASL -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2CASL -> ExtModalSL Source #

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

targetLogic :: ExtModal2CASL -> CASL Source #

mapSublogic :: ExtModal2CASL -> ExtModalSL -> Maybe CASL_Sublogics Source #

map_theory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: ExtModal2CASL -> ExtModalMorph -> Result CASLMor Source #

map_sentence :: ExtModal2CASL -> ExtModalSign -> ExtModalFORMULA -> Result CASLFORMULA Source #

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

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

is_model_transportable :: ExtModal2CASL -> Bool Source #

has_model_expansion :: ExtModal2CASL -> Bool Source #

is_weakly_amalgamable :: ExtModal2CASL -> Bool Source #

constituents :: ExtModal2CASL -> [String] Source #

isInclusionComorphism :: ExtModal2CASL -> Bool Source #

rps :: ExtModal2CASL -> Bool Source #

eps :: ExtModal2CASL -> Bool Source #

isGTC :: ExtModal2CASL -> Bool Source #

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

Defined in Comorphisms.DFOL2CASL

Methods

sourceLogic :: DFOL2CASL -> DFOL Source #

sourceSublogic :: DFOL2CASL -> () Source #

sourceSublogicLossy :: DFOL2CASL -> () Source #

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

targetLogic :: DFOL2CASL -> CASL Source #

mapSublogic :: DFOL2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: DFOL2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: DFOL2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: DFOL2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: DFOL2CASL -> Sign -> FORMULA -> Result CASLFORMULA Source #

map_symbol :: DFOL2CASL -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: DFOL2CASL -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source #

is_model_transportable :: DFOL2CASL -> Bool Source #

has_model_expansion :: DFOL2CASL -> Bool Source #

is_weakly_amalgamable :: DFOL2CASL -> Bool Source #

constituents :: DFOL2CASL -> [String] Source #

isInclusionComorphism :: DFOL2CASL -> Bool Source #

rps :: DFOL2CASL -> Bool Source #

eps :: DFOL2CASL -> Bool Source #

isGTC :: DFOL2CASL -> Bool Source #

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

Defined in Comorphisms.CommonLogic2CASL

Methods

sourceLogic :: CL2CFOL -> CommonLogic Source #

sourceSublogic :: CL2CFOL -> CommonLogicSL Source #

sourceSublogicLossy :: CL2CFOL -> CommonLogicSL Source #

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

targetLogic :: CL2CFOL -> CASL Source #

mapSublogic :: CL2CFOL -> CommonLogicSL -> Maybe CASL_Sublogics Source #

map_theory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CL2CFOL -> Morphism -> Result CASLMor Source #

map_sentence :: CL2CFOL -> Sign -> TEXT_META -> Result CASLFORMULA Source #

map_symbol :: CL2CFOL -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: CL2CFOL -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source #

is_model_transportable :: CL2CFOL -> Bool Source #

has_model_expansion :: CL2CFOL -> Bool Source #

is_weakly_amalgamable :: CL2CFOL -> Bool Source #

constituents :: CL2CFOL -> [String] Source #

isInclusionComorphism :: CL2CFOL -> Bool Source #

rps :: CL2CFOL -> Bool Source #

eps :: CL2CFOL -> Bool Source #

isGTC :: CL2CFOL -> Bool Source #

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

Defined in Comorphisms.CSMOF2CASL

Methods

sourceLogic :: CSMOF2CASL -> CSMOF Source #

sourceSublogic :: CSMOF2CASL -> () Source #

sourceSublogicLossy :: CSMOF2CASL -> () Source #

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

targetLogic :: CSMOF2CASL -> CASL Source #

mapSublogic :: CSMOF2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: CSMOF2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CSMOF2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CSMOF2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: CSMOF2CASL -> Sign -> Sen -> Result CASLFORMULA Source #

map_symbol :: CSMOF2CASL -> Sign -> () -> Set Symbol Source #

extractModel :: CSMOF2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source #

is_model_transportable :: CSMOF2CASL -> Bool Source #

has_model_expansion :: CSMOF2CASL -> Bool Source #

is_weakly_amalgamable :: CSMOF2CASL -> Bool Source #

constituents :: CSMOF2CASL -> [String] Source #

isInclusionComorphism :: CSMOF2CASL -> Bool Source #

rps :: CSMOF2CASL -> Bool Source #

eps :: CSMOF2CASL -> Bool Source #

isGTC :: CSMOF2CASL -> Bool Source #

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

Defined in Comorphisms.QVTR2CASL

Methods

sourceLogic :: QVTR2CASL -> QVTR Source #

sourceSublogic :: QVTR2CASL -> () Source #

sourceSublogicLossy :: QVTR2CASL -> () Source #

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

targetLogic :: QVTR2CASL -> CASL Source #

mapSublogic :: QVTR2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: QVTR2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: QVTR2CASL -> Sign -> Sen -> Result CASLFORMULA Source #

map_symbol :: QVTR2CASL -> Sign -> () -> Set Symbol Source #

extractModel :: QVTR2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source #

is_model_transportable :: QVTR2CASL -> Bool Source #

has_model_expansion :: QVTR2CASL -> Bool Source #

is_weakly_amalgamable :: QVTR2CASL -> Bool Source #

constituents :: QVTR2CASL -> [String] Source #

isInclusionComorphism :: QVTR2CASL -> Bool Source #

rps :: QVTR2CASL -> Bool Source #

eps :: QVTR2CASL -> Bool Source #

isGTC :: QVTR2CASL -> Bool Source #

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

Defined in Comorphisms.CFOL2IsabelleHOL

Methods

sourceLogic :: CFOL2IsabelleHOL -> CASL Source #

sourceSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics Source #

sourceSublogicLossy :: CFOL2IsabelleHOL -> CASL_Sublogics Source #

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

targetLogic :: CFOL2IsabelleHOL -> Isabelle Source #

mapSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics -> Maybe () Source #

map_theory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source #

mapMarkedTheory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source #

map_morphism :: CFOL2IsabelleHOL -> CASLMor -> Result IsabelleMorphism Source #

map_sentence :: CFOL2IsabelleHOL -> CASLSign -> CASLFORMULA -> Result Sentence Source #

map_symbol :: CFOL2IsabelleHOL -> CASLSign -> Symbol -> Set () Source #

extractModel :: CFOL2IsabelleHOL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CFOL2IsabelleHOL -> Bool Source #

has_model_expansion :: CFOL2IsabelleHOL -> Bool Source #

is_weakly_amalgamable :: CFOL2IsabelleHOL -> Bool Source #

constituents :: CFOL2IsabelleHOL -> [String] Source #

isInclusionComorphism :: CFOL2IsabelleHOL -> Bool Source #

rps :: CFOL2IsabelleHOL -> Bool Source #

eps :: CFOL2IsabelleHOL -> Bool Source #

isGTC :: CFOL2IsabelleHOL -> Bool Source #

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

Defined in Comorphisms.CASL2TopSort

Methods

sourceLogic :: CASL2TopSort -> CASL Source #

sourceSublogic :: CASL2TopSort -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2TopSort -> CASL_Sublogics Source #

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

targetLogic :: CASL2TopSort -> CASL Source #

mapSublogic :: CASL2TopSort -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2TopSort -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2TopSort -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2TopSort -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2TopSort -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2TopSort -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2TopSort -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2TopSort -> Bool Source #

has_model_expansion :: CASL2TopSort -> Bool Source #

is_weakly_amalgamable :: CASL2TopSort -> Bool Source #

constituents :: CASL2TopSort -> [String] Source #

isInclusionComorphism :: CASL2TopSort -> Bool Source #

rps :: CASL2TopSort -> Bool Source #

eps :: CASL2TopSort -> Bool Source #

isGTC :: CASL2TopSort -> Bool Source #

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

Defined in Comorphisms.CASL2SubCFOL

Methods

sourceLogic :: CASL2SubCFOL -> CASL Source #

sourceSublogic :: CASL2SubCFOL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2SubCFOL -> CASL_Sublogics Source #

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

targetLogic :: CASL2SubCFOL -> CASL Source #

mapSublogic :: CASL2SubCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2SubCFOL -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2SubCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2SubCFOL -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2SubCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2SubCFOL -> Bool Source #

has_model_expansion :: CASL2SubCFOL -> Bool Source #

is_weakly_amalgamable :: CASL2SubCFOL -> Bool Source #

constituents :: CASL2SubCFOL -> [String] Source #

isInclusionComorphism :: CASL2SubCFOL -> Bool Source #

rps :: CASL2SubCFOL -> Bool Source #

eps :: CASL2SubCFOL -> Bool Source #

isGTC :: CASL2SubCFOL -> Bool Source #

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

Defined in Comorphisms.CASL2Skolem

Methods

sourceLogic :: CASL2Skolem -> CASL Source #

sourceSublogic :: CASL2Skolem -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2Skolem -> CASL_Sublogics Source #

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

targetLogic :: CASL2Skolem -> CASL Source #

mapSublogic :: CASL2Skolem -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2Skolem -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2Skolem -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2Skolem -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2Skolem -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2Skolem -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2Skolem -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2Skolem -> Bool Source #

has_model_expansion :: CASL2Skolem -> Bool Source #

is_weakly_amalgamable :: CASL2Skolem -> Bool Source #

constituents :: CASL2Skolem -> [String] Source #

isInclusionComorphism :: CASL2Skolem -> Bool Source #

rps :: CASL2Skolem -> Bool Source #

eps :: CASL2Skolem -> Bool Source #

isGTC :: CASL2Skolem -> Bool Source #

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

Defined in Comorphisms.CASL2Prop

Methods

sourceLogic :: CASL2Prop -> CASL Source #

sourceSublogic :: CASL2Prop -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2Prop -> CASL_Sublogics Source #

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

targetLogic :: CASL2Prop -> Propositional Source #

mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL Source #

map_theory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #

mapMarkedTheory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #

map_morphism :: CASL2Prop -> CASLMor -> Result Morphism Source #

map_sentence :: CASL2Prop -> CASLSign -> CASLFORMULA -> Result FORMULA Source #

map_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source #

extractModel :: CASL2Prop -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2Prop -> Bool Source #

has_model_expansion :: CASL2Prop -> Bool Source #

is_weakly_amalgamable :: CASL2Prop -> Bool Source #

constituents :: CASL2Prop -> [String] Source #

isInclusionComorphism :: CASL2Prop -> Bool Source #

rps :: CASL2Prop -> Bool Source #

eps :: CASL2Prop -> Bool Source #

isGTC :: CASL2Prop -> Bool Source #

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

Defined in Comorphisms.CASL2Prenex

Methods

sourceLogic :: CASL2Prenex -> CASL Source #

sourceSublogic :: CASL2Prenex -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2Prenex -> CASL_Sublogics Source #

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

targetLogic :: CASL2Prenex -> CASL Source #

mapSublogic :: CASL2Prenex -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2Prenex -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2Prenex -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2Prenex -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2Prenex -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2Prenex -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2Prenex -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2Prenex -> Bool Source #

has_model_expansion :: CASL2Prenex -> Bool Source #

is_weakly_amalgamable :: CASL2Prenex -> Bool Source #

constituents :: CASL2Prenex -> [String] Source #

isInclusionComorphism :: CASL2Prenex -> Bool Source #

rps :: CASL2Prenex -> Bool Source #

eps :: CASL2Prenex -> Bool Source #

isGTC :: CASL2Prenex -> Bool Source #

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

Defined in Comorphisms.CASL2PCFOL

Methods

sourceLogic :: CASL2PCFOL -> CASL Source #

sourceSublogic :: CASL2PCFOL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2PCFOL -> CASL_Sublogics Source #

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

targetLogic :: CASL2PCFOL -> CASL Source #

mapSublogic :: CASL2PCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2PCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2PCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2PCFOL -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2PCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2PCFOL -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2PCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2PCFOL -> Bool Source #

has_model_expansion :: CASL2PCFOL -> Bool Source #

is_weakly_amalgamable :: CASL2PCFOL -> Bool Source #

constituents :: CASL2PCFOL -> [String] Source #

isInclusionComorphism :: CASL2PCFOL -> Bool Source #

rps :: CASL2PCFOL -> Bool Source #

eps :: CASL2PCFOL -> Bool Source #

isGTC :: CASL2PCFOL -> Bool Source #

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

Defined in Comorphisms.CASL2NNF

Methods

sourceLogic :: CASL2NNF -> CASL Source #

sourceSublogic :: CASL2NNF -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2NNF -> CASL_Sublogics Source #

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

targetLogic :: CASL2NNF -> CASL Source #

mapSublogic :: CASL2NNF -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2NNF -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2NNF -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2NNF -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2NNF -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2NNF -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2NNF -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2NNF -> Bool Source #

has_model_expansion :: CASL2NNF -> Bool Source #

is_weakly_amalgamable :: CASL2NNF -> Bool Source #

constituents :: CASL2NNF -> [String] Source #

isInclusionComorphism :: CASL2NNF -> Bool Source #

rps :: CASL2NNF -> Bool Source #

eps :: CASL2NNF -> Bool Source #

isGTC :: CASL2NNF -> Bool Source #

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

Defined in Comorphisms.CASL2Modal

Methods

sourceLogic :: CASL2Modal -> CASL Source #

sourceSublogic :: CASL2Modal -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2Modal -> CASL_Sublogics Source #

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

targetLogic :: CASL2Modal -> Modal Source #

mapSublogic :: CASL2Modal -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #

mapMarkedTheory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #

map_morphism :: CASL2Modal -> CASLMor -> Result ModalMor Source #

map_sentence :: CASL2Modal -> CASLSign -> CASLFORMULA -> Result ModalFORMULA Source #

map_symbol :: CASL2Modal -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2Modal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2Modal -> Bool Source #

has_model_expansion :: CASL2Modal -> Bool Source #

is_weakly_amalgamable :: CASL2Modal -> Bool Source #

constituents :: CASL2Modal -> [String] Source #

isInclusionComorphism :: CASL2Modal -> Bool Source #

rps :: CASL2Modal -> Bool Source #

eps :: CASL2Modal -> Bool Source #

isGTC :: CASL2Modal -> Bool Source #

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

Defined in Comorphisms.CASL2Hybrid

Methods

sourceLogic :: CASL2Hybrid -> CASL Source #

sourceSublogic :: CASL2Hybrid -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2Hybrid -> CASL_Sublogics Source #

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

targetLogic :: CASL2Hybrid -> Hybrid Source #

mapSublogic :: CASL2Hybrid -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source #

mapMarkedTheory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source #

map_morphism :: CASL2Hybrid -> CASLMor -> Result HybridMor Source #

map_sentence :: CASL2Hybrid -> CASLSign -> CASLFORMULA -> Result HybridFORMULA Source #

map_symbol :: CASL2Hybrid -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2Hybrid -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2Hybrid -> Bool Source #

has_model_expansion :: CASL2Hybrid -> Bool Source #

is_weakly_amalgamable :: CASL2Hybrid -> Bool Source #

constituents :: CASL2Hybrid -> [String] Source #

isInclusionComorphism :: CASL2Hybrid -> Bool Source #

rps :: CASL2Hybrid -> Bool Source #

eps :: CASL2Hybrid -> Bool Source #

isGTC :: CASL2Hybrid -> Bool Source #

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

Defined in Comorphisms.CASL2HasCASL

Methods

sourceLogic :: CASL2HasCASL -> CASL Source #

sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source #

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

targetLogic :: CASL2HasCASL -> HasCASL Source #

mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source #

map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source #

mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source #

map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source #

map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source #

map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source #

extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2HasCASL -> Bool Source #

has_model_expansion :: CASL2HasCASL -> Bool Source #

is_weakly_amalgamable :: CASL2HasCASL -> Bool Source #

constituents :: CASL2HasCASL -> [String] Source #

isInclusionComorphism :: CASL2HasCASL -> Bool Source #

rps :: CASL2HasCASL -> Bool Source #

eps :: CASL2HasCASL -> Bool Source #

isGTC :: CASL2HasCASL -> Bool Source #

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

Defined in Comorphisms.CASL2ExtModal

Methods

sourceLogic :: CASL2ExtModal -> CASL Source #

sourceSublogic :: CASL2ExtModal -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2ExtModal -> CASL_Sublogics Source #

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

targetLogic :: CASL2ExtModal -> ExtModal Source #

mapSublogic :: CASL2ExtModal -> CASL_Sublogics -> Maybe ExtModalSL Source #

map_theory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

mapMarkedTheory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

map_morphism :: CASL2ExtModal -> CASLMor -> Result ExtModalMorph Source #

map_sentence :: CASL2ExtModal -> CASLSign -> CASLFORMULA -> Result ExtModalFORMULA Source #

map_symbol :: CASL2ExtModal -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2ExtModal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2ExtModal -> Bool Source #

has_model_expansion :: CASL2ExtModal -> Bool Source #

is_weakly_amalgamable :: CASL2ExtModal -> Bool Source #

constituents :: CASL2ExtModal -> [String] Source #

isInclusionComorphism :: CASL2ExtModal -> Bool Source #

rps :: CASL2ExtModal -> Bool Source #

eps :: CASL2ExtModal -> Bool Source #

isGTC :: CASL2ExtModal -> Bool Source #

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

Defined in Comorphisms.CASL2CspCASL

Methods

sourceLogic :: CASL2CspCASL -> CASL Source #

sourceSublogic :: CASL2CspCASL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2CspCASL -> CASL_Sublogics Source #

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

targetLogic :: CASL2CspCASL -> CspCASL Source #

mapSublogic :: CASL2CspCASL -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #

mapMarkedTheory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #

map_morphism :: CASL2CspCASL -> CASLMor -> Result CspCASLMorphism Source #

map_sentence :: CASL2CspCASL -> CASLSign -> CASLFORMULA -> Result CspCASLSen Source #

map_symbol :: CASL2CspCASL -> CASLSign -> Symbol -> Set CspSymbol Source #

extractModel :: CASL2CspCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2CspCASL -> Bool Source #

has_model_expansion :: CASL2CspCASL -> Bool Source #

is_weakly_amalgamable :: CASL2CspCASL -> Bool Source #

constituents :: CASL2CspCASL -> [String] Source #

isInclusionComorphism :: CASL2CspCASL -> Bool Source #

rps :: CASL2CspCASL -> Bool Source #

eps :: CASL2CspCASL -> Bool Source #

isGTC :: CASL2CspCASL -> Bool Source #

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

Defined in Comorphisms.Adl2CASL

Methods

sourceLogic :: Adl2CASL -> Adl Source #

sourceSublogic :: Adl2CASL -> () Source #

sourceSublogicLossy :: Adl2CASL -> () Source #

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

targetLogic :: Adl2CASL -> CASL Source #

mapSublogic :: Adl2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: Adl2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: Adl2CASL -> Sign -> Sen -> Result CASLFORMULA Source #

map_symbol :: Adl2CASL -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: Adl2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source #

is_model_transportable :: Adl2CASL -> Bool Source #

has_model_expansion :: Adl2CASL -> Bool Source #

is_weakly_amalgamable :: Adl2CASL -> Bool Source #

constituents :: Adl2CASL -> [String] Source #

isInclusionComorphism :: Adl2CASL -> Bool Source #

rps :: Adl2CASL -> Bool Source #

eps :: Adl2CASL -> Bool Source #

isGTC :: Adl2CASL -> Bool Source #

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

Defined in Comorphisms.CASL2CoCASL

Methods

sourceLogic :: CASL2CoCASL -> CASL Source #

sourceSublogic :: CASL2CoCASL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2CoCASL -> CASL_Sublogics Source #

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

targetLogic :: CASL2CoCASL -> CoCASL Source #

mapSublogic :: CASL2CoCASL -> CASL_Sublogics -> Maybe CoCASL_Sublogics Source #

map_theory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #

mapMarkedTheory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #

map_morphism :: CASL2CoCASL -> CASLMor -> Result CoCASLMor Source #

map_sentence :: CASL2CoCASL -> CASLSign -> CASLFORMULA -> Result CoCASLFORMULA Source #

map_symbol :: CASL2CoCASL -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2CoCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2CoCASL -> Bool Source #

has_model_expansion :: CASL2CoCASL -> Bool Source #

is_weakly_amalgamable :: CASL2CoCASL -> Bool Source #

constituents :: CASL2CoCASL -> [String] Source #

isInclusionComorphism :: CASL2CoCASL -> Bool Source #

rps :: CASL2CoCASL -> Bool Source #

eps :: CASL2CoCASL -> Bool Source #

isGTC :: CASL2CoCASL -> Bool Source #

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

Defined in Comorphisms.CASL_DL2CASL

Methods

sourceLogic :: CASL_DL2CASL -> CASL_DL Source #

sourceSublogic :: CASL_DL2CASL -> CASL_DL_SL Source #

sourceSublogicLossy :: CASL_DL2CASL -> CASL_DL_SL Source #

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

targetLogic :: CASL_DL2CASL -> CASL Source #

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

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

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

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

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

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

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

is_model_transportable :: CASL_DL2CASL -> Bool Source #

has_model_expansion :: CASL_DL2CASL -> Bool Source #

is_weakly_amalgamable :: CASL_DL2CASL -> Bool Source #

constituents :: CASL_DL2CASL -> [String] Source #

isInclusionComorphism :: CASL_DL2CASL -> Bool Source #

rps :: CASL_DL2CASL -> Bool Source #

eps :: CASL_DL2CASL -> Bool Source #

isGTC :: CASL_DL2CASL -> Bool Source #

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

Defined in Comorphisms.CASL2VSERefine

Methods

sourceLogic :: CASL2VSERefine -> CASL Source #

sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source #

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

targetLogic :: CASL2VSERefine -> VSE Source #

mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source #

map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source #

map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2VSERefine -> Bool Source #

has_model_expansion :: CASL2VSERefine -> Bool Source #

is_weakly_amalgamable :: CASL2VSERefine -> Bool Source #

constituents :: CASL2VSERefine -> [String] Source #

isInclusionComorphism :: CASL2VSERefine -> Bool Source #

rps :: CASL2VSERefine -> Bool Source #

eps :: CASL2VSERefine -> Bool Source #

isGTC :: CASL2VSERefine -> Bool Source #

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

Defined in Comorphisms.CASL2VSEImport

Methods

sourceLogic :: CASL2VSEImport -> CASL Source #

sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source #

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

targetLogic :: CASL2VSEImport -> VSE Source #

mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source #

map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source #

map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2VSEImport -> Bool Source #

has_model_expansion :: CASL2VSEImport -> Bool Source #

is_weakly_amalgamable :: CASL2VSEImport -> Bool Source #

constituents :: CASL2VSEImport -> [String] Source #

isInclusionComorphism :: CASL2VSEImport -> Bool Source #

rps :: CASL2VSEImport -> Bool Source #

eps :: CASL2VSEImport -> Bool Source #

isGTC :: CASL2VSEImport -> Bool Source #

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

Defined in Comorphisms.CASL2VSE

Methods

sourceLogic :: CASL2VSE -> CASL Source #

sourceSublogic :: CASL2VSE -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source #

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

targetLogic :: CASL2VSE -> VSE Source #

mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source #

map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source #

map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2VSE -> Bool Source #

has_model_expansion :: CASL2VSE -> Bool Source #

is_weakly_amalgamable :: CASL2VSE -> Bool Source #

constituents :: CASL2VSE -> [String] Source #

isInclusionComorphism :: CASL2VSE -> Bool Source #

rps :: CASL2VSE -> Bool Source #

eps :: CASL2VSE -> Bool Source #

isGTC :: CASL2VSE -> Bool Source #

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

Defined in Modifications.ModalEmbedding

Methods

tauSigma :: MODAL_EMBEDDING -> CASLSign -> Result CASLMor Source #

sourceComorphism :: MODAL_EMBEDDING -> InclComorphism CASL CASL_Sublogics Source #

targetComorphism :: MODAL_EMBEDDING -> CompComorphism CASL2Modal Modal2CASL Source #

type CASLBasicSpec = BASIC_SPEC () () () Source #

trueC :: a -> b -> Bool Source #

class Lattice a => MinSL a f where Source #

Methods

minSL :: f -> CASL_SL a Source #

Instances

Instances details
MinSL Bool C_FORMULA Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

minSL :: C_FORMULA -> CASL_SL Bool Source #

MinSL Bool C_SIG_ITEM Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

minSL :: C_SIG_ITEM -> CASL_SL Bool Source #

MinSL Bool C_BASIC_ITEM Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

minSL :: C_BASIC_ITEM -> CASL_SL Bool Source #

MinSL Bool CoCASLSign Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

minSL :: CoCASLSign -> CASL_SL Bool Source #

MinSL () () Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

minSL :: () -> CASL_SL () Source #

MinSL () ConstraintFORMULA Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Methods

minSL :: ConstraintFORMULA -> CASL_SL () Source #

MinSL Sublogic EM_FORMULA Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

minSL :: EM_FORMULA -> CASL_SL Sublogic Source #

MinSL Sublogic EM_SIG_ITEM Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

minSL :: EM_SIG_ITEM -> CASL_SL Sublogic Source #

MinSL Sublogic EM_BASIC_ITEM Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

minSL :: EM_BASIC_ITEM -> CASL_SL Sublogic Source #

MinSL Sublogic EModalSign Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

minSL :: EModalSign -> CASL_SL Sublogic Source #

class NameSL a where Source #

Methods

nameSL :: a -> String Source #

Instances

Instances details
NameSL Bool Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

nameSL :: Bool -> String Source #

NameSL () Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

nameSL :: () -> String Source #

NameSL Sublogic Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

nameSL :: Sublogic -> String Source #

class Lattice a => ProjForm a f where Source #

Methods

projForm :: CASL_SL a -> f -> Maybe (FORMULA f) Source #

Instances

Instances details
ProjForm Bool C_FORMULA Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

projForm :: CASL_SL Bool -> C_FORMULA -> Maybe (FORMULA C_FORMULA) Source #

ProjForm () ConstraintFORMULA Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Methods

projForm :: CASL_SL () -> ConstraintFORMULA -> Maybe (FORMULA ConstraintFORMULA) Source #

Lattice a => ProjForm a () Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

projForm :: CASL_SL a -> () -> Maybe (FORMULA ()) Source #

ProjForm Sublogic EM_FORMULA Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

projForm :: CASL_SL Sublogic -> EM_FORMULA -> Maybe (FORMULA EM_FORMULA) Source #

class (Lattice a, ProjForm a f) => ProjSigItem a s f where Source #

Methods

projSigItems :: CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]) Source #

Instances

Instances details
ProjSigItem Bool C_SIG_ITEM C_FORMULA Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

projSigItems :: CASL_SL Bool -> C_SIG_ITEM -> (Maybe (SIG_ITEMS C_SIG_ITEM C_FORMULA), [SORT]) Source #

(Lattice a, ProjForm a f) => ProjSigItem a () f Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

projSigItems :: CASL_SL a -> () -> (Maybe (SIG_ITEMS () f), [SORT]) Source #

ProjSigItem Sublogic EM_SIG_ITEM EM_FORMULA Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

projSigItems :: CASL_SL Sublogic -> EM_SIG_ITEM -> (Maybe (SIG_ITEMS EM_SIG_ITEM EM_FORMULA), [SORT]) Source #

class (Lattice a, ProjForm a f) => ProjBasic a b s f where Source #

Methods

projBasicItems :: CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT]) Source #

Instances

Instances details
ProjBasic Bool C_BASIC_ITEM C_SIG_ITEM C_FORMULA Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

projBasicItems :: CASL_SL Bool -> C_BASIC_ITEM -> (Maybe (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA), [SORT]) Source #

(Lattice a, ProjForm a f, ProjSigItem a s f) => ProjBasic a () s f Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

projBasicItems :: CASL_SL a -> () -> (Maybe (BASIC_ITEMS () s f), [SORT]) Source #

ProjBasic Sublogic EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

projBasicItems :: CASL_SL Sublogic -> EM_BASIC_ITEM -> (Maybe (BASIC_ITEMS EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA), [SORT]) Source #

Orphan instances

NameSL a => SublogicName (CASL_SL a) Source # 
Instance details

Methods

sublogicName :: CASL_SL a -> String Source #

Lattice a => SemiLatticeWithTop (CASL_SL a) Source # 
Instance details

Methods

lub :: CASL_SL a -> CASL_SL a -> CASL_SL a Source #

top :: CASL_SL a Source #

Lattice a => ProjectSublogicM (CASL_SL a) Symbol Source # 
Instance details

Methods

projectSublogicM :: CASL_SL a -> Symbol -> Maybe Symbol Source #

Lattice a => ProjectSublogicM (CASL_SL a) SYMB_MAP_ITEMS Source # 
Instance details

Methods

projectSublogicM :: CASL_SL a -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS Source #

Lattice a => ProjectSublogicM (CASL_SL a) SYMB_ITEMS Source # 
Instance details

Methods

projectSublogicM :: CASL_SL a -> SYMB_ITEMS -> Maybe SYMB_ITEMS Source #

Lattice a => MinSublogic (CASL_SL a) Symbol Source # 
Instance details

Methods

minSublogic :: Symbol -> CASL_SL a Source #

Lattice a => MinSublogic (CASL_SL a) SYMB_MAP_ITEMS Source # 
Instance details

Methods

minSublogic :: SYMB_MAP_ITEMS -> CASL_SL a Source #

Lattice a => MinSublogic (CASL_SL a) SYMB_ITEMS Source # 
Instance details

Methods

minSublogic :: SYMB_ITEMS -> CASL_SL a Source #

MinSL a f => MinSublogic (CASL_SL a) (FORMULA f) Source # 
Instance details

Methods

minSublogic :: FORMULA f -> CASL_SL a Source #

MinSL a e => ProjectSublogic (CASL_SL a) (Sign f e) Source # 
Instance details

Methods

projectSublogic :: CASL_SL a -> Sign f e -> Sign f e Source #

MinSL a e => MinSublogic (CASL_SL a) (Sign f e) Source # 
Instance details

Methods

minSublogic :: Sign f e -> CASL_SL a Source #

MinSL a e => ProjectSublogic (CASL_SL a) (Morphism f e m) Source # 
Instance details

Methods

projectSublogic :: CASL_SL a -> Morphism f e m -> Morphism f e m 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

Methods

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

MinSL a e => MinSublogic (CASL_SL a) (Morphism f e m) Source # 
Instance details

Methods

minSublogic :: Morphism f e m -> CASL_SL a Source #

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

Methods

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

(Ord f, Ord e, Ord m, MorphismExtension e m) => Category (Sign f e) (Morphism f e m) Source # 
Instance details

Methods

ide :: Sign f e -> Morphism f e m Source #

composeMorphisms :: Morphism f e m -> Morphism f e m -> Result (Morphism f e m) Source #

dom :: Morphism f e m -> Sign f e Source #

cod :: Morphism f e m -> Sign f e Source #

inverse :: Morphism f e m -> Result (Morphism f e m) Source #

isInclusion :: Morphism f e m -> Bool Source #

legal_mor :: Morphism f e m -> Result () Source #

Semigroup (BASIC_SPEC b s f) Source # 
Instance details

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) Source # 
Instance details

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