501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt{- |

8e5fce1f9ceba17dd7e3ff0eb287e1e999c14249Mark AndrewsModule : $Header$

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntCopyright : (c) Till Mossakowski and Uni Bremen 2004

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntMaintainer : luettich@tzi.de

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntStability : provisional

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntPortability : non-portable (imports Logic.Logic)

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntThe embedding comorphism from CASL to ModalCASL.

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt-}

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntmodule Comorphisms.CASL2Modal where

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport Logic.Logic

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport Logic.Comorphism

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport qualified Common.Lib.Set as Set

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt-- CASL

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport CASL.Logic_CASL

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport CASL.Sublogic

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport CASL.Sign

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport CASL.AS_Basic_CASL

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport CASL.Morphism

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt-- ModalCASL

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport Modal.Logic_Modal

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport Modal.AS_Modal

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntimport Modal.ModalSign

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt-- | The identity of the comorphism

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntdata CASL2Modal = CASL2Modal deriving (Show)

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

4eb998928b9aef0ceda42d7529980d658138698aEvan Huntinstance Language CASL2Modal -- default definition is okay

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Huntinstance Comorphism CASL2Modal

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt CASL CASL_Sublogics

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt CASLSign

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt CASLMor

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Symbol RawSymbol ()

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Modal ()

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt MSign

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt ModalMor

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Symbol RawSymbol () where

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt sourceLogic CASL2Modal = CASL

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt sourceSublogic CASL2Modal = CASL_SL

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt { has_sub = True,

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt has_part = True,

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt has_cons = True,

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt has_eq = True,

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt has_pred = True,

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt which_logic = FOL

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt }

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt targetLogic CASL2Modal = Modal

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt targetSublogic CASL2Modal = ()

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt map_theory CASL2Modal = return . simpleTheoryMapping mapSig mapSen

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt map_morphism CASL2Modal = return . mapMor

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt map_sentence CASL2Modal _ = return . mapSen

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt map_symbol CASL2Modal = Set.singleton . mapSym

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntmapSig :: CASLSign -> MSign

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntmapSig sign =

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt (emptySign emptyModalSign) {sortSet = sortSet sign

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt , sortRel = sortRel sign

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt , opMap = opMap sign

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt , assocOps = assocOps sign

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt , predMap = predMap sign }

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntmapMor :: CASLMor -> ModalMor

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntmapMor m = Morphism {msource = mapSig $ msource m

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt , mtarget = mapSig $ mtarget m

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt , sort_map = sort_map m

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt , fun_map = fun_map m

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt , pred_map = pred_map m

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt , extended_map = ()}

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntmapSym :: Symbol -> Symbol

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntmapSym = id -- needs to be changed once modal symbols are added

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntmapSen :: CASLFORMULA -> ModalFORMULA

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan HuntmapSen f = case f of

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Quantification q vs frm ps ->

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Quantification q vs (mapSen frm) ps

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Conjunction fs ps ->

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Conjunction (map mapSen fs) ps

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Disjunction fs ps ->

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Disjunction (map mapSen fs) ps

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Implication f1 f2 b ps ->

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Implication (mapSen f1) (mapSen f2) b ps

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Equivalence f1 f2 ps ->

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Equivalence (mapSen f1) (mapSen f2) ps

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Negation frm ps -> Negation (mapSen frm) ps

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt True_atom ps -> True_atom ps

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt False_atom ps -> False_atom ps

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Existl_equation t1 t2 ps ->

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Existl_equation (mapTERM t1) (mapTERM t2) ps

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Strong_equation t1 t2 ps ->

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt Strong_equation (mapTERM t1) (mapTERM t2) ps

501941f0b6cce74c2ff75b10aff3f230d5d37e4cEvan Hunt 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 "CASL2Modal.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 "CASL2Modal.mapTERM"