content: {-# 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)
  