Logic.hs revision 143fb54d0265592fab56951d09e7912bf0d8cf02
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder-- needs ghc -fglasgow-exts -fallow-overlapping-instances -package data
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder{- HetCATS/Logic.hs
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder $Id$
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Till Mossakowski, Christian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder Provides data structures for logics (with symbols). Logics are
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder a type class with an "identitiy" type (usually interpreted
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski by a singleton set) which serves to treat logics as
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski data. All the functions in the type class take the
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski identity as first argument in order to determine the logic.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski For logic representations see LogicRepr.hs
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder References:
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski J. A. Goguen and R. M. Burstall
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Institutions: Abstract Model Theory for Specification and
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Programming
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski JACM 39, p. 95--146, 1992
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (general notion of logic - model theory only)
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski
ae7058143db9e9993b5eff70bd6b7aede7cec658Till Mossakowski J. Meseguer
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski General Logics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic Colloquium 87, p. 275--329, North Holland, 1989
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (general notion of logic - also proof theory;
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski notion of logic representation, called map there)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski T. Mossakowski:
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder Specification in an arbitrary institution with symbols
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski 14th WADT 1999, LNCS 1827, p. 252--270
9e2e744c6b967c3f5f581acf01c13769b6769285Till Mossakowski (treatment of symbols and raw symbols, see also CASL semantics)
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski T. Mossakowski, B. Klin:
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder Institution Independent Static Analysis for CASL
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (what is needed for static anaylsis)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski S. Autexier and T. Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Integrating HOLCASL into the Development Graph Manager MAYA
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski FroCoS 2002, to appear
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (interface to provers)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Todo:
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ATerm, XML
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Weak amalgamability
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder Metavars
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-}
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskimodule Logic where
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskiimport Id
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowskiimport GlobalAnnotations
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskiimport Set
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowskiimport FiniteMap
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskiimport Graph
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskiimport Result
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski--import Parsec
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskiimport Prover -- for one half of class Sentences
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport PrettyPrint
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- for coercion used in Grothendieck.hs and Analysis modules
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowskiimport UnsafeCoerce
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski
9a36df4f63e0214bc0b4aef9b388c8d4e48632bbTill Mossakowski-- maps
9a36df4f63e0214bc0b4aef9b388c8d4e48632bbTill Mossakowski
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowskitype EndoMap a = FiniteMap a a
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski
62867c8459918ce0a96960093eb43d758b97a603Till Mossakowski-- diagrams are just graphs
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Diagram object morphism = Graph object morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- languages, define like "data CASL = CASL deriving Show"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass Show lid => Language lid where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name :: lid -> String
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski language_name i = show i
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski-- (a bit unsafe) coercion using the language name
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskicoerce :: (Language lid1, Language lid2) => lid1 -> lid2 -> a -> Maybe b
586af0e9490a14dd3075095692b584c652584875Till Mossakowskicoerce i1 i2 a = if language_name i1 == language_name i2 then
586af0e9490a14dd3075095692b584c652584875Till Mossakowski (Just $ unsafeCoerce a) else Nothing
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowskircoerce :: (Language lid1, Language lid2) => lid1 -> lid2 -> Pos-> a -> Result b
586af0e9490a14dd3075095692b584c652584875Till Mossakowskircoerce i1 i2 pos a =
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder maybeToResult pos
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ("Logic "++ language_name i1 ++ " expected, but "
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++ language_name i2++" found")
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (coerce i1 i2 a)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
586af0e9490a14dd3075095692b584c652584875Till Mossakowski-- Categories are given by a quotient,
586af0e9490a14dd3075095692b584c652584875Till Mossakowski-- i.e. we need equality
70066d44c2dc2f151e44dd0b98955c2dcd35b70bTill Mossakowski-- Should we allow arbitrary composition graphs and build paths?
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass (Language lid, Eq sign, Show sign, Eq morphism) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Category lid sign morphism | lid -> sign, lid -> morphism where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ide :: lid -> sign -> morphism
586af0e9490a14dd3075095692b584c652584875Till Mossakowski comp :: lid -> morphism -> morphism -> Maybe morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- diagrammatic order
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski dom, cod :: lid -> morphism -> sign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski legal_obj :: lid -> sign -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski legal_mor :: lid -> morphism -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- abstract syntax, parsing and printing
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
586af0e9490a14dd3075095692b584c652584875Till Mossakowskitype ParseFun a = FilePath -> Int -> Int -> String -> (a,String,Int,Int)
586af0e9490a14dd3075095692b584c652584875Till Mossakowski -- args: filename, line, column, input text
586af0e9490a14dd3075095692b584c652584875Till Mossakowski -- result: value, remaining text, line, column
586af0e9490a14dd3075095692b584c652584875Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass (Language lid, PrettyPrint basic_spec, Eq basic_spec,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski PrettyPrint symb_items, Eq symb_items,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski PrettyPrint symb_map_items, Eq symb_map_items) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Syntax lid basic_spec symb_items symb_map_items
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski | lid -> basic_spec, lid -> symb_items,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid -> symb_map_items
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder where
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder -- parsing
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski parse_basic_spec :: lid -> Maybe(ParseFun basic_spec)
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski parse_symb_items :: lid -> Maybe(ParseFun symb_items)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder parse_symb_map_items :: lid -> Maybe(ParseFun symb_map_items)
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass (Category lid sign morphism, Show sentence,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Ord symbol, Show symbol)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski => Sentences lid sentence sign morphism symbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | lid -> sentence, lid -> sign, lid -> morphism,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid -> symbol
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder where
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder -- sentence translation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sen :: lid -> morphism -> sentence -> Result sentence
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- parsing of sentences
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder parse_sentence :: lid -> sign -> String -> Result sentence
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- is a term parser needed as well?
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski provers :: lid -> [Prover sentence symbol]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cons_checkers :: lid -> [Cons_checker
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (TheoryMorphism sign sentence morphism)]
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- static analysis
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass ( Syntax lid basic_spec symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , Sentences lid sentence sign morphism symbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , Show raw_symbol, Eq raw_symbol)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski => StaticAnalysis lid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign morphism symbol raw_symbol
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder | lid -> basic_spec, lid -> sentence, lid -> symb_items,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid -> symb_map_items,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid -> sign, lid -> morphism, lid -> symbol, lid -> raw_symbol
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- static analysis of basic specifications and symbol maps
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_analysis :: lid ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Maybe((basic_spec, -- abstract syntax tree
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign, -- efficient table for env signature
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski GlobalAnnos) -> -- global annotations
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski Result (sign,sign,[(String,sentence)]))
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski -- the first output sign is the accumulated sign
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski -- the second output sign united with the input sing
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski -- should yield the first output sign
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski stat_symb_map_items ::
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski lid -> [symb_map_items] -> Result (EndoMap raw_symbol)
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- architectural sharing analysis for one morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ensures_amalgamability :: lid ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Diagram sign morphism, Node, sign, LEdge morphism, morphism) ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Result (Diagram sign morphism)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder -- do we need it also for sinks consisting of two morphisms?
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder -- symbols and symbol maps
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski symbol_to_raw :: lid -> symbol -> raw_symbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski id_to_raw :: lid -> Id -> raw_symbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sym_of :: lid -> sign -> Set symbol
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder symmap_of :: lid -> morphism -> EndoMap symbol
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder matches :: lid -> symbol -> raw_symbol -> Bool
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sym_name :: lid -> symbol -> Id
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski -- operations on signatures and morphisms
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski add_sign :: lid -> sign -> sign -> sign
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder empty_signature :: lid -> sign
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder signature_union :: lid -> sign -> sign -> Result sign
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder final_union :: lid -> sign -> sign -> Result sign
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder is_subsig :: lid -> sign -> sign -> Bool
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder generated_sign, cogenerated_sign ::
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder lid -> [raw_symbol] -> sign -> Result morphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder induced_from_morphism ::
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder lid -> EndoMap raw_symbol -> sign -> Result morphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder induced_from_to_morphism ::
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder lid -> EndoMap raw_symbol -> sign -> sign -> Result morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski extend_morphism ::
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder lid -> sign -> morphism -> sign -> sign -> Result morphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- sublogics
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass Ord l => LatticeWithTop l where
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski meet, join :: l -> l -> l
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski top :: l
-- logics
class (StaticAnalysis lid
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol,
LatticeWithTop sublogics) =>
Logic lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol
| lid -> sublogics, lid -> basic_spec, lid -> sentence, lid -> symb_items,
lid -> symb_map_items,
lid -> sign, lid -> morphism, lid ->symbol, lid -> raw_symbol
where
sublogic_names :: lid -> sublogics -> [String]
-- the first name is the principal name
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
{- class hierarchy:
Language
__________/
Category
| /
Sentences Syntax
\ /
StaticAnalysis (no sublogics)
\
\
Logic
-}