277c685b1429c51f92b006f38aca4b89e0f4f2fdChristian Maeder{- |

277c685b1429c51f92b006f38aca4b89e0f4f2fdChristian MaederModule : $Header$

277c685b1429c51f92b006f38aca4b89e0f4f2fdChristian MaederCopyright : (c) Markus Roggenbach, Till Mossakowski and Uni Bremen 2003

277c685b1429c51f92b006f38aca4b89e0f4f2fdChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

277c685b1429c51f92b006f38aca4b89e0f4f2fdChristian Maeder

277c685b1429c51f92b006f38aca4b89e0f4f2fdChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk

277c685b1429c51f92b006f38aca4b89e0f4f2fdChristian MaederStability : experimental

8cd8515a95c02d0701aa8a52d3dba93b96b8f875Christian MaederPortability : non-portable(import Logic.Logic)

8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maeder

2a776f7803cf5250668849ab0af9d378dfefd2f3Christian MaederHere is the place where the class Logic is instantiated for CspCASL.

8cd8515a95c02d0701aa8a52d3dba93b96b8f875Christian Maeder Also the instances for Syntax an Category.

8cd8515a95c02d0701aa8a52d3dba93b96b8f875Christian Maeder-}

2a776f7803cf5250668849ab0af9d378dfefd2f3Christian Maeder{-

8cd8515a95c02d0701aa8a52d3dba93b96b8f875Christian Maeder todo:

8cd8515a95c02d0701aa8a52d3dba93b96b8f875Christian Maeder - writing real functions

8cd8515a95c02d0701aa8a52d3dba93b96b8f875Christian Maeder - Modul Sign.hs mit CSP-CASL-Signaturen und Morphismen, basiernd auf CASL.Sign

dda27ed86257e0480f862b841259819f59d4724ecmaeder CSP-CASL-Signatur = (CASL-Sig,Menge von Kanalnamen)

dda27ed86257e0480f862b841259819f59d4724ecmaeder CSP-CASL-Morphismus = (CASL-Morphismus, Kanalnamenabbildung)

dda27ed86257e0480f862b841259819f59d4724ecmaeder oder nur CASL-Morphismus

e938e50e25d4a2365fab789af709590d3d6ce89dcmaeder SYMB_ITEMS SYMB_MAP_ITEMS: erstmal von CASL (d.h. nur CASL-Morphismus)

516ca24f64f1b6e45577ee44dced94e7e358336bChristian Maeder - instance Sentences

8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maeder S�tze = entweder CASL-S�tze oder CSP-CASL-S�tze

277c685b1429c51f92b006f38aca4b89e0f4f2fdChristian Maeder Rest soweit wie m�glich von CASL �bernehmen

- statische Analyse (gem�� Typ in Logic.Logic) schreiben

und unten f�r basic_analysis einh�ngen

K�r:

- Teillogiken (instance SemiLatticeWithTop ...)

-}

module CspCASL.Logic_CspCASL(CspCASL(CspCASL)) where

import CspCASL.AS_CSP_CASL

import CspCASL.CCKeywords

import CspCASL.Parse_AS_CSP_CASL

import CspCASL.Print_AS_CSP_CASL()

import CspCASL.ATC_CspCASL()

import CspCASL.SignCSP

import CspCASL.StatAnaCSP

import CASL.AS_Basic_CASL

import CASL.SymbolParser

import CASL.Logic_CASL(CASL(CASL))

import CASL.Sign

import CASL.Morphism

import Logic.Logic

import Common.Lib.Map as Map

-- a dummy datatype for the LogicGraph and for identifying the right

-- instances

data CspCASL = CspCASL deriving (Show)

instance Language CspCASL -- default definition is okay

instance Category CspCASL CSPSign CSPMorphism

where

-- ide :: id -> object -> morphism

ide CspCASL sigma =

let idAdd =

CSPAddMorphism { channelMap = Map.empty -- ??? too simplistic!

, processMap = Map.empty -- ??? too simplistic!

}

in idMor (\ _ _ -> idAdd) sigma

-- o :: id -> morphism -> morphism -> Maybe morphism

comp CspCASL = compose (const id) -- ??? too simplistic!

-- dom, cod :: id -> morphism -> object

dom CspCASL = msource

cod CspCASL = mtarget

-- legal_obj :: id -> object -> Bool

legal_obj CspCASL _ = fun_err "legall_obj"

-- legal_mor :: id -> morphism -> Bool

legal_mor CspCASL _ = fun_err "legal_mor"

-- abstract syntax, parsing (and printing)

instance Syntax CspCASL Basic_CSP_CASL_C_SPEC

SYMB_ITEMS SYMB_MAP_ITEMS

where

parse_basic_spec CspCASL = Just basicCspCaslCSpec

parse_symb_items CspCASL = Just $ symbItems csp_casl_keywords

parse_symb_map_items CspCASL = Just $ symbMapItems csp_casl_keywords

-- lattices (for sublogics) missing

-- CspCASL logic

instance Sentences CspCASL () () CSPSign CSPMorphism () where

parse_sentence CspCASL = Nothing

instance StaticAnalysis CspCASL Basic_CSP_CASL_C_SPEC () ()

SYMB_ITEMS SYMB_MAP_ITEMS

CSPSign CSPMorphism () () where

basic_analysis CspCASL = Just basicAnalysisCspCASL

stat_symb_map_items CspCASL = error "Logic_CspCASL.hs"

stat_symb_items CspCASL = error "Logic_CspCASL.hs"

empty_signature CspCASL = emptyCSPSign

inclusion CspCASL = sigInclusion computeExt isInclusion

is_subsig CspCASL = isSubSig isInclusion

signature_union CspCASL sigma1 sigma2 =

return $ addSig (\e _ -> e) sigma1 sigma2 -- ???

instance Logic CspCASL ()

Basic_CSP_CASL_C_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS

CSPSign

CSPMorphism

() () () where

data_logic CspCASL = Just (Logic CASL)

---- helper ---------------------------------

fun_err :: String -> a

fun_err fname =

error $ "*** CspCASL.Logic_CspCASL: Function \"" ++ fname

++ "\" is not yet implemented!"