content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/CspCASL2Modal.hs
  Copyright   :  (c) Till Mossakowski and Uni Bremen 2004
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  till@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Logic)
  
  The embedding comorphism from CspCASL to ModalCASL.
     It keeps the CASL part and interprets the CspCASL LTS semantics as
     Kripke structure
  -}
  
  module Comorphisms.CspCASL2Modal where
  
  import Logic.Logic
  import Logic.Comorphism
  
  -- CASL
  import CASL.Sign
  import CASL.AS_Basic_CASL
  import CASL.Morphism
  
  -- CspCASL
  import CspCASL.Logic_CspCASL
  import CspCASL.SignCSP
  import CspCASL.StatAnaCSP (CspBasicSpec)
  import CspCASL.Morphism (CspCASLMorphism)
  import CspCASL.SymbItems
  import CspCASL.Symbol
  
  -- ModalCASL
  import Modal.Logic_Modal
  import Modal.AS_Modal
  import Modal.ModalSign
  
  -- | The identity of the comorphism
  data CspCASL2Modal = CspCASL2Modal deriving (Show)
  
  instance Language CspCASL2Modal -- default definition is okay
  
  instance Comorphism CspCASL2Modal
      CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems
          CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()
      Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
          MSign ModalMor Symbol RawSymbol () where
      sourceLogic CspCASL2Modal = cspCASL
      sourceSublogic CspCASL2Modal = ()
      targetLogic CspCASL2Modal = Modal
      mapSublogic CspCASL2Modal _ = Just ()
      map_theory CspCASL2Modal = return . embedTheory mapSen emptyModalSign
      map_morphism CspCASL2Modal = return . mapCASLMor emptyModalSign emptyMorExt
      map_sentence CspCASL2Modal _ = return . mapSen
  
  mapSen :: CspCASLSen -> ModalFORMULA
  mapSen _ = trueForm
  