Hets - the Heterogeneous Tool Set

CopyrightDominik Luecke Uni Bremen 2008
LicenseGPLv2 or higher, see LICENSE.txt or LIZENZ.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

RelationalScheme.Sign

Description

Signature for Relational Schemes

Synopsis

Documentation

type RSIsKey = Bool Source #

data RSDatatype Source #

Instances

Eq RSDatatype Source # 

Methods

(==) :: RSDatatype -> RSDatatype -> Bool

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

Data RSDatatype Source # 

Methods

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

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

toConstr :: RSDatatype -> Constr

dataTypeOf :: RSDatatype -> DataType

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

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

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

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

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

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

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

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

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

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

Ord RSDatatype Source # 
Show RSDatatype Source # 

Methods

showsPrec :: Int -> RSDatatype -> ShowS

show :: RSDatatype -> String

showList :: [RSDatatype] -> ShowS

Pretty RSDatatype Source # 

data RSColumn Source #

Constructors

RSColumn 

Fields

Instances

Eq RSColumn Source # 

Methods

(==) :: RSColumn -> RSColumn -> Bool

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

Data RSColumn Source # 

Methods

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

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

toConstr :: RSColumn -> Constr

dataTypeOf :: RSColumn -> DataType

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

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

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

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

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

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

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

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

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

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

Ord RSColumn Source # 

Methods

compare :: RSColumn -> RSColumn -> Ordering

(<) :: RSColumn -> RSColumn -> Bool

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

(>) :: RSColumn -> RSColumn -> Bool

(>=) :: RSColumn -> RSColumn -> Bool

max :: RSColumn -> RSColumn -> RSColumn

min :: RSColumn -> RSColumn -> RSColumn

Show RSColumn Source # 

Methods

showsPrec :: Int -> RSColumn -> ShowS

show :: RSColumn -> String

showList :: [RSColumn] -> ShowS

Pretty RSColumn Source # 

data RSTable Source #

Constructors

RSTable 

Fields

Instances

Eq RSTable Source # 

Methods

(==) :: RSTable -> RSTable -> Bool

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

Data RSTable Source # 

Methods

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

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

toConstr :: RSTable -> Constr

dataTypeOf :: RSTable -> DataType

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

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

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

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

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

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

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

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

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

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

Ord RSTable Source # 

Methods

compare :: RSTable -> RSTable -> Ordering

(<) :: RSTable -> RSTable -> Bool

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

(>) :: RSTable -> RSTable -> Bool

(>=) :: RSTable -> RSTable -> Bool

max :: RSTable -> RSTable -> RSTable

min :: RSTable -> RSTable -> RSTable

Show RSTable Source # 

Methods

showsPrec :: Int -> RSTable -> ShowS

show :: RSTable -> String

showList :: [RSTable] -> ShowS

Pretty RSTable Source # 

data RSTables Source #

Constructors

RSTables 

Fields

Instances

Eq RSTables Source # 

Methods

(==) :: RSTables -> RSTables -> Bool

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

Data RSTables Source # 

Methods

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

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

toConstr :: RSTables -> Constr

dataTypeOf :: RSTables -> DataType

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

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

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

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

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

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

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

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

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

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

Ord RSTables Source # 

Methods

compare :: RSTables -> RSTables -> Ordering

(<) :: RSTables -> RSTables -> Bool

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

(>) :: RSTables -> RSTables -> Bool

(>=) :: RSTables -> RSTables -> Bool

max :: RSTables -> RSTables -> RSTables

min :: RSTables -> RSTables -> RSTables

Show RSTables Source # 

Methods

showsPrec :: Int -> RSTables -> ShowS

show :: RSTables -> String

showList :: [RSTables] -> ShowS

GetRange RSTables Source # 
Pretty RSTables Source # 
Sentences RelScheme Sentence Sign RSMorphism RSSymbol Source #

Instance of Sentences for Rel

StaticAnalysis RelScheme RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol Source #

Static Analysis for Rel

Methods

basic_analysis :: RelScheme -> Maybe ((RSScheme, Sign, GlobalAnnos) -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence])) Source #

sen_analysis :: RelScheme -> Maybe ((RSScheme, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: RelScheme -> IRI -> LibName -> RSScheme -> Sign -> GlobalAnnos -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence]) Source #

stat_symb_map_items :: RelScheme -> Sign -> Maybe Sign -> [()] -> Result (EndoMap RSRawSymbol) Source #

stat_symb_items :: RelScheme -> Sign -> [()] -> Result [RSRawSymbol] Source #

convertTheory :: RelScheme -> Maybe ((Sign, [Named Sentence]) -> RSScheme) Source #

ensures_amalgamability :: RelScheme -> ([CASLAmalgOpt], Gr Sign (Int, RSMorphism), [(Int, RSMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: RelScheme -> RSMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: RelScheme -> Gr Sign (Int, RSMorphism) -> Result (Sign, Map Int RSMorphism) Source #

qualify :: RelScheme -> SIMPLE_ID -> LibName -> RSMorphism -> Sign -> Result (RSMorphism, [Named Sentence]) Source #

symbol_to_raw :: RelScheme -> RSSymbol -> RSRawSymbol Source #

id_to_raw :: RelScheme -> Id -> RSRawSymbol Source #

matches :: RelScheme -> RSSymbol -> RSRawSymbol -> Bool Source #

empty_signature :: RelScheme -> Sign Source #

add_symb_to_sign :: RelScheme -> Sign -> RSSymbol -> Result Sign Source #

signature_union :: RelScheme -> Sign -> Sign -> Result Sign Source #

signatureDiff :: RelScheme -> Sign -> Sign -> Result Sign Source #

intersection :: RelScheme -> Sign -> Sign -> Result Sign Source #

final_union :: RelScheme -> Sign -> Sign -> Result Sign Source #

morphism_union :: RelScheme -> RSMorphism -> RSMorphism -> Result RSMorphism Source #

is_subsig :: RelScheme -> Sign -> Sign -> Bool Source #

subsig_inclusion :: RelScheme -> Sign -> Sign -> Result RSMorphism Source #

generated_sign :: RelScheme -> Set RSSymbol -> Sign -> Result RSMorphism Source #

cogenerated_sign :: RelScheme -> Set RSSymbol -> Sign -> Result RSMorphism Source #

induced_from_morphism :: RelScheme -> EndoMap RSRawSymbol -> Sign -> Result RSMorphism Source #

induced_from_to_morphism :: RelScheme -> EndoMap RSRawSymbol -> ExtSign Sign RSSymbol -> ExtSign Sign RSSymbol -> Result RSMorphism Source #

is_transportable :: RelScheme -> RSMorphism -> Bool Source #

is_injective :: RelScheme -> RSMorphism -> Bool Source #

theory_to_taxonomy :: RelScheme -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: RelScheme -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap RSSymbol -> EndoMap RSSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap RSSymbol, EndoMap RSSymbol) Source #

equiv2cospan :: RelScheme -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap RSSymbol, EndoMap RSSymbol) Source #

extract_module :: RelScheme -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

Logic RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () Source #

Instance of Logic for Relational Schemes

Methods

parse_basic_sen :: RelScheme -> Maybe (RSScheme -> AParser st Sentence) Source #

stability :: RelScheme -> Stability Source #

data_logic :: RelScheme -> Maybe AnyLogic Source #

top_sublogic :: RelScheme -> () Source #

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

bottomSublogic :: RelScheme -> Maybe () Source #

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

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

proj_sublogic_epsilon :: RelScheme -> () -> Sign -> RSMorphism Source #

provers :: RelScheme -> [Prover Sign Sentence RSMorphism () ()] Source #

default_prover :: RelScheme -> String Source #

cons_checkers :: RelScheme -> [ConsChecker Sign Sentence () RSMorphism ()] Source #

conservativityCheck :: RelScheme -> [ConservativityChecker Sign Sentence RSMorphism] Source #

empty_proof_tree :: RelScheme -> () Source #

syntaxTable :: RelScheme -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: RelScheme -> Maybe OMCD Source #

export_symToOmdoc :: RelScheme -> NameMap RSSymbol -> RSSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: RelScheme -> NameMap RSSymbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: RelScheme -> SigMap RSSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: RelScheme -> SigMapI RSSymbol -> TCElement -> String -> Result RSSymbol Source #

omdocToSen :: RelScheme -> SigMapI RSSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: RelScheme -> SigMapI RSSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: RelScheme -> SigMapI RSSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) 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 # 

data RSMorphism Source #

Constructors

RSMorphism 

Instances

Eq RSMorphism Source # 

Methods

(==) :: RSMorphism -> RSMorphism -> Bool

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

