DGTranslation.hs revision 2eeec5240b424984e3ee26296da1eeab6c6d739e
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederModule : $Header$
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Heng Jiang, Uni Bremen 2004-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederMaintainer : jiang@informatik.uni-bremen.de
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederStability : provisional
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederPortability : non-portable (Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederdisplay the logic graph
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maedermodule GUI.DGTranslation (getDGLogic) where
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder-- data structure
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport Static.DGTranslation (showFromTo)
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport qualified Data.Map as Map
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder-- | get the maximal sublogic of a graph.
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | each DGraph and each node will be tested, in order to find
d3bca27d616c5741d0b18776c8a0848ec31c87f4Christian Maeder-- | the maximal sublogic of th Graph.
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder-- | All edges and nodes will be searched also in the meantime, so as to test,
f9a73de15ef09dbd6b391c7b1f695c79b4446fe2Christian Maeder-- | whether the GMorphism of edges is homogeneous, and the logics of nodes are
f9a73de15ef09dbd6b391c7b1f695c79b4446fe2Christian MaedergetDGLogic :: LibEnv -> Res.Result G_sublogics
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaedergetDGLogic libEnv =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let sublogicsMap = map (getSublogicFromDGraph libEnv)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder in foldr comResSublogics (Res.Result [] Nothing) sublogicsMap
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedergetSublogicFromDGraph :: LibEnv -> LIB_NAME -> Res.Result G_sublogics
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedergetSublogicFromDGraph le ln =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let edgesList = labEdgesDG gc
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder nodesList = labNodesDG gc
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder slList1 = map testAndGetSublogicFromEdge edgesList
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder slList2 = map (getSubLogicsFromNodes $ getFirstLogic nodesList)
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder in foldr comResSublogics (Res.Result [] Nothing) (slList1 ++ slList2)
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder gc = lookupDGraph ln le
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder testAndGetSublogicFromEdge :: LEdge DGLinkLab -> Res.Result G_sublogics
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder testAndGetSublogicFromEdge (from, to,
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder DGLink gm@(GMorphism cid' lsign _ lmorphism _) _ _ _)
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder if isHomogeneous gm then
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder Result [] (comSublogics g_mor g_sign)
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder ("the edge " ++ (showFromTo from to gc) ++
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder " is not homogeneous.") () ] Nothing
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder where g_mor = G_sublogics (targetLogic cid') $ minSublogic lmorphism
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder g_sign = G_sublogics (sourceLogic cid') $ minSublogic lsign
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder getSubLogicsFromNodes :: AnyLogic -> LNode DGNodeLab
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder getSubLogicsFromNodes logic (_, lnode) =
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder case dgn_theory lnode of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder th@(G_theory lid _ _ _ _) ->
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder if Logic lid == logic then
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder Res.Result [] (Just $ sublogicOfTh th)
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder ("the node " ++ (getDGNodeName lnode) ++
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder " has a different logic \"" ++ (show lid) ++
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder "\" as the logic of Graph \"" ++ (show logic) ++
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder " is not homogeneous.") () ] Nothing
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder getFirstLogic :: [LNode DGNodeLab] -> AnyLogic
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder getFirstLogic list =
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder case dgn_theory $ snd $ head list of
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder G_theory lid _ _ _ _ ->
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercomResSublogics :: Res.Result G_sublogics
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercomResSublogics (Res.Result diags1 msubl1@(Just subl1))
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (Res.Result diags2 msubl2) =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder case msubl2 of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Nothing -> Res.Result (diags1 ++ diags2) msubl1
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Just subl2 ->
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Res.Result (diags1 ++ diags2) $ comSublogics subl1 subl2
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercomResSublogics (Res.Result diags1 Nothing) (Res.Result diags2 _) =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Result (diags1 ++ diags2) Nothing
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercomSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercomSublogics (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder case coerceSublogic lid1 lid2 "coerce Sublogic" l1 of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Just sl -> Just (G_sublogics lid2 (join sl l2))
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder Nothing -> Nothing