LogicList.hs revision 36b9e4cf34070e81d93765f129044abc5dbcf678
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{-# LANGUAGE CPP #-}
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederModule : $Header$
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederDescription : Assembles all the logics into a list, as a prerequisite
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian Maeder for the logic graph
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederMaintainer : till@informatik.uni-bremen.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (existential types)
44fb55f639914f4f531641f32dd4904f15c510a4Till MossakowskiAssembles all the logics into a list, as a prerequisite for the logic graph.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski The modules for the Grothendieck logic are logic graph indepdenent,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski and here is the logic graph that is used to instantiate these.
af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowski Since the logic graph depends on a large number of modules for the
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski individual logics, this separation of concerns (and possibility for
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski separate compilation) is quite useful.
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder J. A. Goguen, R. M. Burstall: Institutions:
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Abstract Model Theory for Specification and Programming,
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Journal of the Association for Computing Machinery 39, p. 95-146.
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder J. Meseguer: General logics. Logic Colloquium 87, p. 275-329, North Holland.
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Add many many logics.
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , addLogicName
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , defaultLogic
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , preLogicGraph
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport qualified Data.Map as Map
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport CASL.Logic_CASL -- also serves as default logic
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder#ifdef PROGRAMATICA
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder#ifdef CASLEXTENSIONS
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- no CASL extension, but omit them as non-essential
3a87487c048b275c56e502c4a933273788e8d0bbChristian Maeder#ifndef NOOWLLOGIC
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaederlogicList :: [AnyLogic]
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski , Logic HasCASL
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder , Logic Isabelle
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder , Logic SoftFOL
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski , Logic Propositional
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder#ifdef PROGRAMATICA
bba825b39570777866d560bfde3807731131097eKlaus Luettich , Logic Haskell
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder#ifdef CASLEXTENSIONS
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder , Logic CoCASL
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder , Logic ExtModal
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder , Logic Modal
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder , Logic cspCASL
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder , Logic traceCspCASL
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder , Logic failureCspCASL
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder , Logic CASL_DL
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder , Logic ConstraintCASL
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder , Logic RelScheme
83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu , Logic Temporal
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder , Logic Framework
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder , Logic Maude
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder , Logic Reduce
63324a97283728a30932828a612c7b0b0f687624Christian Maeder , Logic CommonLogic
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu#ifndef NOOWLLOGIC
f2c050360525df494e6115073b0edc4c443a847cMihai CodescuaddLogicName :: AnyLogic -> (String,AnyLogic)
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaederaddLogicName l@(Logic lid) = (language_name lid, l)
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaederdefaultLogic :: AnyLogic
f2c050360525df494e6115073b0edc4c443a847cMihai CodescudefaultLogic = Logic CASL
0e51a998b1b213654c7a9eca451562041971f100Till MossakowskipreLogicGraph :: LogicGraph
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaederpreLogicGraph =
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder emptyLogicGraph { logics = Map.fromList $ map addLogicName logicList }