fdbad18e66c0e293f94694458d47df305f050c71Christian Maeder{-# OPTIONS -cpp #-}

fdbad18e66c0e293f94694458d47df305f050c71Christian Maeder{- |

fdbad18e66c0e293f94694458d47df305f050c71Christian MaederModule : $Header$

fdbad18e66c0e293f94694458d47df305f050c71Christian MaederDescription : Assembles all the logics into a list, as a prerequisite for the logic graph

5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003

5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

b96b500ba4430269d97a08f07de87838278e9c5dChristian Maeder

b96b500ba4430269d97a08f07de87838278e9c5dChristian MaederMaintainer : till@informatik.uni-bremen.de

5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian MaederStability : provisional

5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian MaederPortability : non-portable (existential types)

5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian Maeder

5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian MaederAssembles all the logics into a list, as a prerequisite for the logic graph.

The modules for the Grothendieck logic are logic graph indepdenent,

and here is the logic graph that is used to instantiate these.

Since the logic graph depends on a large number of modules for the

individual logics, this separation of concerns (and possibility for

separate compilation) is quite useful.

References:

J. A. Goguen, R. M. Burstall: Institutions:

Abstract Model Theory for Specification and Programming,

Journal of the Association for Computing Machinery 39, p. 95-146.

J. Meseguer: General logics. Logic Colloquium 87, p. 275-329, North Holland.

Todo:

Add many many logics.

-}

module Comorphisms.LogicList

( logicList

, addLogicName

, defaultLogic

, lookupLogic_in_LG

) where

import Common.Result

import qualified Data.Map as Map

import Logic.Logic

import Logic.Grothendieck

import CASL.Logic_CASL -- also serves as default logic

import HasCASL.Logic_HasCASL

import Propositional.Logic_Propositional

#ifdef PROGRAMATICA

import Haskell.Logic_Haskell

#endif

import Isabelle.Logic_Isabelle

import SoftFOL.Logic_SoftFOL

#ifdef CASLEXTENSIONS

import Modal.Logic_Modal

import CoCASL.Logic_CoCASL

import CspCASL.Logic_CspCASL

import COL.Logic_COL ()

import OWL.Logic_OWL11

import CASL_DL.Logic_CASL_DL

import ConstraintCASL.Logic_ConstraintCASL

import DL.Logic_DL

import RelationalScheme.Logic_Rel

import VSE.Logic_VSE

#endif

logicList :: [AnyLogic]

logicList = [Logic CASL, Logic HasCASL,

#ifdef PROGRAMATICA

Logic Haskell,

#endif

#ifdef CASLEXTENSIONS

Logic CoCASL, Logic Modal, Logic CspCASL, -- Logic COL,

Logic OWL11, Logic CASL_DL, Logic ConstraintCASL, Logic DL,

Logic RelScheme, Logic VSE,

#endif

Logic Isabelle,Logic SoftFOL,

Logic Propositional]

addLogicName :: AnyLogic -> (String,AnyLogic)

addLogicName l@(Logic lid) = (language_name lid, l)

defaultLogic :: AnyLogic

defaultLogic = Logic CASL

preLogicGraph :: LogicGraph

preLogicGraph =

emptyLogicGraph { logics = Map.fromList $ map addLogicName logicList }

lookupLogic_in_LG :: String -> String -> AnyLogic

lookupLogic_in_LG errorPrefix logname =

propagateErrors $ lookupLogic errorPrefix logname preLogicGraph

-- currently only used in ATC/Grothendieck.hs

-- and indirectly in ATC/DevGraph.der.hs