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

data RSRelType
- = RSone_to_one
- | RSone_to_many
- | RSmany_to_one
- | RSmany_to_many
data RSQualId = RSQualId {
- table :: Id
- column :: Id
- q_pos :: Range
}
data RSRel = RSRel {
- r_lhs :: [RSQualId]
- r_rhs :: [RSQualId]
- r_type :: RSRelType
- r_pos :: Range
}
data RSRelationships = RSRelationships [Annoted RSRel] Range
data RSScheme = RSScheme RSTables RSRelationships Range
type Sentence = RSRel
map_rel :: RSMorphism -> RSRel -> Result RSRel
getRels :: RSScheme -> [Annoted RSRel]
getSignature :: RSScheme -> RSTables

Documentation

data RSRelType Source #

Constructors

RSone_to_one
RSone_to_many
RSmany_to_one
RSmany_to_many

Instances

Instances details

Eq RSRelType Source #
Instance details Defined in RelationalScheme.AS Methods (==) :: RSRelType -> RSRelType -> Bool (/=) :: RSRelType -> RSRelType -> Bool
Data RSRelType Source #
Instance details Defined in RelationalScheme.AS 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 :: forall r r'. (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 #
Instance details Defined in RelationalScheme.AS 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 #
Instance details Defined in RelationalScheme.AS Methods showsPrec :: Int -> RSRelType -> ShowS show :: RSRelType -> String showList :: [RSRelType] -> ShowS
Generic RSRelType
Instance details Defined in RelationalScheme.ATC_RelationalScheme Associated Types type Rep RSRelType :: Type -> Type Methods from :: RSRelType -> Rep RSRelType x to :: Rep RSRelType x -> RSRelType
GetRange RSRelType Source #
Instance details Defined in RelationalScheme.AS Methods getRange :: RSRelType -> Range Source # rangeSpan :: RSRelType -> [Pos] Source #
FromJSON RSRelType
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods parseJSON :: Value -> Parser RSRelType parseJSONList :: Value -> Parser [RSRelType]
ToJSON RSRelType
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toJSON :: RSRelType -> Value toEncoding :: RSRelType -> Encoding toJSONList :: [RSRelType] -> Value toEncodingList :: [RSRelType] -> Encoding
ShATermConvertible RSRelType
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toShATermAux :: ATermTable -> RSRelType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RSRelType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RSRelType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RSRelType])
type Rep RSRelType
Instance details Defined in RelationalScheme.ATC_RelationalScheme type Rep RSRelType = D1 ('MetaData "RSRelType" "RelationalScheme.AS" "main" 'False) ((C1 ('MetaCons "RSone_to_one" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RSone_to_many" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RSmany_to_one" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RSmany_to_many" 'PrefixI 'False) (U1 :: Type -> Type)))

data RSQualId Source #

Constructors

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

Instances

Instances details

Eq RSQualId Source #
Instance details Defined in RelationalScheme.AS Methods (==) :: RSQualId -> RSQualId -> Bool (/=) :: RSQualId -> RSQualId -> Bool
Data RSQualId Source #
Instance details Defined in RelationalScheme.AS 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 :: forall r r'. (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 #
Instance details Defined in RelationalScheme.AS 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 #
Instance details Defined in RelationalScheme.AS Methods showsPrec :: Int -> RSQualId -> ShowS show :: RSQualId -> String showList :: [RSQualId] -> ShowS
Generic RSQualId
Instance details Defined in RelationalScheme.ATC_RelationalScheme Associated Types type Rep RSQualId :: Type -> Type Methods from :: RSQualId -> Rep RSQualId x to :: Rep RSQualId x -> RSQualId
GetRange RSQualId Source #
Instance details Defined in RelationalScheme.AS Methods getRange :: RSQualId -> Range Source # rangeSpan :: RSQualId -> [Pos] Source #
FromJSON RSQualId
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods parseJSON :: Value -> Parser RSQualId parseJSONList :: Value -> Parser [RSQualId]
ToJSON RSQualId
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toJSON :: RSQualId -> Value toEncoding :: RSQualId -> Encoding toJSONList :: [RSQualId] -> Value toEncodingList :: [RSQualId] -> Encoding
ShATermConvertible RSQualId
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toShATermAux :: ATermTable -> RSQualId -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RSQualId] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RSQualId) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RSQualId])
Pretty RSQualId Source #
Instance details Defined in RelationalScheme.AS Methods pretty :: RSQualId -> Doc Source # pretties :: [RSQualId] -> Doc Source #
type Rep RSQualId
Instance details Defined in RelationalScheme.ATC_RelationalScheme type Rep RSQualId = D1 ('MetaData "RSQualId" "RelationalScheme.AS" "main" 'False) (C1 ('MetaCons "RSQualId" 'PrefixI 'True) (S1 ('MetaSel ('Just "table") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :: (S1 ('MetaSel ('Just "column") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :: S1 ('MetaSel ('Just "q_pos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data RSRel Source #

Constructors

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

Instances

Instances details

Eq RSRel Source #
Instance details Defined in RelationalScheme.AS Methods (==) :: RSRel -> RSRel -> Bool (/=) :: RSRel -> RSRel -> Bool
Data RSRel Source #
Instance details Defined in RelationalScheme.AS 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 :: forall r r'. (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 #
Instance details Defined in RelationalScheme.AS 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 #
Instance details Defined in RelationalScheme.AS Methods showsPrec :: Int -> RSRel -> ShowS show :: RSRel -> String showList :: [RSRel] -> ShowS
Generic RSRel
Instance details Defined in RelationalScheme.ATC_RelationalScheme Associated Types type Rep RSRel :: Type -> Type Methods from :: RSRel -> Rep RSRel x to :: Rep RSRel x -> RSRel
GetRange RSRel Source #
Instance details Defined in RelationalScheme.AS Methods getRange :: RSRel -> Range Source # rangeSpan :: RSRel -> [Pos] Source #
FromJSON RSRel
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods parseJSON :: Value -> Parser RSRel parseJSONList :: Value -> Parser [RSRel]
ToJSON RSRel
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toJSON :: RSRel -> Value toEncoding :: RSRel -> Encoding toJSONList :: [RSRel] -> Value toEncodingList :: [RSRel] -> Encoding
ShATermConvertible RSRel
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toShATermAux :: ATermTable -> RSRel -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RSRel] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RSRel) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RSRel])
Pretty RSRel Source #
Instance details Defined in RelationalScheme.AS Methods pretty :: RSRel -> Doc Source # pretties :: [RSRel] -> Doc Source #
Sentences RelScheme Sentence Sign RSMorphism RSSymbol Source #	Instance of Sentences for Rel
Instance details Defined in RelationalScheme.Logic_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
Instance details Defined in RelationalScheme.Logic_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
Instance details Defined in RelationalScheme.Logic_Rel 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 #
Instance details Defined in Comorphisms.RelScheme2CASL Methods sourceLogic :: RelScheme2CASL -> RelScheme Source # sourceSublogic :: RelScheme2CASL -> () Source # sourceSublogicLossy :: RelScheme2CASL -> () Source # minSourceTheory :: RelScheme2CASL -> Maybe (LibName, String) Source # targetLogic :: RelScheme2CASL -> CASL Source # mapSublogic :: RelScheme2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: RelScheme2CASL -> RSMorphism -> Result CASLMor Source # map_sentence :: RelScheme2CASL -> Sign -> Sentence -> Result CASLFORMULA Source # map_symbol :: RelScheme2CASL -> Sign -> RSSymbol -> Set Symbol Source # extractModel :: RelScheme2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: RelScheme2CASL -> Bool Source # has_model_expansion :: RelScheme2CASL -> Bool Source # is_weakly_amalgamable :: RelScheme2CASL -> Bool Source # constituents :: RelScheme2CASL -> [String] Source # isInclusionComorphism :: RelScheme2CASL -> Bool Source # rps :: RelScheme2CASL -> Bool Source # eps :: RelScheme2CASL -> Bool Source # isGTC :: RelScheme2CASL -> Bool Source #
type Rep RSRel
Instance details Defined in RelationalScheme.ATC_RelationalScheme type Rep RSRel = D1 ('MetaData "RSRel" "RelationalScheme.AS" "main" 'False) (C1 ('MetaCons "RSRel" 'PrefixI 'True) ((S1 ('MetaSel ('Just "r_lhs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RSQualId]) :: S1 ('MetaSel ('Just "r_rhs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RSQualId])) :: (S1 ('MetaSel ('Just "r_type") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RSRelType) :*: S1 ('MetaSel ('Just "r_pos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data RSRelationships Source #

Constructors

RSRelationships [Annoted RSRel] Range

Instances

Instances details

Eq RSRelationships Source #
Instance details Defined in RelationalScheme.AS Methods (==) :: RSRelationships -> RSRelationships -> Bool (/=) :: RSRelationships -> RSRelationships -> Bool
Data RSRelationships Source #
Instance details Defined in RelationalScheme.AS 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 :: forall r r'. (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 #
Instance details Defined in RelationalScheme.AS 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 #
Instance details Defined in RelationalScheme.AS Methods showsPrec :: Int -> RSRelationships -> ShowS show :: RSRelationships -> String showList :: [RSRelationships] -> ShowS
Generic RSRelationships
Instance details Defined in RelationalScheme.ATC_RelationalScheme Associated Types type Rep RSRelationships :: Type -> Type Methods from :: RSRelationships -> Rep RSRelationships x to :: Rep RSRelationships x -> RSRelationships
Semigroup RSRelationships
Instance details Defined in RelationalScheme.Logic_Rel Methods (<>) :: RSRelationships -> RSRelationships -> RSRelationships # sconcat :: NonEmpty RSRelationships -> RSRelationships stimes :: Integral b => b -> RSRelationships -> RSRelationships
Monoid RSRelationships
Instance details Defined in RelationalScheme.Logic_Rel Methods mempty :: RSRelationships mappend :: RSRelationships -> RSRelationships -> RSRelationships mconcat :: [RSRelationships] -> RSRelationships
GetRange RSRelationships Source #
Instance details Defined in RelationalScheme.AS Methods getRange :: RSRelationships -> Range Source # rangeSpan :: RSRelationships -> [Pos] Source #
FromJSON RSRelationships
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods parseJSON :: Value -> Parser RSRelationships parseJSONList :: Value -> Parser [RSRelationships]
ToJSON RSRelationships
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toJSON :: RSRelationships -> Value toEncoding :: RSRelationships -> Encoding toJSONList :: [RSRelationships] -> Value toEncodingList :: [RSRelationships] -> Encoding
ShATermConvertible RSRelationships
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toShATermAux :: ATermTable -> RSRelationships -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RSRelationships] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RSRelationships) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RSRelationships])
Pretty RSRelationships Source #
Instance details Defined in RelationalScheme.AS Methods pretty :: RSRelationships -> Doc Source # pretties :: [RSRelationships] -> Doc Source #
type Rep RSRelationships
Instance details Defined in RelationalScheme.ATC_RelationalScheme type Rep RSRelationships = D1 ('MetaData "RSRelationships" "RelationalScheme.AS" "main" 'False) (C1 ('MetaCons "RSRelationships" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted RSRel]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data RSScheme Source #

Constructors

RSScheme RSTables RSRelationships Range

Instances

Instances details

Eq RSScheme Source #
Instance details Defined in RelationalScheme.AS Methods (==) :: RSScheme -> RSScheme -> Bool (/=) :: RSScheme -> RSScheme -> Bool
Data RSScheme Source #
Instance details Defined in RelationalScheme.AS 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 :: forall r r'. (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 #
Instance details Defined in RelationalScheme.AS 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 #
Instance details Defined in RelationalScheme.AS Methods showsPrec :: Int -> RSScheme -> ShowS show :: RSScheme -> String showList :: [RSScheme] -> ShowS
Generic RSScheme
Instance details Defined in RelationalScheme.ATC_RelationalScheme Associated Types type Rep RSScheme :: Type -> Type Methods from :: RSScheme -> Rep RSScheme x to :: Rep RSScheme x -> RSScheme
Semigroup RSScheme
Instance details Defined in RelationalScheme.Logic_Rel Methods (<>) :: RSScheme -> RSScheme -> RSScheme # sconcat :: NonEmpty RSScheme -> RSScheme stimes :: Integral b => b -> RSScheme -> RSScheme
Monoid RSScheme
Instance details Defined in RelationalScheme.Logic_Rel Methods mempty :: RSScheme mappend :: RSScheme -> RSScheme -> RSScheme mconcat :: [RSScheme] -> RSScheme
GetRange RSScheme Source #
Instance details Defined in RelationalScheme.AS Methods getRange :: RSScheme -> Range Source # rangeSpan :: RSScheme -> [Pos] Source #
FromJSON RSScheme
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods parseJSON :: Value -> Parser RSScheme parseJSONList :: Value -> Parser [RSScheme]
ToJSON RSScheme
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toJSON :: RSScheme -> Value toEncoding :: RSScheme -> Encoding toJSONList :: [RSScheme] -> Value toEncodingList :: [RSScheme] -> Encoding
ShATermConvertible RSScheme
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toShATermAux :: ATermTable -> RSScheme -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RSScheme] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RSScheme) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RSScheme])
Pretty RSScheme Source #
Instance details Defined in RelationalScheme.AS Methods pretty :: RSScheme -> Doc Source # pretties :: [RSScheme] -> Doc Source #
Syntax RelScheme RSScheme RSSymbol () () Source #	Syntax of Rel
Instance details Defined in RelationalScheme.Logic_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 (PrefixMap -> AParser st ()) Source # parse_symb_items :: RelScheme -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: RelScheme -> Maybe (PrefixMap -> 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
Instance details Defined in RelationalScheme.Logic_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
Instance details Defined in RelationalScheme.Logic_Rel 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 #
Instance details Defined in Comorphisms.RelScheme2CASL Methods sourceLogic :: RelScheme2CASL -> RelScheme Source # sourceSublogic :: RelScheme2CASL -> () Source # sourceSublogicLossy :: RelScheme2CASL -> () Source # minSourceTheory :: RelScheme2CASL -> Maybe (LibName, String) Source # targetLogic :: RelScheme2CASL -> CASL Source # mapSublogic :: RelScheme2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: RelScheme2CASL -> RSMorphism -> Result CASLMor Source # map_sentence :: RelScheme2CASL -> Sign -> Sentence -> Result CASLFORMULA Source # map_symbol :: RelScheme2CASL -> Sign -> RSSymbol -> Set Symbol Source # extractModel :: RelScheme2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: RelScheme2CASL -> Bool Source # has_model_expansion :: RelScheme2CASL -> Bool Source # is_weakly_amalgamable :: RelScheme2CASL -> Bool Source # constituents :: RelScheme2CASL -> [String] Source # isInclusionComorphism :: RelScheme2CASL -> Bool Source # rps :: RelScheme2CASL -> Bool Source # eps :: RelScheme2CASL -> Bool Source # isGTC :: RelScheme2CASL -> Bool Source #
type Rep RSScheme
Instance details Defined in RelationalScheme.ATC_RelationalScheme type Rep RSScheme = D1 ('MetaData "RSScheme" "RelationalScheme.AS" "main" 'False) (C1 ('MetaCons "RSScheme" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RSTables) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RSRelationships) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

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 #