Comorphism.hs revision c44c23429c72f3a709e22a18f2ed6f05fc8cc765
c1d71ac637c449feb0a25369f029397e6a1f241cChristian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
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@tzi.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable (via Logic)
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.
af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowski References: see Logic.hs
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maederclass (Language cid,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid1 sublogics1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid2 sublogics2
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski 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
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder | cid -> lid1, cid -> lid2
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- source and target logic and sublogic
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- the source sublogic is the maximal one for which the comorphism works
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski sourceLogic :: cid -> lid1
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic :: cid -> sublogics1
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski targetLogic :: cid -> lid2
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- finer information of target sublogics corresponding to source sublogics
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski mapSublogic :: cid -> sublogics1 -> sublogics2
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -- the translation functions are partial
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- because the target may be a sublanguage
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- cover theoroidal comorphisms as well
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski map_theory :: cid -> (sign1,[Named sentence1])
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -> Result (sign2,[Named sentence2])
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- also covers semi-comorphisms
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- with no sentence translation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- - but these are spans!
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder map_symbol :: cid -> symbol1 -> Set.Set symbol2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu --properties of comorphisms
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu is_model_transportable :: cid -> Bool
e8e532bb58c6c550866a9603cf388df53cc03872Christian Maeder -- default implementation
e8e532bb58c6c550866a9603cf388df53cc03872Christian Maeder is_model_transportable _ = False
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu -- a comorphism (\phi, \alpha, \beta) is model-transportable
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu -- if for any signature \Sigma, any \Sigma-model M and any \phi(\Sigma)-model N
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu -- for any isomorphism h : \beta_\Sigma(N) -> M
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu -- there exists an isomorphism h': N -> M' such that \beta_\Sigma(h') = h
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski constituents :: cid -> [String]
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski -- default implementation
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski constituents cid = [language_name cid]
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 = mapSublogic cid $ sourceSublogic cid
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder-- | this function is base on 'map_theory' using no sentences as input
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedermap_sign :: Comorphism cid
19298cbfd6ee2abd904f3181af7760b965b822c3Christian 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
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder => cid -> sign1 -> Result (sign2,[Named sentence2])
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maedermap_sign cid sign = wrapMapTheory cid (sign,[])
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapDefaultMorphism :: 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 -> morphism1 -> Result morphism2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapDefaultMorphism cid mor = do
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let src = sourceLogic cid
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (sig1, _) <- map_sign cid $ dom src mor
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (sig2, _) <- map_sign cid $ cod src mor
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder inclusion (targetLogic cid) sig1 sig2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederfailMapSentence :: 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 -> sentence1 -> Result sentence2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederfailMapSentence cid _ _ =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fail $ "Unsupported sentence translation " ++ show cid
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedererrMapSymbol :: 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 -> symbol1 -> Set.Set symbol2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedererrMapSymbol cid _ = error $ "no symbol mapping for " ++ show cid
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder-- | use this function instead of 'map_theory'
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaederwrapMapTheory :: Comorphism cid
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder => cid -> (sign1, [Named sentence1])
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder -> Result (sign2, [Named sentence2])
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederwrapMapTheory cid (sign, sens) =
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder case sourceSublogic cid of
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder sub -> case minSublogic sign of
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder sigLog -> case foldl join sigLog
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder $ map (minSublogic . sentence) sens of
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder if isSubElem senLog sub
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder then map_theory cid (sign, sens)
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder else fail $ "for '" ++ language_name cid ++
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder "' expected sublogic '" ++
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder concat (sublogic_names sub) ++
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder "'\n but found sublogic '" ++
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder concat (sublogic_names senLog) ++
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder "' with signature sublogic '" ++
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder concat (sublogic_names sigLog) ++ "'\n" ++
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder show (vcat $ pretty sign : map
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder (print_named $ sourceLogic cid) sens)
53310804002cd9e3c9c5844db3b984abcf001788Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -> (sign1, [Named sentence1])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> (sign2, [Named sentence2])
53310804002cd9e3c9c5844db3b984abcf001788Christian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (mapSig sign, map (mapNamed mapSen) sens)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -> (sign1 -> sentence1 -> m sentence2)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -> (sign1, [Named sentence1])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> m (sign2, [Named sentence2])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (sign',sens') <- mapSig sign
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sens'' <- mapM (mapNamedM $ mapSen sign) sens
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder return (sign', disambiguateSens Set.empty . nameSens $ sens' ++ sens'')
53310804002cd9e3c9c5844db3b984abcf001788Christian Maederdata IdComorphism lid sublogics =
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder IdComorphism lid sublogics
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowskiinstance Logic lid sublogics
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski basic_spec sentence symb_items symb_map_items
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski Show (IdComorphism lid sublogics)
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski show = language_name
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
586af0e9490a14dd3075095692b584c652584875Till Mossakowski Language (IdComorphism lid sublogics) where
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder language_name (IdComorphism lid sub) =
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder case sublogic_names sub of
933baca0720dae81434de384b32a93b47e754d09Christian Maeder [] -> error "language_name IdComorphism"
933baca0720dae81434de384b32a93b47e754d09Christian Maeder h : _ -> "id_" ++ language_name lid ++ "." ++ h
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
586af0e9490a14dd3075095692b584c652584875Till Mossakowski Comorphism (IdComorphism lid sublogics)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sign morphism symbol raw_symbol proof_tree
933baca0720dae81434de384b32a93b47e754d09Christian Maeder sourceLogic (IdComorphism lid _sub) = lid
933baca0720dae81434de384b32a93b47e754d09Christian Maeder targetLogic (IdComorphism lid _sub) = lid
933baca0720dae81434de384b32a93b47e754d09Christian Maeder sourceSublogic (IdComorphism _lid sub) = sub
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski mapSublogic _ = id
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder map_theory _ = return
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_morphism _ = return
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_sentence _ = \_ -> return
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski constituents _ = []
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu is_model_transportable _ = True
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
ca8550c6d47234042130bdc10a152806ecbc9832Christian Maederinstance (Language cid1, Language cid2)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder => Language (CompComorphism cid1 cid2) where
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder language_name (CompComorphism cid1 cid2) =
ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder language_name cid1++ ";" ++language_name cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Comorphism cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski 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
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid2
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder => Comorphism (CompComorphism cid1 cid2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sourceLogic (CompComorphism cid1 _) =
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski sourceLogic cid1
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder targetLogic (CompComorphism _ cid2) =
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski targetLogic cid2
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sourceSublogic (CompComorphism cid1 _) =
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic cid1
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder mapSublogic (CompComorphism cid1 cid2) =
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder mapSublogic cid2
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder . forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2)
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski . mapSublogic cid1
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder map_sentence (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do (si2,_) <- map_sign cid1 si1
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder se2 <- map_sentence cid1 si1 se1
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (si2', se2') <- coerceBasicTheory
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (targetLogic cid1) (sourceLogic cid2)
c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian Maeder "Mapping sentence along comorphism" (si2, [makeNamed "" se2])
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder [x] -> map_sentence cid2 si2' $ sentence x
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder map_theory (CompComorphism cid1 cid2) =
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder do ti2 <- map_theory cid1 ti1
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder "Mapping theory along comorphism" ti2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder wrapMapTheory cid2 ti2'
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder map_morphism (CompComorphism cid1 cid2) = \ m1 ->
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder do m2 <- map_morphism cid1 m1
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski "Mapping signature morphism along comorphism"m2
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_morphism cid2 m3
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder map_symbol (CompComorphism cid1 cid2) = \ s1 ->
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (map (map_symbol cid2 . mycast)
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder (Set.toList (map_symbol cid1 s1)))
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder constituents (CompComorphism cid1 cid2) =
933baca0720dae81434de384b32a93b47e754d09Christian Maeder constituents cid1 ++ constituents cid2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu is_model_transportable (CompComorphism cid1 cid2) =
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu is_model_transportable cid1 && is_model_transportable cid2