Hets - the Heterogeneous Tool Set

Copyright(c) Dominik Luecke Uni Bremen 2008
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityexperimental
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

RelationalScheme.Logic_Rel

Contents

Description

Instance of class Logic for RelationalSchemes

Synopsis

Documentation

data RelScheme Source #

Constructors

RelScheme 

Instances

Show RelScheme Source # 

Methods

showsPrec :: Int -> RelScheme -> ShowS

show :: RelScheme -> String

showList :: [RelScheme] -> ShowS

Language RelScheme Source # 

Methods

language_name :: RelScheme -> String Source #

description :: RelScheme -> String Source #

Sentences RelScheme Sentence Sign RSMorphism RSSymbol Source #

Instance of Sentences for Rel

Syntax RelScheme RSScheme RSSymbol () () Source #

Syntax of Rel

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

Static Analysis for Rel

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

empty_signature :: RelScheme -> Sign Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Instance of Logic for Relational Schemes

Methods

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

stability :: RelScheme -> Stability Source #

data_logic :: RelScheme -> Maybe AnyLogic Source #

top_sublogic :: RelScheme -> () Source #

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

bottomSublogic :: RelScheme -> Maybe () Source #

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

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

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

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

default_prover :: RelScheme -> String Source #

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

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

empty_proof_tree :: RelScheme -> () Source #

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

omdoc_metatheory :: RelScheme -> Maybe OMCD Source #

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

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

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

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

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

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

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

Comorphism RelScheme2CASL RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 

Orphan instances