hets -- a heterogenous Specification (CASL) tool setContentsIndex
Logic.Logic
Portability non-portable (various -fglasgow-exts extensions)
Stability provisional
Maintainer till@tzi.de
Description

Provides data structures for logics (with symbols). Logics are a type class with an identitiy type (usually interpreted by a singleton set) which serves to treat logics as data. All the functions in the type class take the identity as first argument in order to determine the logic.

For logic (co)morphisms see Comorphism.hs

References:

J. A. Goguen and R. M. Burstall Institutions: Abstract Model Theory for Specification and Programming JACM 39, p. 95--146, 1992 (general notion of logic - model theory only)

J. Meseguer General Logics Logic Colloquium 87, p. 275--329, North Holland, 1989 (general notion of logic - also proof theory; notion of logic representation, called map there)

T. Mossakowski: Specification in an arbitrary institution with symbols 14th WADT 1999, LNCS 1827, p. 252--270 (treatment of symbols and raw symbols, see also CASL semantics)

T. Mossakowski, B. Klin: Institution Independent Static Analysis for CASL 15h WADT 2001, LNCS 2267, p. 221-237, 2002. (what is needed for static anaylsis)

S. Autexier and T. Mossakowski Integrating HOLCASL into the Development Graph Manager MAYA FroCoS 2002, to appear (interface to provers)

Todo: ATerm, XML Weak amalgamability Metavars raw symbols are now symbols, symbols are now signature symbols provide both signature symbol set and symbol set of a signature

Synopsis
type Diagram object morphism = Graph object morphism
class Show lid => Language lid where
language_name :: lid -> String
coerce :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) => lid1 -> lid2 -> a -> Maybe b
rcoerce1 :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) => lid1 -> lid2 -> Pos -> a -> b -> Result b
rcoerce :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) => lid1 -> lid2 -> Pos -> a -> Result b
class (Language lid, Eq sign, Show sign, Eq morphism, Show morphism) => Category lid sign morphism | lid -> sign, lid -> morphism where
ide :: lid -> sign -> morphism
comp :: lid -> morphism -> morphism -> Maybe morphism
dom :: lid -> morphism -> sign
cod :: lid -> morphism -> sign
legal_obj :: lid -> sign -> Bool
legal_mor :: lid -> morphism -> Bool
type ParseFun a = Pos -> String -> (a, String, Pos)
class (Language lid, PrettyPrint basic_spec, PrettyPrint symb_items, Eq symb_items, PrettyPrint symb_map_items, Eq symb_map_items, ATermConvertible basic_spec, ATermConvertible symb_items, ATermConvertible symb_map_items) => Syntax lid basic_spec symb_items symb_map_items | lid -> basic_spec, lid -> symb_items, lid -> symb_map_items where
parse_basic_spec :: lid -> Maybe (ParseFun basic_spec)
parse_symb_items :: lid -> Maybe (ParseFun symb_items)
parse_symb_map_items :: lid -> Maybe (ParseFun symb_map_items)
fromShATerm_basic_spec :: lid -> ATermTable -> basic_spec
fromShATerm_symb_items :: lid -> ATermTable -> symb_items
fromShATerm_symb_map_items :: lid -> ATermTable -> symb_map_items
fromShATerm_symb_items_list :: lid -> ATermTable -> [symb_items]
fromShATerm_symb_map_items_list :: lid -> ATermTable -> [symb_map_items]
class (Category lid sign morphism, Eq sentence, Show sentence, PrettyPrint sign, PrettyPrint morphism, Ord symbol, Show symbol, PrettyPrint symbol, ATermConvertible sentence, ATermConvertible symbol, ATermConvertible sign, ATermConvertible morphism, ATermConvertible proof_tree) => Sentences lid sentence proof_tree sign morphism symbol | lid -> sentence, lid -> sign, lid -> morphism, lid -> symbol, lid -> proof_tree where
map_sen :: lid -> morphism -> sentence -> Result sentence
parse_sentence :: lid -> sign -> String -> Result sentence
sym_of :: lid -> sign -> Set symbol
symmap_of :: lid -> morphism -> EndoMap symbol
sym_name :: lid -> symbol -> Id
provers :: lid -> [Prover sentence proof_tree symbol]
cons_checkers :: lid -> [Cons_checker (TheoryMorphism sign sentence morphism)]
fromShATerm_sentence :: lid -> ATermTable -> sentence
fromShATerm_symbol :: lid -> ATermTable -> symbol
fromShATerm_sign :: lid -> ATermTable -> sign
fromShATerm_sign_list :: lid -> ATermTable -> [sign]
fromShATerm_morphism :: lid -> ATermTable -> morphism
fromShATerm_proof_tree :: lid -> ATermTable -> proof_tree
fromShATerm_l_sentence_list :: lid -> ATermTable -> [Named sentence]
fromShATerm_diagram :: lid -> ATermTable -> Diagram sign morphism
class (Syntax lid basic_spec symb_items symb_map_items, Sentences lid sentence proof_tree sign morphism symbol, Show raw_symbol, Eq raw_symbol, Ord raw_symbol, PrettyPrint raw_symbol) => StaticAnalysis lid basic_spec sentence proof_tree symb_items symb_map_items sign morphism symbol raw_symbol | lid -> basic_spec, lid -> sentence, lid -> symb_items, lid -> symb_map_items, lid -> proof_tree, lid -> sign, lid -> morphism, lid -> symbol, lid -> raw_symbol where
basic_analysis :: lid -> Maybe ((basic_spec, sign, GlobalAnnos) -> Result (basic_spec, sign, sign, [Named sentence]))
sign_to_basic_spec :: lid -> sign -> [Named sentence] -> basic_spec
stat_symb_map_items :: lid -> [symb_map_items] -> Result (EndoMap raw_symbol)
stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]
ensures_amalgamability :: lid -> (Diagram sign morphism, Node, sign, LEdge morphism, morphism) -> Result (Diagram sign morphism)
symbol_to_raw :: lid -> symbol -> raw_symbol
id_to_raw :: lid -> Id -> raw_symbol
matches :: lid -> symbol -> raw_symbol -> Bool
empty_signature :: lid -> sign
signature_union :: lid -> sign -> sign -> Result sign
morphism_union :: lid -> morphism -> morphism -> Result morphism
final_union :: lid -> sign -> sign -> Result sign
is_subsig :: lid -> sign -> sign -> Bool
inclusion :: lid -> sign -> sign -> Result morphism
generated_sign :: lid -> Set symbol -> sign -> Result morphism
cogenerated_sign :: lid -> Set symbol -> sign -> Result morphism
induced_from_morphism :: lid -> EndoMap raw_symbol -> sign -> Result morphism
induced_from_to_morphism :: lid -> EndoMap raw_symbol -> sign -> sign -> Result morphism
class (Eq l, Show l) => LatticeWithTop l where
meet :: l -> l -> l
join :: l -> l -> l
top :: l
(<<=) :: LatticeWithTop l => l -> l -> Bool
class (StaticAnalysis lid basic_spec sentence proof_tree symb_items symb_map_items sign morphism symbol raw_symbol, LatticeWithTop sublogics, ATermConvertible sublogics, Typeable sublogics, Typeable basic_spec, Typeable sentence, Typeable symb_items, Typeable symb_map_items, Typeable sign, Typeable morphism, Typeable symbol, Typeable raw_symbol, Typeable proof_tree) => Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree | lid -> sublogics, lid -> basic_spec, lid -> sentence, lid -> symb_items, lid -> symb_map_items, lid -> proof_tree, lid -> sign, lid -> morphism, lid -> symbol, lid -> raw_symbol where
data_logic :: lid -> Maybe AnyLogic
sublogic_names :: lid -> sublogics -> [String]
all_sublogics :: lid -> [sublogics]
is_in_basic_spec :: lid -> sublogics -> basic_spec -> Bool
is_in_sentence :: lid -> sublogics -> sentence -> Bool
is_in_symb_items :: lid -> sublogics -> symb_items -> Bool
is_in_symb_map_items :: lid -> sublogics -> symb_map_items -> Bool
is_in_sign :: lid -> sublogics -> sign -> Bool
is_in_morphism :: lid -> sublogics -> morphism -> Bool
is_in_symbol :: lid -> sublogics -> symbol -> Bool
min_sublogic_basic_spec :: lid -> basic_spec -> sublogics
min_sublogic_sentence :: lid -> sentence -> sublogics
min_sublogic_symb_items :: lid -> symb_items -> sublogics
min_sublogic_symb_map_items :: lid -> symb_map_items -> sublogics
min_sublogic_sign :: lid -> sign -> sublogics
min_sublogic_morphism :: lid -> morphism -> sublogics
min_sublogic_symbol :: lid -> symbol -> sublogics
proj_sublogic_basic_spec :: lid -> sublogics -> basic_spec -> basic_spec
proj_sublogic_symb_items :: lid -> sublogics -> symb_items -> Maybe symb_items
proj_sublogic_symb_map_items :: lid -> sublogics -> symb_map_items -> Maybe symb_map_items
proj_sublogic_sign :: lid -> sublogics -> sign -> sign
proj_sublogic_morphism :: lid -> sublogics -> morphism -> morphism
proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
proj_sublogic_symbol :: lid -> sublogics -> symbol -> Maybe symbol
fromShATerm_sublogics :: lid -> ATermTable -> sublogics
data AnyLogic = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => Logic lid
setTc :: TyCon
mapTc :: TyCon
Produced by Haddock version 0.6