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.Sign

Description

Signature for Relational Schemes

Synopsis

type RSIsKey = Bool
data RSDatatype
- = RSboolean
- | RSbinary
- | RSdate
- | RSdatetime
- | RSdecimal
- | RSfloat
- | RSinteger
- | RSstring
- | RStext
- | RStime
- | RStimestamp
- | RSdouble
- | RSnonPosInteger
- | RSnonNegInteger
- | RSlong
- | RSPointer
type RSRawSymbol = Id
data RSColumn = RSColumn {
- c_name :: Id
- c_data :: RSDatatype
- c_key :: RSIsKey
}
data RSTable = RSTable {
- t_name :: Id
- columns :: [RSColumn]
- rsannos :: [Annotation]
- t_keys :: Set (Id, RSDatatype)
}
data RSTables = RSTables {
- tables :: Set RSTable
}
type Sign = RSTables
data RSMorphism = RSMorphism {
- domain :: RSTables
- codomain :: RSTables
- table_map :: Map Id Id
- column_map :: Map Id RSTMap
}
data RSTMap = RSTMap {
- col_map :: Map Id Id
}
emptyRSSign :: RSTables
isRSSubsig :: RSTables -> RSTables -> Bool
idMor :: RSTables -> RSMorphism
rsInclusion :: RSTables -> RSTables -> Result RSMorphism
uniteSig :: MonadFail m => RSTables -> RSTables -> m RSTables
comp_rst_mor :: RSMorphism -> RSMorphism -> Result RSMorphism
data RSSymbol
- = STable Id
- | SColumn Id Id RSDatatype RSIsKey
data RSSymbolKind
- = STableK
- | SColumnK
sym_kind :: RSSymbol -> RSSymbolKind

Documentation

type RSIsKey = Bool Source #

data RSDatatype Source #

Constructors

RSboolean
RSbinary
RSdate
RSdatetime
RSdecimal
RSfloat
RSinteger
RSstring
RStext
RStime
RStimestamp
RSdouble
RSnonPosInteger
RSnonNegInteger
RSlong
RSPointer

Instances

Instances details

Eq RSDatatype Source #
Instance details Defined in RelationalScheme.Sign Methods (==) :: RSDatatype -> RSDatatype -> Bool (/=) :: RSDatatype -> RSDatatype -> Bool
Data RSDatatype Source #
Instance details Defined in RelationalScheme.Sign 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 :: forall r r'. (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 #
Instance details Defined in RelationalScheme.Sign Methods compare :: RSDatatype -> RSDatatype -> Ordering (<) :: RSDatatype -> RSDatatype -> Bool (<=) :: RSDatatype -> RSDatatype -> Bool (>) :: RSDatatype -> RSDatatype -> Bool (>=) :: RSDatatype -> RSDatatype -> Bool max :: RSDatatype -> RSDatatype -> RSDatatype min :: RSDatatype -> RSDatatype -> RSDatatype
Show RSDatatype Source #
Instance details Defined in RelationalScheme.Sign Methods showsPrec :: Int -> RSDatatype -> ShowS show :: RSDatatype -> String showList :: [RSDatatype] -> ShowS
Generic RSDatatype
Instance details Defined in RelationalScheme.ATC_RelationalScheme Associated Types type Rep RSDatatype :: Type -> Type Methods from :: RSDatatype -> Rep RSDatatype x to :: Rep RSDatatype x -> RSDatatype
FromJSON RSDatatype
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods parseJSON :: Value -> Parser RSDatatype parseJSONList :: Value -> Parser [RSDatatype]
ToJSON RSDatatype
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toJSON :: RSDatatype -> Value toEncoding :: RSDatatype -> Encoding toJSONList :: [RSDatatype] -> Value toEncodingList :: [RSDatatype] -> Encoding
ShATermConvertible RSDatatype
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toShATermAux :: ATermTable -> RSDatatype -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RSDatatype] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RSDatatype) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RSDatatype])
Pretty RSDatatype Source #
Instance details Defined in RelationalScheme.Sign Methods pretty :: RSDatatype -> Doc Source # pretties :: [RSDatatype] -> Doc Source #
type Rep RSDatatype
Instance details Defined in RelationalScheme.ATC_RelationalScheme type Rep RSDatatype = D1 ('MetaData "RSDatatype" "RelationalScheme.Sign" "main" 'False) ((((C1 ('MetaCons "RSboolean" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RSbinary" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RSdate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RSdatetime" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RSdecimal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RSfloat" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RSinteger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RSstring" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "RStext" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RStime" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RStimestamp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RSdouble" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RSnonPosInteger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RSnonNegInteger" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RSlong" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RSPointer" 'PrefixI 'False) (U1 :: Type -> Type)))))

type RSRawSymbol = Id Source #

data RSColumn Source #

Constructors

RSColumn
Fields c_name :: Id c_data :: RSDatatype c_key :: RSIsKey

Instances

Instances details

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

data RSTable Source #

Constructors

RSTable
Fields t_name :: Id columns :: [RSColumn] rsannos :: [Annotation] t_keys :: Set (Id, RSDatatype)

Instances

Instances details

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

data RSTables Source #

Constructors

RSTables
Fields tables :: Set RSTable

Instances

Instances details

Eq RSTables Source #
Instance details Defined in RelationalScheme.Sign Methods (==) :: RSTables -> RSTables -> Bool (/=) :: RSTables -> RSTables -> Bool
Data RSTables Source #
Instance details Defined in RelationalScheme.Sign 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 :: forall r r'. (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 #
Instance details Defined in RelationalScheme.Sign 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 #
Instance details Defined in RelationalScheme.Sign Methods showsPrec :: Int -> RSTables -> ShowS show :: RSTables -> String showList :: [RSTables] -> ShowS
Generic RSTables
Instance details Defined in RelationalScheme.ATC_RelationalScheme Associated Types type Rep RSTables :: Type -> Type Methods from :: RSTables -> Rep RSTables x to :: Rep RSTables x -> RSTables
Semigroup RSTables
Instance details Defined in RelationalScheme.Logic_Rel Methods (<>) :: RSTables -> RSTables -> RSTables # sconcat :: NonEmpty RSTables -> RSTables stimes :: Integral b => b -> RSTables -> RSTables
Monoid RSTables
Instance details Defined in RelationalScheme.Logic_Rel Methods mempty :: RSTables mappend :: RSTables -> RSTables -> RSTables mconcat :: [RSTables] -> RSTables
GetRange RSTables Source #
Instance details Defined in RelationalScheme.Sign Methods getRange :: RSTables -> Range Source # rangeSpan :: RSTables -> [Pos] Source #
FromJSON RSTables
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods parseJSON :: Value -> Parser RSTables parseJSONList :: Value -> Parser [RSTables]
ToJSON RSTables
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toJSON :: RSTables -> Value toEncoding :: RSTables -> Encoding toJSONList :: [RSTables] -> Value toEncodingList :: [RSTables] -> Encoding
ShATermConvertible RSTables
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toShATermAux :: ATermTable -> RSTables -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RSTables] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RSTables) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RSTables])
Pretty RSTables Source #
Instance details Defined in RelationalScheme.Sign Methods pretty :: RSTables -> Doc Source # pretties :: [RSTables] -> Doc Source #
Category Sign RSMorphism Source #	Instance of Category for Rel
Instance details Defined in RelationalScheme.Logic_Rel Methods ide :: Sign -> RSMorphism Source # composeMorphisms :: RSMorphism -> RSMorphism -> Result RSMorphism Source # dom :: RSMorphism -> Sign Source # cod :: RSMorphism -> Sign Source # inverse :: RSMorphism -> Result RSMorphism Source # isInclusion :: RSMorphism -> Bool Source # legal_mor :: RSMorphism -> Result () 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 RSTables
Instance details Defined in RelationalScheme.ATC_RelationalScheme type Rep RSTables = D1 ('MetaData "RSTables" "RelationalScheme.Sign" "main" 'False) (C1 ('MetaCons "RSTables" 'PrefixI 'True) (S1 ('MetaSel ('Just "tables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set RSTable))))

type Sign = RSTables Source #

data RSMorphism Source #

Constructors

RSMorphism
Fields domain :: RSTables codomain :: RSTables table_map :: Map Id Id column_map :: Map Id RSTMap

Instances

Instances details

Eq RSMorphism Source #
Instance details Defined in RelationalScheme.Sign Methods (==) :: RSMorphism -> RSMorphism -> Bool (/=) :: RSMorphism -> RSMorphism -> Bool
Data RSMorphism Source #
Instance details Defined in RelationalScheme.Sign 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 :: forall r r'. (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 #
Instance details Defined in RelationalScheme.Sign Methods compare :: RSMorphism -> RSMorphism -> Ordering (<) :: RSMorphism -> RSMorphism -> Bool (<=) :: RSMorphism -> RSMorphism -> Bool (>) :: RSMorphism -> RSMorphism -> Bool (>=) :: RSMorphism -> RSMorphism -> Bool max :: RSMorphism -> RSMorphism -> RSMorphism min :: RSMorphism -> RSMorphism -> RSMorphism
Show RSMorphism Source #
Instance details Defined in RelationalScheme.Sign Methods showsPrec :: Int -> RSMorphism -> ShowS show :: RSMorphism -> String showList :: [RSMorphism] -> ShowS
Generic RSMorphism
Instance details Defined in RelationalScheme.ATC_RelationalScheme Associated Types type Rep RSMorphism :: Type -> Type Methods from :: RSMorphism -> Rep RSMorphism x to :: Rep RSMorphism x -> RSMorphism
FromJSON RSMorphism
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods parseJSON :: Value -> Parser RSMorphism parseJSONList :: Value -> Parser [RSMorphism]
ToJSON RSMorphism
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toJSON :: RSMorphism -> Value toEncoding :: RSMorphism -> Encoding toJSONList :: [RSMorphism] -> Value toEncodingList :: [RSMorphism] -> Encoding
ShATermConvertible RSMorphism
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toShATermAux :: ATermTable -> RSMorphism -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RSMorphism] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RSMorphism) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RSMorphism])
Pretty RSMorphism Source #
Instance details Defined in RelationalScheme.Sign Methods pretty :: RSMorphism -> Doc Source # pretties :: [RSMorphism] -> Doc Source #
Category Sign RSMorphism Source #	Instance of Category for Rel
Instance details Defined in RelationalScheme.Logic_Rel Methods ide :: Sign -> RSMorphism Source # composeMorphisms :: RSMorphism -> RSMorphism -> Result RSMorphism Source # dom :: RSMorphism -> Sign Source # cod :: RSMorphism -> Sign Source # inverse :: RSMorphism -> Result RSMorphism Source # isInclusion :: RSMorphism -> Bool Source # legal_mor :: RSMorphism -> Result () 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 RSMorphism
Instance details Defined in RelationalScheme.ATC_RelationalScheme type Rep RSMorphism = D1 ('MetaData "RSMorphism" "RelationalScheme.Sign" "main" 'False) (C1 ('MetaCons "RSMorphism" 'PrefixI 'True) ((S1 ('MetaSel ('Just "domain") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RSTables) :: S1 ('MetaSel ('Just "codomain") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RSTables)) :: (S1 ('MetaSel ('Just "table_map") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Id Id)) :*: S1 ('MetaSel ('Just "column_map") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Id RSTMap)))))

data RSTMap Source #

Constructors

RSTMap
Fields col_map :: Map Id Id

Instances

Instances details

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

emptyRSSign :: RSTables Source #

id-morphism for RS

isRSSubsig :: RSTables -> RSTables -> Bool Source #

idMor :: RSTables -> RSMorphism Source #

rsInclusion :: RSTables -> RSTables -> Result RSMorphism Source #

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

comp_rst_mor :: RSMorphism -> RSMorphism -> Result RSMorphism Source #

data RSSymbol Source #

Constructors

STable Id
SColumn Id Id RSDatatype RSIsKey

Instances

Instances details

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

data RSSymbolKind Source #

Constructors

STableK
SColumnK

Instances

Instances details

Eq RSSymbolKind Source #
Instance details Defined in RelationalScheme.Sign Methods (==) :: RSSymbolKind -> RSSymbolKind -> Bool (/=) :: RSSymbolKind -> RSSymbolKind -> Bool
Data RSSymbolKind Source #
Instance details Defined in RelationalScheme.Sign 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 :: forall r r'. (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 #
Instance details Defined in RelationalScheme.Sign Methods compare :: RSSymbolKind -> RSSymbolKind -> Ordering (<) :: RSSymbolKind -> RSSymbolKind -> Bool (<=) :: RSSymbolKind -> RSSymbolKind -> Bool (>) :: RSSymbolKind -> RSSymbolKind -> Bool (>=) :: RSSymbolKind -> RSSymbolKind -> Bool max :: RSSymbolKind -> RSSymbolKind -> RSSymbolKind min :: RSSymbolKind -> RSSymbolKind -> RSSymbolKind
Show RSSymbolKind Source #
Instance details Defined in RelationalScheme.Sign Methods showsPrec :: Int -> RSSymbolKind -> ShowS show :: RSSymbolKind -> String showList :: [RSSymbolKind] -> ShowS
Generic RSSymbolKind
Instance details Defined in RelationalScheme.ATC_RelationalScheme Associated Types type Rep RSSymbolKind :: Type -> Type Methods from :: RSSymbolKind -> Rep RSSymbolKind x to :: Rep RSSymbolKind x -> RSSymbolKind
FromJSON RSSymbolKind
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods parseJSON :: Value -> Parser RSSymbolKind parseJSONList :: Value -> Parser [RSSymbolKind]
ToJSON RSSymbolKind
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toJSON :: RSSymbolKind -> Value toEncoding :: RSSymbolKind -> Encoding toJSONList :: [RSSymbolKind] -> Value toEncodingList :: [RSSymbolKind] -> Encoding
ShATermConvertible RSSymbolKind
Instance details Defined in RelationalScheme.ATC_RelationalScheme Methods toShATermAux :: ATermTable -> RSSymbolKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RSSymbolKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RSSymbolKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RSSymbolKind])
Pretty RSSymbolKind Source #
Instance details Defined in RelationalScheme.Sign Methods pretty :: RSSymbolKind -> Doc Source # pretties :: [RSSymbolKind] -> Doc Source #
type Rep RSSymbolKind
Instance details Defined in RelationalScheme.ATC_RelationalScheme type Rep RSSymbolKind = D1 ('MetaData "RSSymbolKind" "RelationalScheme.Sign" "main" 'False) (C1 ('MetaCons "STableK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SColumnK" 'PrefixI 'False) (U1 :: Type -> Type))

sym_kind :: RSSymbol -> RSSymbolKind Source #