1060N/A{- |

1060N/AModule : $Header$

1060N/ACopyright : (c) Heng Jiang, Uni Bremen 2004-2006

1060N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

1060N/A

1060N/AMaintainer : jiang@tzi.de

1060N/AStability : provisional

1060N/APortability : non-portable (Logic)

1060N/A

1060N/Adisplay the logic graph

1060N/A-}

1060N/A

1060N/Amodule GUI.DGTranslation (getDGLogic) where

1060N/A

1060N/A-- data structure

1060N/Aimport Logic.Grothendieck

1060N/Aimport Logic.Coerce

1060N/Aimport Logic.Logic

1060N/Aimport Logic.Comorphism

1060N/Aimport Syntax.AS_Library

1060N/Aimport Static.DevGraph

1060N/Aimport Static.DGTranslation (showFromTo)

1060N/A

1060N/Aimport qualified Data.Map as Map

1060N/Aimport Common.Result as Res

4495N/Aimport Data.Graph.Inductive.Graph as Graph

5636N/Aimport Data.Maybe

1060N/A

1060N/A-- | get the maximal sublogic of a graph.

1060N/A-- | each GlobalContext and each node will be tested, in order to find

3831N/A-- | the maximal sublogic of th Graph.

3831N/A-- | All edges and nodes will be searched also in the meantime, so as to test,

3831N/A-- | whether the GMorphism of edges is homogeneous, and the logics of nodes are

3831N/A-- | equal.

3831N/AgetDGLogic :: LibEnv -> Res.Result G_sublogics

3831N/AgetDGLogic libEnv =

3831N/A let sublogicsMap = map (getSublogicFromGlobalContext libEnv)

3831N/A (Map.keys libEnv)

3831N/A in foldr comResSublogics (Res.Result [] Nothing) sublogicsMap

3842N/A

3831N/AgetSublogicFromGlobalContext :: LibEnv -> LIB_NAME -> Res.Result G_sublogics

3842N/AgetSublogicFromGlobalContext le ln =

3831N/A let edgesList = Graph.labEdges $ devGraph gc

3831N/A nodesList = Graph.labNodes $ devGraph gc

3831N/A slList1 = map testAndGetSublogicFromEdge edgesList

3831N/A slList2 = map (getSubLogicsFromNodes $ getFirstLogic nodesList)

3831N/A nodesList

3831N/A in foldr comResSublogics (Res.Result [] Nothing) (slList1 ++ slList2)

3842N/A

3842N/A where

3831N/A gc = lookupGlobalContext ln le

3842N/A

3831N/A testAndGetSublogicFromEdge :: LEdge DGLinkLab -> Res.Result G_sublogics

5636N/A testAndGetSublogicFromEdge (from, to,

2976N/A DGLink gm@(GMorphism cid' lsign _ lmorphism _) _ _)

3831N/A =

1060N/A if isHomogeneous gm then

Result [] (comSublogics g_mor g_sign)

else Result [Res.mkDiag Res.Error

("the edge " ++ (showFromTo from to gc) ++

" is not homogeneous.") () ] Nothing

where g_mor = G_sublogics (targetLogic cid') $ minSublogic lmorphism

g_sign = G_sublogics (sourceLogic cid') $ minSublogic lsign

getSubLogicsFromNodes :: AnyLogic -> LNode DGNodeLab

-> Res.Result G_sublogics

getSubLogicsFromNodes logic (_, lnode) =

case dgn_theory lnode of

th@(G_theory lid _ _ _ _) ->

if Logic lid == logic then

Res.Result [] (Just $ sublogicOfTh th)

else Res.Result [Res.mkDiag Res.Error

("the node " ++ (getDGNodeName lnode) ++

" has a different logic \"" ++ (show lid) ++

"\" as the logic of Graph \"" ++ (show logic) ++

" is not homogeneous.") () ] Nothing

getFirstLogic :: [LNode DGNodeLab] -> AnyLogic

getFirstLogic list =

case dgn_theory $ snd $ head list of

G_theory lid _ _ _ _ ->

Logic lid

comResSublogics :: Res.Result G_sublogics

-> Res.Result G_sublogics

-> Res.Result G_sublogics

comResSublogics (Res.Result diags1 msubl1@(Just subl1))

(Res.Result diags2 msubl2) =

case msubl2 of

Nothing -> Res.Result (diags1 ++ diags2) msubl1

Just subl2 ->

Res.Result (diags1 ++ diags2) $ comSublogics subl1 subl2

comResSublogics (Res.Result diags1 Nothing) (Res.Result diags2 _) =

Result (diags1 ++ diags2) Nothing

comSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics

comSublogics (G_sublogics lid1 l1) (G_sublogics lid2 l2) =

case coerceSublogic lid1 lid2 "coerce Sublogic" l1 of

Just sl -> Just (G_sublogics lid2 (join sl l2))

Nothing -> Nothing