Hets - the Heterogeneous Tool Set

Copyright(c) Hendrik Iben Uni Bremen 2005-2007
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerhiben@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable
Safe HaskellNone

OMDoc.Logic_OMDoc

Contents

Description

Logic and related instances for OMDoc.

Documentation

data OMDoc_PUN Source #

Constructors

OMDoc_PUN 

Instances

Show OMDoc_PUN Source # 

Methods

showsPrec :: Int -> OMDoc_PUN -> ShowS

show :: OMDoc_PUN -> String

showList :: [OMDoc_PUN] -> ShowS

Language OMDoc_PUN Source # 

Methods

language_name :: OMDoc_PUN -> String Source #

description :: OMDoc_PUN -> String Source #

Sentences OMDoc_PUN () OMDoc_Sign OMDoc_Morphism Symbol Source # 
Syntax OMDoc_PUN () Symbol () () Source # 

Methods

parsersAndPrinters :: OMDoc_PUN -> Map String (PrefixMap -> AParser st (), () -> Doc) Source #

parse_basic_spec :: OMDoc_PUN -> Maybe (PrefixMap -> AParser st ()) Source #

parseSingleSymbItem :: OMDoc_PUN -> Maybe (AParser st ()) Source #

parse_symb_items :: OMDoc_PUN -> Maybe (AParser st ()) Source #

parse_symb_map_items :: OMDoc_PUN -> Maybe (AParser st ()) Source #

toItem :: OMDoc_PUN -> () -> Item Source #

symb_items_name :: OMDoc_PUN -> () -> [String] Source #

StaticAnalysis OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism Symbol () Source # 

Methods

basic_analysis :: OMDoc_PUN -> Maybe (((), OMDoc_Sign, GlobalAnnos) -> Result ((), ExtSign OMDoc_Sign Symbol, [Named ()])) Source #

sen_analysis :: OMDoc_PUN -> Maybe (((), OMDoc_Sign, ()) -> Result ()) Source #

extBasicAnalysis :: OMDoc_PUN -> IRI -> LibName -> () -> OMDoc_Sign -> GlobalAnnos -> Result ((), ExtSign OMDoc_Sign Symbol, [Named ()]) Source #

stat_symb_map_items :: OMDoc_PUN -> OMDoc_Sign -> Maybe OMDoc_Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: OMDoc_PUN -> OMDoc_Sign -> [()] -> Result [()] Source #

convertTheory :: OMDoc_PUN -> Maybe ((OMDoc_Sign, [Named ()]) -> ()) Source #

ensures_amalgamability :: OMDoc_PUN -> ([CASLAmalgOpt], Gr OMDoc_Sign (Int, OMDoc_Morphism), [(Int, OMDoc_Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: OMDoc_PUN -> OMDoc_Morphism -> [Named ()] -> Result (OMDoc_Sign, [Named ()]) Source #

signature_colimit :: OMDoc_PUN -> Gr OMDoc_Sign (Int, OMDoc_Morphism) -> Result (OMDoc_Sign, Map Int OMDoc_Morphism) Source #

qualify :: OMDoc_PUN -> SIMPLE_ID -> LibName -> OMDoc_Morphism -> OMDoc_Sign -> Result (OMDoc_Morphism, [Named ()]) Source #

symbol_to_raw :: OMDoc_PUN -> Symbol -> () Source #

id_to_raw :: OMDoc_PUN -> Id -> () Source #

matches :: OMDoc_PUN -> Symbol -> () -> Bool Source #

empty_signature :: OMDoc_PUN -> OMDoc_Sign Source #

add_symb_to_sign :: OMDoc_PUN -> OMDoc_Sign -> Symbol -> Result OMDoc_Sign Source #

signature_union :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source #

signatureDiff :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source #

intersection :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source #

final_union :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Sign Source #

morphism_union :: OMDoc_PUN -> OMDoc_Morphism -> OMDoc_Morphism -> Result OMDoc_Morphism Source #

is_subsig :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Bool Source #

subsig_inclusion :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> Result OMDoc_Morphism Source #

generated_sign :: OMDoc_PUN -> Set Symbol -> OMDoc_Sign -> Result OMDoc_Morphism Source #

cogenerated_sign :: OMDoc_PUN -> Set Symbol -> OMDoc_Sign -> Result OMDoc_Morphism Source #

induced_from_morphism :: OMDoc_PUN -> EndoMap () -> OMDoc_Sign -> Result OMDoc_Morphism Source #

induced_from_to_morphism :: OMDoc_PUN -> EndoMap () -> ExtSign OMDoc_Sign Symbol -> ExtSign OMDoc_Sign Symbol -> Result OMDoc_Morphism Source #

is_transportable :: OMDoc_PUN -> OMDoc_Morphism -> Bool Source #

is_injective :: OMDoc_PUN -> OMDoc_Morphism -> Bool Source #

theory_to_taxonomy :: OMDoc_PUN -> TaxoGraphKind -> MMiSSOntology -> OMDoc_Sign -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: OMDoc_PUN -> String -> Bool -> OMDoc_Sign -> OMDoc_Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (OMDoc_Sign, [Named ()], OMDoc_Sign, OMDoc_Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: OMDoc_PUN -> OMDoc_Sign -> OMDoc_Sign -> [()] -> [()] -> Result (OMDoc_Sign, OMDoc_Sign, OMDoc_Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: OMDoc_PUN -> [IRI] -> (OMDoc_Sign, [Named ()]) -> Result (OMDoc_Sign, [Named ()]) Source #

Logic OMDoc_PUN () () () () () OMDoc_Sign OMDoc_Morphism Symbol () () Source # 

Methods

parse_basic_sen :: OMDoc_PUN -> Maybe (() -> AParser st ()) Source #

stability :: OMDoc_PUN -> Stability Source #

data_logic :: OMDoc_PUN -> Maybe AnyLogic Source #

top_sublogic :: OMDoc_PUN -> () Source #

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

bottomSublogic :: OMDoc_PUN -> Maybe () Source #

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

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

proj_sublogic_epsilon :: OMDoc_PUN -> () -> OMDoc_Sign -> OMDoc_Morphism Source #

provers :: OMDoc_PUN -> [Prover OMDoc_Sign () OMDoc_Morphism () ()] Source #

default_prover :: OMDoc_PUN -> String Source #

cons_checkers :: OMDoc_PUN -> [ConsChecker OMDoc_Sign () () OMDoc_Morphism ()] Source #

conservativityCheck :: OMDoc_PUN -> [ConservativityChecker OMDoc_Sign () OMDoc_Morphism] Source #

empty_proof_tree :: OMDoc_PUN -> () Source #

syntaxTable :: OMDoc_PUN -> OMDoc_Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: OMDoc_PUN -> Maybe OMCD Source #

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

export_senToOmdoc :: OMDoc_PUN -> NameMap Symbol -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: OMDoc_PUN -> SigMap Symbol -> OMDoc_Sign -> [Named ()] -> Result [TCElement] Source #

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

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

addOMadtToTheory :: OMDoc_PUN -> SigMapI Symbol -> (OMDoc_Sign, [Named ()]) -> [[OmdADT]] -> Result (OMDoc_Sign, [Named ()]) Source #

addOmdocToTheory :: OMDoc_PUN -> SigMapI Symbol -> (OMDoc_Sign, [Named ()]) -> [TCElement] -> Result (OMDoc_Sign, [Named ()]) Source #

Orphan instances