LogicList.hs revision 88c66e48620750c42b94db9feb01b42ae23dba97
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{- |
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maeder
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Module : $Header$
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Copyright : (c) Till Mossakowski and Uni Bremen 2003
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Maintainer : hets@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Stability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder Portability : non-portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder Assembles all the logics into a list, as a prerequisite for the logic graph.
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder The modules for the Grothendieck logic are logic graph indepdenent,
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder and here is the logic graph that is used to instantiate these.
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder Since the logic graph depends on a large number of modules for the
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder individual logics, this separation of concerns (and possibility for
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder separate compilation) is quite useful.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder References:
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder J. A. Goguen, R. M. Burstall: Institutions:
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Abstract Model Theory for Specification and Programming,
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder Journal of the Association for Computing Machinery 39, p. 95-146.
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder J. Meseguer: General logics. Logic Colloquium 87, p. 275-329, North Holland.
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder Todo:
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Add many many logics.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder
74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maeder-}
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maedermodule Comorphisms.LogicList
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederwhere
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederimport Common.Result
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Logic.Logic
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maederimport Logic.Grothendieck
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport CASL.Logic_CASL -- also serves as default logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport HasCASL.Logic_HasCASL
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maederimport Haskell.Logic_Haskell
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport CspCASL.Logic_CspCASL
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport Isabelle.Logic_Isabelle
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maederimport Modal.Logic_Modal
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maederimport CoCASL.Logic_CoCASL
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maederimport qualified Common.Lib.Map as Map
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maederimport CASL.ATC_CASL
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaederlogicList :: [AnyLogic]
c3053d57f642ca507cdf79512e604437c4546cb9Christian MaederlogicList = [Logic CASL, Logic HasCASL, Logic Haskell,
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder Logic CoCASL, Logic Modal, Logic CspCASL, Logic Isabelle]
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederaddLogicName :: AnyLogic -> (String,AnyLogic)
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian MaederaddLogicName l@(Logic lid) = (language_name lid, l)
05a62e84edac8c64de04f8349dee418598d216b9Christian Maeder
1cd4f6541984962658add5cfaa9f28a93879881bChristian MaederdefaultLogic :: AnyLogic
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaederdefaultLogic = Logic CASL
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederpreLogicGraph :: LogicGraph
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederpreLogicGraph =
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder LogicGraph {
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder logics = Map.fromList $ map addLogicName logicList,
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder comorphisms = Map.empty,
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder inclusions = Map.empty
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder }
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder
624e6701e0deb7ac6c03c0cba0190fbc5033cf93Ewaryst SchulzlookupLogic_in_LG :: String -> String -> AnyLogic
8cacad2a09782249243b80985f28e9387019fe40Christian MaederlookupLogic_in_LG errorPrefix logname =
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder lookupLogic errorPrefix logname preLogicGraph
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder