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
|
type Diagram object morphism = Graph object morphism | | class Show lid => Language lid where | | | 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 | | | 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 | | | 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 | | | 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 | | | class (Eq l, Show l) => LatticeWithTop l where | | | (<<=) :: 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 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 |
|