Hets - the Heterogeneous Tool Set

Copyright(c) Pascal Schmidt C. Maeder and Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellNone

CASL.Sublogic

Contents

Description

Sublogic analysis for CASL

This module provides the sublogic functions (as required by Logic.hs) for CASL. The functions allow to compute the minimal sublogics needed by a given element, to check whether an item is part of a given sublogic, and to project an element into a given sublogic.

Synopsis

types

data CASL_SL a Source #

Constructors

CASL_SL 

Fields

Instances

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

Methods

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

stability :: CASL -> Stability Source #

data_logic :: CASL -> Maybe AnyLogic Source #

top_sublogic :: CASL -> CASL_Sublogics Source #

all_sublogics :: CASL -> [CASL_Sublogics] Source #

bottomSublogic :: CASL -> Maybe CASL_Sublogics Source #

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

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

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

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

default_prover :: CASL -> String Source #

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

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

empty_proof_tree :: CASL -> ProofTree Source #

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

omdoc_metatheory :: CASL -> Maybe OMCD Source #

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

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

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

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

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

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

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

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

Methods

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

stability :: CoCASL -> Stability Source #

data_logic :: CoCASL -> Maybe AnyLogic Source #

top_sublogic :: CoCASL -> CoCASL_Sublogics Source #

all_sublogics :: CoCASL -> [CoCASL_Sublogics] Source #

bottomSublogic :: CoCASL -> Maybe CoCASL_Sublogics Source #

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

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

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

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

default_prover :: CoCASL -> String Source #

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

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

empty_proof_tree :: CoCASL -> () Source #

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

omdoc_metatheory :: CoCASL -> Maybe OMCD Source #

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

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

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

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

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

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

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

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

Methods

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

stability :: ConstraintCASL -> Stability Source #

data_logic :: ConstraintCASL -> Maybe AnyLogic Source #

top_sublogic :: ConstraintCASL -> CASL_Sublogics Source #

all_sublogics :: ConstraintCASL -> [CASL_Sublogics] Source #

bottomSublogic :: ConstraintCASL -> Maybe CASL_Sublogics Source #

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

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

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

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

default_prover :: ConstraintCASL -> String Source #

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

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

empty_proof_tree :: ConstraintCASL -> () Source #

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

omdoc_metatheory :: ConstraintCASL -> Maybe OMCD Source #

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

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

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

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

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

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

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

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

Methods

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

stability :: ExtModal -> Stability Source #

data_logic :: ExtModal -> Maybe AnyLogic Source #

top_sublogic :: ExtModal -> ExtModalSL Source #

all_sublogics :: ExtModal -> [ExtModalSL] Source #

bottomSublogic :: ExtModal -> Maybe ExtModalSL Source #

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

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

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

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

default_prover :: ExtModal -> String Source #

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

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

empty_proof_tree :: ExtModal -> () Source #

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

omdoc_metatheory :: ExtModal -> Maybe OMCD Source #

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

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

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

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

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

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

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

Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism CASL2NNF CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2PCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CoCASL2CoPCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Comorphism CASL2Prenex CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2Skolem CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2SubCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CoCASL2CoSubCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Comorphism CASL2TopSort CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL_DL2CASL CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism RelScheme2CASL RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source # 
Comorphism CASL2ExtModal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Comorphism ExtModal2CASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 

Methods

sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source #

sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source #

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

targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source #

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

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

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

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

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

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

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

is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source #

has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source #

is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source #

constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source #

isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source #

rps :: ExtModal2ExtModalNoSubsorts -> Bool Source #

eps :: ExtModal2ExtModalNoSubsorts -> Bool Source #

Comorphism ExtModal2ExtModalTotal ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism CASL2Hybrid CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source # 
Comorphism CASL2Modal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Comorphism Modal2CASL Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2OWL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Comorphism OWL22CASL OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism DFOL2CASL DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism Maude2CASL Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2Prop CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism Prop2CASL Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics) (CompComorphism CASL2Modal Modal2CASL) CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Eq a => Eq (CASL_SL a) Source # 

Methods

(==) :: CASL_SL a -> CASL_SL a -> Bool

(/=) :: CASL_SL a -> CASL_SL a -> Bool

Data a => Data (CASL_SL a) Source # 

Methods

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

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

toConstr :: CASL_SL a -> Constr

dataTypeOf :: CASL_SL a -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> CASL_SL a -> CASL_SL a

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

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

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

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

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

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

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

Ord a => Ord (CASL_SL a) Source # 

Methods

compare :: CASL_SL a -> CASL_SL a -> Ordering

(<) :: CASL_SL a -> CASL_SL a -> Bool

(<=) :: CASL_SL a -> CASL_SL a -> Bool

(>) :: CASL_SL a -> CASL_SL a -> Bool

(>=) :: CASL_SL a -> CASL_SL a -> Bool

max :: CASL_SL a -> CASL_SL a -> CASL_SL a

min :: CASL_SL a -> CASL_SL a -> CASL_SL a

Show a => Show (CASL_SL a) Source # 

Methods

showsPrec :: Int -> CASL_SL a -> ShowS

show :: CASL_SL a -> String

showList :: [CASL_SL a] -> ShowS

data CASL_Formulas Source #

Constructors

Atomic

atomic logic

Horn

positive conditional logic

GHorn

generalized positive conditional logic

Prenex

formulas in prenex normal form

FOL

first-order logic

SOL

second-order logic

Instances

Eq CASL_Formulas Source # 
Data CASL_Formulas Source # 

Methods

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

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

toConstr :: CASL_Formulas -> Constr

dataTypeOf :: CASL_Formulas -> DataType

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

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

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

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

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

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

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

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

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

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

Ord CASL_Formulas Source # 
Show CASL_Formulas Source # 

Methods

showsPrec :: Int -> CASL_Formulas -> ShowS

show :: CASL_Formulas -> String

showList :: [CASL_Formulas] -> ShowS

data SubsortingFeatures Source #

Constructors

NoSub 
LocFilSub 
Sub 

Instances

Eq SubsortingFeatures Source # 
Data SubsortingFeatures Source # 

Methods

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

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

toConstr :: SubsortingFeatures -> Constr

dataTypeOf :: SubsortingFeatures -> DataType

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

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

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

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

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

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

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

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

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

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

Ord SubsortingFeatures Source # 
Show SubsortingFeatures Source # 

Methods

showsPrec :: Int -> SubsortingFeatures -> ShowS

show :: SubsortingFeatures -> String

showList :: [SubsortingFeatures] -> ShowS

data SortGenerationFeatures Source #

Constructors

NoSortGen 
SortGen 

Fields

Instances

Eq SortGenerationFeatures Source # 
Data SortGenerationFeatures Source # 

Methods

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

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

toConstr :: SortGenerationFeatures -> Constr

dataTypeOf :: SortGenerationFeatures -> DataType

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

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

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

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

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

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

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

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

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

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

Ord SortGenerationFeatures Source # 
Show SortGenerationFeatures Source # 

class

class (Ord l, Show l) => Lattice l where Source #

Minimal complete definition

cjoin, ctop, bot

Methods

cjoin :: l -> l -> l Source #

ctop :: l Source #

bot :: l Source #

Instances

Lattice Bool Source # 

Methods

cjoin :: Bool -> Bool -> Bool Source #

ctop :: Bool Source #

bot :: Bool Source #

Lattice () Source # 

Methods

cjoin :: () -> () -> () Source #

ctop :: () Source #

bot :: () Source #

Lattice Sublogic Source # 
(Lattice a, Lattice b) => Lattice (a, b) Source # 

Methods

cjoin :: (a, b) -> (a, b) -> (a, b) Source #

ctop :: (a, b) Source #

bot :: (a, b) Source #

predicates on CASL_SL

has_sub :: CASL_SL a -> Bool Source #

has_cons :: CASL_SL a -> Bool Source #

functions for SemiLatticeWithTop instance

mkTop :: a -> CASL_SL a Source #

functions for the creation of minimal sublogics

mkBot :: a -> CASL_SL a Source #

updExtFeature :: (a -> a) -> CASL_SL a -> CASL_SL a Source #

functions for Logic instance sublogic to string conversion

sublogics_name :: (a -> String) -> CASL_SL a -> String Source #

parseSL :: (String -> Maybe (a, String)) -> String -> Maybe (CASL_SL a) Source #

parseBool :: String -> String -> (Bool, String) Source #

list of all sublogics

sublogics_all :: Lattice a => [a] -> [CASL_SL a] Source #

sDims :: Lattice a => [[a]] -> [[CASL_SL a]] Source #

computes the sublogic of a given element

sl_sig_items :: Lattice a => (s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a Source #

sl_basic_spec :: Lattice a => (b -> CASL_SL a) -> (s -> CASL_SL a) -> (f -> CASL_SL a) -> BASIC_SPEC b s f -> CASL_SL a Source #

sl_op_item :: Lattice a => (f -> CASL_SL a) -> OP_ITEM f -> CASL_SL a Source #

sl_pred_item :: Lattice a => (f -> CASL_SL a) -> PRED_ITEM f -> CASL_SL a Source #

sl_sentence :: Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a Source #

sl_term :: Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a Source #

sl_sign :: Lattice a => (e -> CASL_SL a) -> Sign f e -> CASL_SL a Source #

sl_morphism :: Lattice a => (e -> CASL_SL a) -> Morphism f e m -> CASL_SL a Source #

projects an element into a given sublogic

pr_basic_spec :: Lattice a => (CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])) -> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])) -> (CASL_SL a -> f -> Maybe (FORMULA f)) -> CASL_SL a -> BASIC_SPEC b s f -> BASIC_SPEC b s f Source #

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

pr_morphism :: Lattice a => CASL_SL a -> Morphism f e m -> Morphism f e m Source #

pr_epsilon :: m -> CASL_SL a -> Sign f e -> Morphism f e m Source #

pr_symbol :: Lattice a => CASL_SL a -> Symbol -> Maybe Symbol Source #