a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa{-# LANGUAGE CPP #-}

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa{- |

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaModule : $Header$

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaDescription : Assembles all the logics into a list, as a prerequisite

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa for the logic graph

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaCopyright : (c) Till Mossakowski and Uni Bremen 2003

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaLicense : GPLv2 or higher, see LICENSE.txt

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaMaintainer : till@informatik.uni-bremen.de

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaStability : provisional

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaPortability : non-portable (existential types)

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaAssembles all the logics into a list, as a prerequisite for the logic graph.

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa The modules for the Grothendieck logic are logic graph indepdenent,

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

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

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa individual logics, this separation of concerns (and possibility for

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa separate compilation) is quite useful.

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa

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

, preLogicGraph

) where

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

import QBF.Logic_QBF

import HolLight.Logic_HolLight

import CSL.Logic_CSL

import FreeCAD.Logic_FreeCAD

#ifdef PROGRAMATICA

import Haskell.Logic_Haskell

#endif

import Isabelle.Logic_Isabelle

import SoftFOL.Logic_SoftFOL

#ifdef CASLEXTENSIONS

import THF.Logic_THF

import Fpl.Logic_Fpl

import Adl.Logic_Adl

import Modal.Logic_Modal

import ExtModal.Logic_ExtModal

import CoCASL.Logic_CoCASL

import CspCASL.Logic_CspCASL

import COL.Logic_COL ()

import CASL_DL.Logic_CASL_DL

import ConstraintCASL.Logic_ConstraintCASL

import VSE.Logic_VSE

-- no CASL extension, but omit them as non-essential

import OMDoc.Logic_OMDoc

import RelationalScheme.Logic_Rel

import Temporal.Logic_Temporal

import DFOL.Logic_DFOL

import LF.Logic_LF

import Framework.Logic_Framework

import Maude.Logic_Maude

import CommonLogic.Logic_CommonLogic

#endif

#ifndef NOOWLLOGIC

import DMU.Logic_DMU

import OWL2.Logic_OWL2

#endif

#ifdef RDFLOGIC

import RDF.Logic_RDF

#endif

import Comorphisms.DynLogicList

logicList :: [AnyLogic]

logicList =

[ Logic CASL

, Logic HasCASL

, Logic HolLight

, Logic Isabelle

, Logic SoftFOL

, Logic Propositional

, Logic QBF

, Logic HolLight

, Logic FreeCAD

, Logic CSL

#ifdef PROGRAMATICA

, Logic Haskell

#endif

#ifdef CASLEXTENSIONS

, Logic OMDoc_PUN

, Logic THF

, Logic Fpl

, Logic Adl

, Logic CoCASL

, Logic ExtModal

, Logic Modal

, Logic cspCASL

, Logic traceCspCASL

, Logic failureCspCASL

, Logic CASL_DL

, Logic ConstraintCASL

, Logic VSE

, Logic RelScheme

, Logic Temporal

, Logic DFOL

, Logic LF

, Logic Framework

, Logic Maude

, Logic CommonLogic

#endif

#ifndef NOOWLLOGIC

, Logic DMU

, Logic OWL2

#endif

#ifdef RDFLOGIC

, Logic RDF

#endif

] ++ dynLogicList

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}