LogicList.hs revision b92e4eba198fcbffab302375b6c3527a8492bc66
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{-# OPTIONS -cpp #-}
ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Header$
ca010363454de207082dfaa4b753531ce2a34551Christian MaederDescription : Assembles all the logics into a list, as a prerequisite
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder for the logic graph
ca010363454de207082dfaa4b753531ce2a34551Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003
ca010363454de207082dfaa4b753531ce2a34551Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ca010363454de207082dfaa4b753531ce2a34551Christian MaederMaintainer : till@informatik.uni-bremen.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : provisional
ca010363454de207082dfaa4b753531ce2a34551Christian MaederPortability : non-portable (existential types)
ca010363454de207082dfaa4b753531ce2a34551Christian MaederAssembles all the logics into a list, as a prerequisite for the logic graph.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder The modules for the Grothendieck logic are logic graph indepdenent,
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder and here is the logic graph that is used to instantiate these.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder Since the logic graph depends on a large number of modules for the
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder individual logics, this separation of concerns (and possibility for
9379646a4fecb772e793a8875bb92723e854268cChristian Maeder separate compilation) is quite useful.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder J. A. Goguen, R. M. Burstall: Institutions:
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder Abstract Model Theory for Specification and Programming,
3ec187613707411408c677058155bc618f16dabbChristian Maeder Journal of the Association for Computing Machinery 39, p. 95-146.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder J. Meseguer: General logics. Logic Colloquium 87, p. 275-329, North Holland.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder Add many many logics.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder , addLogicName
51c8e05cd5ba40a3264ed3e486b34bc45b7a060aChristian Maeder , defaultLogic
b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maeder , lookupLogic_in_LG
51c8e05cd5ba40a3264ed3e486b34bc45b7a060aChristian Maederimport qualified Data.Map as Map
51c8e05cd5ba40a3264ed3e486b34bc45b7a060aChristian Maederimport CASL.Logic_CASL -- also serves as default logic
b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maeder#ifdef PROGRAMATICA
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder#ifdef CASLEXTENSIONS
9379646a4fecb772e793a8875bb92723e854268cChristian Maeder-- no CASL extension, but omit them as non-essential
ee0c5c1f995da3283814a2b7680e9f9876223900Christian Maeder#ifndef NOOWLLOGIC
ee0c5c1f995da3283814a2b7680e9f9876223900Christian MaederlogicList :: [AnyLogic]
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder , Logic HasCASL
ee0c5c1f995da3283814a2b7680e9f9876223900Christian Maeder , Logic Isabelle
ee0c5c1f995da3283814a2b7680e9f9876223900Christian Maeder , Logic SoftFOL
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder , Logic Propositional
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder#ifdef PROGRAMATICA
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder , Logic Haskell
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder#ifdef CASLEXTENSIONS
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder , Logic CoCASL
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder , Logic Modal
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder , Logic cspCASL
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder , Logic traceCspCASL
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder , Logic failureCspCASL
88d16ba9fcfb786c4e953f99982e3056ad2045ecChristian Maeder , Logic CASL_DL
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder , Logic ConstraintCASL
9379646a4fecb772e793a8875bb92723e854268cChristian Maeder , Logic RelScheme
b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maeder , Logic Temporal
b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maeder , Logic Maude
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder#ifndef NOOWLLOGIC
b5699d97a9e2b4496f98d624f4b0a537986651c3Christian MaederaddLogicName :: AnyLogic -> (String,AnyLogic)
ca010363454de207082dfaa4b753531ce2a34551Christian MaederaddLogicName l@(Logic lid) = (language_name lid, l)
ca010363454de207082dfaa4b753531ce2a34551Christian MaederdefaultLogic :: AnyLogic
ca010363454de207082dfaa4b753531ce2a34551Christian MaederdefaultLogic = Logic CASL
9379646a4fecb772e793a8875bb92723e854268cChristian MaederpreLogicGraph :: LogicGraph
9379646a4fecb772e793a8875bb92723e854268cChristian MaederpreLogicGraph =
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder emptyLogicGraph { logics = Map.fromList $ map addLogicName logicList }
9379646a4fecb772e793a8875bb92723e854268cChristian MaederlookupLogic_in_LG :: String -> String -> AnyLogic
b5699d97a9e2b4496f98d624f4b0a537986651c3Christian MaederlookupLogic_in_LG errorPrefix logname =
b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maeder propagateErrors $ lookupLogic errorPrefix logname preLogicGraph
b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maeder-- currently only used in ATC/Grothendieck.hs
9379646a4fecb772e793a8875bb92723e854268cChristian Maeder-- and indirectly in ATC/DevGraph.der.hs