content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/CASL2CspCASL.hs
  Copyright   :  (c) Till Mossakowski and Uni Bremen 2003
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  M.Roggenbach@swansea.ac.uk
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Logic)
  
  The embedding comorphism from CASL to CspCASL.
  -}
  
  module Comorphisms.CASL2CspCASL where
  
  import Logic.Logic
  import Logic.Comorphism
  import Common.ProofTree
  
  -- CASL
  import CASL.AS_Basic_CASL
  import CASL.Logic_CASL
  import CASL.Morphism
  import CASL.Sign
  import CASL.Sublogic as SL
  
  -- CspCASL
  import CspCASL.Logic_CspCASL
  import CspCASL.StatAnaCSP (CspBasicSpec)
  import CspCASL.SignCSP
  import CspCASL.Morphism (CspCASLMorphism, emptyCspAddMorphism)
  import CspCASL.SymbItems
  import CspCASL.Symbol
  
  import qualified Data.Set as Set
  
  -- | The identity of the comorphism
  data CASL2CspCASL = CASL2CspCASL deriving (Show)
  
  instance Language CASL2CspCASL -- default definition is okay
  
  instance Comorphism CASL2CspCASL
      CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
          CASLSign CASLMor Symbol RawSymbol ProofTree
      CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems
          CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () where
      sourceLogic CASL2CspCASL = CASL
      sourceSublogic CASL2CspCASL = SL.top
      targetLogic CASL2CspCASL = cspCASL
      mapSublogic CASL2CspCASL _ = Just ()
      map_theory CASL2CspCASL =
        return . embedCASLTheory emptyCspSign
      map_symbol CASL2CspCASL _ = Set.singleton . caslToCspSymbol
      map_morphism CASL2CspCASL =
        return . mapCASLMor emptyCspSign emptyCspAddMorphism
      map_sentence CASL2CspCASL _sig = return . mapFORMULA
      has_model_expansion CASL2CspCASL = True
      is_weakly_amalgamable CASL2CspCASL = True
      isInclusionComorphism CASL2CspCASL = True
  