hets/Logic/Comorphism.hs

	Comorphism.hs revision 6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fc
c1d71ac637c449feb0a25369f029397e6a1f241cChristian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder{- |
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule      :  $Header$
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederDescription :  central interface (type class) for logic translations (comorphisms) in Hets
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederCopyright   :  (c) Till Mossakowski, Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer  :  till@informatik.uni-bremen.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability   :  provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability :  non-portable (via Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederCentral interface (type class) for logic translations (comorphisms) in Hets
44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski   These are just collections of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   functions between (some of) the types of logics.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowski   References: see Logic.hs
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-}
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimodule Logic.Comorphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    ( CompComorphism(..)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    , InclComorphism
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder    , inclusion_logic
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder    , inclusion_source_sublogic
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder    , inclusion_target_sublogic
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder    , mkInclComorphism
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder    , mkIdComorphism
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder    , Comorphism(..)
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder    , targetSublogic
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    , map_sign
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder    , ext_map_sign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    , mapDefaultMorphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    , wrapMapTheory
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    , simpleTheoryMapping
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    , mkTheoryMapping
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder    ) where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Logic.Logic
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Logic.ExtSign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Logic.Coerce
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Data.Set as Set
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.ExtSign
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederimport Common.Result
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.ProofUtils
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskiimport Common.AS_Annotation
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskiimport Common.Doc
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskiimport Common.DocUtils
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskiclass (Language cid,
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski       Logic lid1 sublogics1
bba825b39570777866d560bfde3807731131097eKlaus Luettich        basic_spec1 sentence1 symb_items1 symb_map_items1
bba825b39570777866d560bfde3807731131097eKlaus Luettich        sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder       Logic lid2 sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski        basic_spec2 sentence2 symb_items2 symb_map_items2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder        sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski  Comorphism cid
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski             | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu  where
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu    -- source and target logic and sublogic
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu    -- the source sublogic is the maximal one for which the comorphism works
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu    sourceLogic :: cid -> lid1
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu    sourceSublogic :: cid -> sublogics1
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu    targetLogic :: cid -> lid2
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu    -- finer information of target sublogics corresponding to source sublogics
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu    -- this function must be partial because mapTheory is partial
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu    mapSublogic :: cid -> sublogics1 -> Maybe sublogics2
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu    -- the translation functions are partial
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu    -- because the target may be a sublanguage
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu    -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu    -- cover theoroidal comorphisms as well
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski    map_theory :: cid -> (sign1,[Named sentence1])
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski                      -> Result (sign2,[Named sentence2])
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski    map_morphism :: cid -> morphism1 -> Result morphism2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder          -- also covers semi-comorphisms
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder          -- with no sentence translation
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder          -- - but these are spans!
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder    map_symbol :: cid -> symbol1 -> Set.Set symbol2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder    --properties of comorphisms
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder    is_model_transportable :: cid -> Bool
bba825b39570777866d560bfde3807731131097eKlaus Luettich    -- a comorphism (\phi, \alpha, \beta) is model-transportable
bba825b39570777866d560bfde3807731131097eKlaus Luettich    -- if for any signature \Sigma,
bba825b39570777866d560bfde3807731131097eKlaus Luettich    -- any \Sigma-model M and any \phi(\Sigma)-model N
bba825b39570777866d560bfde3807731131097eKlaus Luettich    -- for any isomorphism           h : \beta_\Sigma(N) -> M
bba825b39570777866d560bfde3807731131097eKlaus Luettich    -- there exists an isomorphism   h': N -> M' such that \beta_\Sigma(h') = h
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder    has_model_expansion :: cid -> Bool
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder    is_weakly_amalgamable :: cid -> Bool
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder    --default implementation for properties
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder    is_model_transportable _ = False
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder    has_model_expansion _ = False
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder    is_weakly_amalgamable _ = False
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder    constituents :: cid -> [String]
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder    -- default implementation
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder    constituents cid = [language_name cid]
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder    map_sentence = failMapSentence
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder    map_symbol = errMapSymbol
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedertargetSublogic :: Comorphism cid
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder         => cid -> sublogics2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedertargetSublogic cid = maybe (error ("Logic.Comorphism: " ++
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder                                   language_name cid ++
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder                                   " does not provide a mapping for it's " ++
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder                                   "source sublogic"))
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder                           id $ mapSublogic cid $ sourceSublogic cid
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder-- | this function is base on 'map_theory' using no sentences as input
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maedermap_sign :: Comorphism cid
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder         => cid -> sign1 -> Result (sign2,[Named sentence2])
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maedermap_sign cid sign = wrapMapTheory cid (sign,[])
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederext_map_sign :: Comorphism cid
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder         => cid -> ExtSign sign1 symbol1
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder                -> Result (ExtSign sign2 symbol2, [Named sentence2])
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederext_map_sign cid (ExtSign sign _) = do
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder    (sign2, sens2) <- map_sign cid sign
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder    return (makeExtSign (targetLogic cid) sign2, sens2)
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaedermapDefaultMorphism :: Comorphism cid
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder         => cid -> morphism1 -> Result morphism2
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaedermapDefaultMorphism cid mor = do
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder  let src = sourceLogic cid
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder  (sig1, _) <- map_sign cid $ dom src mor
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder  (sig2, _) <- map_sign cid $ cod src mor
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder  inclusion (targetLogic cid) sig1 sig2
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederfailMapSentence :: Comorphism cid
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder         => cid -> sign1 -> sentence1 -> Result sentence2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederfailMapSentence cid _ _ =
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder    fail $ "Unsupported sentence translation " ++ show cid
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedererrMapSymbol :: Comorphism cid
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder         => cid -> symbol1 -> Set.Set symbol2
53310804002cd9e3c9c5844db3b984abcf001788Christian MaedererrMapSymbol cid _ = error $ "no symbol mapping for " ++ show cid
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- | use this function instead of 'map_theory'
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederwrapMapTheory :: Comorphism cid
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder            => cid -> (sign1, [Named sentence1])
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski                   -> Result (sign2, [Named sentence2])
797595aad6dfd626bc1c9df52616f1ac4235c669Till MossakowskiwrapMapTheory cid (sign, sens) =
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski      case sourceSublogic cid of
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski        sub -> case minSublogic sign of
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski          sigLog -> case foldl join sigLog
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder                    $ map (minSublogic . sentence) sens of
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski            senLog ->
933baca0720dae81434de384b32a93b47e754d09Christian Maeder              if isSubElem senLog sub
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                 then map_theory cid (sign, sens)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                 else fail $ "for '" ++ language_name cid ++
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                           "' expected sublogic '" ++
586af0e9490a14dd3075095692b584c652584875Till Mossakowski                           concat (sublogic_names sub) ++
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder                           "'\n but found sublogic '" ++
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder                           concat (sublogic_names senLog) ++
933baca0720dae81434de384b32a93b47e754d09Christian Maeder                           "' with signature sublogic '" ++
933baca0720dae81434de384b32a93b47e754d09Christian Maeder                           concat (sublogic_names sigLog) ++ "'\n" ++
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                 show (vcat $ pretty sign : map
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                                (print_named $ sourceLogic cid) sens)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskisimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
586af0e9490a14dd3075095692b584c652584875Till Mossakowski                    -> (sign1, [Named sentence1])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                    -> (sign2, [Named sentence2])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskisimpleTheoryMapping mapSig mapSen (sign,sens) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    (mapSig sign, map (mapNamed mapSen) sens)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder                   -> (sign1 -> sentence1 -> m sentence2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                   -> (sign1, [Named sentence1])
933baca0720dae81434de384b32a93b47e754d09Christian Maeder                   -> m (sign2, [Named sentence2])
933baca0720dae81434de384b32a93b47e754d09Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do
933baca0720dae81434de384b32a93b47e754d09Christian Maeder       (sign',sens') <- mapSig sign
bba825b39570777866d560bfde3807731131097eKlaus Luettich       sens'' <- mapM (mapNamedM $ mapSen sign) sens
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder       return (sign', disambiguateSens Set.empty . nameSens $ sens' ++ sens'')
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder-- type IdComorphism lid sublogics = InclComorphism lid sublogics
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowskidata InclComorphism lid sublogics =
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu    InclComorphism { inclusion_logic :: lid
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu                   , inclusion_source_sublogic :: sublogics
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu                   , inclusion_target_sublogic :: sublogics
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu                   }
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- | construction of an identity comorphism
ca8550c6d47234042130bdc10a152806ecbc9832Christian MaedermkIdComorphism :: (Logic lid sublogics
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder                      basic_spec sentence symb_items symb_map_items
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder                      sign morphism symbol raw_symbol proof_tree) =>
ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder                  lid -> sublogics -> InclComorphism lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimkIdComorphism lid sub =
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder    InclComorphism { inclusion_logic = lid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                   , inclusion_source_sublogic = sub
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                   , inclusion_target_sublogic = sub
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                   }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder-- | construction of an inclusion comorphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimkInclComorphism :: (Logic lid sublogics
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder                           basic_spec sentence symb_items symb_map_items
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder                           sign morphism symbol raw_symbol proof_tree,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                     Monad m) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski                    lid -> sublogics -> sublogics
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder                 -> m (InclComorphism lid sublogics)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimkInclComorphism lid srcSub trgSub =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    if isSubElem srcSub trgSub
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski    then return $ InclComorphism { inclusion_logic = lid
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder                                 , inclusion_source_sublogic = srcSub
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder                                 , inclusion_target_sublogic = trgSub
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski                                 }
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder    else fail ("mkInclComorphism: first sublogic must be a "++
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski               "subElem of the second sublogic")
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski
bba825b39570777866d560bfde3807731131097eKlaus Luettich
bba825b39570777866d560bfde3807731131097eKlaus Luettichinstance Logic lid sublogics
bba825b39570777866d560bfde3807731131097eKlaus Luettich        basic_spec sentence symb_items symb_map_items
bba825b39570777866d560bfde3807731131097eKlaus Luettich        sign morphism symbol raw_symbol proof_tree =>
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder   Show (InclComorphism lid sublogics)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder   where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski   show = language_name
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder
53310804002cd9e3c9c5844db3b984abcf001788Christian Maederinstance Logic lid sublogics
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder        basic_spec sentence symb_items symb_map_items
c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian Maeder        sign morphism symbol raw_symbol proof_tree =>
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder         Language (InclComorphism lid sublogics) where
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder           language_name (InclComorphism lid sub_src sub_trg) =
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder               if sub_src == sub_trg
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski               then "id_" ++ language_name lid ++
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder                    if null (sblName sub_src)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder                    then "" else "." ++ (sblName sub_src)
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder               else "incl_" ++ language_name lid ++ ": " ++
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder                    sblName sub_src ++ " -> " ++ sblName sub_trg
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder             where sblName sub = case sublogic_names sub of
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder                                   [] -> error "language_name IdComorphism"
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder                                   h : _ -> h
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder
53310804002cd9e3c9c5844db3b984abcf001788Christian Maederinstance Logic lid sublogics
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder        basic_spec sentence symb_items symb_map_items
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski        sign morphism symbol raw_symbol proof_tree =>
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder         Comorphism (InclComorphism lid sublogics)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski          lid sublogics
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder          basic_spec sentence symb_items symb_map_items
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder          sign morphism symbol raw_symbol proof_tree
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder          lid sublogics
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder          basic_spec sentence symb_items symb_map_items
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder          sign morphism symbol raw_symbol proof_tree
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder         where
933baca0720dae81434de384b32a93b47e754d09Christian Maeder           sourceLogic = inclusion_logic
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu           targetLogic = inclusion_logic
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu           sourceSublogic = inclusion_source_sublogic
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu           mapSublogic incC subl =
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu               if subl == inclusion_source_sublogic incC--isSubOf
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu               then Just $ inclusion_target_sublogic incC
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu               else Nothing
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu           map_theory _ = return
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu           map_morphism _ = return
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu           map_sentence _ = \_ -> return
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu           map_symbol _ = Set.singleton
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu           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