{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CspCASL2Modal.hs
Copyright   :  (c) Till Mossakowski and Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from CspCASL to ModalCASL.
   It keeps the CASL part and interprets the CspCASL LTS semantics as
   Kripke structure
-}

module Comorphisms.CspCASL2Modal where

import Logic.Logic
import Logic.Comorphism

-- CASL
import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.Morphism

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

-- ModalCASL
import Modal.Logic_Modal
import Modal.AS_Modal
import Modal.ModalSign

-- | The identity of the comorphism
data CspCASL2Modal = CspCASL2Modal deriving (Int -> CspCASL2Modal -> ShowS
[CspCASL2Modal] -> ShowS
CspCASL2Modal -> String
(Int -> CspCASL2Modal -> ShowS)
-> (CspCASL2Modal -> String)
-> ([CspCASL2Modal] -> ShowS)
-> Show CspCASL2Modal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CspCASL2Modal] -> ShowS
$cshowList :: [CspCASL2Modal] -> ShowS
show :: CspCASL2Modal -> String
$cshow :: CspCASL2Modal -> String
showsPrec :: Int -> CspCASL2Modal -> ShowS
$cshowsPrec :: Int -> CspCASL2Modal -> ShowS
Show)

instance Language CspCASL2Modal -- default definition is okay

instance Comorphism CspCASL2Modal
    CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems
        CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()
    Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
        MSign ModalMor Symbol RawSymbol () where
    sourceLogic :: CspCASL2Modal -> CspCASL
sourceLogic CspCASL2Modal = CspCASL
cspCASL
    sourceSublogic :: CspCASL2Modal -> ()
sourceSublogic CspCASL2Modal = ()
    targetLogic :: CspCASL2Modal -> Modal
targetLogic CspCASL2Modal = Modal
Modal
    mapSublogic :: CspCASL2Modal -> () -> Maybe ()
mapSublogic CspCASL2Modal _ = () -> Maybe ()
forall a. a -> Maybe a
Just ()
    map_theory :: CspCASL2Modal
-> (CspCASLSign, [Named CspCASLSen])
-> Result (MSign, [Named ModalFORMULA])
map_theory CspCASL2Modal = (MSign, [Named ModalFORMULA])
-> Result (MSign, [Named ModalFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return ((MSign, [Named ModalFORMULA])
 -> Result (MSign, [Named ModalFORMULA]))
-> ((CspCASLSign, [Named CspCASLSen])
    -> (MSign, [Named ModalFORMULA]))
-> (CspCASLSign, [Named CspCASLSen])
-> Result (MSign, [Named ModalFORMULA])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CspCASLSen -> ModalFORMULA)
-> ModalSign
-> (CspCASLSign, [Named CspCASLSen])
-> (MSign, [Named ModalFORMULA])
forall f1 f e e1.
(FORMULA f1 -> FORMULA f)
-> e
-> (Sign f1 e1, [Named (FORMULA f1)])
-> (Sign f e, [Named (FORMULA f)])
embedTheory CspCASLSen -> ModalFORMULA
mapSen ModalSign
emptyModalSign
    map_morphism :: CspCASL2Modal -> CspCASLMorphism -> Result ModalMor
map_morphism CspCASL2Modal = ModalMor -> Result ModalMor
forall (m :: * -> *) a. Monad m => a -> m a
return (ModalMor -> Result ModalMor)
-> (CspCASLMorphism -> ModalMor)
-> CspCASLMorphism
-> Result ModalMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModalSign -> DefMorExt ModalSign -> CspCASLMorphism -> ModalMor
forall e m f1 e1 m1 f.
e -> m -> Morphism f1 e1 m1 -> Morphism f e m
mapCASLMor ModalSign
emptyModalSign DefMorExt ModalSign
forall e. DefMorExt e
emptyMorExt
    map_sentence :: CspCASL2Modal -> CspCASLSign -> CspCASLSen -> Result ModalFORMULA
map_sentence CspCASL2Modal _ = ModalFORMULA -> Result ModalFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (ModalFORMULA -> Result ModalFORMULA)
-> (CspCASLSen -> ModalFORMULA)
-> CspCASLSen
-> Result ModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CspCASLSen -> ModalFORMULA
mapSen

mapSen :: CspCASLSen -> ModalFORMULA
mapSen :: CspCASLSen -> ModalFORMULA
mapSen _ = ModalFORMULA
forall f. FORMULA f
trueForm