5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen{- |

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenModule : $Header$

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenDescription : embedding from CASL to ModalCASL

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenCopyright : (c) Till Mossakowski and Uni Bremen 2004

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenLicense : GPLv2 or higher, see LICENSE.txt

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenMaintainer : luecke@informatik.uni-bremen.de

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenStability : provisional

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenPortability : non-portable (imports Logic.Logic)

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenThe embedding comorphism from CASL to ModalCASL.

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-}

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenmodule Comorphisms.CASL2Modal (CASL2Modal(..)) where

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Logic.Logic

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Logic.Comorphism

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport qualified Data.Set as Set

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Common.ProofTree

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- CASL

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport CASL.Logic_CASL

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport CASL.Sublogic as SL

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport CASL.Sign

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport CASL.AS_Basic_CASL

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport CASL.Morphism

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- ModalCASL

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Modal.Logic_Modal

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Modal.AS_Modal

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Modal.ModalSign

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- | The identity of the comorphism

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowendata CASL2Modal = CASL2Modal deriving (Show)

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Boweninstance Language CASL2Modal -- default definition is okay

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Boweninstance Comorphism CASL2Modal

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen CASL CASL_Sublogics

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen CASLSign

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen CASLMor

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Symbol RawSymbol ProofTree

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Modal ()

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen MSign

3d8ee1629200b24b539b887a7feaec640fe610a8Kajetan Hemzaczek ModalMor

3d8ee1629200b24b539b887a7feaec640fe610a8Kajetan Hemzaczek Symbol RawSymbol () where

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen sourceLogic CASL2Modal = CASL

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen sourceSublogic CASL2Modal = SL.top

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen targetLogic CASL2Modal = Modal

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen mapSublogic CASL2Modal _ = Just ()

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen map_theory CASL2Modal = return . simpleTheoryMapping mapSig mapSen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen map_morphism CASL2Modal = return . mapMor

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen map_sentence CASL2Modal _ = return . mapSen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen map_symbol CASL2Modal _ = Set.singleton . mapSym

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen has_model_expansion CASL2Modal = True

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen is_weakly_amalgamable CASL2Modal = True

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen isInclusionComorphism CASL2Modal = True

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

3d8ee1629200b24b539b887a7feaec640fe610a8Kajetan HemzaczekmapSig :: CASLSign -> MSign

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenmapSig sign =

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen (emptySign emptyModalSign)

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen { sortRel = sortRel sign

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen , opMap = opMap sign

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen , assocOps = assocOps sign

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen , predMap = predMap sign }

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenmapMor :: CASLMor -> ModalMor

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenmapMor m = (embedMorphism emptyMorExt (mapSig $ msource m) $ mapSig $ mtarget m)

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen { sort_map = sort_map m

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen , op_map = op_map m

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen , pred_map = pred_map m }

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

3d8ee1629200b24b539b887a7feaec640fe610a8Kajetan HemzaczekmapSym :: Symbol -> Symbol

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenmapSym = id -- needs to be changed once modal symbols are added

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenmapSen :: CASLFORMULA -> ModalFORMULA

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenmapSen f = case f of

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Quantification q vs frm ps ->

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Quantification q vs (mapSen frm) ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Conjunction fs ps ->

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Conjunction (map mapSen fs) ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Disjunction fs ps ->

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Disjunction (map mapSen fs) ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Implication f1 f2 b ps ->

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Implication (mapSen f1) (mapSen f2) b ps

3d8ee1629200b24b539b887a7feaec640fe610a8Kajetan Hemzaczek Equivalence f1 f2 ps ->

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Equivalence (mapSen f1) (mapSen f2) ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Negation frm ps -> Negation (mapSen frm) ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen True_atom ps -> True_atom ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen False_atom ps -> False_atom ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Existl_equation t1 t2 ps ->

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Existl_equation (mapTERM t1) (mapTERM t2) ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Strong_equation t1 t2 ps ->

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Strong_equation (mapTERM t1) (mapTERM t2) ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Predication pn as qs ->

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Predication pn (map mapTERM as) qs

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Definedness t ps -> Definedness (mapTERM t) ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Membership t ty ps -> Membership (mapTERM t) ty ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Sort_gen_ax constrs isFree -> Sort_gen_ax constrs isFree

3d8ee1629200b24b539b887a7feaec640fe610a8Kajetan Hemzaczek _ -> error "CASL2Modal.mapSen"

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenmapTERM :: TERM () -> TERM M_FORMULA

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenmapTERM t = case t of

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Qual_var v ty ps -> Qual_var v ty ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Application opsym as qs -> Application opsym (map mapTERM as) qs

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Sorted_term trm ty ps -> Sorted_term (mapTERM trm) ty ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Cast trm ty ps -> Cast (mapTERM trm) ty ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Conditional t1 f t2 ps ->

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen Conditional (mapTERM t1) (mapSen f) (mapTERM t2) ps

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen _ -> error "CASL2Modal.mapTERM"

5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen