640b2adac05bb7f5e9fba064434c91852c3a72e6nd{- |

8e34905974b7a442a55adac3b3fdb196c389e807takashi

640b2adac05bb7f5e9fba064434c91852c3a72e6nd Module : $Header$

640b2adac05bb7f5e9fba064434c91852c3a72e6nd Copyright : (c) Till Mossakowski and Uni Bremen 2003

8e34905974b7a442a55adac3b3fdb196c389e807takashi Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6nd Maintainer : hets@tzi.de

6e89d4f6c259afc94f8806c74a33a8fe81392499sf Stability : provisional

640b2adac05bb7f5e9fba064434c91852c3a72e6nd Portability : non-portable

8e34905974b7a442a55adac3b3fdb196c389e807takashi

8e34905974b7a442a55adac3b3fdb196c389e807takashi Assembles all the logics and comorphisms into a graph.

640b2adac05bb7f5e9fba064434c91852c3a72e6nd The modules for the Grothendieck logic are logic graph indepdenent,

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

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

8e34905974b7a442a55adac3b3fdb196c389e807takashi individual logics, this separation of concerns (and possibility for

8e34905974b7a442a55adac3b3fdb196c389e807takashi separate compilation) is quite useful.

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6nd References:

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6nd The FLIRTS home page: <http://www.tzi.de/flirts>

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6nd T. Mossakowski:

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Relating CASL with Other Specification Languages:

8e34905974b7a442a55adac3b3fdb196c389e807takashi the Institution Level

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

ef685e00a47967e27d89709461728a229d762172nd

ef685e00a47967e27d89709461728a229d762172nd Todo:

ef685e00a47967e27d89709461728a229d762172nd Add many many logics and comorphisms.

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

6e89d4f6c259afc94f8806c74a33a8fe81392499sf-}

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

51853aa2ebfdf9903a094467e1d02099f143639daaronmodule Comorphisms.LogicGraph (defaultLogic, logicList, logicGraph,

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive lookupLogic_in_LG, lookupComorphism_in_LG)

51853aa2ebfdf9903a094467e1d02099f143639daaronwhere

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.Result

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Logic.Logic

51853aa2ebfdf9903a094467e1d02099f143639daaronimport Logic.Comorphism

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Logic.Grothendieck

51853aa2ebfdf9903a094467e1d02099f143639daaronimport Comorphisms.CASL2PCFOL

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Comorphisms.PCFOL2FOL

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Comorphisms.CASL2HasCASL

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Comorphisms.HasCASL2Haskell

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Comorphisms.HasCASL2HasCASL

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Comorphisms.CASL2IsabelleHOL

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Comorphisms.CoCASL2IsabelleHOL

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Comorphisms.CASL2Modal

8e34905974b7a442a55adac3b3fdb196c389e807takashiimport Comorphisms.Modal2CASL

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Comorphisms.CASL2CoCASL

ef685e00a47967e27d89709461728a229d762172ndimport Comorphisms.HasCASL2IsabelleHOL

ef685e00a47967e27d89709461728a229d762172ndimport qualified Common.Lib.Map as Map

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

6e89d4f6c259afc94f8806c74a33a8fe81392499sf-- This needs to be seperated for utils/InlineAxioms/InlineAxioms.hs

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58sliveimport Comorphisms.LogicList

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58sliveaddComorphismName :: AnyComorphism -> (String,AnyComorphism)

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

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

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveaddInclusionNames c@(Comorphism cid) =

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive ((language_name $ sourceLogic cid,

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive language_name $ targetLogic cid),

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive c)

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveinclusionList :: [AnyComorphism]

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveinclusionList = [Comorphism CASL2HasCASL, Comorphism HasCASL2HasCASL,

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Comorphism HasCASL2Haskell,

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Comorphism CASL2IsabelleHOL,

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Comorphism CASL2Modal,

069aec3ea15c5ad699f98f50091aad653b1c6021rbowen Comorphism Modal2CASL,

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Comorphism CASL2CoCASL, Comorphism CoCASL2IsabelleHOL,

17ca00f92106c825382359ebf0a754f8df21e316rbowen Comorphism HasCASL2IsabelleHOL]

069aec3ea15c5ad699f98f50091aad653b1c6021rbowen

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivecomorphismList :: [AnyComorphism]

6e89d4f6c259afc94f8806c74a33a8fe81392499sfcomorphismList = inclusionList ++ [Comorphism CASL2PCFOL, Comorphism PCFOL2FOL]

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

17ca00f92106c825382359ebf0a754f8df21e316rbowenlogicGraph :: LogicGraph

069aec3ea15c5ad699f98f50091aad653b1c6021rbowenlogicGraph =

069aec3ea15c5ad699f98f50091aad653b1c6021rbowen LogicGraph {

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive logics = Map.fromList $ map addLogicName logicList,

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive comorphisms = Map.fromList $ map addComorphismName comorphismList,

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive inclusions = Map.fromList $ map addInclusionNames inclusionList

17ca00f92106c825382359ebf0a754f8df21e316rbowen }

17ca00f92106c825382359ebf0a754f8df21e316rbowen

17ca00f92106c825382359ebf0a754f8df21e316rbowenlookupComorphism_in_LG :: String -> Result AnyComorphism

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivelookupComorphism_in_LG coname =

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive lookupComorphism coname logicGraph

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive