967e5f3c25249c779575864692935627004d3f9eChristian Maeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable

967e5f3c25249c779575864692935627004d3f9eChristian Maeder , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}

81d182b21020b815887e9057959228546cf61b6bChristian Maeder{- |

f11f713bebd8e1e623a0a4361065df256033de47Christian MaederModule : $Header$

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : interface and class for logic translations

967e5f3c25249c779575864692935627004d3f9eChristian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : till@informatik.uni-bremen.de

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederStability : provisional

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (via Logic)

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederCentral interface (type class) for logic translations (comorphisms) in Hets

967e5f3c25249c779575864692935627004d3f9eChristian Maeder These are just collections of

967e5f3c25249c779575864692935627004d3f9eChristian Maeder functions between (some of) the types of logics.

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maeder References: see Logic.hs

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder-}

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maedermodule Logic.Comorphism

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder ( CompComorphism (..)

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder , InclComorphism

ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder , inclusion_logic

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder , inclusion_source_sublogic

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder , inclusion_target_sublogic

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder , mkInclComorphism

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder , mkIdComorphism

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , Comorphism (..)

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , targetSublogic

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , map_sign

967e5f3c25249c779575864692935627004d3f9eChristian Maeder , ext_map_sign

8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder , mapDefaultMorphism

78eeae099616e255ccf2e5f9122387bb10c68338Christian Maeder , wrapMapTheory

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , simpleTheoryMapping

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , mkTheoryMapping

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , AnyComorphism (..)

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , idComorphism

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , isIdComorphism

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , isModelTransportable

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , hasModelExpansion

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , isWeaklyAmalgamable

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , compComorphism

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder ) where

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederimport Logic.Logic

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederimport Logic.Coerce

51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maederimport Logic.ExtSign

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederimport Common.AS_Annotation

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederimport Common.Doc

51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maederimport Common.DocUtils

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederimport Common.ExtSign

67d92da5e9610aabad39055a16031154b4dc3748Christian Maederimport Common.Id

67d92da5e9610aabad39055a16031154b4dc3748Christian Maederimport Common.ProofUtils

67d92da5e9610aabad39055a16031154b4dc3748Christian Maederimport Common.Result

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder

67d92da5e9610aabad39055a16031154b4dc3748Christian Maederimport Data.Maybe

67d92da5e9610aabad39055a16031154b4dc3748Christian Maederimport qualified Data.Set as Set

67d92da5e9610aabad39055a16031154b4dc3748Christian Maederimport Data.Typeable

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder

