{-# 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
