hets/Comorphisms/LogicList.hs

	LogicList.hs revision 1f9274bb2aa44ea236327814dce99946be52e348
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# LANGUAGE CPP #-}
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maeder{- |
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederModule      :  $Header$
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederDescription :  Assembles all the logics into a list, as a prerequisite
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder  for the logic graph
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright   :  (c)  Till Mossakowski and Uni Bremen 2003
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense     :  GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederMaintainer  :  till@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability   :  provisional
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederPortability :  non-portable (existential types)
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian MaederAssembles all the logics into a list, as a prerequisite for the logic graph.
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder   The modules for the Grothendieck logic are logic graph indepdenent,
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder   and here is the logic graph that is used to instantiate these.
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder   Since the logic graph depends on a large number of modules for the
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder   individual logics, this separation of concerns (and possibility for
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder   separate compilation) is quite useful.
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder   References:
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder   J. A. Goguen, R. M. Burstall: Institutions:
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder     Abstract Model Theory for Specification and Programming,
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder     Journal of the Association for Computing Machinery 39, p. 95-146.
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder   J. Meseguer: General logics. Logic Colloquium 87, p. 275-329, North Holland.
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder   Todo:
74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maeder   Add many many logics.
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-}
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maedermodule Comorphisms.LogicList
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder    ( logicList
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder    , addLogicName
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder    , defaultLogic
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder    , preLogicGraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder    , dolLogicNames
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder    ) where
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport qualified Data.Map as Map
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport Logic.Logic
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maederimport Logic.Grothendieck
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maederimport CASL.Logic_CASL  -- also serves as default logic
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maederimport HasCASL.Logic_HasCASL
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maederimport Propositional.Logic_Propositional
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport QBF.Logic_QBF
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport HolLight.Logic_HolLight
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maederimport CSL.Logic_CSL
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maederimport FreeCAD.Logic_FreeCAD
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder#ifdef PROGRAMATICA
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederimport Haskell.Logic_Haskell
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder#endif
05a62e84edac8c64de04f8349dee418598d216b9Christian Maederimport Isabelle.Logic_Isabelle
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maederimport SoftFOL.Logic_SoftFOL
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder#ifdef CASLEXTENSIONS
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport THF.Logic_THF
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Fpl.Logic_Fpl
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Adl.Logic_Adl
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Modal.Logic_Modal
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport ExtModal.Logic_ExtModal
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport CoCASL.Logic_CoCASL
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederimport CspCASL.Logic_CspCASL
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maederimport COL.Logic_COL ()
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maederimport CASL_DL.Logic_CASL_DL
624e6701e0deb7ac6c03c0cba0190fbc5033cf93Ewaryst Schulzimport ConstraintCASL.Logic_ConstraintCASL
8cacad2a09782249243b80985f28e9387019fe40Christian Maederimport VSE.Logic_VSE
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- no CASL extension, but omit them as non-essential
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maederimport OMDoc.Logic_OMDoc
363939beade943a02b31004cea09dec34fa8a6d9Christian Maederimport RelationalScheme.Logic_Rel
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maederimport Temporal.Logic_Temporal
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettichimport DFOL.Logic_DFOL
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maederimport LF.Logic_LF
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maederimport Framework.Logic_Framework
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maederimport Maude.Logic_Maude
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederimport CommonLogic.Logic_CommonLogic
498aa48bdb931ab50990d3b74318a5db2312186cChristian Maeder#endif
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder#ifndef NOOWLLOGIC
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederimport DMU.Logic_DMU
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederimport OWL2.Logic_OWL2
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder#endif
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maeder#ifdef RDFLOGIC
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederimport RDF.Logic_RDF
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder#endif
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Comorphisms.DynLogicList
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederlogicList :: [AnyLogic]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederlogicList =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder  [ Logic CASL
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder  , Logic HasCASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic HolLight
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic Isabelle
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic SoftFOL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder  , Logic Propositional
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder  , Logic QBF
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder  , Logic HolLight
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic FreeCAD
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder  , Logic CSL
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder#ifdef PROGRAMATICA
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder  , Logic Haskell
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder#endif
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder#ifdef CASLEXTENSIONS
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder  , Logic OMDoc_PUN
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder  , Logic THF
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder  , Logic Fpl
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder  , Logic Adl
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maeder  , Logic CoCASL
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maeder  , Logic ExtModal
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder  , Logic Modal
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic cspCASL
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder  , Logic traceCspCASL
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder  , Logic failureCspCASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic CASL_DL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic ConstraintCASL
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder  , Logic VSE
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder  , Logic RelScheme
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic Temporal
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic DFOL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic LF
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic Framework
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder  , Logic Maude
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder  , Logic CommonLogic
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder#endif
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder#ifndef NOOWLLOGIC
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder  , Logic DMU
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder  , Logic OWL2
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder#endif
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder#ifdef RDFLOGIC
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder  , Logic RDF
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder#endif
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder  ] ++ dynLogicList
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichaddLogicName :: AnyLogic -> (String, AnyLogic)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederaddLogicName l@(Logic lid) = (language_name lid, l)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederdefaultLogic :: AnyLogic
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederdefaultLogic = Logic CASL
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaederpreLogicGraph :: LogicGraph
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaederpreLogicGraph =
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder  emptyLogicGraph { logics = Map.fromList $ map addLogicName logicList}
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- quick fix for support of LOGIC-REF in DOL
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- only used in Comorphisms.LogicGraph.logicGraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederdolLogicNames :: [(String, AnyLogic)]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederdolLogicNames =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder  [ ("http://purl.net/dol/logic/CommonLogic", Logic CommonLogic)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder  , ("http://purl.net/dol/logic/OWL", Logic OWL2)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder  ]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder