Copyright	Dominik Luecke Uni Bremen 2008
License	GPLv2 or higher, see LICENSE.txt or LIZENZ.txt
Maintainer	luecke@informatik.uni-bremen.de
Stability	provisional
Portability	portable
Safe Haskell	None

RelationalScheme.AS

Description

Abstract syntax for Relational Schemes

Synopsis

Documentation

data RSRelType Source #

Constructors

RSone_to_one
RSone_to_many
RSmany_to_one
RSmany_to_many

Instances

Eq RSRelType Source #
Methods (==) :: RSRelType -> RSRelType -> Bool (/=) :: RSRelType -> RSRelType -> Bool
Data RSRelType Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RSRelType -> c RSRelType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RSRelType toConstr :: RSRelType -> Constr dataTypeOf :: RSRelType -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c RSRelType) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RSRelType) gmapT :: (forall b. Data b => b -> b) -> RSRelType -> RSRelType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RSRelType -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RSRelType -> r gmapQ :: (forall d. Data d => d -> u) -> RSRelType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RSRelType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RSRelType -> m RSRelType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RSRelType -> m RSRelType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RSRelType -> m RSRelType
Ord RSRelType Source #
Methods compare :: RSRelType -> RSRelType -> Ordering (<) :: RSRelType -> RSRelType -> Bool (<=) :: RSRelType -> RSRelType -> Bool (>) :: RSRelType -> RSRelType -> Bool (>=) :: RSRelType -> RSRelType -> Bool max :: RSRelType -> RSRelType -> RSRelType min :: RSRelType -> RSRelType -> RSRelType
Show RSRelType Source #
Methods showsPrec :: Int -> RSRelType -> ShowS show :: RSRelType -> String showList :: [RSRelType] -> ShowS
GetRange RSRelType Source #
Methods getRange :: RSRelType -> Range Source # rangeSpan :: RSRelType -> [Pos] Source #

data RSQualId Source #

Constructors

RSQualId
Fields table :: Id column :: Id q_pos :: Range

Instances

Eq RSQualId Source #
Methods (==) :: RSQualId -> RSQualId -> Bool (/=) :: RSQualId -> RSQualId -> Bool
Data RSQualId Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RSQualId -> c RSQualId gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RSQualId toConstr :: RSQualId -> Constr dataTypeOf :: RSQualId -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c RSQualId) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RSQualId) gmapT :: (forall b. Data b => b -> b) -> RSQualId -> RSQualId gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RSQualId -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RSQualId -> r gmapQ :: (forall d. Data d => d -> u) -> RSQualId -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RSQualId -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RSQualId -> m RSQualId gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RSQualId -> m RSQualId gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RSQualId -> m RSQualId
Ord RSQualId Source #
Methods compare :: RSQualId -> RSQualId -> Ordering (<) :: RSQualId -> RSQualId -> Bool (<=) :: RSQualId -> RSQualId -> Bool (>) :: RSQualId -> RSQualId -> Bool (>=) :: RSQualId -> RSQualId -> Bool max :: RSQualId -> RSQualId -> RSQualId min :: RSQualId -> RSQualId -> RSQualId
Show RSQualId Source #
Methods showsPrec :: Int -> RSQualId -> ShowS show :: RSQualId -> String showList :: [RSQualId] -> ShowS
GetRange RSQualId Source #
Methods getRange :: RSQualId -> Range Source # rangeSpan :: RSQualId -> [Pos] Source #
Pretty RSQualId Source #
Methods pretty :: RSQualId -> Doc Source # pretties :: [RSQualId] -> Doc Source #

data RSRel Source #

Constructors

RSRel
Fields r_lhs :: [RSQualId] r_rhs :: [RSQualId] r_type :: RSRelType r_pos :: Range

Instances

Eq RSRel Source #
Methods (==) :: RSRel -> RSRel -> Bool (/=) :: RSRel -> RSRel -> Bool
Data RSRel Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RSRel -> c RSRel gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RSRel toConstr :: RSRel -> Constr dataTypeOf :: RSRel -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c RSRel) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RSRel) gmapT :: (forall b. Data b => b -> b) -> RSRel -> RSRel gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RSRel -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RSRel -> r gmapQ :: (forall d. Data d => d -> u) -> RSRel -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RSRel -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RSRel -> m RSRel gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RSRel -> m RSRel gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RSRel -> m RSRel
Ord RSRel Source #
Methods compare :: RSRel -> RSRel -> Ordering (<) :: RSRel -> RSRel -> Bool (<=) :: RSRel -> RSRel -> Bool (>) :: RSRel -> RSRel -> Bool (>=) :: RSRel -> RSRel -> Bool max :: RSRel -> RSRel -> RSRel min :: RSRel -> RSRel -> RSRel
Show RSRel Source #
Methods showsPrec :: Int -> RSRel -> ShowS show :: RSRel -> String showList :: [RSRel] -> ShowS
GetRange RSRel Source #
Methods getRange :: RSRel -> Range Source # rangeSpan :: RSRel -> [Pos] Source #
Pretty RSRel Source #
Methods pretty :: RSRel -> Doc Source # pretties :: [RSRel] -> Doc Source #
Sentences RelScheme Sentence Sign RSMorphism RSSymbol Source #	Instance of Sentences for Rel
Methods map_sen :: RelScheme -> RSMorphism -> Sentence -> Result Sentence Source # simplify_sen :: RelScheme -> Sign -> Sentence -> Sentence Source # negation :: RelScheme -> Sentence -> Maybe Sentence Source # print_sign :: RelScheme -> Sign -> Doc Source # print_named :: RelScheme -> Named Sentence -> Doc Source # sym_of :: RelScheme -> Sign -> [Set RSSymbol] Source # mostSymsOf :: RelScheme -> Sign -> [RSSymbol] Source # symmap_of :: RelScheme -> RSMorphism -> EndoMap RSSymbol Source # sym_name :: RelScheme -> RSSymbol -> Id Source # sym_label :: RelScheme -> RSSymbol -> Maybe String Source # fullSymName :: RelScheme -> RSSymbol -> String Source # symKind :: RelScheme -> RSSymbol -> String Source # symsOfSen :: RelScheme -> Sign -> Sentence -> [RSSymbol] Source # pair_symbols :: RelScheme -> RSSymbol -> RSSymbol -> Result RSSymbol Source #
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 # sublogicOfTheo :: RelScheme -> (Sign, [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 #
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 #

data RSRelationships Source #

Constructors

RSRelationships [Annoted RSRel] Range

Instances

Eq RSRelationships Source #
Methods (==) :: RSRelationships -> RSRelationships -> Bool (/=) :: RSRelationships -> RSRelationships -> Bool
Data RSRelationships Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RSRelationships -> c RSRelationships gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RSRelationships toConstr :: RSRelationships -> Constr dataTypeOf :: RSRelationships -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c RSRelationships) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RSRelationships) gmapT :: (forall b. Data b => b -> b) -> RSRelationships -> RSRelationships gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RSRelationships -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RSRelationships -> r gmapQ :: (forall d. Data d => d -> u) -> RSRelationships -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RSRelationships -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RSRelationships -> m RSRelationships gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RSRelationships -> m RSRelationships gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RSRelationships -> m RSRelationships
Ord RSRelationships Source #
Methods compare :: RSRelationships -> RSRelationships -> Ordering (<) :: RSRelationships -> RSRelationships -> Bool (<=) :: RSRelationships -> RSRelationships -> Bool (>) :: RSRelationships -> RSRelationships -> Bool (>=) :: RSRelationships -> RSRelationships -> Bool max :: RSRelationships -> RSRelationships -> RSRelationships min :: RSRelationships -> RSRelationships -> RSRelationships
Show RSRelationships Source #
Methods showsPrec :: Int -> RSRelationships -> ShowS show :: RSRelationships -> String showList :: [RSRelationships] -> ShowS
GetRange RSRelationships Source #
Methods getRange :: RSRelationships -> Range Source # rangeSpan :: RSRelationships -> [Pos] Source #
Pretty RSRelationships Source #
Methods pretty :: RSRelationships -> Doc Source # pretties :: [RSRelationships] -> Doc Source #

data RSScheme Source #

Constructors

RSScheme RSTables RSRelationships Range

Instances

Eq RSScheme Source #
Methods (==) :: RSScheme -> RSScheme -> Bool (/=) :: RSScheme -> RSScheme -> Bool
Data RSScheme Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RSScheme -> c RSScheme gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RSScheme toConstr :: RSScheme -> Constr dataTypeOf :: RSScheme -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c RSScheme) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RSScheme) gmapT :: (forall b. Data b => b -> b) -> RSScheme -> RSScheme gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RSScheme -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RSScheme -> r gmapQ :: (forall d. Data d => d -> u) -> RSScheme -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RSScheme -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RSScheme -> m RSScheme gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RSScheme -> m RSScheme gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RSScheme -> m RSScheme
Ord RSScheme Source #
Methods compare :: RSScheme -> RSScheme -> Ordering (<) :: RSScheme -> RSScheme -> Bool (<=) :: RSScheme -> RSScheme -> Bool (>) :: RSScheme -> RSScheme -> Bool (>=) :: RSScheme -> RSScheme -> Bool max :: RSScheme -> RSScheme -> RSScheme min :: RSScheme -> RSScheme -> RSScheme
Show RSScheme Source #
Methods showsPrec :: Int -> RSScheme -> ShowS show :: RSScheme -> String showList :: [RSScheme] -> ShowS
GetRange RSScheme Source #
Methods getRange :: RSScheme -> Range Source # rangeSpan :: RSScheme -> [Pos] Source #
Pretty RSScheme Source #
Methods pretty :: RSScheme -> Doc Source # pretties :: [RSScheme] -> Doc Source #
Syntax RelScheme RSScheme RSSymbol () () Source #	Syntax of Rel
Methods parsersAndPrinters :: RelScheme -> Map String (PrefixMap -> AParser st RSScheme, RSScheme -> Doc) Source # parse_basic_spec :: RelScheme -> Maybe (PrefixMap -> AParser st RSScheme) Source # parseSingleSymbItem :: RelScheme -> Maybe (AParser st ()) Source # parse_symb_items :: RelScheme -> Maybe (AParser st ()) Source # parse_symb_map_items :: RelScheme -> Maybe (AParser st ()) Source # toItem :: RelScheme -> RSScheme -> Item Source # symb_items_name :: RelScheme -> () -> [String] Source #
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 # sublogicOfTheo :: RelScheme -> (Sign, [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 #
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 #

type Sentence = RSRel Source #

map_rel :: RSMorphism -> RSRel -> Result RSRel Source #

oo-style getter function for Relations

getRels :: RSScheme -> [Annoted RSRel] Source #

oo-style getter function for signatures

getSignature :: RSScheme -> RSTables Source #