Logic.hs revision 89d5b892ca2fd8eb8f72dba097759a6d54f0a78c
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder-- needs ghc -fglasgow-exts -fallow-overlapping-instances -package data
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder Till Mossakowski, Christian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder Provides data structures for logics (with symbols). Logics are
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder a type class with an "identitiy" type (usually interpreted
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder by a singleton set) which serves to treat logics as
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder data. All the functions in the type class take the
44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski identity as first argument in order to determine the logic.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski For logic representations see LogicRepr.hs
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder J. A. Goguen and R. M. Burstall
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Institutions: Abstract Model Theory for Specification and
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder JACM 39, p. 95--146, 1992
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (general notion of logic - model theory only)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder General Logics
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Logic Colloquium 87, p. 275--329, North Holland, 1989
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (general notion of logic - also proof theory;
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder notion of logic representation, called map there)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder T. Mossakowski:
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Specification in an arbitrary institution with symbols
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder 14th WADT 1999, LNCS 1827, p. 252--270
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (treatment of symbols and raw symbols, see also CASL semantics)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder T. Mossakowski, B. Klin:
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Institution Independent Static Analysis for CASL
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (what is needed for static anaylsis)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder S. Autexier and T. Mossakowski
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Integrating HOLCASL into the Development Graph Manager MAYA
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski FroCoS 2002, to appear
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (interface to provers)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder Weak amalgamability
63324a97283728a30932828a612c7b0b0f687624Christian Maedermodule Logic where
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maederimport GlobalAnnotations
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport FiniteMap
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder--import Parsec
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Prover -- for one half of class Sentences
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport PrettyPrint
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- for coercion used in Grothendieck.hs and Analysis modules
3a87487c048b275c56e502c4a933273788e8d0bbChristian Maederimport UnsafeCoerce
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskitype EndoMap a = FiniteMap a a
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski-- diagrams are just graphs
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowskidata Diagram object morphism = Graph object morphism
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski-- languages, define like "data CASL = CASL deriving Show"
bba825b39570777866d560bfde3807731131097eKlaus Luettichclass Show id => Language id where
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder language_name :: id -> String
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name i = show i
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- (a bit unsafe) coercion using the language name
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowskicoerce :: (Language id1, Language id2) => id1 -> id2 -> a -> Maybe b
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maedercoerce i1 i2 a = if language_name i1 == language_name i2 then
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder (Just $ unsafeCoerce a) else Nothing
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- Categories are given by a quotient,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- i.e. we need equality
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- Should we allow arbitrary composition graphs and build paths?
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maederclass (Language id, Eq sign, Show sign, Eq morphism) =>
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder Category id sign morphism | id -> sign, id -> morphism where
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder ide :: id -> sign -> morphism
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder o :: id -> morphism -> morphism -> Maybe morphism
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder dom, cod :: id -> morphism -> sign
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder legal_obj :: id -> sign -> Bool
63324a97283728a30932828a612c7b0b0f687624Christian Maeder legal_mor :: id -> morphism -> Bool
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- abstract syntax, parsing and printing
b4e202184f6977662c439c82866fe93f06cebe41Christian Maedertype ParseFun a = FilePath -> Int -> Int -> String -> (a,String,Int,Int)
830e14495f9cac8e154dd4813dae010166f33d09Mihai Codescu -- args: filename, line, column, input text
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu -- result: value, remaining text, line, column
f2c050360525df494e6115073b0edc4c443a847cMihai Codescuclass (Language id, PrettyPrint basic_spec, Eq basic_spec,
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder PrettyPrint symb_items, Eq symb_items,
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu PrettyPrint symb_map_items, Eq symb_map_items) =>
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder Syntax id basic_spec symb_items symb_map_items
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu | id -> basic_spec, id -> symb_items,
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski id -> symb_map_items
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder parse_basic_spec :: id -> Maybe(ParseFun basic_spec)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski parse_symb_items :: id -> Maybe(ParseFun symb_items)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder parse_symb_map_items :: id -> Maybe(ParseFun symb_map_items)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederclass (Category id sign morphism, Show sentence,
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Ord symbol, Show symbol)
da955132262baab309a50fdffe228c9efe68251dCui Jian => Sentences id sentence sign morphism symbol
da955132262baab309a50fdffe228c9efe68251dCui Jian | id -> sentence, id -> sign, id -> morphism,
bba825b39570777866d560bfde3807731131097eKlaus Luettich -- sentence translation
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder map_sen :: id -> morphism -> sentence -> Result sentence
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder -- parsing of sentences
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder parse_sentence :: id -> sign -> String -> Result sentence
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -- is a term parser needed as well?
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder provers :: id -> [Prover sentence symbol]
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder cons_checkers :: id -> [Cons_checker
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (TheoryMorphism sign sentence morphism)]
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- static analysis
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederclass ( Syntax id basic_spec symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , Sentences id sentence sign morphism symbol
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , Show raw_symbol, Eq raw_symbol)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder => StaticAnalysis id
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec sentence symb_items symb_map_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign morphism symbol raw_symbol
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | id -> basic_spec, id -> sentence, id -> symb_items,
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder id -> symb_map_items,
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder id -> sign, id -> morphism, id -> symbol, id -> raw_symbol
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder -- static analysis of basic specifications and symbol maps
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_analysis :: id ->
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Maybe((basic_spec, -- abstract syntax tree
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign, -- efficient table for env signature
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder GlobalAnnos) -> -- global annotations
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Result (sign,sign,[(String,sentence)]))
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -- the first output sign is the accumulated sign
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -- the second output sign united with the input sing
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -- should yield the first output sign
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder stat_symb_map_items ::
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder id -> symb_map_items -> Result (EndoMap raw_symbol)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder stat_symb_items :: id -> symb_items -> Result [raw_symbol]
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -- architectural sharing analysis for one morphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder ensures_amalgamability :: id ->
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (Diagram sign morphism, Node, sign, LEdge morphism, morphism) ->
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Result (Diagram sign morphism)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -- do we need it also for sinks consisting of two morphisms?
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -- symbols and symbol maps
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder symbol_to_raw :: id -> symbol -> raw_symbol
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder id_to_raw :: id -> Id -> raw_symbol
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sym_of :: id -> sign -> Set symbol
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder symmap_of :: id -> morphism -> EndoMap symbol
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder matches :: id -> symbol -> raw_symbol -> Bool
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sym_name :: id -> symbol -> Id
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -- operations on signatures and morphisms
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder add_sign :: id -> sign -> sign -> sign
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder empty_signature :: id -> sign
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder signature_union :: id -> sign -> sign -> Result sign
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder final_union :: id -> sign -> sign -> Result sign
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder is_subsig :: id -> sign -> sign -> Bool
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder generated_sign, cogenerated_sign ::
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder id -> [raw_symbol] -> sign -> Result morphism
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder induced_from_morphism ::
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder id -> EndoMap raw_symbol -> sign -> Result morphism
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder induced_from_to_morphism ::
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder id -> EndoMap raw_symbol -> sign -> sign -> Result morphism
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder extend_morphism ::
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder id -> sign -> morphism -> sign -> sign -> Result morphism
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederclass Ord l => LatticeWithTop l where
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder meet, join :: l -> l -> l
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maederclass (StaticAnalysis id
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder basic_spec sentence symb_items symb_map_items
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder sign morphism symbol raw_symbol,
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder LatticeWithTop sublogics) =>
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder Logic id sublogics
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder basic_spec sentence symb_items symb_map_items
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sign morphism symbol raw_symbol
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder | id -> sublogics, id -> basic_spec, id -> sentence, id -> symb_items,
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder id -> symb_map_items,
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder id -> sign, id -> morphism, id ->symbol, id -> raw_symbol
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sublogic_names :: id -> sublogics -> [String]
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -- the first name is the principal name
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder all_sublogics :: id -> [sublogics]
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder is_in_basic_spec :: id -> sublogics -> basic_spec -> Bool
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder is_in_sentence :: id -> sublogics -> sentence -> Bool
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder is_in_symb_items :: id -> sublogics -> symb_items -> Bool
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder is_in_symb_map_items :: id -> sublogics -> symb_map_items -> Bool
a129422b14eea673dc481d2553cec108e35e72efChristian Maeder is_in_sign :: id -> sublogics -> sign -> Bool
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder is_in_morphism :: id -> sublogics -> morphism -> Bool
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder is_in_symbol :: id -> sublogics -> symbol -> Bool
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder min_sublogic_basic_spec :: id -> basic_spec -> sublogics
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder min_sublogic_sentence :: id -> sentence -> sublogics
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder min_sublogic_symb_items :: id -> symb_items -> sublogics
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich min_sublogic_symb_map_items :: id -> symb_map_items -> sublogics
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich min_sublogic_sign :: id -> sign -> sublogics
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich min_sublogic_morphism :: id -> morphism -> sublogics
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich min_sublogic_symbol :: id -> symbol -> sublogics
6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu proj_sublogic_basic_spec :: id -> sublogics -> basic_spec -> basic_spec
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder proj_sublogic_symb_items :: id -> sublogics -> symb_items -> Maybe symb_items
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder proj_sublogic_symb_map_items :: id -> sublogics -> symb_map_items -> Maybe symb_map_items
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder proj_sublogic_sign :: id -> sublogics -> sign -> sign
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder proj_sublogic_morphism :: id -> sublogics -> morphism -> morphism
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich proj_sublogic_epsilon :: id -> sublogics -> sign -> morphism
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich proj_sublogic_symbol :: id -> sublogics -> symbol -> Maybe symbol
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich{- class hierarchy:
da955132262baab309a50fdffe228c9efe68251dCui Jian __________/
da955132262baab309a50fdffe228c9efe68251dCui Jian Sentences Syntax
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder StaticAnalysis (no sublogics)