ModalEmbedding.hs revision d29201dd5328b88140ce050100693c501852657d
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances, FlexibleInstances
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , TypeSynonymInstances #-}
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- institution modification
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder-- CASL -------------------------id------------------> CASL
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- CASL ---CASL2Modal----> ModalCASL --Modal2CASL----> CASL
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedermodule Modifications.ModalEmbedding where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Logic.Modification
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Logic.Logic
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Logic.Comorphism
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Comorphisms.CASL2Modal
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Comorphisms.Modal2CASL
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.Logic_CASL
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.Sign
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.Morphism
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.AS_Basic_CASL
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.Sublogic as SL
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Common.ProofTree
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdata MODAL_EMBEDDING = MODAL_EMBEDDING deriving Show
d6025ee06343191f356a59704d467866afa29900Paolo Torrini
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torriniinstance Language MODAL_EMBEDDING
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederinstance Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (CompComorphism CASL2Modal Modal2CASL)
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrini CASL CASL_Sublogics
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLSign
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLMor
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Symbol RawSymbol ProofTree
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASL CASL_Sublogics
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLSign
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrini CASLMor
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Symbol RawSymbol ProofTree
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASL CASL_Sublogics
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLSign
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLMor
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Symbol RawSymbol ProofTree
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASL CASL_Sublogics
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLSign
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLMor
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Symbol RawSymbol ProofTree
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder sourceComorphism MODAL_EMBEDDING = mkIdComorphism CASL (top_sublogic CASL)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder targetComorphism MODAL_EMBEDDING = CompComorphism CASL2Modal Modal2CASL
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder tauSigma MODAL_EMBEDDING sigma = do
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (sigma1, _ ) <- wrapMapTheory CASL2Modal (sigma, [])
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (sigma2, _ ) <- wrapMapTheory Modal2CASL (sigma1, [])
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder return (embedMorphism () sigma sigma2)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder