Copyright	(c) Dominik Luecke Uni Bremen 2008
License	GPLv2 or higher, see LICENSE.txt
Maintainer	luecke@informatik.uni-bremen.de
Stability	experimental
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

RelationalScheme.Logic_Rel

Contents

Orphan instances

Description

Instance of class Logic for RelationalSchemes

Documentation

data RelScheme Source #

Constructors

RelScheme

Instances

Instances details

Show RelScheme Source #
Instance details Defined in RelationalScheme.Logic_Rel Methods showsPrec :: Int -> RelScheme -> ShowS show :: RelScheme -> String showList :: [RelScheme] -> ShowS
Language RelScheme Source #
Instance details Defined in RelationalScheme.Logic_Rel Methods language_name :: RelScheme -> String Source # description :: RelScheme -> String 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 #

Orphan instances

Semigroup RSTables Source #
Instance details Methods (<>) :: RSTables -> RSTables -> RSTables # sconcat :: NonEmpty RSTables -> RSTables stimes :: Integral b => b -> RSTables -> RSTables
Semigroup RSScheme Source #
Instance details Methods (<>) :: RSScheme -> RSScheme -> RSScheme # sconcat :: NonEmpty RSScheme -> RSScheme stimes :: Integral b => b -> RSScheme -> RSScheme
Semigroup RSRelationships Source #
Instance details Methods (<>) :: RSRelationships -> RSRelationships -> RSRelationships # sconcat :: NonEmpty RSRelationships -> RSRelationships stimes :: Integral b => b -> RSRelationships -> RSRelationships
Monoid RSTables Source #
Instance details Methods mempty :: RSTables mappend :: RSTables -> RSTables -> RSTables mconcat :: [RSTables] -> RSTables
Monoid RSScheme Source #
Instance details Methods mempty :: RSScheme mappend :: RSScheme -> RSScheme -> RSScheme mconcat :: [RSScheme] -> RSScheme
Monoid RSRelationships Source #
Instance details Methods mempty :: RSRelationships mappend :: RSRelationships -> RSRelationships -> RSRelationships mconcat :: [RSRelationships] -> RSRelationships
Category Sign RSMorphism Source #	Instance of Category for Rel
Instance details 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 #