131N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

131N/A{- |

131N/AModule : $Header$

131N/ACopyright : (c) Till Mossakowski and Uni Bremen 2004

131N/ALicense : GPLv2 or higher, see LICENSE.txt

131N/A

131N/AMaintainer : till@informatik.uni-bremen.de

131N/AStability : provisional

131N/APortability : non-portable (imports Logic.Logic)

131N/A

131N/AThe embedding comorphism from CspCASL to ModalCASL.

131N/A It keeps the CASL part and interprets the CspCASL LTS semantics as

131N/A Kripke structure

131N/A-}

131N/A

131N/Amodule Comorphisms.CspCASL2Modal where

131N/A

131N/Aimport Logic.Logic

131N/Aimport Logic.Comorphism

131N/Aimport Common.Id

131N/A

131N/A-- CASL

844N/Aimport CASL.Sign

131N/Aimport CASL.AS_Basic_CASL

131N/Aimport CASL.Morphism

131N/A

131N/A-- CspCASL

131N/Aimport CspCASL.Logic_CspCASL

131N/Aimport CspCASL.SignCSP

618N/Aimport CspCASL.StatAnaCSP (CspBasicSpec)

131N/Aimport CspCASL.Morphism (CspCASLMorphism)

131N/Aimport CspCASL.SymbItems

844N/Aimport CspCASL.Symbol

844N/A

131N/A-- ModalCASL

131N/Aimport Modal.Logic_Modal

131N/Aimport Modal.AS_Modal

131N/Aimport Modal.ModalSign

131N/A

628N/A-- | The identity of the comorphism

628N/Adata CspCASL2Modal = CspCASL2Modal deriving (Show)

628N/A

131N/Ainstance Language CspCASL2Modal -- default definition is okay

131N/A

131N/Ainstance Comorphism CspCASL2Modal

131N/A CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems

131N/A CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()

131N/A Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

131N/A MSign ModalMor Symbol RawSymbol () where

131N/A sourceLogic CspCASL2Modal = cspCASL

131N/A sourceSublogic CspCASL2Modal = ()

131N/A targetLogic CspCASL2Modal = Modal

131N/A mapSublogic CspCASL2Modal _ = Just ()

181N/A map_theory CspCASL2Modal = return . simpleTheoryMapping mapSig mapSen

131N/A map_morphism CspCASL2Modal = return . mapMor

181N/A map_sentence CspCASL2Modal _ = return . mapSen

131N/A

181N/AmapSig :: CspCASLSign -> MSign

131N/AmapSig sign =

131N/A (emptySign emptyModalSign)

131N/A { sortRel = sortRel sign

131N/A , opMap = opMap sign

, assocOps = assocOps sign

, predMap = predMap sign }

-- ??? add modalities

mapMor :: CspCASLMorphism -> ModalMor

mapMor m = (embedMorphism emptyMorExt (mapSig $ msource m) $ mapSig $ mtarget m)

{ sort_map = sort_map m

, op_map = op_map m

, pred_map = pred_map m }

-- ??? add modalities

mapSym :: Symbol -> Symbol

mapSym = error "CspCASL2Modal.mapSym not yet implemented"

-- needs to be changed once modal symbols are added

mapSen :: CspCASLSen -> ModalFORMULA

mapSen _f = True_atom nullRange

{- case f of

Quantification q vs frm ps ->

Quantification q vs (mapSen frm) ps

Conjunction fs ps ->

Conjunction (map mapSen fs) ps

Disjunction fs ps ->

Disjunction (map mapSen fs) ps

Implication f1 f2 b ps ->

Implication (mapSen f1) (mapSen f2) b ps

Equivalence f1 f2 ps ->

Equivalence (mapSen f1) (mapSen f2) ps

Negation frm ps -> Negation (mapSen frm) ps

True_atom ps -> True_atom ps

False_atom ps -> False_atom ps

Existl_equation t1 t2 ps ->

Existl_equation (mapTERM t1) (mapTERM t2) ps

Strong_equation t1 t2 ps ->

Strong_equation (mapTERM t1) (mapTERM t2) ps

Predication pn as qs ->

Predication pn (map mapTERM as) qs

Definedness t ps -> Definedness (mapTERM t) ps

Membership t ty ps -> Membership (mapTERM t) ty ps

Sort_gen_ax constrs isFree -> Sort_gen_ax constrs isFree

_ -> error "CspCASL2Modal.mapSen"

mapTERM :: TERM () -> TERM M_FORMULA

mapTERM t = case t of

Qual_var v ty ps -> Qual_var v ty ps

Application opsym as qs -> Application opsym (map mapTERM as) qs

Sorted_term trm ty ps -> Sorted_term (mapTERM trm) ty ps

Cast trm ty ps -> Cast (mapTERM trm) ty ps

Conditional t1 f t2 ps ->

Conditional (mapTERM t1) (mapSen f) (mapTERM t2) ps

_ -> error "CspCASL2Modal.mapTERM"

-}