Data RSMorphism Source # 

Methods

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

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

toConstr :: RSMorphism -> Constr

dataTypeOf :: RSMorphism -> DataType

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

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

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

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

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

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

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

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

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

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

Ord RSMorphism Source # 
Show RSMorphism Source # 

Methods

showsPrec :: Int -> RSMorphism -> ShowS

show :: RSMorphism -> String

showList :: [RSMorphism] -> ShowS

Pretty RSMorphism Source # 
Sentences RelScheme Sentence Sign RSMorphism RSSymbol Source #

Instance of Sentences for Rel

StaticAnalysis RelScheme RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol Source #

Static Analysis for Rel

Methods

basic_analysis :: RelScheme -> Maybe ((RSScheme, Sign, GlobalAnnos) -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence])) Source #

sen_analysis :: RelScheme -> Maybe ((RSScheme, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: RelScheme -> IRI -> LibName -> RSScheme -> Sign -> GlobalAnnos -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence]) Source #

stat_symb_map_items :: RelScheme -> Sign -> Maybe Sign -> [()] -> Result (EndoMap RSRawSymbol) Source #

stat_symb_items :: RelScheme -> Sign -> [()] -> Result [RSRawSymbol] Source #

convertTheory :: RelScheme -> Maybe ((Sign, [Named Sentence]) -> RSScheme) Source #

ensures_amalgamability :: RelScheme -> ([CASLAmalgOpt], Gr Sign (Int, RSMorphism), [(Int, RSMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: RelScheme -> RSMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: RelScheme -> Gr Sign (Int, RSMorphism) -> Result (Sign, Map Int RSMorphism) Source #

qualify :: RelScheme -> SIMPLE_ID -> LibName -> RSMorphism -> Sign -> Result (RSMorphism, [Named Sentence]) Source #

symbol_to_raw :: RelScheme -> RSSymbol -> RSRawSymbol Source #

id_to_raw :: RelScheme -> Id -> RSRawSymbol Source #

matches :: RelScheme -> RSSymbol -> RSRawSymbol -> Bool Source #

empty_signature :: RelScheme -> Sign Source #

add_symb_to_sign :: RelScheme -> Sign -> RSSymbol -> Result Sign Source #

signature_union :: RelScheme -> Sign -> Sign -> Result Sign Source #

signatureDiff :: RelScheme -> Sign -> Sign -> Result Sign Source #

intersection :: RelScheme -> Sign -> Sign -> Result Sign Source #

final_union :: RelScheme -> Sign -> Sign -> Result Sign Source #

morphism_union :: RelScheme -> RSMorphism -> RSMorphism -> Result RSMorphism Source #

is_subsig :: RelScheme -> Sign -> Sign -> Bool Source #

subsig_inclusion :: RelScheme -> Sign -> Sign -> Result RSMorphism Source #

generated_sign :: RelScheme -> Set RSSymbol -> Sign -> Result RSMorphism Source #

cogenerated_sign :: RelScheme -> Set RSSymbol -> Sign -> Result RSMorphism Source #

induced_from_morphism :: RelScheme -> EndoMap RSRawSymbol -> Sign -> Result RSMorphism Source #

induced_from_to_morphism :: RelScheme -> EndoMap RSRawSymbol -> ExtSign Sign RSSymbol -> ExtSign Sign RSSymbol -> Result RSMorphism Source #

is_transportable :: RelScheme -> RSMorphism -> Bool Source #

is_injective :: RelScheme -> RSMorphism -> Bool Source #

theory_to_taxonomy :: RelScheme -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: RelScheme -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap RSSymbol -> EndoMap RSSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap RSSymbol, EndoMap RSSymbol) Source #

equiv2cospan :: RelScheme -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap RSSymbol, EndoMap RSSymbol) Source #

extract_module :: RelScheme -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

Logic RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () Source #

Instance of Logic for Relational Schemes

Methods

parse_basic_sen :: RelScheme -> Maybe (RSScheme -> AParser st Sentence) Source #

stability :: RelScheme -> Stability Source #

data_logic :: RelScheme -> Maybe AnyLogic Source #

top_sublogic :: RelScheme -> () Source #

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

bottomSublogic :: RelScheme -> Maybe () Source #

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

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

proj_sublogic_epsilon :: RelScheme -> () -> Sign -> RSMorphism Source #

provers :: RelScheme -> [Prover Sign Sentence RSMorphism () ()] Source #

default_prover :: RelScheme -> String Source #

cons_checkers :: RelScheme -> [ConsChecker Sign Sentence () RSMorphism ()] Source #

conservativityCheck :: RelScheme -> [ConservativityChecker Sign Sentence RSMorphism] Source #

empty_proof_tree :: RelScheme -> () Source #

syntaxTable :: RelScheme -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: RelScheme -> Maybe OMCD Source #

export_symToOmdoc :: RelScheme -> NameMap RSSymbol -> RSSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: RelScheme -> NameMap RSSymbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: RelScheme -> SigMap RSSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: RelScheme -> SigMapI RSSymbol -> TCElement -> String -> Result RSSymbol Source #

omdocToSen :: RelScheme -> SigMapI RSSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: RelScheme -> SigMapI RSSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: RelScheme -> SigMapI RSSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) 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 # 

data RSTMap Source #

Constructors

RSTMap 

Fields

Instances

Eq RSTMap Source # 

Methods

(==) :: RSTMap -> RSTMap -> Bool

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

Data RSTMap Source # 

Methods

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

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

toConstr :: RSTMap -> Constr

dataTypeOf :: RSTMap -> DataType

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

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

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

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

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

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

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

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

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

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

Ord RSTMap Source # 

Methods

compare :: RSTMap -> RSTMap -> Ordering

(<) :: RSTMap -> RSTMap -> Bool

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

(>) :: RSTMap -> RSTMap -> Bool

(>=) :: RSTMap -> RSTMap -> Bool

max :: RSTMap -> RSTMap -> RSTMap

min :: RSTMap -> RSTMap -> RSTMap

Show RSTMap Source # 

Methods

showsPrec :: Int -> RSTMap -> ShowS

show :: RSTMap -> String

showList :: [RSTMap] -> ShowS

Pretty RSTMap Source # 

emptyRSSign :: RSTables Source #

id-morphism for RS

uniteSig :: Monad m => RSTables -> RSTables -> m RSTables Source #

data RSSymbol Source #

Instances

Eq RSSymbol Source # 

Methods

(==) :: RSSymbol -> RSSymbol -> Bool

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

Data RSSymbol Source # 

Methods

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

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

toConstr :: RSSymbol -> Constr

dataTypeOf :: RSSymbol -> DataType

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

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

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

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

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

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

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

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

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

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

Ord RSSymbol Source # 

Methods

compare :: RSSymbol -> RSSymbol -> Ordering

(<) :: RSSymbol -> RSSymbol -> Bool

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

(>) :: RSSymbol -> RSSymbol -> Bool

(>=) :: RSSymbol -> RSSymbol -> Bool

max :: RSSymbol -> RSSymbol -> RSSymbol

min :: RSSymbol -> RSSymbol -> RSSymbol

Show RSSymbol Source # 

Methods

showsPrec :: Int -> RSSymbol -> ShowS

show :: RSSymbol -> String

showList :: [RSSymbol] -> ShowS

GetRange RSSymbol Source # 
Pretty RSSymbol Source # 
Sentences RelScheme Sentence Sign RSMorphism RSSymbol Source #

Instance of Sentences for Rel

Syntax RelScheme RSScheme RSSymbol () () Source #

Syntax of Rel

StaticAnalysis RelScheme RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol Source #

Static Analysis for Rel

Methods

basic_analysis :: RelScheme -> Maybe ((RSScheme, Sign, GlobalAnnos) -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence])) Source #

sen_analysis :: RelScheme -> Maybe ((RSScheme, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: RelScheme -> IRI -> LibName -> RSScheme -> Sign -> GlobalAnnos -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence]) Source #

stat_symb_map_items :: RelScheme -> Sign -> Maybe Sign -> [()] -> Result (EndoMap RSRawSymbol) Source #

stat_symb_items :: RelScheme -> Sign -> [()] -> Result [RSRawSymbol] Source #

convertTheory :: RelScheme -> Maybe ((Sign, [Named Sentence]) -> RSScheme) Source #

ensures_amalgamability :: RelScheme -> ([CASLAmalgOpt], Gr Sign (Int, RSMorphism), [(Int, RSMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: RelScheme -> RSMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: RelScheme -> Gr Sign (Int, RSMorphism) -> Result (Sign, Map Int RSMorphism) Source #

qualify :: RelScheme -> SIMPLE_ID -> LibName -> RSMorphism -> Sign -> Result (RSMorphism, [Named Sentence]) Source #

symbol_to_raw :: RelScheme -> RSSymbol -> RSRawSymbol Source #

id_to_raw :: RelScheme -> Id -> RSRawSymbol Source #

matches :: RelScheme -> RSSymbol -> RSRawSymbol -> Bool Source #

empty_signature :: RelScheme -> Sign Source #

add_symb_to_sign :: RelScheme -> Sign -> RSSymbol -> Result Sign Source #

signature_union :: RelScheme -> Sign -> Sign -> Result Sign Source #

signatureDiff :: RelScheme -> Sign -> Sign -> Result Sign Source #

intersection :: RelScheme -> Sign -> Sign -> Result Sign Source #

final_union :: RelScheme -> Sign -> Sign -> Result Sign Source #

morphism_union :: RelScheme -> RSMorphism -> RSMorphism -> Result RSMorphism Source #

is_subsig :: RelScheme -> Sign -> Sign -> Bool Source #

subsig_inclusion :: RelScheme -> Sign -> Sign -> Result RSMorphism Source #

generated_sign :: RelScheme -> Set RSSymbol -> Sign -> Result RSMorphism Source #

cogenerated_sign :: RelScheme -> Set RSSymbol -> Sign -> Result RSMorphism Source #

induced_from_morphism :: RelScheme -> EndoMap RSRawSymbol -> Sign -> Result RSMorphism Source #

induced_from_to_morphism :: RelScheme -> EndoMap RSRawSymbol -> ExtSign Sign RSSymbol -> ExtSign Sign RSSymbol -> Result RSMorphism Source #

is_transportable :: RelScheme -> RSMorphism -> Bool Source #

is_injective :: RelScheme -> RSMorphism -> Bool Source #

theory_to_taxonomy :: RelScheme -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: RelScheme -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap RSSymbol -> EndoMap RSSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap RSSymbol, EndoMap RSSymbol) Source #

equiv2cospan :: RelScheme -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap RSSymbol, EndoMap RSSymbol) Source #

extract_module :: RelScheme -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

Logic RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () Source #

Instance of Logic for Relational Schemes

Methods

parse_basic_sen :: RelScheme -> Maybe (RSScheme -> AParser st Sentence) Source #

stability :: RelScheme -> Stability Source #

data_logic :: RelScheme -> Maybe AnyLogic Source #

top_sublogic :: RelScheme -> () Source #

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

bottomSublogic :: RelScheme -> Maybe () Source #

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

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

proj_sublogic_epsilon :: RelScheme -> () -> Sign -> RSMorphism Source #

provers :: RelScheme -> [Prover Sign Sentence RSMorphism () ()] Source #

default_prover :: RelScheme -> String Source #

cons_checkers :: RelScheme -> [ConsChecker Sign Sentence () RSMorphism ()] Source #

conservativityCheck :: RelScheme -> [ConservativityChecker Sign Sentence RSMorphism] Source #

empty_proof_tree :: RelScheme -> () Source #

syntaxTable :: RelScheme -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: RelScheme -> Maybe OMCD Source #

export_symToOmdoc :: RelScheme -> NameMap RSSymbol -> RSSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: RelScheme -> NameMap RSSymbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: RelScheme -> SigMap RSSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: RelScheme -> SigMapI RSSymbol -> TCElement -> String -> Result RSSymbol Source #

omdocToSen :: RelScheme -> SigMapI RSSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: RelScheme -> SigMapI RSSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: RelScheme -> SigMapI RSSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) 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 # 

data RSSymbolKind Source #

Constructors

STableK 
SColumnK 

Instances

Eq RSSymbolKind Source # 

Methods

(==) :: RSSymbolKind -> RSSymbolKind -> Bool

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

Data RSSymbolKind Source # 

Methods

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

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

toConstr :: RSSymbolKind -> Constr

dataTypeOf :: RSSymbolKind -> DataType

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

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

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

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

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

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

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

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

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

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

Ord RSSymbolKind Source # 
Show RSSymbolKind Source # 

Methods

showsPrec :: Int -> RSSymbolKind -> ShowS

show :: RSSymbolKind -> String

showList :: [RSSymbolKind] -> ShowS

Pretty RSSymbolKind Source #