{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances, FlexibleInstances

, TypeSynonymInstances #-}

{- |

Module : ./Modifications/ModalEmbedding.hs

Copyright : (c) Mihai Codescu, Uni Bremen 2002-2004

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Mihai.Codescu@dfki.de

Stability : experimental

Portability : non-portable (Logic)

institution modification

-}

{-

CASL -------------------------id------------------> CASL

CASL ---CASL2Modal----> ModalCASL --Modal2CASL----> CASL

-}

module Modifications.ModalEmbedding where

import Logic.Modification

import Logic.Logic

import Logic.Comorphism

import Comorphisms.CASL2Modal

import Comorphisms.Modal2CASL

import CASL.Logic_CASL

import CASL.Sign

import CASL.Morphism

import CASL.AS_Basic_CASL

import CASL.Sublogic as SL

import Common.ProofTree

data MODAL_EMBEDDING = MODAL_EMBEDDING deriving Show

instance Language MODAL_EMBEDDING

instance Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics)

(CompComorphism CASL2Modal Modal2CASL)

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree

where

sourceComorphism MODAL_EMBEDDING = mkIdComorphism CASL (top_sublogic CASL)

targetComorphism MODAL_EMBEDDING = CompComorphism CASL2Modal Modal2CASL

tauSigma MODAL_EMBEDDING sigma = do

(sigma1, _ ) <- wrapMapTheory CASL2Modal (sigma, [])

(sigma2, _ ) <- wrapMapTheory Modal2CASL (sigma1, [])

return (embedMorphism () sigma sigma2)