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
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdata MODAL_EMBEDDING = MODAL_EMBEDDING deriving Show
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torriniinstance Language MODAL_EMBEDDING
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 Symbol RawSymbol ProofTree
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASL CASL_Sublogics
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Symbol RawSymbol ProofTree
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASL CASL_Sublogics
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Symbol RawSymbol ProofTree
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASL CASL_Sublogics
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Symbol RawSymbol ProofTree
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)