{-# 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 Int -> CspCASL2CspCASL a b -> ShowS
[CspCASL2CspCASL a b] -> ShowS
CspCASL2CspCASL a b -> String
(Int -> CspCASL2CspCASL a b -> ShowS)
-> (CspCASL2CspCASL a b -> String)
-> ([CspCASL2CspCASL a b] -> ShowS)
-> Show (CspCASL2CspCASL a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> CspCASL2CspCASL a b -> ShowS
forall a b. (Show a, Show b) => [CspCASL2CspCASL a b] -> ShowS
forall a b. (Show a, Show b) => CspCASL2CspCASL a b -> String
showList :: [CspCASL2CspCASL a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [CspCASL2CspCASL a b] -> ShowS
show :: CspCASL2CspCASL a b -> String
$cshow :: forall a b. (Show a, Show b) => CspCASL2CspCASL a b -> String
showsPrec :: Int -> CspCASL2CspCASL a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> CspCASL2CspCASL a b -> ShowS
Show

cspCASLTrace :: CspCASL2CspCASL () Trace
cspCASLTrace :: CspCASL2CspCASL () Trace
cspCASLTrace = () -> Trace -> CspCASL2CspCASL () Trace
forall a b. a -> b -> CspCASL2CspCASL a b
CspCASL2CspCASL () Trace
Trace

cspCASLFailure :: CspCASL2CspCASL () Failure
cspCASLFailure :: CspCASL2CspCASL () Failure
cspCASLFailure = () -> Failure -> CspCASL2CspCASL () Failure
forall a b. a -> b -> CspCASL2CspCASL a b
CspCASL2CspCASL () Failure
Failure

instance (Show a, Show b) => Language (CspCASL2CspCASL a b) where
  language_name :: CspCASL2CspCASL a b -> String
language_name (CspCASL2CspCASL a :: a
a b :: b
b) =
      GenCspCASL a -> String
forall lid. Language lid => lid -> String
language_name (a -> GenCspCASL a
forall a. a -> GenCspCASL a
GenCspCASL a
a)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ "2" String -> ShowS
forall a. [a] -> [a] -> [a]
++ GenCspCASL b -> String
forall lid. Language lid => lid -> String
language_name (b -> GenCspCASL b
forall a. a -> GenCspCASL a
GenCspCASL b
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 b -> GenCspCASL a
sourceLogic (CspCASL2CspCASL a :: a
a _) = a -> GenCspCASL a
forall a. a -> GenCspCASL a
GenCspCASL a
a
    sourceSublogic :: CspCASL2CspCASL a b -> ()
sourceSublogic _ = ()
    targetLogic :: CspCASL2CspCASL a b -> GenCspCASL b
targetLogic (CspCASL2CspCASL _ b :: b
b) = b -> GenCspCASL b
forall a. a -> GenCspCASL a
GenCspCASL b
b
    mapSublogic :: CspCASL2CspCASL a b -> () -> Maybe ()
mapSublogic _ _ = () -> Maybe ()
forall a. a -> Maybe a
Just ()
    map_theory :: CspCASL2CspCASL a b
-> (CspCASLSign, [Named CspCASLSen])
-> Result (CspCASLSign, [Named CspCASLSen])
map_theory _ = (CspCASLSign, [Named CspCASLSen])
-> Result (CspCASLSign, [Named CspCASLSen])
forall (m :: * -> *) a. Monad m => a -> m a
return
    map_morphism :: CspCASL2CspCASL a b -> CspCASLMorphism -> Result CspCASLMorphism
map_morphism _ = CspCASLMorphism -> Result CspCASLMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return
    map_sentence :: CspCASL2CspCASL a b
-> CspCASLSign -> CspCASLSen -> Result CspCASLSen
map_sentence _ = (CspCASLSen -> Result CspCASLSen)
-> CspCASLSign -> CspCASLSen -> Result CspCASLSen
forall a b. a -> b -> a
const CspCASLSen -> Result CspCASLSen
forall (m :: * -> *) a. Monad m => a -> m a
return
    map_symbol :: CspCASL2CspCASL a b -> CspCASLSign -> CspSymbol -> Set CspSymbol
map_symbol _ _ = CspSymbol -> Set CspSymbol
forall a. a -> Set a
Set.singleton
    is_model_transportable :: CspCASL2CspCASL a b -> Bool
is_model_transportable _ = Bool
True
    has_model_expansion :: CspCASL2CspCASL a b -> Bool
has_model_expansion _ = Bool
True
    is_weakly_amalgamable :: CspCASL2CspCASL a b -> Bool
is_weakly_amalgamable _ = Bool
True
    isInclusionComorphism :: CspCASL2CspCASL a b -> Bool
isInclusionComorphism _ = Bool
True