Comorphism.hs revision 53f347ab16f992d909f47a50bf2059f57f3c7ad0
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{-# LANGUAGE UndecidableInstances #-}
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{- |
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederModule : $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : interface and class for logic translations
ca010363454de207082dfaa4b753531ce2a34551Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ca010363454de207082dfaa4b753531ce2a34551Christian MaederMaintainer : till@informatik.uni-bremen.de
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederStability : provisional
ca010363454de207082dfaa4b753531ce2a34551Christian MaederPortability : non-portable (via Logic)
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maeder
ca010363454de207082dfaa4b753531ce2a34551Christian MaederCentral interface (type class) for logic translations (comorphisms) in Hets
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder These are just collections of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder functions between (some of) the types of logics.
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder References: see Logic.hs
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder-}
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian Maedermodule Logic.Comorphism
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder ( CompComorphism (..)
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder , InclComorphism
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder , inclusion_logic
fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maeder , inclusion_source_sublogic
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder , inclusion_target_sublogic
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder , mkInclComorphism
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder , mkIdComorphism
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder , Comorphism (..)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder , targetSublogic
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder , map_sign
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder , ext_map_sign
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder , mapDefaultMorphism
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder , wrapMapTheory
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder , simpleTheoryMapping
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder , mkTheoryMapping
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maeder , AnyComorphism (..)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder , idComorphism
1bc3627bdb66ecc1efe23eeaeca0ee1f3151ab14Christian Maeder , isIdComorphism
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder , isModelTransportable
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder , hasModelExpansion
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder , isWeaklyAmalgamable
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder , compComorphism
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder ) where
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederimport Logic.Logic
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Logic.Coerce
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Logic.ExtSign
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maederimport Common.ExtSign
08f8731b34de5dc1ced274594978ad8879c831bdChristian Maederimport Common.Result
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederimport Common.ProofUtils
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederimport Common.AS_Annotation
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederimport Common.Doc
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Common.DocUtils
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederimport qualified Data.Set as Set
eed6203a39f88e398d86431a66d367036a3d17baChristian Maederimport Data.Typeable
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederclass (Language cid,
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Logic lid1 sublogics1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Logic lid2 sublogics2
d48085f765fca838c1d972d2123601997174583dChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Comorphism cid
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder where
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- source and target logic and sublogic
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- the source sublogic is the maximal one for which the comorphism works
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sourceLogic :: cid -> lid1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sourceSublogic :: cid -> sublogics1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder targetLogic :: cid -> lid2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- finer information of target sublogics corresponding to source sublogics
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- this function must be partial because mapTheory is partial
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mapSublogic :: cid -> sublogics1 -> Maybe sublogics2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- the translation functions are partial
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- because the target may be a sublanguage
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- cover theoroidal comorphisms as well
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map_theory :: cid -> (sign1,[Named sentence1])
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -> Result (sign2,[Named sentence2])
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- also covers semi-comorphisms
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- with no sentence translation
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder -- - but these are spans!
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_sentence = failMapSentence
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map_symbol = errMapSymbol
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder extractModel :: cid -> sign1 -> proof_tree2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -> Result (sign1, [Named sentence1])
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder extractModel cid _ _ = fail
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder $ "extractModel not implemented for comorphism "
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder ++ language_name cid
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder --properties of comorphisms
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder is_model_transportable :: cid -> Bool
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- a comorphism (\phi, \alpha, \beta) is model-transportable
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder -- if for any signature \Sigma,
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- any \Sigma-model M and any \phi(\Sigma)-model N
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder -- for any isomorphism h : \beta_\Sigma(N) -> M
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -- there exists an isomorphism h': N -> M' such that \beta_\Sigma(h') = h
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder is_model_transportable _ = False
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder has_model_expansion :: cid -> Bool
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder has_model_expansion _ = False
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder is_weakly_amalgamable :: cid -> Bool
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder is_weakly_amalgamable _ = False
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder constituents :: cid -> [String]
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder constituents cid = [language_name cid]
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder isInclusionComorphism :: cid -> Bool
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder isInclusionComorphism _ = False
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedertargetSublogic :: Comorphism cid
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder => cid -> sublogics2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedertargetSublogic cid = maybe (top_sublogic $ targetLogic cid)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder id $ mapSublogic cid $ sourceSublogic cid
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- | this function is base on 'map_theory' using no sentences as input
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maedermap_sign :: Comorphism cid
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
3f7009c892b16d172314abbba83d663fa0d87a65Christian Maeder => cid -> sign1 -> Result (sign2,[Named sentence2])
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maedermap_sign cid sign = wrapMapTheory cid (sign,[])
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederext_map_sign :: Comorphism cid
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder => cid -> ExtSign sign1 symbol1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -> Result (ExtSign sign2 symbol2, [Named sentence2])
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederext_map_sign cid (ExtSign sign _) = do
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (sign2, sens2) <- map_sign cid sign
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder return (makeExtSign (targetLogic cid) sign2, sens2)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian MaedermapDefaultMorphism :: Comorphism cid
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder => cid -> morphism1 -> Result morphism2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedermapDefaultMorphism cid mor = do
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder (sig1, _) <- map_sign cid $ dom mor
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder (sig2, _) <- map_sign cid $ cod mor
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder inclusion (targetLogic cid) sig1 sig2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederfailMapSentence :: Comorphism cid
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder => cid -> sign1 -> sentence1 -> Result sentence2
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederfailMapSentence cid _ _ =
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder fail $ "Unsupported sentence translation " ++ show cid
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
13b24998210d193b38cae06485da6f06c61d7f62Christian MaedererrMapSymbol :: Comorphism cid
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder => cid -> sign1 -> symbol1 -> Set.Set symbol2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedererrMapSymbol cid _ _ = error $ "no symbol mapping for " ++ show cid
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- | use this function instead of 'map_theory'
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaederwrapMapTheory :: Comorphism cid
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder => cid -> (sign1, [Named sentence1])
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski -> Result (sign2, [Named sentence2])
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederwrapMapTheory cid (sign, sens) = let res = map_theory cid (sign, sens) in
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder if isIdComorphism $ Comorphism cid then res else case sourceSublogic cid of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sub -> case minSublogic sign of
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sigLog -> case foldl join sigLog
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder $ map (minSublogic . sentence) sens of
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder senLog ->
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski if isSubElem senLog sub
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder then res
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder else fail $ "for '" ++ language_name cid ++
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder "' expected sublogic '" ++
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder sublogicName sub ++
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder "'\n but found sublogic '" ++
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder sublogicName senLog ++
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder "' with signature sublogic '" ++
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder sublogicName sigLog ++ "'\n" ++
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder show (vcat $ pretty sign : map
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder (print_named $ sourceLogic cid) sens)
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -> (sign1, [Named sentence1])
46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder -> (sign2, [Named sentence2])
975642b989852fc24119c59cf40bc1af653608ffChristian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (mapSig sign, map (mapNamed mapSen) sens)
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -> (sign1 -> sentence1 -> m sentence2)
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder -> (sign1, [Named sentence1])
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder -> m (sign2, [Named sentence2])
13b24998210d193b38cae06485da6f06c61d7f62Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder (sign',sens') <- mapSig sign
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder sens'' <- mapM (mapNamedM $ mapSen sign) sens
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder return (sign', nameAndDisambiguate $ sens' ++ sens'')
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederdata InclComorphism lid sublogics = InclComorphism
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder { inclusion_logic :: lid
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder , inclusion_source_sublogic :: sublogics
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder , inclusion_target_sublogic :: sublogics }
fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maeder deriving Show
a1d523aa255a291c0154af764fbdb8597c445918Christian Maeder
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- | construction of an identity comorphism
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedermkIdComorphism :: (Logic lid sublogics
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder basic_spec sentence symb_items symb_map_items
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder sign morphism symbol raw_symbol proof_tree) =>
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder lid -> sublogics -> InclComorphism lid sublogics
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaedermkIdComorphism lid sub = InclComorphism
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder { inclusion_logic = lid
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder , inclusion_source_sublogic = sub
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder , inclusion_target_sublogic = sub }
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder-- | construction of an inclusion comorphism
13b24998210d193b38cae06485da6f06c61d7f62Christian MaedermkInclComorphism :: (Logic lid sublogics
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder basic_spec sentence symb_items symb_map_items
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder sign morphism symbol raw_symbol proof_tree,
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Monad m) =>
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder lid -> sublogics -> sublogics
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder -> m (InclComorphism lid sublogics)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedermkInclComorphism lid srcSub trgSub =
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder if isSubElem srcSub trgSub
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder then return $ InclComorphism
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder { inclusion_logic = lid
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder , inclusion_source_sublogic = srcSub
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder , inclusion_target_sublogic = trgSub }
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder else fail ("mkInclComorphism: first sublogic must be a "++
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder "subElem of the second sublogic")
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian Maederinstance (Language lid, Eq sublogics, Show sublogics, SublogicName sublogics)
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder => Language (InclComorphism lid sublogics) where
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder language_name (InclComorphism lid sub_src sub_trg) =
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder let sblName = sublogicName sub_src
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder lname = language_name lid
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder in if sub_src == sub_trg
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder then "id_" ++ lname ++
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder if null sblName
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder then "" else "." ++ sblName
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder else "incl_" ++ lname ++ ":" ++
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder sblName ++ "->" ++ sublogicName sub_trg
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederinstance Logic lid sublogics
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder basic_spec sentence symb_items symb_map_items
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder sign morphism symbol raw_symbol proof_tree =>
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder Comorphism (InclComorphism lid sublogics)
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder lid sublogics
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder basic_spec sentence symb_items symb_map_items
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder sign morphism symbol raw_symbol proof_tree
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder lid sublogics
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder basic_spec sentence symb_items symb_map_items
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder sign morphism symbol raw_symbol proof_tree
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder where
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder sourceLogic = inclusion_logic
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder targetLogic = inclusion_logic
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder sourceSublogic = inclusion_source_sublogic
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder mapSublogic cid subl =
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder if isSubElem subl $ inclusion_source_sublogic cid
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder then Just subl
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder else Nothing
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map_theory _ = return
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder map_morphism _ = return
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder map_sentence _ = \_ -> return
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map_symbol _ _ = Set.singleton
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder constituents cid =
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder if inclusion_source_sublogic cid
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder == inclusion_target_sublogic cid
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder then []
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder else [language_name cid]
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder is_model_transportable _ = True
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder has_model_expansion _ = True
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder is_weakly_amalgamable _ = True
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder isInclusionComorphism _ = True
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maederdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maederinstance (Language cid1, Language cid2)
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder => Language (CompComorphism cid1 cid2) where
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder language_name (CompComorphism cid1 cid2) =
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder language_name cid1 ++ ";" ++ language_name cid2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederinstance (Comorphism cid1
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder Comorphism cid2
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder => Comorphism (CompComorphism cid1 cid2)
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder sourceLogic (CompComorphism cid1 _) =
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder sourceLogic cid1
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder targetLogic (CompComorphism _ cid2) =
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder targetLogic cid2
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder sourceSublogic (CompComorphism cid1 _) =
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder sourceSublogic cid1
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder mapSublogic (CompComorphism cid1 cid2) sl =
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder 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) sig1 = let
th = map_sign cid1 sig1 in
case maybeResult th of
Nothing -> error "failed translating signature"
Just (sig2', _) -> let
th2 = coerceBasicTheory
(targetLogic cid1) (sourceLogic cid2)
"Mapping symbol along comorphism" (sig2', [])
in case maybeResult th2 of
Nothing -> error "failed coercing"
Just (sig2, _) ->
\ s1 ->
let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)
in Set.unions
(map (map_symbol cid2 sig2 . mycast)
(Set.toList (map_symbol cid1 sig1 s1)))
extractModel (CompComorphism cid1 cid2) sign pt3 =
let lid1 = sourceLogic cid1
lid4 = sourceLogic cid2
in if language_name lid1 == language_name lid4 then do
(sign', _) <- coerceBasicTheory lid1 lid4 "extractModel1" (sign, [])
(sign'', sens') <- extractModel cid2 sign' pt3
bTh <- coerceBasicTheory lid4 lid1 "extractModel2" (sign'', sens')
return bTh
else fail $ "extractModel not implemented for comorphism composition with "
++ language_name cid1
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
isInclusionComorphism (CompComorphism cid1 cid2) =
isInclusionComorphism cid1 && isInclusionComorphism cid2
-- * Comorphisms and existential types for the logic graph
-- | Existential type for comorphisms
data AnyComorphism = forall cid 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 cid
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 cid deriving Typeable -- used for GTheory
instance Eq AnyComorphism where
a == b = compare a b == EQ
instance Ord AnyComorphism where
compare (Comorphism cid1) (Comorphism cid2) = compare
(language_name cid1, constituents cid1)
(language_name cid2, constituents cid2)
-- maybe needs to be refined, using comorphism translations?
instance Show AnyComorphism where
show (Comorphism cid) = language_name cid
++ " : " ++ language_name (sourceLogic cid)
++ " -> " ++ language_name (targetLogic cid)
instance Pretty AnyComorphism where
pretty = text . show
-- | compute the identity comorphism for a logic
idComorphism :: AnyLogic -> AnyComorphism
idComorphism (Logic lid) = Comorphism (mkIdComorphism lid (top_sublogic lid))
-- | Test whether a comporphism is the identity
isIdComorphism :: AnyComorphism -> Bool
isIdComorphism (Comorphism cid) = null $ constituents cid
-- * Properties of comorphisms
-- | Test whether a comorphism is model-transportable
isModelTransportable :: AnyComorphism -> Bool
isModelTransportable (Comorphism cid) = is_model_transportable cid
-- | Test whether a comorphism has model expansion
hasModelExpansion :: AnyComorphism -> Bool
hasModelExpansion (Comorphism cid) = has_model_expansion cid
-- | Test whether a comorphism is weakly amalgamable
isWeaklyAmalgamable :: AnyComorphism -> Bool
isWeaklyAmalgamable (Comorphism cid) = is_weakly_amalgamable cid
-- | Compose comorphisms
compComorphism :: Monad m => AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (Comorphism cid1) (Comorphism cid2) =
let l1 = targetLogic cid1
l2 = sourceLogic cid2
msg = "ogic mismatch in composition of " ++ language_name cid1
++ " and " ++ language_name cid2
in
if language_name l1 == language_name l2 then
if isSubElem (forceCoerceSublogic l1 l2 $ targetSublogic cid1)
$ sourceSublogic cid2
then {- case (isIdComorphism cm1,isIdComorphism cm2) of
(True,_) -> return cm2
(_,True) -> return cm1
_ -> -} return $ Comorphism (CompComorphism cid1 cid2)
else fail $ "Subl" ++ msg
else fail $ "L" ++ msg