67d92da5e9610aabad39055a16031154b4dc3748Christian Maederclass (Language cid,

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder Logic lid1 sublogics1

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder Logic lid2 sublogics2

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder Comorphism cid

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder where

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder -- source and target logic and sublogic

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder -- the source sublogic is the maximal one for which the comorphism works

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sourceLogic :: cid -> lid1

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder sourceSublogic :: cid -> sublogics1

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder targetLogic :: cid -> lid2

a89389521ddf76109168a0b339031575aafbd512Christian Maeder -- finer information of target sublogics corresponding to source sublogics

a89389521ddf76109168a0b339031575aafbd512Christian Maeder -- this function must be partial because mapTheory is partial

a89389521ddf76109168a0b339031575aafbd512Christian Maeder mapSublogic :: cid -> sublogics1 -> Maybe sublogics2

a89389521ddf76109168a0b339031575aafbd512Christian Maeder -- the translation functions are partial

a89389521ddf76109168a0b339031575aafbd512Christian Maeder -- because the target may be a sublanguage

a89389521ddf76109168a0b339031575aafbd512Christian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2

a89389521ddf76109168a0b339031575aafbd512Christian Maeder -- cover theoroidal comorphisms as well

a89389521ddf76109168a0b339031575aafbd512Christian Maeder map_theory :: cid -> (sign1,[Named sentence1])

a89389521ddf76109168a0b339031575aafbd512Christian Maeder -> Result (sign2,[Named sentence2])

3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2

3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder -- also covers semi-comorphisms

9b30898b139ee02f97ac933b6d935ef0a4206921Christian Maeder -- with no sentence translation

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder -- - but these are spans!

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder map_sentence = failMapSentence

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2

51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder map_symbol = errMapSymbol

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder extractModel :: cid -> sign1 -> proof_tree2

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder -> Result (sign1, [Named sentence1])

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder extractModel cid _ _ = fail

51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder $ "extractModel not implemented for comorphism "

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder ++ language_name cid

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder --properties of comorphisms

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder is_model_transportable :: cid -> Bool

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder -- a comorphism (\phi, \alpha, \beta) is model-transportable

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder -- if for any signature \Sigma,

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder -- any \Sigma-model M and any \phi(\Sigma)-model N

51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder -- for any isomorphism h : \beta_\Sigma(N) -> M

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder -- there exists an isomorphism h': N -> M' such that \beta_\Sigma(h') = h

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder is_model_transportable _ = False

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder has_model_expansion :: cid -> Bool

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder has_model_expansion _ = False

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder is_weakly_amalgamable :: cid -> Bool

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder is_weakly_amalgamable _ = False

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder constituents :: cid -> [String]

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder constituents cid = [language_name cid]

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder isInclusionComorphism :: cid -> Bool

ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder isInclusionComorphism _ = False

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaedertargetSublogic :: Comorphism cid

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

d48085f765fca838c1d972d2123601997174583dChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

d48085f765fca838c1d972d2123601997174583dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder => cid -> sublogics2

d48085f765fca838c1d972d2123601997174583dChristian MaedertargetSublogic cid = fromMaybe (top_sublogic $ targetLogic cid)

d48085f765fca838c1d972d2123601997174583dChristian Maeder $ mapSublogic cid $ sourceSublogic cid

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder

d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | this function is base on 'map_theory' using no sentences as input

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maedermap_sign :: Comorphism cid

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

9b30898b139ee02f97ac933b6d935ef0a4206921Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder => cid -> sign1 -> Result (sign2,[Named sentence2])

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maedermap_sign cid sign = wrapMapTheory cid (sign,[])

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederext_map_sign :: Comorphism cid

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder => cid -> ExtSign sign1 symbol1

67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder -> Result (ExtSign sign2 symbol2, [Named sentence2])

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maederext_map_sign cid (ExtSign sign _) = do

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (sign2, sens2) <- map_sign cid sign

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder return (makeExtSign (targetLogic cid) sign2, sens2)

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapDefaultMorphism :: Comorphism cid

f11f713bebd8e1e623a0a4361065df256033de47Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

967e5f3c25249c779575864692935627004d3f9eChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

18b513ff41708f24e1a7407f36b719add813ffeaChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder => cid -> morphism1 -> Result morphism2

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedermapDefaultMorphism cid mor = do

a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder (sig1, _) <- map_sign cid $ dom mor

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder (sig2, _) <- map_sign cid $ cod mor

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder inclusion (targetLogic cid) sig1 sig2

3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian MaederfailMapSentence :: Comorphism cid

f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

81d182b21020b815887e9057959228546cf61b6bChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

242397ba0f1cc490e892130bf0df239deeecf5daChristian Maeder => cid -> sign1 -> sentence1 -> Result sentence2

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian MaederfailMapSentence cid _ _ =

242397ba0f1cc490e892130bf0df239deeecf5daChristian Maeder fail $ "Unsupported sentence translation " ++ show cid

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder

d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian MaedererrMapSymbol :: Comorphism cid

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian Maeder => cid -> sign1 -> symbol1 -> Set.Set symbol2

d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian MaedererrMapSymbol cid _ _ = error $ "no symbol mapping for " ++ show cid

3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder

d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian Maeder-- | use this function instead of 'map_theory'

58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian MaederwrapMapTheory :: Comorphism cid

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder => cid -> (sign1, [Named sentence1])

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder -> Result (sign2, [Named sentence2])

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederwrapMapTheory cid (sign, sens) = let res = map_theory cid (sign, sens) in

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder if isIdComorphism $ Comorphism cid then res else case sourceSublogic cid of

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder sub -> case minSublogic sign of

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder sigLog -> case foldl join sigLog

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski $ map (minSublogic . sentence) sens of

967e5f3c25249c779575864692935627004d3f9eChristian Maeder senLog ->

967e5f3c25249c779575864692935627004d3f9eChristian Maeder if isSubElem senLog sub

f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu then res

967e5f3c25249c779575864692935627004d3f9eChristian Maeder else Result

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder [ Diag Hint

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder (show (vcat $ pretty sign : map

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder (print_named $ sourceLogic cid) sens))

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder nullRange

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder , Diag Error

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder ("for '" ++ language_name cid ++

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder "' expected sublogic '" ++

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sublogicName sub ++

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder "'\n but found sublogic '" ++

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sublogicName senLog ++

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder "' with signature sublogic '" ++

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sublogicName sigLog ++ "'") nullRange] Nothing

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder -> (sign1, [Named sentence1])

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder -> (sign2, [Named sentence2])

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder (mapSig sign, map (mapNamed mapSen) sens)

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder -> (sign1 -> sentence1 -> m sentence2)

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder -> (sign1, [Named sentence1])

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder -> m (sign2, [Named sentence2])

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder (sign',sens') <- mapSig sign

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sens'' <- mapM (mapNamedM $ mapSen sign) sens

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder return (sign', nameAndDisambiguate $ sens' ++ sens'')

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maederdata InclComorphism lid sublogics = InclComorphism

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder { inclusion_logic :: lid

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , inclusion_source_sublogic :: sublogics

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , inclusion_target_sublogic :: sublogics }

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder deriving Show

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder-- | construction of an identity comorphism

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermkIdComorphism :: (Logic lid sublogics

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder basic_spec sentence symb_items symb_map_items

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign morphism symbol raw_symbol proof_tree) =>

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid -> sublogics -> InclComorphism lid sublogics

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaedermkIdComorphism lid sub = InclComorphism

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder { inclusion_logic = lid

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , inclusion_source_sublogic = sub

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder , inclusion_target_sublogic = sub }

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder-- | construction of an inclusion comorphism

1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermkInclComorphism :: (Logic lid sublogics

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder basic_spec sentence symb_items symb_map_items

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder sign morphism symbol raw_symbol proof_tree,

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Monad m) =>

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid -> sublogics -> sublogics

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder -> m (InclComorphism lid sublogics)

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaedermkInclComorphism lid srcSub trgSub =

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder if isSubElem srcSub trgSub

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder then return InclComorphism

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder { inclusion_logic = lid

9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder , inclusion_source_sublogic = srcSub

9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder , inclusion_target_sublogic = trgSub }

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder else fail ("mkInclComorphism: first sublogic must be a "++

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder "subElem of the second sublogic")

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maederinstance (Language lid, Eq sublogics, Show sublogics, SublogicName sublogics)

9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder => Language (InclComorphism lid sublogics) where

9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder language_name (InclComorphism lid sub_src sub_trg) =

551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder let sblName = sublogicName sub_src

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder lname = language_name lid

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder in if sub_src == sub_trg

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder then "id_" ++ lname ++

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder if null sblName then "" else '.' : sblName

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder else "incl_" ++ lname ++ ':'

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder : sblName ++ "->" ++ sublogicName sub_trg

a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maederinstance Logic lid sublogics

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder basic_spec sentence symb_items symb_map_items

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder sign morphism symbol raw_symbol proof_tree =>

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder Comorphism (InclComorphism lid sublogics)

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder lid sublogics

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder basic_spec sentence symb_items symb_map_items

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign morphism symbol raw_symbol proof_tree

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid sublogics

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder basic_spec sentence symb_items symb_map_items

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign morphism symbol raw_symbol proof_tree

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder where

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder sourceLogic = inclusion_logic

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder targetLogic = inclusion_logic

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder sourceSublogic = inclusion_source_sublogic

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder mapSublogic cid subl =

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder if isSubElem subl $ inclusion_source_sublogic cid

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder then Just subl

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder else Nothing

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder map_theory _ = return

1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder map_morphism _ = return

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder map_sentence _ _ = return

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder map_symbol _ _ = Set.singleton

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder 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

isInclusionComorphism _ = 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 >>=

mapSublogic cid2 .

forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2)

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

lid3 = sourceLogic cid2

in if language_name lid1 == language_name lid3 then do

bTh1 <- map_sign cid1 sign

(sign1, _) <-

coerceBasicTheory (targetLogic cid1) lid3 "extractModel1" bTh1

bTh2 <- extractModel cid2 sign1 pt3

coerceBasicTheory lid3 lid1 "extractModel2" bTh2

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