{- |

Module : $Header$

Description : Translation of development graphs along comorphisms

Copyright : 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)

Translation of development graphs along comorphisms

Follows Sect. IV:4.3 of the CASL Reference Manual.

-}

module Static.DGTranslation

( libEnv_translation

, dg_translation

, showFromTo )

where

import Logic.Logic

import Logic.ExtSign

import Logic.Coerce

import Logic.Comorphism

import Logic.Grothendieck

import Logic.Prover

import Syntax.AS_Library

import Static.GTheory

import Static.DevGraph

import Common.Result

import qualified Data.Set as Set

import qualified Data.Map as Map

import qualified List as List (nub)

import Data.Maybe

import Data.Graph.Inductive.Graph

import Control.Exception

-- | translation of a LibEnv (a map of globalcontext)

libEnv_translation :: LibEnv -> AnyComorphism -> Result LibEnv

libEnv_translation libEnv comorphism =

updateGc (Map.keys libEnv) libEnv []

where updateGc :: [LIB_NAME] -> LibEnv -> [Diagnosis] -> Result LibEnv

updateGc [] le diag = Result diag (Just le)

updateGc (k1:kr) le diagnosis =

let gc = lookupDGraph k1 le

Result diagTran gc' = dg_translation gc comorphism

in updateGc kr (Map.update (\_ -> gc') k1 le)

(diagnosis ++ diagTran)

dg_translation :: DGraph -> AnyComorphism -> Result DGraph

dg_translation gc acm@(Comorphism cidMor) =

let labNodesList = labNodesDG gc

labEdgesList = labEdgesDG gc

in do

resOfEdges <- mapR updateEdges labEdgesList

resOfNodes <- mapR updateNodes labNodesList

return $ mkGraphDG resOfNodes resOfEdges emptyDG

where

slid = sourceLogic cidMor

tlid = targetLogic cidMor

updateEdges :: LEdge DGLinkLab -> Result (LEdge DGLinkLab)

updateEdges

(from,to,(links@(DGLink { dgl_morphism=

gm@(GMorphism cid' (ExtSign lsign _) ind1 lmorphism ind2)}))) =

if isHomogeneous gm

then

let sourceLid = sourceLogic cid'

targetLid = targetLogic cid'

minTargetSublogic = G_sublogics targetLid $ minSublogic lmorphism

in if lessSublogicComor (G_sublogics sourceLid $ minSublogic lsign) acm

&& lessSublogicComor minTargetSublogic acm

then

do -- translate sign of GMorphism

(lsign', _) <- fSign sourceLid lsign

-- translate morphism of GMorphism

lmorphism' <- fMor targetLid lmorphism

-- build a new GMorphism of an edge

case idComorphism (Logic tlid) of

Comorphism cid2 ->

let newSign = fromJust $ coercePlainSign tlid

(sourceLogic cid2) "DGTranslation.updateEdges"

lsign'

newMor = fromJust $ coerceMorphism tlid

(targetLogic cid2) "DGTranslation.updateEdges"

lmorphism'

slNewSign = G_sublogics (sourceLogic cid2)

$ minSublogic newSign

targetLogic2 = targetLogic cid2

domMor = G_sublogics targetLogic2

$ minSublogic $ dom targetLogic2 newMor

in

-- ("old:\n" ++ showDoc lsign "\nnew:\n" ++ showDoc newSign "\n\n")

return $ assert (slNewSign == domMor) $

(from, to,

links{dgl_morphism= GMorphism cid2

(mkExtSign newSign)

ind1 newMor ind2

}

)

else Result [mkDiag Error ("the sublogic of GMorphism :\"" ++

show minTargetSublogic

++ " of edge " ++ showFromTo from to gc

++ " is not less than " ++ show acm) ()] Nothing

else Result [mkDiag Error ("Link "++ showFromTo from to gc ++

" is not homogeneous.") ()] Nothing

updateNodes :: LNode DGNodeLab -> Result (LNode DGNodeLab)

updateNodes (node, dgNodeLab) =

case fTh node $ dgn_theory dgNodeLab of

Result diagsT maybeTh ->

maybe (Result diagsT (Nothing))

(\th' -> Result diagsT

(Just (node, dgNodeLab {dgn_theory = th'

,dgn_nf = Nothing

,dgn_sigma = Nothing

}))) maybeTh

-- !! the sign from fSign and from fTh maybe different.

-- to translate sign

fSign sourceID sign =

coercePlainSign sourceID slid "DGTranslation.fSign" sign >>=

map_sign cidMor

fTh _ (G_theory lid sign _ thSens _) = do

-- (sign', _) <- fSign lid sign

(ExtSign sign' _) <-

coerceSign lid slid "DGTranslation.fTh.sign" sign

thSens' <- coerceThSens lid slid "DGTranslation.fTh.sen" thSens

(sign'', namedS) <- wrapMapTheory cidMor (sign', toNamedList thSens')

return $ G_theory tlid (mkExtSign sign'') 0

(toThSens $ List.nub namedS) 0

fMor sourceID mor =

coerceMorphism sourceID slid "DGTranslation.fMor" mor >>=

map_morphism cidMor

-- | get the name of a node from the number of node

getNameOfNode :: Node -> DGraph -> String

getNameOfNode index gc =

let (_, _, node, _) = fromJust $ fst $ matchDG index gc

in getDGNodeName node

showFromTo :: Node -> Node -> DGraph -> String

showFromTo from to gc =

"from " ++ getNameOfNode from gc ++ " to " ++ getNameOfNode to gc