content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/CASL2Modal.hs
  Description :  embedding from CASL to ModalCASL
  Copyright   :  (c) Till Mossakowski and Uni Bremen 2004
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  luecke@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Logic)
  
  The embedding comorphism from CASL to ModalCASL.
  
  -}
  
  module Comorphisms.CASL2Modal (CASL2Modal (..)) where
  
  import Logic.Logic
  import Logic.Comorphism
  import qualified Data.Set as Set
  import Common.ProofTree
  
  -- CASL
  import CASL.Logic_CASL
  import CASL.Sublogic as SL
  import CASL.Sign
  import CASL.AS_Basic_CASL
  import CASL.Morphism
  
  -- ModalCASL
  import Modal.Logic_Modal
  import Modal.AS_Modal
  import Modal.ModalSign
  
  -- | The identity of the comorphism
  data CASL2Modal = CASL2Modal deriving (Show)
  
  instance Language CASL2Modal -- default definition is okay
  
  instance Comorphism CASL2Modal
                 CASL CASL_Sublogics
                 CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
                 CASLSign
                 CASLMor
                 Symbol RawSymbol ProofTree
                 Modal ()
                 M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
                 MSign
                 ModalMor
                 Symbol RawSymbol () where
      sourceLogic CASL2Modal = CASL
      sourceSublogic CASL2Modal = SL.top
      targetLogic CASL2Modal = Modal
      mapSublogic CASL2Modal _ = Just ()
      map_theory CASL2Modal = return . embedCASLTheory emptyModalSign
      map_morphism CASL2Modal = return . mapCASLMor emptyModalSign emptyMorExt
      map_sentence CASL2Modal _ = return . mapFORMULA
      map_symbol CASL2Modal _ = Set.singleton . id
      has_model_expansion CASL2Modal = True
      is_weakly_amalgamable CASL2Modal = True
      isInclusionComorphism CASL2Modal = True
  