Hets - the Heterogeneous Tool Set

Copyright(c) T.Mossakowski C.Maeder Uni Bremen 2004-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerhausmann@informatik.uni-bremen.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe

CoCASL.AS_CoCASL

Description

Abstract syntax for CoCASL, the coalgebraic extension of CASL Only the added syntax is specified

Documentation

type C_BASIC_SPEC = BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA Source #

type AnModFORM = Annoted (FORMULA C_FORMULA) Source #

data C_BASIC_ITEM Source #

Constructors

CoFree_datatype [Annoted CODATATYPE_DECL] Range 
CoSort_gen [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] Range 

Instances

Data C_BASIC_ITEM Source # 

Methods

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

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

toConstr :: C_BASIC_ITEM -> Constr

dataTypeOf :: C_BASIC_ITEM -> DataType

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

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

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

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

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

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

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

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

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

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

Show C_BASIC_ITEM Source # 

Methods

showsPrec :: Int -> C_BASIC_ITEM -> ShowS

show :: C_BASIC_ITEM -> String

showList :: [C_BASIC_ITEM] -> ShowS

GetRange C_BASIC_ITEM Source # 
Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # 

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

empty_signature :: CoCASL -> CSign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 #

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 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 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 CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

data C_SIG_ITEM Source #

Constructors

CoDatatype_items [Annoted CODATATYPE_DECL] Range 

Instances

Data C_SIG_ITEM Source # 

Methods

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

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

toConstr :: C_SIG_ITEM -> Constr

dataTypeOf :: C_SIG_ITEM -> DataType

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

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

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

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

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

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

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

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

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

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

Show C_SIG_ITEM Source # 

Methods

showsPrec :: Int -> C_SIG_ITEM -> ShowS

show :: C_SIG_ITEM -> String

showList :: [C_SIG_ITEM] -> ShowS

GetRange C_SIG_ITEM Source # 
Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # 

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

empty_signature :: CoCASL -> CSign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 #

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 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 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 CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

data CODATATYPE_DECL Source #

Constructors

CoDatatype_decl SORT [Annoted COALTERNATIVE] Range 

Instances

Data CODATATYPE_DECL Source # 

Methods

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

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

toConstr :: CODATATYPE_DECL -> Constr

dataTypeOf :: CODATATYPE_DECL -> DataType

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

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

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

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

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

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

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

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

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

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

Show CODATATYPE_DECL Source # 

Methods

showsPrec :: Int -> CODATATYPE_DECL -> ShowS

show :: CODATATYPE_DECL -> String

showList :: [CODATATYPE_DECL] -> ShowS

GetRange CODATATYPE_DECL Source # 

data COALTERNATIVE Source #

Constructors

Co_construct OpKind (Maybe OP_NAME) [COCOMPONENTS] Range 
CoSubsorts [SORT] Range 

Instances

Data COALTERNATIVE Source # 

Methods

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

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

toConstr :: COALTERNATIVE -> Constr

dataTypeOf :: COALTERNATIVE -> DataType

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

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

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

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

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

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

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

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

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

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

Show COALTERNATIVE Source # 

Methods

showsPrec :: Int -> COALTERNATIVE -> ShowS

show :: COALTERNATIVE -> String

showList :: [COALTERNATIVE] -> ShowS

GetRange COALTERNATIVE Source # 

data COCOMPONENTS Source #

Constructors

CoSelect [OP_NAME] OP_TYPE Range 

Instances

Data COCOMPONENTS Source # 

Methods

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

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

toConstr :: COCOMPONENTS -> Constr

dataTypeOf :: COCOMPONENTS -> DataType

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

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

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

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

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

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

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

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

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

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

Show COCOMPONENTS Source # 

Methods

showsPrec :: Int -> COCOMPONENTS -> ShowS

show :: COCOMPONENTS -> String

showList :: [COCOMPONENTS] -> ShowS

GetRange COCOMPONENTS Source # 

data MODALITY Source #

Constructors

Simple_mod SIMPLE_ID 
Term_mod (TERM C_FORMULA) 

Instances

Eq MODALITY Source # 

Methods

(==) :: MODALITY -> MODALITY -> Bool

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

Data MODALITY Source # 

Methods

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

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

toConstr :: MODALITY -> Constr

dataTypeOf :: MODALITY -> DataType

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

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

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

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

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

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

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

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

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

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

Ord MODALITY Source # 

Methods

compare :: MODALITY -> MODALITY -> Ordering

(<) :: MODALITY -> MODALITY -> Bool

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

(>) :: MODALITY -> MODALITY -> Bool

(>=) :: MODALITY -> MODALITY -> Bool

max :: MODALITY -> MODALITY -> MODALITY

min :: MODALITY -> MODALITY -> MODALITY

Show MODALITY Source # 

Methods

showsPrec :: Int -> MODALITY -> ShowS

show :: MODALITY -> String

showList :: [MODALITY] -> ShowS

GetRange MODALITY Source # 

data C_FORMULA Source #

Constructors

BoxOrDiamond Bool MODALITY (FORMULA C_FORMULA) Range 
CoSort_gen_ax [SORT] [OP_SYMB] Bool 

Instances

Eq C_FORMULA Source # 

Methods

(==) :: C_FORMULA -> C_FORMULA -> Bool

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

Data C_FORMULA Source # 

Methods

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

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

toConstr :: C_FORMULA -> Constr

dataTypeOf :: C_FORMULA -> DataType

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

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

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

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

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

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

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

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

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

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

Ord C_FORMULA Source # 

Methods

compare :: C_FORMULA -> C_FORMULA -> Ordering

(<) :: C_FORMULA -> C_FORMULA -> Bool

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

(>) :: C_FORMULA -> C_FORMULA -> Bool

(>=) :: C_FORMULA -> C_FORMULA -> Bool

max :: C_FORMULA -> C_FORMULA -> C_FORMULA

min :: C_FORMULA -> C_FORMULA -> C_FORMULA

Show C_FORMULA Source # 

Methods

showsPrec :: Int -> C_FORMULA -> ShowS

show :: C_FORMULA -> String

showList :: [C_FORMULA] -> ShowS

GetRange C_FORMULA Source # 
Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol Source # 
Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # 

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

empty_signature :: CoCASL -> CSign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 #

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 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 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 CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #