LogicList.hs revision 7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7f
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# LANGUAGE CPP #-}
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
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederMaintainer : till@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederPortability : non-portable (existential types)
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.
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder J. A. Goguen, R. M. Burstall: Institutions:
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder Abstract Model Theory for Specification and Programming,
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Journal of the Association for Computing Machinery 39, p. 95-146.
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder J. Meseguer: General logics. Logic Colloquium 87, p. 275-329, North Holland.
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder Add many many logics.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , addLogicName
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder , preLogicGraph
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Data.Map as Map
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport CASL.Logic_CASL -- also serves as default logic
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport Propositional.Logic_Propositional
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder#ifdef PROGRAMATICA
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder#ifdef CASLEXTENSIONS
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian Maeder-- no CASL extension, but omit them as non-essential
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder#ifndef NOOWLLOGIC
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder#ifdef RDFLOGIC
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederlogicList :: [AnyLogic]
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic HasCASL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic HolLight
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder , Logic Isabelle
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder , Logic SoftFOL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic Propositional
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic HolLight
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic FreeCAD
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder#ifdef PROGRAMATICA
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder , Logic Haskell
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder#ifdef CASLEXTENSIONS
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder , Logic OMDoc_PUN
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , Logic CoCASL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic ExtModal
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic Modal
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic Hybrid
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic Hybridize
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic cspCASL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic traceCspCASL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic failureCspCASL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic CASL_DL
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , Logic ConstraintCASL
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder , Logic RelScheme
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder , Logic Temporal
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder , Logic Framework
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder , Logic Maude
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder , Logic CommonLogic
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder#ifndef NOOWLLOGIC
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder#ifdef RDFLOGIC
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder , Logic CSMOF
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder ] ++ dynLogicList
ea5432ff6f61c64469b11d9352b23fef4ff152e8Christian MaederaddLogicName :: AnyLogic -> (String, AnyLogic)
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian MaederaddLogicName l@(Logic lid) = (language_name lid, l)
7d0ee72ee91ec305408688b969c43f07b9667c80Christian MaederdefaultLogic :: AnyLogic
7d0ee72ee91ec305408688b969c43f07b9667c80Christian MaederdefaultLogic = Logic CASL
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederpreLogicGraph :: LogicGraph
0e5b095a19790411e5352fa7cf57cb0388e70472Christian MaederpreLogicGraph =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder emptyLogicGraph { logics = Map.fromList $ map addLogicName logicList}