c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe{- |

c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweModule : $Header$

c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweDescription : Translation of development graphs along comorphisms

c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweCopyright : Heng Jiang, Uni Bremen 2004-2006

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

c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweMaintainer : jiang@tzi.de

c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweStability : provisional

c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowePortability : non-portable(Logic)

c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe

c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweTranslation of development graphs along comorphisms

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

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov-}

c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankovmodule Static.DGTranslation

0b5ce10aee80822ecc7df77df92a5e24078ba196Andy Stormont ( libEnv_translation

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov , dg_translation

c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , showFromTo )

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov where

c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankovimport Logic.Logic

c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport Logic.Coerce

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankovimport Logic.Comorphism

c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport Logic.Grothendieck

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankovimport Logic.Prover

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankovimport Syntax.AS_Library

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankovimport Static.DevGraph

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankovimport qualified Data.Map as Map

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankovimport qualified List as List (nub)

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankovimport Common.Result

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankovimport Data.Maybe

0b5ce10aee80822ecc7df77df92a5e24078ba196Andy Stormontimport Data.Graph.Inductive.Graph

0b5ce10aee80822ecc7df77df92a5e24078ba196Andy Stormontimport Control.Exception

0b5ce10aee80822ecc7df77df92a5e24078ba196Andy Stormont

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

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri PankovlibEnv_translation :: LibEnv -> AnyComorphism -> Result LibEnv

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri PankovlibEnv_translation libEnv comorphism =

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov updateGc (Map.keys libEnv) libEnv []

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov

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

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

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov updateGc (k1:kr) le diagnosis =

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov let gc = lookupGlobalContext k1 le

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov Result diagTran gc' = dg_translation gc comorphism

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

0b5ce10aee80822ecc7df77df92a5e24078ba196Andy Stormont (diagnosis ++ diagTran)

c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe

c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowedg_translation :: GlobalContext -> AnyComorphism -> Result GlobalContext

c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowedg_translation gc acm@(Comorphism cidMor) =

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov let labNodesList = labNodesDG $ devGraph gc

c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe labEdgesList = labEdgesDG $ devGraph gc

a9478106a12424322498e53cf7cd75bd8a4d6004Yuri Pankov in do

resOfEdges <- mapR updateEdges labEdgesList

resOfNodes <- mapR updateNodes labNodesList

return gc{devGraph= mkGraphDG resOfNodes resOfEdges}

where

slid = sourceLogic cidMor

tlid = targetLogic cidMor

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

updateEdges

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

gm@(GMorphism cid' 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 $ coerceSign 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

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 =

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

map_sign cidMor

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

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

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 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 -> GlobalContext -> String

getNameOfNode index gc =

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

in getDGNodeName node

showFromTo :: Node -> Node -> GlobalContext -> String

showFromTo from to gc =

"from " ++ (getNameOfNode from gc) ++ " to " ++ (getNameOfNode to gc)