{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances, FlexibleInstances
  , TypeSynonymInstances #-}
{- |
Module      :  ./Modifications/ModalEmbedding.hs
Copyright   :  (c) Mihai Codescu, Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Mihai.Codescu@dfki.de
Stability   :  experimental
Portability :  non-portable (Logic)

institution modification
-}

{-
   CASL -------------------------id------------------> CASL
   CASL ---CASL2Modal----> ModalCASL --Modal2CASL----> CASL
-}

module Modifications.ModalEmbedding where

import Logic.Modification
import Logic.Logic
import Logic.Comorphism

import Comorphisms.CASL2Modal
import Comorphisms.Modal2CASL


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

import Common.ProofTree

data MODAL_EMBEDDING = MODAL_EMBEDDING deriving Int -> MODAL_EMBEDDING -> ShowS
[MODAL_EMBEDDING] -> ShowS
MODAL_EMBEDDING -> String
(Int -> MODAL_EMBEDDING -> ShowS)
-> (MODAL_EMBEDDING -> String)
-> ([MODAL_EMBEDDING] -> ShowS)
-> Show MODAL_EMBEDDING
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MODAL_EMBEDDING] -> ShowS
$cshowList :: [MODAL_EMBEDDING] -> ShowS
show :: MODAL_EMBEDDING -> String
$cshow :: MODAL_EMBEDDING -> String
showsPrec :: Int -> MODAL_EMBEDDING -> ShowS
$cshowsPrec :: Int -> MODAL_EMBEDDING -> ShowS
Show

instance Language MODAL_EMBEDDING

instance Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics)
    (CompComorphism CASL2Modal Modal2CASL)
        CASL CASL_Sublogics
        CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
        CASLSign
        CASLMor
        Symbol RawSymbol ProofTree
        CASL CASL_Sublogics
        CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
        CASLSign
        CASLMor
        Symbol RawSymbol ProofTree
        CASL CASL_Sublogics
        CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
        CASLSign
        CASLMor
        Symbol RawSymbol ProofTree
        CASL CASL_Sublogics
        CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
        CASLSign
        CASLMor
        Symbol RawSymbol ProofTree
 where
  sourceComorphism :: MODAL_EMBEDDING -> InclComorphism CASL CASL_Sublogics
sourceComorphism MODAL_EMBEDDING = CASL -> CASL_Sublogics -> InclComorphism CASL CASL_Sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> InclComorphism lid sublogics
mkIdComorphism CASL
CASL (CASL -> CASL_Sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics
top_sublogic CASL
CASL)
  targetComorphism :: MODAL_EMBEDDING -> CompComorphism CASL2Modal Modal2CASL
targetComorphism MODAL_EMBEDDING = CASL2Modal -> Modal2CASL -> CompComorphism CASL2Modal Modal2CASL
forall cid1 cid2. cid1 -> cid2 -> CompComorphism cid1 cid2
CompComorphism CASL2Modal
CASL2Modal Modal2CASL
Modal2CASL
  tauSigma :: MODAL_EMBEDDING -> CASLSign -> Result CASLMor
tauSigma MODAL_EMBEDDING sigma :: CASLSign
sigma = do
      (sigma1 :: MSign
sigma1, _ ) <- CASL2Modal
-> (CASLSign, [Named CASLFORMULA])
-> Result (MSign, [Named ModalFORMULA])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory CASL2Modal
CASL2Modal (CASLSign
sigma, [])
      (sigma2 :: CASLSign
sigma2, _ ) <- Modal2CASL
-> (MSign, [Named ModalFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory Modal2CASL
Modal2CASL (MSign
sigma1, [])
      CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> CASLSign -> CASLSign -> CASLMor
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism () CASLSign
sigma CASLSign
sigma2)