Comorphism.hs revision e8e532bb58c6c550866a9603cf388df53cc03872
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederModule : $Header$
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederDescription : central interface (type class) for logic translations (comorphisms) in Hets
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederMaintainer : till@tzi.de
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederStability : provisional
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederPortability : non-portable (via Logic)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederCentral interface (type class) for logic translations (comorphisms) in Hets
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder These are just collections of
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder functions between (some of) the types of logics.
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder References: see Logic.hs
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederimport qualified Data.Set as Set
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maederclass (Language cid,
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder Logic lid1 sublogics1
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder Logic lid2 sublogics2
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder Comorphism cid
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder | cid -> lid1, cid -> lid2
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder -- source and target logic and sublogic
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder -- the source sublogic is the maximal one for which the comorphism works
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder sourceLogic :: cid -> lid1
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder sourceSublogic :: cid -> sublogics1
d2e1ea7e00412ba6a7c29b491e6fca6ca4d6fb18Christian Maeder targetLogic :: cid -> lid2
d2e1ea7e00412ba6a7c29b491e6fca6ca4d6fb18Christian Maeder -- finer information of target sublogics corresponding to source sublogics
d2e1ea7e00412ba6a7c29b491e6fca6ca4d6fb18Christian Maeder mapSublogic :: cid -> sublogics1 -> sublogics2
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder -- the translation functions are partial
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder -- because the target may be a sublanguage
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder -- cover theoroidal comorphisms as well
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian Maeder map_theory :: cid -> (sign1,[Named sentence1])
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian Maeder -> Result (sign2,[Named sentence2])
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian Maeder map_morphism :: cid -> morphism1 -> Result morphism2
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder -- also covers semi-comorphisms
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder -- with no sentence translation
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder -- - but these are spans!
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder map_symbol :: cid -> symbol1 -> Set.Set symbol2
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder --properties of comorphisms
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder is_model_transportable :: cid -> Bool
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder -- default implementation
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder is_model_transportable _ = False
dcf7a9c571e15547fd5302de8064663a486c26faChristian Maeder -- a comorphism (\phi, \alpha, \beta) is model-transportable
918c36f05614a959f186fe02bd4f943e0a1d91e3Christian Maeder -- if for any signature \Sigma, any \Sigma-model M and any \phi(\Sigma)-model N
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder -- for any isomorphism h : \beta_\Sigma(N) -> M
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder -- there exists an isomorphism h': N -> M' such that \beta_\Sigma(h') = h
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder constituents :: cid -> [String]
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder -- default implementation
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder constituents cid = [language_name cid]
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaedertargetSublogic :: Comorphism cid
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder => cid -> sublogics2
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaedertargetSublogic cid = mapSublogic cid $ sourceSublogic cid
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder-- | this function is base on 'map_theory' using no sentences as input
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maedermap_sign :: Comorphism cid
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder => cid -> sign1 -> Result (sign2,[Named sentence2])
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maedermap_sign cid sign = wrapMapTheory cid (sign,[])
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian MaedermapDefaultMorphism :: Comorphism cid
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder => cid -> morphism1 -> Result morphism2
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaedermapDefaultMorphism cid mor = do
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder let src = sourceLogic cid
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder (sig1, _) <- map_sign cid $ dom src mor
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder (sig2, _) <- map_sign cid $ cod src mor
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder inclusion (targetLogic cid) sig1 sig2
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederfailMapSentence :: Comorphism cid
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder => cid -> sign1 -> sentence1 -> Result sentence2
16e124196c6b204769042028c74f533509c9b5d3Christian MaederfailMapSentence cid _ _ =
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder fail $ "Unsupported sentence translation " ++ show cid
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian MaedererrMapSymbol :: Comorphism cid
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
32562a567baac248a00782d2727716c13117dc4aChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
32562a567baac248a00782d2727716c13117dc4aChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
32562a567baac248a00782d2727716c13117dc4aChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
32562a567baac248a00782d2727716c13117dc4aChristian Maeder => cid -> symbol1 -> Set.Set symbol2
32562a567baac248a00782d2727716c13117dc4aChristian MaedererrMapSymbol cid _ = error $ "no symbol mapping for " ++ show cid
32562a567baac248a00782d2727716c13117dc4aChristian Maeder-- | use this function instead of 'map_theory'
32562a567baac248a00782d2727716c13117dc4aChristian MaederwrapMapTheory :: Comorphism cid
32562a567baac248a00782d2727716c13117dc4aChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
32562a567baac248a00782d2727716c13117dc4aChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
32562a567baac248a00782d2727716c13117dc4aChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
32562a567baac248a00782d2727716c13117dc4aChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
32562a567baac248a00782d2727716c13117dc4aChristian Maeder => cid -> (sign1, [Named sentence1])
32562a567baac248a00782d2727716c13117dc4aChristian Maeder -> Result (sign2, [Named sentence2])
32562a567baac248a00782d2727716c13117dc4aChristian MaederwrapMapTheory cid (sign, sens) =
57a32fb13a6acc1748bb1c68028cb2382d6bdb3fChristian Maeder case sourceSublogic cid of
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder sub -> case minSublogic sign of
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder sigLog -> case foldl join sigLog
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder $ map (minSublogic . sentence) sens of
32562a567baac248a00782d2727716c13117dc4aChristian Maeder if isSubElem senLog sub
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder then map_theory cid (sign, sens)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder else fail $ "for '" ++ language_name cid ++
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder "' expected sublogic '" ++
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder concat (sublogic_names sub) ++
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder "'\n but found sublogic '" ++
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder concat (sublogic_names senLog) ++
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder "' with signature sublogic '" ++
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder concat (sublogic_names sigLog) ++ "'\n" ++
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder show (vcat $ pretty sign : map
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder (print_named $ sourceLogic cid) sens)
904efdc72d29946a966c65fcc624068f38127c84Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder -> (sign1, [Named sentence1])
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder -> (sign2, [Named sentence2])
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (mapSig sign, map (mapNamed mapSen) sens)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder -> (sign1 -> sentence1 -> m sentence2)
e68cfdc781c4fd65d42f99173efc2aef342ce0eeChristian Maeder -> (sign1, [Named sentence1])
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder -> m (sign2, [Named sentence2])
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder (sign',sens') <- mapSig sign
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder sens'' <- mapM (mapNamedM $ mapSen sign) sens
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder return (sign', disambiguateSens Set.empty . nameSens $ sens' ++ sens'')
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederdata IdComorphism lid sublogics =
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder IdComorphism lid sublogics
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederinstance Logic lid sublogics
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder basic_spec sentence symb_items symb_map_items
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder sign morphism symbol raw_symbol proof_tree =>
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Show (IdComorphism lid sublogics)
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder show = language_name
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederinstance Logic lid sublogics
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder basic_spec sentence symb_items symb_map_items
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder sign morphism symbol raw_symbol proof_tree =>
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder Language (IdComorphism lid sublogics) where
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder language_name (IdComorphism lid sub) =
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder case sublogic_names sub of
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder [] -> error "language_name IdComorphism"
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder h : _ -> "id_" ++ language_name lid ++ "." ++ h
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance Logic lid sublogics
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder basic_spec sentence symb_items symb_map_items
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder sign morphism symbol raw_symbol proof_tree =>
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Comorphism (IdComorphism lid sublogics)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder lid sublogics
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder basic_spec sentence symb_items symb_map_items
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder sign morphism symbol raw_symbol proof_tree
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder lid sublogics
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder basic_spec sentence symb_items symb_map_items
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder sign morphism symbol raw_symbol proof_tree
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder sourceLogic (IdComorphism lid _sub) = lid
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder targetLogic (IdComorphism lid _sub) = lid
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder sourceSublogic (IdComorphism _lid sub) = sub
dcf7a9c571e15547fd5302de8064663a486c26faChristian Maeder mapSublogic _ = id
918c36f05614a959f186fe02bd4f943e0a1d91e3Christian Maeder map_theory _ = return
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder map_morphism _ = return
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder map_sentence _ = \_ -> return
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder constituents _ = []
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder is_model_transportable _ = True
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maederdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
0243238805d31e597195ef974e8e7eccb587a390Christian Maederinstance (Language cid1, Language cid2)
0a757184b9336a91b2ba735dd58c5ed4e4378e51Christian Maeder => Language (CompComorphism cid1 cid2) where
0a757184b9336a91b2ba735dd58c5ed4e4378e51Christian Maeder language_name (CompComorphism cid1 cid2) =
0a757184b9336a91b2ba735dd58c5ed4e4378e51Christian Maeder language_name cid1++ ";" ++language_name cid2
0243238805d31e597195ef974e8e7eccb587a390Christian Maederinstance (Comorphism cid1
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder Comorphism cid2
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder => Comorphism (CompComorphism cid1 cid2)
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder sourceLogic (CompComorphism cid1 _) =
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder sourceLogic cid1
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu targetLogic (CompComorphism _ cid2) =
2dbb344c4f3fe8f3b9c49db7f95f851d0472c2b2Christian Maeder targetLogic cid2
2dbb344c4f3fe8f3b9c49db7f95f851d0472c2b2Christian Maeder sourceSublogic (CompComorphism cid1 _) =
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder sourceSublogic cid1
2dbb344c4f3fe8f3b9c49db7f95f851d0472c2b2Christian Maeder mapSublogic (CompComorphism cid1 cid2) =
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu mapSublogic cid2
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder . forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2)
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder . mapSublogic cid1
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder map_sentence (CompComorphism cid1 cid2) =
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder do (si2,_) <- map_sign cid1 si1
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder se2 <- map_sentence cid1 si1 se1
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder (si2', se2') <- coerceBasicTheory
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder (targetLogic cid1) (sourceLogic cid2)
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder "Mapping sentence along comorphism" (si2, [emptyName se2])
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder [x] -> map_sentence cid2 si2' $ sentence x
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder map_theory (CompComorphism cid1 cid2) =
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder do ti2 <- map_theory cid1 ti1
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder "Mapping theory along comorphism" ti2
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder wrapMapTheory cid2 ti2'
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder map_morphism (CompComorphism cid1 cid2) = \ m1 ->
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder do m2 <- map_morphism cid1 m1
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder "Mapping signature morphism along comorphism"m2
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder map_morphism cid2 m3
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder map_symbol (CompComorphism cid1 cid2) = \ s1 ->
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder (map (map_symbol cid2 . mycast)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu (Set.toList (map_symbol cid1 s1)))
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder constituents (CompComorphism cid1 cid2) =
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu constituents cid1 ++ constituents cid2
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder is_model_transportable (CompComorphism cid1 cid2) =
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder is_model_transportable cid1 && is_model_transportable cid2