DGTranslation.hs revision 1842453990fed8a1bd7a5ac792d7982c1d2bfcd5
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederCopyright : (c) Heng Jiang, Uni Bremen 2004-2006
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederMaintainer : jiang@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable (Logic)
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederdisplay the logic graph
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maedermodule GUI.DGTranslation (getDGLogic) where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- data structure
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maederimport Static.DGTranslation (showFromTo)
01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maederimport qualified Data.Map as Map
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- | get the maximal sublogic of a graph.
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- | each DGraph and each node will be tested, in order to find
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | the maximal sublogic of th Graph.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | All edges and nodes will be searched also in the meantime, so as to test,
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder-- | whether the GMorphism of edges is homogeneous, and the logics of nodes are
8410667510a76409aca9bb24ff0eda0420088274Christian MaedergetDGLogic :: LibEnv -> Res.Result G_sublogics
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedergetDGLogic libEnv =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let sublogicsMap = map (getSublogicFromDGraph libEnv)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich in foldr comResSublogics (Res.Result [] Nothing) sublogicsMap
ad270004874ce1d0697fb30d7309f180553bb315Christian MaedergetSublogicFromDGraph :: LibEnv -> LIB_NAME -> Res.Result G_sublogics
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian MaedergetSublogicFromDGraph le ln =
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder let edgesList = labEdgesDG gc
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder nodesList = labNodesDG gc
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich slList1 = map testAndGetSublogicFromEdge edgesList
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder slList2 = map (getSubLogicsFromNodes $ getFirstLogic nodesList)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder in foldr comResSublogics (Res.Result [] Nothing) (slList1 ++ slList2)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder gc = lookupDGraph ln le
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder testAndGetSublogicFromEdge :: LEdge DGLinkLab -> Res.Result G_sublogics
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder testAndGetSublogicFromEdge (from, to,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder DGLink gm@(GMorphism cid' lsign _ lmorphism _) _ _ _)
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder if isHomogeneous gm then
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Result [] (comSublogics g_mor g_sign)
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder ("the edge " ++ (showFromTo from to gc) ++
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder " is not homogeneous.") () ] Nothing
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder where g_mor = G_sublogics (targetLogic cid') $ minSublogic lmorphism
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder g_sign = G_sublogics (sourceLogic cid') $ minSublogic lsign
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder getSubLogicsFromNodes :: AnyLogic -> LNode DGNodeLab
2c9df69accd8924e7cef3bf8f686626958499c7aChristian Maeder getSubLogicsFromNodes logic (_, lnode) =
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maeder case dgn_theory lnode of
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder th@(G_theory lid _ _ _ _) ->
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder if Logic lid == logic then
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder Res.Result [] (Just $ sublogicOfTh th)
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder ("the node " ++ (getDGNodeName lnode) ++
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder " has a different logic \"" ++ (show lid) ++
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder "\" as the logic of Graph \"" ++ (show logic) ++
f13d1e86e58da53680e78043e8df182eed867efbChristian Maeder " is not homogeneous.") () ] Nothing
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder getFirstLogic :: [LNode DGNodeLab] -> AnyLogic
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder getFirstLogic list =
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder case dgn_theory $ snd $ head list of
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder G_theory lid _ _ _ _ ->
ecf76bc89d9a2ecd7ac7310d30654b9a79d97d62Klaus LuettichcomResSublogics :: Res.Result G_sublogics
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich -> Res.Result G_sublogics
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich -> Res.Result G_sublogics
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus LuettichcomResSublogics (Res.Result diags1 msubl1@(Just subl1))
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder (Res.Result diags2 msubl2) =
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder case msubl2 of
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Nothing -> Res.Result (diags1 ++ diags2) msubl1
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder Just subl2 ->
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Res.Result (diags1 ++ diags2) $ comSublogics subl1 subl2
8a28707e9155465c6f2236a06eac6580a65c7025Christian MaedercomResSublogics (Res.Result diags1 Nothing) (Res.Result diags2 _) =
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich Result (diags1 ++ diags2) Nothing
797ccd67cb8ae127be097cd43448801b673e3b69Christian MaedercomSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
431d34c7007a787331c4e5ec997badb0f8190fc7Christian MaedercomSublogics (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case coerceSublogic lid1 lid2 "coerce Sublogic" l1 of
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maeder Just sl -> Just (G_sublogics lid2 (join sl l2))
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder Nothing -> Nothing