{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2ExtModal.hs
Description :  embedding from CASL to ExtModal
Copyright   :  (c) C. Maeder, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from CASL to ExtModal.
-}

module Comorphisms.CASL2ExtModal (CASL2ExtModal (..)) where

import qualified Data.Set as Set

import Logic.Logic
import Logic.Comorphism

import CASL.Logic_CASL
import CASL.Sublogic as SL
import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.Morphism

import ExtModal.Logic_ExtModal
import ExtModal.AS_ExtModal
import ExtModal.ExtModalSign
import ExtModal.MorphismExtension
import ExtModal.Sublogic

import Common.ProofTree

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

instance Language CASL2ExtModal -- default definition is okay

instance Comorphism CASL2ExtModal
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
               SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
               Symbol RawSymbol () where
    sourceLogic :: CASL2ExtModal -> CASL
sourceLogic CASL2ExtModal = CASL
CASL
    sourceSublogic :: CASL2ExtModal -> CASL_Sublogics
sourceSublogic CASL2ExtModal = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.top
    targetLogic :: CASL2ExtModal -> ExtModal
targetLogic CASL2ExtModal = ExtModal
ExtModal
    mapSublogic :: CASL2ExtModal -> CASL_Sublogics -> Maybe ExtModalSL
mapSublogic CASL2ExtModal s :: CASL_Sublogics
s = ExtModalSL -> Maybe ExtModalSL
forall a. a -> Maybe a
Just CASL_Sublogics
s { ext_features :: Sublogic
ext_features = Sublogic
botSublogic }
    map_theory :: CASL2ExtModal
-> (CASLSign, [Named CASLFORMULA])
-> Result (ExtModalSign, [Named ExtModalFORMULA])
map_theory CASL2ExtModal = (ExtModalSign, [Named ExtModalFORMULA])
-> Result (ExtModalSign, [Named ExtModalFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return ((ExtModalSign, [Named ExtModalFORMULA])
 -> Result (ExtModalSign, [Named ExtModalFORMULA]))
-> ((CASLSign, [Named CASLFORMULA])
    -> (ExtModalSign, [Named ExtModalFORMULA]))
-> (CASLSign, [Named CASLFORMULA])
-> Result (ExtModalSign, [Named ExtModalFORMULA])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EModalSign
-> (CASLSign, [Named CASLFORMULA])
-> (ExtModalSign, [Named ExtModalFORMULA])
forall e f1 e1 f.
e
-> (Sign f1 e1, [Named (FORMULA f1)])
-> (Sign f e, [Named (FORMULA f)])
embedCASLTheory EModalSign
emptyEModalSign
    map_morphism :: CASL2ExtModal -> CASLMor -> Result ExtModalMorph
map_morphism CASL2ExtModal =
      ExtModalMorph -> Result ExtModalMorph
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtModalMorph -> Result ExtModalMorph)
-> (CASLMor -> ExtModalMorph) -> CASLMor -> Result ExtModalMorph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EModalSign -> MorphExtension -> CASLMor -> ExtModalMorph
forall e m f1 e1 m1 f.
e -> m -> Morphism f1 e1 m1 -> Morphism f e m
mapCASLMor EModalSign
emptyEModalSign MorphExtension
emptyMorphExtension
    map_sentence :: CASL2ExtModal -> CASLSign -> CASLFORMULA -> Result ExtModalFORMULA
map_sentence CASL2ExtModal _ = ExtModalFORMULA -> Result ExtModalFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtModalFORMULA -> Result ExtModalFORMULA)
-> (CASLFORMULA -> ExtModalFORMULA)
-> CASLFORMULA
-> Result ExtModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> ExtModalFORMULA
forall f1 f. FORMULA f1 -> FORMULA f
mapFORMULA
    map_symbol :: CASL2ExtModal -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2ExtModal _ = 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 :: CASL2ExtModal -> Bool
has_model_expansion CASL2ExtModal = Bool
True
    is_weakly_amalgamable :: CASL2ExtModal -> Bool
is_weakly_amalgamable CASL2ExtModal = Bool
True
    isInclusionComorphism :: CASL2ExtModal -> Bool
isInclusionComorphism CASL2ExtModal = Bool
True