{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  $Header$
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
