Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski, and Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

Logic.ExtSign

Description

Functions from the class Logic that operate over signatures are extended to work over signatures with symbol sets.

Synopsis

Documentation

ext_sym_of :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ExtSign sign symbol -> Set symbol

makeExtSign :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> sign -> ExtSign sign symbol

simply put all symbols into the symbol set

ext_ide :: (Ord symbol, Category sign morphism) => ExtSign sign symbol -> morphism

ext_empty_signature :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ExtSign sign symbol

checkExtSign :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> String -> ExtSign sign symbol -> Result ()

ext_signature_union :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ExtSign sign symbol -> ExtSign sign symbol -> Result (ExtSign sign symbol)

ext_is_subsig :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ExtSign sign symbol -> ExtSign sign symbol -> Bool

ext_final_union :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ExtSign sign symbol -> ExtSign sign symbol -> Result (ExtSign sign symbol)

ext_inclusion :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ExtSign sign symbol -> ExtSign sign symbol -> Result morphism

ext_generated_sign :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> Set symbol -> ExtSign sign symbol -> Result morphism

ext_cogenerated_sign :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> Set symbol -> ExtSign sign symbol -> Result morphism

ext_induced_from_morphism :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> EndoMap raw_symbol -> ExtSign sign symbol -> Result morphism

checkRawMap :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> EndoMap raw_symbol -> sign -> Result ()

checkRawSyms :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> [raw_symbol] -> Set symbol -> Result ()

ext_induced_from_to_morphism :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> EndoMap raw_symbol -> ExtSign sign symbol -> ExtSign sign symbol -> Result morphism