Hets - the Heterogeneous Tool Set

Copyright(c) Kristina Sojakova DFKI Bremen 2009
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerk.sojakova@jacobs-university.de
Stabilityexperimental
Portabilityportable Signatures of this logic are composed of a logical framework name (currently one of LF, Isabelle, or Maude) to be used as a meta-logic, and a tuple of signature and morphism names which determine the object logic. As such the logic Framework does not have any sentences and only identity signature morphisms. For reference see Integrating Logical Frameworks in Hets by M. Codescu et al (WADT10).
Safe HaskellNone

Framework.Logic_Framework

Contents

Description

 

Documentation

data Framework Source #

Constructors

Framework 

Instances

Show Framework Source # 

Methods

showsPrec :: Int -> Framework -> ShowS

show :: Framework -> String

showList :: [Framework] -> ShowS

Language Framework Source # 

Methods

language_name :: Framework -> String Source #

description :: Framework -> String Source #

Sentences Framework () LogicDef Morphism () Source # 

Methods

map_sen :: Framework -> Morphism -> () -> Result () Source #

simplify_sen :: Framework -> LogicDef -> () -> () Source #

negation :: Framework -> () -> Maybe () Source #

print_sign :: Framework -> LogicDef -> Doc Source #

print_named :: Framework -> Named () -> Doc Source #

sym_of :: Framework -> LogicDef -> [Set ()] Source #

mostSymsOf :: Framework -> LogicDef -> [()] Source #

symmap_of :: Framework -> Morphism -> EndoMap () Source #

sym_name :: Framework -> () -> Id Source #

sym_label :: Framework -> () -> Maybe String Source #

fullSymName :: Framework -> () -> String Source #

symKind :: Framework -> () -> String Source #

symsOfSen :: Framework -> LogicDef -> () -> [()] Source #

pair_symbols :: Framework -> () -> () -> Result () Source #

Syntax Framework LogicDef () () () Source # 
StaticAnalysis Framework LogicDef () () () LogicDef Morphism () () Source # 

Methods

basic_analysis :: Framework -> Maybe ((LogicDef, LogicDef, GlobalAnnos) -> Result (LogicDef, ExtSign LogicDef (), [Named ()])) Source #

sen_analysis :: Framework -> Maybe ((LogicDef, LogicDef, ()) -> Result ()) Source #

extBasicAnalysis :: Framework -> IRI -> LibName -> LogicDef -> LogicDef -> GlobalAnnos -> Result (LogicDef, ExtSign LogicDef (), [Named ()]) Source #

stat_symb_map_items :: Framework -> LogicDef -> Maybe LogicDef -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: Framework -> LogicDef -> [()] -> Result [()] Source #

convertTheory :: Framework -> Maybe ((LogicDef, [Named ()]) -> LogicDef) Source #

ensures_amalgamability :: Framework -> ([CASLAmalgOpt], Gr LogicDef (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Framework -> Morphism -> [Named ()] -> Result (LogicDef, [Named ()]) Source #

signature_colimit :: Framework -> Gr LogicDef (Int, Morphism) -> Result (LogicDef, Map Int Morphism) Source #

qualify :: Framework -> SIMPLE_ID -> LibName -> Morphism -> LogicDef -> Result (Morphism, [Named ()]) Source #

symbol_to_raw :: Framework -> () -> () Source #

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

matches :: Framework -> () -> () -> Bool Source #

empty_signature :: Framework -> LogicDef Source #

add_symb_to_sign :: Framework -> LogicDef -> () -> Result LogicDef Source #

signature_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

signatureDiff :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

intersection :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

final_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

morphism_union :: Framework -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: Framework -> LogicDef -> LogicDef -> Bool Source #

subsig_inclusion :: Framework -> LogicDef -> LogicDef -> Result Morphism Source #

generated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source #

cogenerated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source #

induced_from_morphism :: Framework -> EndoMap () -> LogicDef -> Result Morphism Source #

induced_from_to_morphism :: Framework -> EndoMap () -> ExtSign LogicDef () -> ExtSign LogicDef () -> Result Morphism Source #

is_transportable :: Framework -> Morphism -> Bool Source #

is_injective :: Framework -> Morphism -> Bool Source #

theory_to_taxonomy :: Framework -> TaxoGraphKind -> MMiSSOntology -> LogicDef -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: Framework -> String -> Bool -> LogicDef -> LogicDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (LogicDef, [Named ()], LogicDef, LogicDef, EndoMap (), EndoMap ()) Source #

equiv2cospan :: Framework -> LogicDef -> LogicDef -> [()] -> [()] -> Result (LogicDef, LogicDef, LogicDef, EndoMap (), EndoMap ()) Source #

extract_module :: Framework -> [IRI] -> (LogicDef, [Named ()]) -> Result (LogicDef, [Named ()]) Source #

Logic Framework () LogicDef () () () LogicDef Morphism () () () Source # 

Methods

parse_basic_sen :: Framework -> Maybe (LogicDef -> AParser st ()) Source #

stability :: Framework -> Stability Source #

data_logic :: Framework -> Maybe AnyLogic Source #

top_sublogic :: Framework -> () Source #

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

bottomSublogic :: Framework -> Maybe () Source #

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

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

proj_sublogic_epsilon :: Framework -> () -> LogicDef -> Morphism Source #

provers :: Framework -> [Prover LogicDef () Morphism () ()] Source #

default_prover :: Framework -> String Source #

cons_checkers :: Framework -> [ConsChecker LogicDef () () Morphism ()] Source #

conservativityCheck :: Framework -> [ConservativityChecker LogicDef () Morphism] Source #

empty_proof_tree :: Framework -> () Source #

syntaxTable :: Framework -> LogicDef -> Maybe SyntaxTable Source #

omdoc_metatheory :: Framework -> Maybe OMCD Source #

export_symToOmdoc :: Framework -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: Framework -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: Framework -> SigMap () -> LogicDef -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: Framework -> SigMapI () -> TCElement -> String -> Result () Source #

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

addOMadtToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [[OmdADT]] -> Result (LogicDef, [Named ()]) Source #

addOmdocToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [TCElement] -> Result (LogicDef, [Named ()]) Source #

data FrameworkCom Source #

Constructors

FrameworkCom 

Instances

Show FrameworkCom Source # 

Methods

showsPrec :: Int -> FrameworkCom -> ShowS

show :: FrameworkCom -> String

showList :: [FrameworkCom] -> ShowS

Language FrameworkCom Source # 
Sentences FrameworkCom () ComorphismDef MorphismCom () Source # 
Syntax FrameworkCom ComorphismDef () () () Source # 
StaticAnalysis FrameworkCom ComorphismDef () () () ComorphismDef MorphismCom () () Source # 

Methods

basic_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, GlobalAnnos) -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()])) Source #

