{- |

Module : $Header$

Copyright : (c) Heng Jiang, Uni Bremen 2004-2006

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : jiang@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable (Logic)

display the logic graph

-}

module GUI.DGTranslation (getDGLogic) where

-- data structure

import Logic.Grothendieck

import Logic.Coerce

import Logic.Logic

import Logic.ExtSign

import Logic.Comorphism

import Syntax.AS_Library

import Static.GTheory

import Static.DevGraph

import Static.DGTranslation (showFromTo)

import qualified Data.Map as Map

import Common.Result as Res

import Data.Graph.Inductive.Graph as Graph

import Data.Maybe

-- | get the maximal sublogic of a graph.

-- | each DGraph and each node will be tested, in order to find

-- | the maximal sublogic of th Graph.

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

-- | whether the GMorphism of edges is homogeneous, and the logics of nodes are

-- | equal.

getDGLogic :: LibEnv -> Res.Result G_sublogics

getDGLogic libEnv =

let sublogicsMap = map (getSublogicFromDGraph libEnv)

(Map.keys libEnv)

in foldr comResSublogics (Res.Result [] Nothing) sublogicsMap

getSublogicFromDGraph :: LibEnv -> LIB_NAME -> Res.Result G_sublogics

getSublogicFromDGraph le ln =

let edgesList = labEdgesDG gc

nodesList = labNodesDG gc

slList1 = map testAndGetSublogicFromEdge edgesList

slList2 = map (getSubLogicsFromNodes $ getFirstLogic nodesList)

nodesList

in foldr comResSublogics (Res.Result [] Nothing) (slList1 ++ slList2)

where

gc = lookupDGraph ln le

testAndGetSublogicFromEdge :: LEdge DGLinkLab -> Res.Result G_sublogics

testAndGetSublogicFromEdge (from, to,

DGLink gm@(GMorphism cid' (ExtSign lsign _) _ lmorphism _) _ _ _)

=

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