224N/A{- |

224N/AModule : $Header$

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

224N/ALicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

224N/A

224N/AMaintainer : hets@tzi.de

224N/AStability : provisional

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

224N/A

224N/A

224N/A The embedding comorphism from CspCASL to ModalCASL.

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

224N/A Kripke structure

224N/A-}

224N/A

224N/Amodule Comorphisms.CspCASL2Modal where

224N/A

224N/Aimport Logic.Logic

224N/Aimport Logic.Comorphism

224N/Aimport qualified Common.Lib.Set as Set

844N/A

224N/A-- CASL

224N/Aimport CASL.Sign

224N/Aimport CASL.AS_Basic_CASL

224N/Aimport CASL.Morphism

1162N/A

1162N/A-- CspCASL

224N/Aimport CspCASL.Logic_CspCASL

224N/Aimport CspCASL.SignCSP

618N/Aimport CspCASL.AS_CSP_CASL

224N/A

844N/A-- ModalCASL

844N/Aimport Modal.Logic_Modal

1162N/Aimport Modal.AS_Modal

224N/Aimport Modal.ModalSign

224N/A

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

224N/Adata CspCASL2Modal = CspCASL2Modal deriving (Show)

224N/A

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

224N/A

224N/Ainstance Comorphism CspCASL2Modal

224N/A CspCASL ()

224N/A Basic_CSP_CASL_C_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS

224N/A CSPSign

224N/A CSPMorphism

224N/A () () ()

224N/A Modal ()

224N/A M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

224N/A MSign

224N/A ModalMor

224N/A Symbol RawSymbol () where

224N/A sourceLogic CspCASL2Modal = CspCASL

224N/A sourceSublogic CspCASL2Modal = ()

224N/A targetLogic CspCASL2Modal = Modal

224N/A targetSublogic CspCASL2Modal = ()

224N/A map_sign CspCASL2Modal sig = let e = mapSig sig in Just (e, [])

224N/A map_morphism CspCASL2Modal = Just . mapMor

224N/A map_sentence CspCASL2Modal _ = Just . mapSen

224N/A map_symbol CspCASL2Modal = Set.single . mapSym

224N/A

224N/AmapSig :: CSPSign -> MSign

224N/AmapSig sign =

224N/A (emptySign emptyModalSign) {sortSet = sortSet sign

224N/A , sortRel = sortRel sign

224N/A , opMap = opMap sign

224N/A , assocOps = assocOps sign

224N/A , predMap = predMap sign }

224N/A -- ??? add modalities

224N/A

224N/AmapMor :: CSPMorphism -> ModalMor

224N/AmapMor m = Morphism {msource = mapSig $ msource m

224N/A , mtarget = mapSig $ mtarget m

224N/A , sort_map = sort_map m

224N/A , fun_map = fun_map m

224N/A , pred_map = pred_map m

224N/A , extended_map = ()}

224N/A -- ??? add modalities

224N/A

224N/A

224N/AmapSym :: () -> Symbol

224N/AmapSym = error "CspCASL2Modal.mapSym not yet implemented"

224N/A -- needs to be changed once modal symbols are added

224N/A

224N/A

224N/AmapSen :: () -> ModalFORMULA

224N/AmapSen f = True_atom []

224N/A

224N/A{- case f of

224N/A Quantification q vs frm ps ->

224N/A Quantification q vs (mapSen frm) ps

224N/A Conjunction fs ps ->

224N/A Conjunction (map mapSen fs) ps

224N/A Disjunction fs ps ->

224N/A Disjunction (map mapSen fs) ps

224N/A Implication f1 f2 b ps ->

224N/A Implication (mapSen f1) (mapSen f2) b ps

224N/A Equivalence f1 f2 ps ->

224N/A Equivalence (mapSen f1) (mapSen f2) ps

224N/A Negation frm ps -> Negation (mapSen frm) ps

224N/A True_atom ps -> True_atom ps

224N/A False_atom ps -> False_atom ps

224N/A Existl_equation t1 t2 ps ->

224N/A Existl_equation (mapTERM t1) (mapTERM t2) ps

224N/A Strong_equation t1 t2 ps ->

224N/A Strong_equation (mapTERM t1) (mapTERM t2) ps

224N/A Predication pn as qs ->

224N/A Predication pn (map mapTERM as) qs

224N/A Definedness t ps -> Definedness (mapTERM t) ps

224N/A Membership t ty ps -> Membership (mapTERM t) ty ps

224N/A Sort_gen_ax constrs isFree -> Sort_gen_ax constrs isFree

224N/A _ -> error "CspCASL2Modal.mapSen"

224N/A

224N/AmapTERM :: TERM () -> TERM M_FORMULA

224N/AmapTERM t = case t of

224N/A Qual_var v ty ps -> Qual_var v ty ps

224N/A Application opsym as qs -> Application opsym (map mapTERM as) qs

224N/A Sorted_term trm ty ps -> Sorted_term (mapTERM trm) ty ps

224N/A Cast trm ty ps -> Cast (mapTERM trm) ty ps

224N/A Conditional t1 f t2 ps ->

224N/A Conditional (mapTERM t1) (mapSen f) (mapTERM t2) ps

224N/A _ -> error "CspCASL2Modal.mapTERM"

224N/A

224N/A-}

224N/A