649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa{- |

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa Module : $Header$

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa Copyright : (c) Till Mossakowski and Uni Bremen 2003

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa Maintainer : hets@tzi.de

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa Stability : provisional

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa Portability : non-portable

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa Assembles all the logics and representations into a graph.

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa The modules for the Grothendieck logic are logic graph indepdenent,

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

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

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

separate compilation) is quite useful.

References:

T. Mossakowski:

Relating CASL with Other Specification Languages:

the Institution Level

Theoretical Computer Science 286, p. 367-475, 2002.

Todo:

Add many many logics and comorphisms.

-}

module Comorphisms.LogicGraph

where

import Logic.Logic

import Logic.Comorphism

import Logic.Grothendieck

import CASL.Logic_CASL -- also serves as default logic

import HasCASL.Logic_HasCASL

import Haskell.Logic_Haskell

import CspCASL.Logic_CspCASL

import Comorphisms.CASL2HasCASL

import qualified Common.Lib.Map as Map

import CASL.ATC_CASL

logicList :: [AnyLogic]

logicList = [Logic CASL, Logic HasCASL, Logic Haskell, Logic CspCASL]

inclusionList :: [AnyComorphism]

inclusionList = [Comorphism CASL2HasCASL]

comorphismList :: [AnyComorphism]

comorphismList = inclusionList ++ []

addLogicName :: AnyLogic -> (String,AnyLogic)

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

addComorphismName :: AnyComorphism -> (String,AnyComorphism)

addComorphismName c@(Comorphism cid) = (language_name cid, c)

addInclusionNames :: AnyComorphism -> ((String,String),AnyComorphism)

addInclusionNames c@(Comorphism cid) =

((language_name $ sourceLogic cid,

language_name $ targetLogic cid),

c)

logicGraph :: LogicGraph

logicGraph =

LogicGraph {

logics = Map.fromList $ map addLogicName logicList,

comorphisms = Map.fromList $ map addComorphismName comorphismList,

inclusions = Map.fromList $ map addInclusionNames inclusionList

}

defaultLogic :: AnyLogic

defaultLogic = Logic CASL

lookupLogic_in_LG :: String -> String -> AnyLogic

lookupLogic_in_LG errorPrefix logname =

lookupLogic errorPrefix (logname) logicGraph

lookupComorphism_in_LG :: String -> String -> AnyComorphism

lookupComorphism_in_LG error_prefix coname =

lookupComorphism error_prefix coname logicGraph