Comorphism.hs revision f3a94a197960e548ecd6520bb768cb0d547457bb
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettModule : $Header$
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettMaintainer : till@tzi.de
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettStability : provisional
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettPortability : non-portable (via Logic)
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettProvides data structures for institution comorphisms.
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett These are just collections of
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett functions between (some of) the types of logics.
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett{- References: see Logic.hs
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Weak amalgamability, also for comorphisms
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett comorphism modifications
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett comorphisms out of sublogic relationships
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett restrictions of comorphisms to sublogics
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett morphisms and other translations via spans
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport qualified Common.Lib.Set as Set
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettclass (Language cid,
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett Logic lid1 sublogics1
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett basic_spec1 sentence1 symb_items1 symb_map_items1
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Logic lid2 sublogics2
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett basic_spec2 sentence2 symb_items2 symb_map_items2
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Comorphism cid
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett | cid -> lid1, cid -> lid2
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- source and target logic and sublogic
8e97dcf353ac3afc326ecfd167abd47897215436Andy Gimblett -- the source sublogic is the maximal one for which the comorphism works
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- the target sublogic is the resulting one
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sourceLogic :: cid -> lid1
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sourceSublogic :: cid -> sublogics1
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett targetLogic :: cid -> lid2
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett targetSublogic :: cid -> sublogics2
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- finer information of target sublogics corresponding to source sublogics
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett mapSublogic :: cid -> sublogics1 -> sublogics2
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- default implementation
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett mapSublogic cid _ = targetSublogic cid
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- the translation functions are partial
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- because the target may be a sublanguage
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- cover theoroidal comorphisms as well
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett map_theory :: cid -> (sign1,[Named sentence1])
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett -> Result (sign2,[Named sentence2])
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett map_morphism :: cid -> morphism1 -> Result morphism2
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett -- also covers semi-comorphisms
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- with no sentence translation
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- - but these are spans!
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett map_symbol :: cid -> symbol1 -> Set.Set symbol2
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett constituents :: cid -> [String]
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -- default implementation
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett constituents cid = [language_name cid]
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettmap_sign :: Comorphism cid
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett => cid -> sign1 -> Result (sign2,[Named sentence2])
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettmap_sign cid sign = map_theory cid (sign,[])
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettsimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett -> (sign1, [Named sentence1])
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett -> (sign2, [Named sentence2])
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettsimpleTheoryMapping mapSig mapSen (sign,sens) =
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett (mapSig sign, map (mapNamed mapSen) sens)
34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettmkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -> (sign1 -> sentence1 -> m sentence2)
bf7d1ec09971b005fff4133bb8b6964ab7d264e7Andy Gimblett -> (sign1, [Named sentence1])
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett -> m (sign2, [Named sentence2])
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettmkTheoryMapping mapSig mapSen (sign,sens) = do
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett (sign',sens') <- mapSig sign
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett sens'' <- mapM (mapNamedM $ mapSen sign) sens
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett return (sign',sens'++sens'')
adce8375991a372444ab995895442dca6faf9677Andy Gimblettdata IdComorphism lid sublogics =
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett IdComorphism lid sublogics
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettinstance Logic lid sublogics
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett basic_spec sentence symb_items symb_map_items
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett sign morphism symbol raw_symbol proof_tree =>
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett Show (IdComorphism lid sublogics)
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett show = language_name
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettinstance Logic lid sublogics
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett basic_spec sentence symb_items symb_map_items
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sign morphism symbol raw_symbol proof_tree =>
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Language (IdComorphism lid sublogics) where
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett language_name (IdComorphism lid sub) =
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett case sublogic_names lid sub of
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett [] -> error "language_name IdComorphism"
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett h : _ -> "id_" ++ language_name lid ++ "." ++ h
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblettinstance Logic lid sublogics
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett basic_spec sentence symb_items symb_map_items
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sign morphism symbol raw_symbol proof_tree =>
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Comorphism (IdComorphism lid sublogics)
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett lid sublogics
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett basic_spec sentence symb_items symb_map_items
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sign morphism symbol raw_symbol proof_tree
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett lid sublogics
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett basic_spec sentence symb_items symb_map_items
adce8375991a372444ab995895442dca6faf9677Andy Gimblett sign morphism symbol raw_symbol proof_tree
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sourceLogic (IdComorphism lid _sub) = lid
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett targetLogic (IdComorphism lid _sub) = lid
29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblett sourceSublogic (IdComorphism _lid sub) = sub
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett targetSublogic (IdComorphism _lid sub) = sub
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett mapSublogic _ = id
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett map_theory _ = return
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett map_morphism _ = return
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett map_sentence _ = \_ -> return
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett constituents _ = []
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblettinstance (Language cid1, Language cid2)
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett => Language (CompComorphism cid1 cid2) where
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett language_name (CompComorphism cid1 cid2) =
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett language_name cid1++ ";" ++language_name cid2
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblettinstance (Comorphism cid1
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett Comorphism cid2
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sign4 morphism4 symbol4 raw_symbol4 proof_tree4
b34e5090387d45b3a35f88eaa23477a83d2a2962Andy Gimblett lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett => Comorphism (CompComorphism cid1 cid2)
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett sourceLogic (CompComorphism cid1 _) =
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sourceLogic cid1
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett targetLogic (CompComorphism _ cid2) =
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett targetLogic cid2
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sourceSublogic (CompComorphism cid1 _) =
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett sourceSublogic cid1
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett targetSublogic (CompComorphism cid1 cid2) =
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett mapSublogic cid2
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett (idcoerce (targetLogic cid1) (sourceLogic cid2)
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett (targetSublogic cid1))
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett mapSublogic (CompComorphism cid1 cid2) =
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett mapSublogic cid2
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett . idcoerce (targetLogic cid1) (sourceLogic cid2)
bf7d1ec09971b005fff4133bb8b6964ab7d264e7Andy Gimblett . mapSublogic cid1
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett map_sentence (CompComorphism cid1 cid2) =
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett do (si2,_) <- map_sign cid1 si1
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett se2 <- map_sentence cid1 si1 se1
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett (si2', se2') <- mcoerce (targetLogic cid1) (sourceLogic cid2)
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett "Mapping sentence along comorphism" (si2, se2)
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett map_sentence cid2 si2' se2'
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett map_theory (CompComorphism cid1 cid2) =
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett do ti2 <- map_theory cid1 ti1
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett ti2' <- mcoerce (targetLogic cid1) (sourceLogic cid2)
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett "Mapping theory along comorphism" ti2
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett map_theory cid2 ti2'
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett map_morphism (CompComorphism cid1 cid2) = \ m1 ->
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett do m2 <- map_morphism cid1 m1
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett m3 <- mcoerce (targetLogic cid1) (sourceLogic cid2)
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett "Mapping signature morphism along comorphism"m2
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett map_morphism cid2 m3
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett map_symbol (CompComorphism cid1 cid2) = \ s1 ->
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett let mycast = fromJust . mcoerce (targetLogic cid1) (sourceLogic cid2)
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett "Mapping symbol along comorphism"
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett (map (map_symbol cid2 . mycast)
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett (Set.toList (map_symbol cid1 s1)))
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett constituents (CompComorphism cid1 cid2) =
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett constituents cid1 ++ constituents cid2