content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/CASL2ExtModal.hs
  Description :  embedding from CASL to ExtModal
  Copyright   :  (c) C. Maeder, DFKI GmbH 2011
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Logic)
  
  The embedding comorphism from CASL to ExtModal.
  -}
  
  module Comorphisms.CASL2ExtModal (CASL2ExtModal (..)) where
  
  import qualified Data.Set as Set
  
  import Logic.Logic
  import Logic.Comorphism
  
  import CASL.Logic_CASL
  import CASL.Sublogic as SL
  import CASL.Sign
  import CASL.AS_Basic_CASL
  import CASL.Morphism
  
  import ExtModal.Logic_ExtModal
  import ExtModal.AS_ExtModal
  import ExtModal.ExtModalSign
  import ExtModal.MorphismExtension
  import ExtModal.Sublogic
  
  import Common.ProofTree
  
  -- | The identity of the comorphism
  data CASL2ExtModal = CASL2ExtModal deriving Show
  
  instance Language CASL2ExtModal -- default definition is okay
  
  instance Comorphism CASL2ExtModal
                 CASL CASL_Sublogics
                 CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
                 CASLSign
                 CASLMor
                 Symbol RawSymbol ProofTree
                 ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
                 SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
                 Symbol RawSymbol () where
      sourceLogic CASL2ExtModal = CASL
      sourceSublogic CASL2ExtModal = SL.top
      targetLogic CASL2ExtModal = ExtModal
      mapSublogic CASL2ExtModal s = Just s { ext_features = botSublogic }
      map_theory CASL2ExtModal = return . embedCASLTheory emptyEModalSign
      map_morphism CASL2ExtModal =
        return . mapCASLMor emptyEModalSign emptyMorphExtension
      map_sentence CASL2ExtModal _ = return . mapFORMULA
      map_symbol CASL2ExtModal _ = Set.singleton . id
      has_model_expansion CASL2ExtModal = True
      is_weakly_amalgamable CASL2ExtModal = True
      isInclusionComorphism CASL2ExtModal = True
  