{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./CspCASL/Comorphisms.hs
Description :  generic CspCASL instance for comorphisms
Copyright   :  (c) Liam O'Reilly, Swansea University 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  csliam@swansea.ac.uk
Stability   :  experimental
Portability :  non-portable(import Logic.Logic)

-}

module CspCASL.Comorphisms where

import Logic.Logic
import Logic.Comorphism

-- CspCASL
import CspCASL.StatAnaCSP (CspBasicSpec)
import CspCASL.Morphism
import CspCASL.Logic_CspCASL
import CspCASL.SignCSP
import CspCASL.SymbItems
import CspCASL.Symbol

import qualified Data.Set as Set

-- | The identity of the comorphism
data CspCASL2CspCASL a b = CspCASL2CspCASL a b deriving Show

cspCASLTrace :: CspCASL2CspCASL () Trace
cspCASLTrace = CspCASL2CspCASL () Trace

cspCASLFailure :: CspCASL2CspCASL () Failure
cspCASLFailure = CspCASL2CspCASL () Failure

instance (Show a, Show b) => Language (CspCASL2CspCASL a b) where
  language_name (CspCASL2CspCASL a b) =
      language_name (GenCspCASL a)
      ++ "2" ++ language_name (GenCspCASL b)

instance (CspCASLSemantics a, CspCASLSemantics b)
  => Comorphism (CspCASL2CspCASL a b)
    (GenCspCASL a) ()
      CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems
        CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()
    (GenCspCASL b) ()
      CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems
        CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () where
    sourceLogic (CspCASL2CspCASL a _) = GenCspCASL a
    sourceSublogic _ = ()
    targetLogic (CspCASL2CspCASL _ b) = GenCspCASL b
    mapSublogic _ _ = Just ()
    map_theory _ = return
    map_morphism _ = return
    map_sentence _ = const return
    map_symbol _ _ = Set.singleton
    is_model_transportable _ = True
    has_model_expansion _ = True
    is_weakly_amalgamable _ = True
    isInclusionComorphism _ = True
