Hets - the Heterogeneous Tool Set

Copyright(c) C. Maeder DFKI 2008
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (via Logic.Logic)
Safe HaskellNone

VSE.Logic_VSE

Contents

Description

morphisms and symbols need to be extended, too

Documentation

data VSE Source #

Constructors

VSE 

Instances

Show VSE Source # 

Methods

showsPrec :: Int -> VSE -> ShowS

show :: VSE -> String

showList :: [VSE] -> ShowS

Language VSE Source # 

Methods

language_name :: VSE -> String Source #

description :: VSE -> String Source #

Sentences VSE Sentence VSESign VSEMor Symbol Source # 
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 

Methods

basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source #

sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source #

ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source #

signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source #

qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source #

symbol_to_raw :: VSE -> Symbol -> RawSymbol Source #

id_to_raw :: VSE -> Id -> RawSymbol Source #

matches :: VSE -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: VSE -> VSESign Source #

add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source #

signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source #

intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source #

final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source #

is_subsig :: VSE -> VSESign -> VSESign -> Bool Source #

subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source #

generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source #

induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source #

is_transportable :: VSE -> VSEMor -> Bool Source #

is_injective :: VSE -> VSEMor -> Bool Source #

theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #

Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source #

stability :: VSE -> Stability Source #

data_logic :: VSE -> Maybe AnyLogic Source #

top_sublogic :: VSE -> () Source #

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

bottomSublogic :: VSE -> Maybe () Source #

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

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

proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source #

provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source #

default_prover :: VSE -> String Source #

cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source #

conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source #

empty_proof_tree :: VSE -> () Source #

syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source #

omdoc_metatheory :: VSE -> Maybe OMCD Source #

export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source #

addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #

Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 

interSigM :: Monad m => (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e) Source #

Orphan instances