Comorphism.hs revision 922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiModule : $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : till@tzi.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (via Logic)
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiProvides data structures for institution comorphisms.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder These are just collections of
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski functions between (some of) the types of logics.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder{- References: see Logic.hs
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Weak amalgamability, also for comorphisms
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder comorphism modifications
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder comorphisms out of sublogic relationships
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder restrictions of comorphisms to sublogics
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder morphisms and other translations via spans
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport qualified Common.Lib.Set as Set
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederclass (Language cid,
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Logic lid1 sublogics1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Logic lid2 sublogics2
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Comorphism cid
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski | cid -> lid1, cid -> lid2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- source and target logic and sublogic
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the source sublogic is the maximal one for which the comorphism works
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the target sublogic is the resulting one
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sourceLogic :: cid -> lid1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sourceSublogic :: cid -> sublogics1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski targetLogic :: cid -> lid2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski targetSublogic :: cid -> sublogics2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- finer information of target sublogics corresponding to source sublogics
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mapSublogic :: cid -> sublogics1 -> sublogics2
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- default implementation
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder mapSublogic cid _ = targetSublogic cid
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- the translation functions are partial
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- because the target may be a sublanguage
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- cover theoroidal comorphisms as well
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder map_theory :: cid -> (sign1,[Named sentence1])
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> Result (sign2,[Named sentence2])
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- also covers semi-comorphisms
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- with no sentence translation
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -- - but these are spans!
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich map_symbol :: cid -> symbol1 -> Set.Set symbol2
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich constituents :: cid -> [String]
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -- default implementation
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich constituents cid = [language_name cid]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedermap_sign :: Comorphism cid
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder => cid -> sign1 -> Result (sign2,[Named sentence2])
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maedermap_sign cid sign = map_theory cid (sign,[])
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskisimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski -> (sign1, [Named sentence1])
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> (sign2, [Named sentence2])
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maeder (mapSig sign, map (mapNamed mapSen) sens)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maeder -> (sign1 -> sentence1 -> m sentence2)
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maeder -> (sign1, [Named sentence1])
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> m (sign2, [Named sentence2])
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (sign',sens') <- mapSig sign
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder sens'' <- mapM (mapNamedM $ mapSen sign) sens
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return (sign',sens'++sens'')
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederdata IdComorphism lid sublogics =
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder IdComorphism lid sublogics
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederinstance Logic lid sublogics
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski basic_spec sentence symb_items symb_map_items
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Show (IdComorphism lid sublogics)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder show = language_name
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederinstance Logic lid sublogics
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder basic_spec sentence symb_items symb_map_items
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder sign morphism symbol raw_symbol proof_tree =>
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Language (IdComorphism lid sublogics) where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder language_name (IdComorphism lid sub) =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder case sublogic_names lid sub of
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder [] -> error "language_name IdComorphism"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski h : _ -> "id_" ++ language_name lid ++ "." ++ h
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Logic lid sublogics
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski basic_spec sentence symb_items symb_map_items
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sign morphism symbol raw_symbol proof_tree =>
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Comorphism (IdComorphism lid sublogics)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder lid sublogics
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder basic_spec sentence symb_items symb_map_items
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder sign morphism symbol raw_symbol proof_tree
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder lid sublogics
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder basic_spec sentence symb_items symb_map_items
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder sign morphism symbol raw_symbol proof_tree
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder sourceLogic (IdComorphism lid _sub) = lid
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder targetLogic (IdComorphism lid _sub) = lid
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder sourceSublogic (IdComorphism _lid sub) = sub
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder targetSublogic (IdComorphism _lid sub) = sub
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mapSublogic _ = id
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder map_theory _ = return
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder map_morphism _ = return
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder map_sentence _ = \_ -> return
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder constituents _ = []
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance (Language cid1, Language cid2)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder => Language (CompComorphism cid1 cid2) where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder language_name (CompComorphism cid1 cid2) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder language_name cid1++ ";" ++language_name cid2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance (Comorphism cid1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Comorphism cid2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder => Comorphism (CompComorphism cid1 cid2)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski sourceLogic (CompComorphism cid1 _) =
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder sourceLogic cid1
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder targetLogic (CompComorphism _ cid2) =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski targetLogic cid2
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder sourceSublogic (CompComorphism cid1 _) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder sourceSublogic cid1
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder targetSublogic (CompComorphism cid1 cid2) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mapSublogic cid2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (coerceSublogic (targetLogic cid1) (sourceLogic cid2)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (targetSublogic cid1))
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder mapSublogic (CompComorphism cid1 cid2) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mapSublogic cid2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder . coerceSublogic (targetLogic cid1) (sourceLogic cid2)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder . mapSublogic cid1
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder map_sentence (CompComorphism cid1 cid2) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do (si2,_) <- map_sign cid1 si1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski se2 <- map_sentence cid1 si1 se1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (si2', se2') <- coerceBasicTheory
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (targetLogic cid1) (sourceLogic cid2)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski "Mapping sentence along comorphism" (si2, [emptyName se2])
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski [x] -> map_sentence cid2 si2' $ sentence x
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski map_theory (CompComorphism cid1 cid2) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder do ti2 <- map_theory cid1 ti1
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder "Mapping theory along comorphism" ti2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski map_theory cid2 ti2'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski map_morphism (CompComorphism cid1 cid2) = \ m1 ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do m2 <- map_morphism cid1 m1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski "Mapping signature morphism along comorphism"m2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski map_morphism cid2 m3
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski map_symbol (CompComorphism cid1 cid2) = \ s1 ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (map (map_symbol cid2 . mycast)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (Set.toList (map_symbol cid1 s1)))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski constituents (CompComorphism cid1 cid2) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski constituents cid1 ++ constituents cid2