hets/Logic/Comorphism.hs

	Comorphism.hs revision 2b565fe5cfb9f99857fd25b52304758d8544e266
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |
81d182b21020b815887e9057959228546cf61b6bChristian MaederModule      :  $Header$
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederDescription :  central interface (type class) for logic translations (comorphisms) in Hets
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright   :  (c) Till Mossakowski, Uni Bremen 2002-2006
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer  :  till@tzi.de
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederStability   :  provisional
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPortability :  non-portable (via Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederCentral interface (type class) for logic translations (comorphisms) in Hets
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder   These are just collections of
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder   functions between (some of) the types of logics.
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder   References: see Logic.hs
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-}
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maedermodule Logic.Comorphism ( CompComorphism(..)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder                        , IdComorphism
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder                        , InclComorphism
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder                        , inclusion_logic
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder                        , inclusion_source_sublogic
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder                        , inclusion_target_sublogic
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder                        , mkInclComorphism
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder                        , mkIdComorphism
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder                        , Comorphism(..)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder                        , targetSublogic
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder                        , map_sign
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder                        , mapDefaultMorphism
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder                        -- , failMapSentence
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder                        -- , errMapSymbol
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder                        , wrapMapTheory
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder                        , simpleTheoryMapping
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder                        , mkTheoryMapping) where
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederimport Logic.Logic
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederimport Logic.Coerce
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederimport qualified Data.Set as Set
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Common.Result
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.ProofUtils
04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Common.AS_Annotation
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Common.Doc
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederimport Common.DocUtils
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiclass (Language cid,
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder       Logic lid1 sublogics1
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder        basic_spec1 sentence1 symb_items1 symb_map_items1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder       Logic lid2 sublogics2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder        basic_spec2 sentence2 symb_items2 symb_map_items2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder  Comorphism cid
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder             | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder  where
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder    -- source and target logic and sublogic
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    -- the source sublogic is the maximal one for which the comorphism works
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder    sourceLogic :: cid -> lid1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    sourceSublogic :: cid -> sublogics1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder    targetLogic :: cid -> lid2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder    -- finer information of target sublogics corresponding to source sublogics
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder    -- this function must be partial because mapTheory is partial
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder    mapSublogic :: cid -> sublogics1 -> Maybe sublogics2
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder    -- the translation functions are partial
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    -- because the target may be a sublanguage
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder    -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder    -- cover theoroidal comorphisms as well
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    map_theory :: cid -> (sign1,[Named sentence1])
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder                      -> Result (sign2,[Named sentence2])
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    map_morphism :: cid -> morphism1 -> Result morphism2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder          -- also covers semi-comorphisms
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder          -- with no sentence translation
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder          -- - but these are spans!
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    map_symbol :: cid -> symbol1 -> Set.Set symbol2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    --properties of comorphisms
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder    is_model_transportable :: cid -> Bool
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    -- a comorphism (\phi, \alpha, \beta) is model-transportable
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    -- if for any signature \Sigma, any \Sigma-model M and any \phi(\Sigma)-model N
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    -- for any isomorphism           h : \beta_\Sigma(N) -> M
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    -- there exists an isomorphism   h': N -> M' such that \beta_\Sigma(h') = h
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder    has_model_expansion :: cid -> Bool
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder    is_weakly_amalgamable :: cid -> Bool
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder    --default implementation for properties
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    is_model_transportable _ = False
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder    has_model_expansion _ = False
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder    is_weakly_amalgamable _ = False
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder    constituents :: cid -> [String]
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder    -- default implementation
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder    constituents cid = [language_name cid]
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    map_sentence = failMapSentence
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder    map_symbol = errMapSymbol
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder
27912d626bf179b82fcb337077e5cd9653bb71cfChristian MaedertargetSublogic :: Comorphism cid
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski         => cid -> sublogics2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedertargetSublogic cid = maybe (error ("Logic.Comorphism: " ++
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder                                   language_name cid ++
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder                                   " does not provide a mapping for it's " ++
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                                   "source sublogic"))
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                           id $ mapSublogic cid $ sourceSublogic cid
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder-- | this function is base on 'map_theory' using no sentences as input
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maedermap_sign :: Comorphism cid
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder         => cid -> sign1 -> Result (sign2,[Named sentence2])
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maedermap_sign cid sign = wrapMapTheory cid (sign,[])
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermapDefaultMorphism :: Comorphism cid
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder         => cid -> morphism1 -> Result morphism2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermapDefaultMorphism cid mor = do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder  let src = sourceLogic cid
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder  (sig1, _) <- map_sign cid $ dom src mor
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder  (sig2, _) <- map_sign cid $ cod src mor
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder  inclusion (targetLogic cid) sig1 sig2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederfailMapSentence :: Comorphism cid
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder         => cid -> sign1 -> sentence1 -> Result sentence2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederfailMapSentence cid _ _ =
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder    fail $ "Unsupported sentence translation " ++ show cid
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedererrMapSymbol :: Comorphism cid
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder         => cid -> symbol1 -> Set.Set symbol2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedererrMapSymbol cid _ = error $ "no symbol mapping for " ++ show cid
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- | use this function instead of 'map_theory'
975642b989852fc24119c59cf40bc1af653608ffChristian MaederwrapMapTheory :: Comorphism cid
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            => cid -> (sign1, [Named sentence1])
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder                   -> Result (sign2, [Named sentence2])
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederwrapMapTheory cid (sign, sens) =
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder      case sourceSublogic cid of
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder        sub -> case minSublogic sign of
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder          sigLog -> case foldl join sigLog
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                    $ map (minSublogic . sentence) sens of
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder            senLog ->
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder              if isSubElem senLog sub
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder                 then map_theory cid (sign, sens)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                 else fail $ "for '" ++ language_name cid ++
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder                           "' expected sublogic '" ++
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder                           concat (sublogic_names sub) ++
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                           "'\n but found sublogic '" ++
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                           concat (sublogic_names senLog) ++
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                           "' with signature sublogic '" ++
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder                           concat (sublogic_names sigLog) ++ "'\n" ++
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder                 show (vcat $ pretty sign : map
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder                                (print_named $ sourceLogic cid) sens)
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                    -> (sign1, [Named sentence1])
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder                    -> (sign2, [Named sentence2])
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder    (mapSig sign, map (mapNamed mapSen) sens)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder                   -> (sign1 -> sentence1 -> m sentence2)
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder                   -> (sign1, [Named sentence1])
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder                   -> m (sign2, [Named sentence2])
2ac1742771a267119f1d839054b5e45d0a468085Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder       (sign',sens') <- mapSig sign
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder       sens'' <- mapM (mapNamedM $ mapSen sign) sens
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder       return (sign', disambiguateSens Set.empty . nameSens $ sens' ++ sens'')
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maedertype IdComorphism lid sublogics = InclComorphism lid sublogics
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederdata InclComorphism lid sublogics =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder    InclComorphism { inclusion_logic :: lid
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder                   , inclusion_source_sublogic :: sublogics
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder                   , inclusion_target_sublogic :: sublogics
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder                   }
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder-- | construction of an identity comorphism
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermkIdComorphism :: (Logic lid sublogics
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski                      basic_spec sentence symb_items symb_map_items
                      sign morphism symbol raw_symbol proof_tree) =>
                  lid -> sublogics -> IdComorphism lid sublogics
mkIdComorphism lid sub =
    InclComorphism { inclusion_logic = lid
                   , inclusion_source_sublogic = sub
                   , inclusion_target_sublogic = sub
                   }

-- | construction of an inclusion comorphism
mkInclComorphism :: (Logic lid sublogics
                           basic_spec sentence symb_items symb_map_items
                           sign morphism symbol raw_symbol proof_tree,
                     Monad m) =>
                    lid -> sublogics -> sublogics
                 -> m (InclComorphism lid sublogics)
mkInclComorphism lid srcSub trgSub =
    if isSubElem srcSub trgSub
    then return $ InclComorphism { inclusion_logic = lid
                                 , inclusion_source_sublogic = srcSub
                                 , inclusion_target_sublogic = trgSub
                                 }
    else fail ("mkInclComorphism: first sublogic must be a "++
               "subElem of the second sublogic")


instance Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree =>
   Show (InclComorphism lid sublogics)
   where
   show = language_name

instance Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree =>
         Language (InclComorphism lid sublogics) where
           language_name (InclComorphism lid sub_src sub_trg) =
               if sub_src == sub_trg
               then "id_" ++ language_name lid ++
                    if null (sblName sub_src)
                    then "" else "." ++ (sblName sub_src)
               else "incl_" ++ language_name lid ++ ": " ++
                    sblName sub_src ++ " -> " ++ sblName sub_trg
             where sblName sub = case sublogic_names sub of
                                   [] -> error "language_name IdComorphism"
                                   h : _ -> h

instance Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree =>
         Comorphism (IdComorphism lid sublogics)
          lid sublogics
          basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree
          lid sublogics
          basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree
         where
           sourceLogic = inclusion_logic
           targetLogic = inclusion_logic
           sourceSublogic = inclusion_source_sublogic
           mapSublogic incC subl =
               if subl == inclusion_source_sublogic incC
               then Just $ inclusion_target_sublogic incC
               else Nothing
           map_theory _ = return
           map_morphism _ = return
           map_sentence _ = \_ -> return
           map_symbol _ = Set.singleton
           constituents cid =
               if inclusion_source_sublogic cid
                      == inclusion_target_sublogic cid
               then []
               else [language_name cid]
           is_model_transportable _ = True
           has_model_expansion _ = True
           is_weakly_amalgamable _ = True

data CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show

instance (Language cid1, Language cid2)
          => Language (CompComorphism cid1 cid2) where
   language_name (CompComorphism cid1 cid2) =
     language_name cid1++ ";" ++language_name cid2


instance (Comorphism cid1
            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 cid2
            lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
                sign4 morphism4 symbol4 raw_symbol4 proof_tree4
            lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
                sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
          => Comorphism (CompComorphism cid1 cid2)
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
              sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
              sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
   sourceLogic (CompComorphism cid1 _) =
     sourceLogic cid1
   targetLogic (CompComorphism _ cid2) =
     targetLogic cid2
   sourceSublogic (CompComorphism cid1 _) =
     sourceSublogic cid1
   mapSublogic (CompComorphism cid1 cid2) sl =
         mapSublogic cid1 sl >>=
           (\ y -> mapSublogic cid2 $
          forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2) y)
   map_sentence (CompComorphism cid1 cid2) =
       \si1 se1 ->
         do (si2,_) <- map_sign cid1 si1
            se2 <- map_sentence cid1 si1 se1
            (si2', se2') <- coerceBasicTheory
                (targetLogic cid1) (sourceLogic cid2)
                "Mapping sentence along comorphism" (si2, [makeNamed "" se2])
            case se2' of
                [x] -> map_sentence cid2 si2' $ sentence x
                _ -> error "CompComorphism.map_sentence"

   map_theory (CompComorphism cid1 cid2) =
       \ti1 ->
         do ti2 <- map_theory cid1 ti1
            ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)
                        "Mapping theory along comorphism" ti2
            wrapMapTheory cid2 ti2'

   map_morphism (CompComorphism cid1 cid2) = \ m1 ->
       do m2 <- map_morphism cid1 m1
          m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)
                  "Mapping signature morphism along comorphism"m2
          map_morphism cid2 m3

   map_symbol (CompComorphism cid1 cid2) = \ s1 ->
         let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)
         in Set.unions
                (map (map_symbol cid2 . mycast)
                 (Set.toList (map_symbol cid1 s1)))
   constituents (CompComorphism cid1 cid2) =
      constituents cid1 ++ constituents cid2

   is_model_transportable (CompComorphism cid1 cid2) =
       is_model_transportable cid1 && is_model_transportable cid2

   has_model_expansion (CompComorphism cid1 cid2) =
        has_model_expansion cid1 && has_model_expansion cid2

   is_weakly_amalgamable (CompComorphism cid1 cid2) =
        is_weakly_amalgamable cid1 && is_weakly_amalgamable cid2