sen_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, ()) -> Result ()) Source #

extBasicAnalysis :: FrameworkCom -> IRI -> LibName -> ComorphismDef -> ComorphismDef -> GlobalAnnos -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()]) Source #

stat_symb_map_items :: FrameworkCom -> ComorphismDef -> Maybe ComorphismDef -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: FrameworkCom -> ComorphismDef -> [()] -> Result [()] Source #

convertTheory :: FrameworkCom -> Maybe ((ComorphismDef, [Named ()]) -> ComorphismDef) Source #

ensures_amalgamability :: FrameworkCom -> ([CASLAmalgOpt], Gr ComorphismDef (Int, MorphismCom), [(Int, MorphismCom)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: FrameworkCom -> MorphismCom -> [Named ()] -> Result (ComorphismDef, [Named ()]) Source #

signature_colimit :: FrameworkCom -> Gr ComorphismDef (Int, MorphismCom) -> Result (ComorphismDef, Map Int MorphismCom) Source #

qualify :: FrameworkCom -> SIMPLE_ID -> LibName -> MorphismCom -> ComorphismDef -> Result (MorphismCom, [Named ()]) Source #

symbol_to_raw :: FrameworkCom -> () -> () Source #

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

matches :: FrameworkCom -> () -> () -> Bool Source #

empty_signature :: FrameworkCom -> ComorphismDef Source #

add_symb_to_sign :: FrameworkCom -> ComorphismDef -> () -> Result ComorphismDef Source #

signature_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

signatureDiff :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

intersection :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

final_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

morphism_union :: FrameworkCom -> MorphismCom -> MorphismCom -> Result MorphismCom Source #

is_subsig :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Bool Source #

subsig_inclusion :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result MorphismCom Source #

generated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source #

cogenerated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source #

induced_from_morphism :: FrameworkCom -> EndoMap () -> ComorphismDef -> Result MorphismCom Source #

induced_from_to_morphism :: FrameworkCom -> EndoMap () -> ExtSign ComorphismDef () -> ExtSign ComorphismDef () -> Result MorphismCom Source #

is_transportable :: FrameworkCom -> MorphismCom -> Bool Source #

is_injective :: FrameworkCom -> MorphismCom -> Bool Source #

theory_to_taxonomy :: FrameworkCom -> TaxoGraphKind -> MMiSSOntology -> ComorphismDef -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: FrameworkCom -> String -> Bool -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (ComorphismDef, [Named ()], ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source #

equiv2cospan :: FrameworkCom -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> Result (ComorphismDef, ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source #

extract_module :: FrameworkCom -> [IRI] -> (ComorphismDef, [Named ()]) -> Result (ComorphismDef, [Named ()]) Source #

Logic FrameworkCom () ComorphismDef () () () ComorphismDef MorphismCom () () () Source # 

Methods

parse_basic_sen :: FrameworkCom -> Maybe (ComorphismDef -> AParser st ()) Source #

stability :: FrameworkCom -> Stability Source #

data_logic :: FrameworkCom -> Maybe AnyLogic Source #

top_sublogic :: FrameworkCom -> () Source #

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

bottomSublogic :: FrameworkCom -> Maybe () Source #

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

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

proj_sublogic_epsilon :: FrameworkCom -> () -> ComorphismDef -> MorphismCom Source #

provers :: FrameworkCom -> [Prover ComorphismDef () MorphismCom () ()] Source #

default_prover :: FrameworkCom -> String Source #

cons_checkers :: FrameworkCom -> [ConsChecker ComorphismDef () () MorphismCom ()] Source #

conservativityCheck :: FrameworkCom -> [ConservativityChecker ComorphismDef () MorphismCom] Source #

empty_proof_tree :: FrameworkCom -> () Source #

syntaxTable :: FrameworkCom -> ComorphismDef -> Maybe SyntaxTable Source #

omdoc_metatheory :: FrameworkCom -> Maybe OMCD Source #

export_symToOmdoc :: FrameworkCom -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: FrameworkCom -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: FrameworkCom -> SigMap () -> ComorphismDef -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result () Source #

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

addOMadtToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [[OmdADT]] -> Result (ComorphismDef, [Named ()]) Source #

addOmdocToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [TCElement] -> Result (ComorphismDef, [Named ()]) Source #

Orphan instances