LogicList.hs revision 81f49ee02aaa3bc870401f8883bf52742eb3ea7a
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# LANGUAGE CPP #-}
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
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
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder#ifdef CASLEXTENSIONS
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder-- no CASL extension, but omit them as non-essential
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder#ifndef NOOWLLOGIC
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder#ifdef RDFLOGIC
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian MaederlogicList :: [AnyLogic]
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic HasCASL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic HolLight
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic Isabelle
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic SoftFOL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic Propositional
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder , Logic HolLight
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic FreeCAD
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder#ifdef PROGRAMATICA
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic Haskell
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder#ifdef CASLEXTENSIONS
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder , Logic OMDoc_PUN
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder , Logic CoCASL
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder , Logic ExtModal
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic Modal
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , Logic Hybrid
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic Hybridize
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic cspCASL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic traceCspCASL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic failureCspCASL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic CASL_DL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , Logic ConstraintCASL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Logic RelScheme
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , Logic Temporal
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder , Logic Framework
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder , Logic Maude
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder , Logic CommonLogic
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder#ifndef NOOWLLOGIC
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder#ifdef RDFLOGIC
8d178ae08a52d61379e6b8074f61646499bc88bbChristian Maeder ] ++ dynLogicList
6cd33d6101fb1b93baa6d86fac158af18a115108Christian MaederaddLogicName :: AnyLogic -> (String, AnyLogic)
6cd33d6101fb1b93baa6d86fac158af18a115108Christian MaederaddLogicName l@(Logic lid) = (language_name lid, l)
6cd33d6101fb1b93baa6d86fac158af18a115108Christian MaederdefaultLogic :: AnyLogic
6cd33d6101fb1b93baa6d86fac158af18a115108Christian MaederdefaultLogic = Logic CASL
ea5432ff6f61c64469b11d9352b23fef4ff152e8Christian MaederpreLogicGraph :: LogicGraph
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian MaederpreLogicGraph =
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder emptyLogicGraph { logics = Map.fromList $ map addLogicName logicList}