{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2Modal.hs
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 (Int -> CASL2Modal -> ShowS
[CASL2Modal] -> ShowS
CASL2Modal -> String
(Int -> CASL2Modal -> ShowS)
-> (CASL2Modal -> String)
-> ([CASL2Modal] -> ShowS)
-> Show CASL2Modal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2Modal] -> ShowS
$cshowList :: [CASL2Modal] -> ShowS
show :: CASL2Modal -> String
$cshow :: CASL2Modal -> String
showsPrec :: Int -> CASL2Modal -> ShowS
$cshowsPrec :: Int -> CASL2Modal -> ShowS
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
sourceLogic CASL2Modal = CASL
CASL
    sourceSublogic :: CASL2Modal -> CASL_Sublogics
sourceSublogic CASL2Modal = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.top
    targetLogic :: CASL2Modal -> Modal
targetLogic CASL2Modal = Modal
Modal
    mapSublogic :: CASL2Modal -> CASL_Sublogics -> Maybe ()
mapSublogic CASL2Modal _ = () -> Maybe ()
forall a. a -> Maybe a
Just ()
    map_theory :: CASL2Modal
-> (CASLSign, [Named CASLFORMULA])
-> Result (MSign, [Named ModalFORMULA])
map_theory CASL2Modal = (MSign, [Named ModalFORMULA])
-> Result (MSign, [Named ModalFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return ((MSign, [Named ModalFORMULA])
 -> Result (MSign, [Named ModalFORMULA]))
-> ((CASLSign, [Named CASLFORMULA])
    -> (MSign, [Named ModalFORMULA]))
-> (CASLSign, [Named CASLFORMULA])
-> Result (MSign, [Named ModalFORMULA])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModalSign
-> (CASLSign, [Named CASLFORMULA]) -> (MSign, [Named ModalFORMULA])
forall e f1 e1 f.
e
-> (Sign f1 e1, [Named (FORMULA f1)])
-> (Sign f e, [Named (FORMULA f)])
embedCASLTheory ModalSign
emptyModalSign
    map_morphism :: CASL2Modal -> CASLMor -> Result ModalMor
map_morphism CASL2Modal = ModalMor -> Result ModalMor
forall (m :: * -> *) a. Monad m => a -> m a
return (ModalMor -> Result ModalMor)
-> (CASLMor -> ModalMor) -> CASLMor -> Result ModalMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModalSign -> DefMorExt ModalSign -> CASLMor -> 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 :: CASL2Modal -> CASLSign -> CASLFORMULA -> Result ModalFORMULA
map_sentence CASL2Modal _ = ModalFORMULA -> Result ModalFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (ModalFORMULA -> Result ModalFORMULA)
-> (CASLFORMULA -> ModalFORMULA)
-> CASLFORMULA
-> Result ModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> ModalFORMULA
forall f1 f. FORMULA f1 -> FORMULA f
mapFORMULA
    map_symbol :: CASL2Modal -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2Modal _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. a -> a
id
    has_model_expansion :: CASL2Modal -> Bool
has_model_expansion CASL2Modal = Bool
True
    is_weakly_amalgamable :: CASL2Modal -> Bool
is_weakly_amalgamable CASL2Modal = Bool
True
    isInclusionComorphism :: CASL2Modal -> Bool
isInclusionComorphism CASL2Modal = Bool
True