{- |
Module : ./Static/ApplyChanges.hs
Description : apply xupdate changes to a development graph
Copyright : (c) Christian Maeder, DFKI GmbH 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : non-portable(Grothendieck)
adjust development graph according to xupdate information
-}
module Static.ApplyChanges (dgXUpdateMods, dgXUpdate) where
import Static.ComputeTheory
import Static.DevGraph
import Static.DgUtils
import Static.FromXml
import Static.GTheory
import Static.History (undoAllChanges, changeDGH, clearHistory)
import Static.ToXml
import Static.XGraph
import Static.XSimplePath
import Driver.Options
import Driver.ReadFn (libNameToFile)
import Driver.WriteFn (writeVerbFile)
import Comorphisms.LogicGraph (logicGraph)
import Common.LibName
import Common.ResultT
import Common.Result
import Common.XUpdate
import Logic.Grothendieck
import Control.Monad
import Control.Monad.Trans (lift)
import Data.Graph.Inductive.Graph (Node, match, lab)
import qualified Data.List as List (nub)
import qualified Data.Set as Set
import qualified Data.Map as Map
import Text.XML.Light hiding (Node)
{- incorporate a previous session (diff) upon an exising dgraph. The structure
is as follows:
- roll back the current dg to it's initial state
- apply diff to initial dg
- create xgraph from dg'
- incorporate changes into current dg; the xgraph serves for structuring.
NOTE: The data-type NodeMod holds information about the changes upon a node.
However, with the current usage, a Boolean value would do since the module only
knows update or don't-update. We kept the NodeMod-approach since proper usage
of the NodeMod data type might allow more precise updating.
NOTE(2): If any element changes, ALL elements that lie underneath in terms of
signature-hierachy will receive updating as well (even if two subsequent
changes would lead to an unchanged signature further down). -}
-- | recieves diff as a string and current dg and prepares those for processing
dgXUpdate :: HetcatsOpts -> String -> LibEnv -> LibName -> DGraph
-> ResultT IO (LibName, LibEnv)
dgXUpdate opts xs le ln dg = case parseXMLDoc xs of
Nothing -> fail "dgXUpdate: cannot parse xupdate file"
Just diff -> let
-- we assume that the diff refers to an unchanged dg..
dgOld = undoAllChanges dg
oldLId = getNewEdgeId dgOld
xorig = dGraph opts le ln dgOld
in dgXUpdateMods opts xorig oldLId diff le ln dg
{- | updates a dgraph partially in accordance with changelist data from a .diff
application. an xgraph is created and used as a guideline for signature-
hierachy and for retrieving required new data. -}
dgXUpdateMods :: HetcatsOpts -> Element -> EdgeId -> Element -> LibEnv
-> LibName -> DGraph -> ResultT IO (LibName, LibEnv)
dgXUpdateMods opts xorig oldLId diff le ln dg = do
-- dg with changes incorporated (diff only) and listing of these changes
(xml, chL) <- liftR $ changeXmlMod xorig diff
lift $ writeVerbFile opts (libNameToFile ln ++ ".xml")
$ ppTopElement $ cleanUpElem xml
xgr <- liftR $ xGraph xml
-- the changes will now be incorporated in the so-far unchanged session-dg.
(dg0, chL') <- liftR $ deleteElements dg chL
let newLId = max (nextLinkId xgr) $ getNewEdgeId dg
-- to anticipate multiple use of link-ids
dg1 = renumberDGLinks oldLId newLId dg0
dg2 = dg1 { globalAnnos = globAnnos xgr
-- TODO as of now, ALL nodes will be removed from globalEnv!
, globalEnv = Map.empty }
(dg3, le', chL'') <- iterateXgBody opts xgr le dg2 chL'
-- for any leftover theorem link updates, the respective links are deleted
dgFin <- fmap clearHistory $ deleteLeftoverChanges dg3 chL''
return (ln, computeLibEnvTheories $ Map.insert ln dgFin le')
{- | deletes theorem links from dg that were left-over in changelist.
fails if any other undone changes are found -}
deleteLeftoverChanges :: Monad m => DGraph -> ChangeList -> m DGraph
deleteLeftoverChanges dg chL = let lIds = Map.keys $ changeLinks chL in do
unless (emptyChangeList == chL { changeLinks = Map.empty })
$ fail $ "some changes could not be processed:\n" ++ show chL
foldM (\ dg' ei -> case getDGLinksById ei dg' of
[ledge@(_, _, lkLab)] | not $ isDefEdge $ dgl_type lkLab -> return
$ changeDGH dg' $ DeleteEdge ledge
_ -> fail $ "deleteLeftoverChanges: conflict with edge #" ++ show ei
) dg lIds
{- | move along xgraph structure and make updates or insertions in accordance
with changelist. In addition to the initial entries of the changelist, all
nodes that were subject to ingoing signature changes as well as all links
adjacent to an updated node will also be updated. -}
iterateXgBody :: HetcatsOpts -> XGraph -> LibEnv -> DGraph
-> ChangeList -> ResultT IO (DGraph, LibEnv, ChangeList)
iterateXgBody opts xgr lv dg chL = let lg = logicGraph in do
rs1 <- foldM (mkNodeUpdate opts lg Nothing) (dg, lv, chL) $ startNodes xgr
rs2 <- foldM (foldM (mkXStepUpdate opts lg)) rs1 $ reverse $ xg_body xgr
mkThmLinkUpdates lg rs2 $ thmLinks xgr
-- | apply updates to one branch of the xgraph.
mkXStepUpdate :: HetcatsOpts -> LogicGraph -> (DGraph, LibEnv, ChangeList)
-> ([XLink], XNode) -> ResultT IO (DGraph, LibEnv, ChangeList)
mkXStepUpdate opts lg (dg, lv, chL) (xlks, xnd) = let
-- first, add the req. signature change from ingoing definition links
sigUpd = getLinkModUnion chL xlks
chL' = if sigUpd == unMod then chL else updateNodeChange (MkUpdate sigUpd)
(nodeName xnd) chL in do
mrs <- mapM (getTypeAndMorphism lg dg) xlks
G_sign lid sg sId <- getSigForXNode lg dg mrs
rs1 <- mkNodeUpdate opts lg (Just $ noSensGTheory lid sg sId)
(dg, lv, chL') xnd
foldM (mkLinkUpdate lg) rs1 mrs
{- | the required node update due to link mods is derived using union.
predecessor signature changes have been collected through markLinkUpdates. -}
getLinkModUnion :: ChangeList -> [XLink] -> NodeMod
getLinkModUnion chL = foldr (\ xl ->
case Map.lookup (edgeId xl) $ changeLinks chL of
-- TODO: Cons symMod was chosen only to ensure updating of adjacent nodes.
Just MkInsert -> mergeNodeMod symMod
Just (MkUpdate nmod) -> mergeNodeMod nmod
Nothing -> id ) unMod
{- | update or insert a node in accordance with XGraph data ONLY if the element
is marked for updating in changelist. -}
mkNodeUpdate :: HetcatsOpts -> LogicGraph -> Maybe G_theory
-> (DGraph, LibEnv, ChangeList) -> XNode
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkNodeUpdate opts lg mGt (dg, lv, chL) xnd = let
nm = nodeName xnd
nd = showName nm in case retrieveNodeChange nm chL of
-- no change required, move on
Nothing -> return (dg, lv, chL)
-- make insertion using DGChange.InsertNode object
Just (MkInsert, chL') -> let n = getNewNodeDG dg in do
(lbl, lv') <- generateNodeLab opts lg mGt xnd (dg, lv)
let dg' = changeDGH dg $ InsertNode (n, lbl)
return (dg', lv', chL')
-- make update using DGChange.SetNodeLab object
Just (MkUpdate nmod, chL') -> do
(lbl, lv') <- generateNodeLab opts lg mGt xnd (dg, lv)
(n, lblOrig) <- case lookupUniqueNodeByName nd dg of
Just ndOrig -> return ndOrig
Nothing -> fail $ "node [" ++ nd ++ "] was not found in dg, but was"
++ " marked for updating"
let dg' = changeDGH dg $ SetNodeLab lblOrig (n, lbl)
-- all adjacent links need to get their morphism updated
return (dg', lv', markLinkUpdates dg' n nmod chL')
-- | mark all links adjacent to a node as update-pending
markLinkUpdates :: DGraph -> Node -> NodeMod -> ChangeList -> ChangeList
markLinkUpdates dg t nmod chL = let
(Just (ins, _, _, outs), _) = match t $ dgBody dg
in foldr (updateLinkChange (MkUpdate nmod) . dgl_id . fst) chL
$ ins ++ outs
-- | update or insert a link if said so in changelist
mkLinkUpdate :: LogicGraph -> (DGraph, LibEnv, ChangeList)
-> (Node, GMorphism, DGLinkType, XLink)
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkLinkUpdate lg (dg, lv, chL) (i, mr, tp, xl) = let ei = edgeId xl in
case retrieveLinkChange ei chL of
Nothing -> return (dg, lv, chL)
Just (chA, chL') -> do
(j, gs) <- signOfNode (target xl) dg
lkLab <- finalizeLink lg xl mr gs tp
-- if updating an existing link, the old one is deleted from dg first
dg' <- if chA == MkInsert then return dg else
fmap (changeDGH dg . DeleteEdge) $ lookupUniqueLink i ei dg
return (changeDGH dg' $ InsertEdge (i, j, lkLab), lv, chL')
-- | updates any necessary ThmLinks
mkThmLinkUpdates :: LogicGraph -> (DGraph, LibEnv, ChangeList) -> [XLink]
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkThmLinkUpdates lg (dg, lv, chL) xlks = do
mrs <- mapM (getTypeAndMorphism lg dg) xlks
foldM (mkLinkUpdate lg) (dg, lv, chL) mrs
{- | deletes those elements from dgraph that are marked for deletion in
changelist. for link deletion, the affected nodes are marked as such in chL -}
deleteElements :: DGraph -> ChangeList -> Result (DGraph, ChangeList)
deleteElements dg chL = do
(dg1, targets) <- foldM deleteLinkAux (dg, []) $ Set.toList $ deleteLinks chL
dg2 <- foldM (\ dg' -> liftM snd . deleteNode dg') dg1 $ Set.toList
$ deleteNodes chL
{- after deletion, all still-existing nodes which lost ingoing definition
links must be marked for updating. -}
chL' <- foldM (flip $ markNodeUpdates dg2) chL $ List.nub targets
return (dg2, chL' { deleteNodes = Set.empty, deleteLinks = Set.empty })
-- | look for given node in dg and mark as update-pending in changelist
markNodeUpdates :: Monad m => DGraph -> Node -> ChangeList -> m ChangeList
markNodeUpdates dg trg = case lab (dgBody dg) trg of
Nothing -> return
-- TODO: symMod was chosen to ensure updating, it does not always apply.
Just lbl -> return . updateNodeChange (MkUpdate symMod) (dgn_name lbl)
-- | deletes a link from dg and returns (def)links target id additionally
deleteLinkAux :: Monad m => (DGraph, [Node]) -> XLink -> m (DGraph, [Node])
deleteLinkAux (dg, tars) xl = case lookupUniqueNodeByName (source xl) dg of
Just (s, _) -> do
dg' <- liftM (changeDGH dg . DeleteEdge)
$ lookupUniqueLink s (edgeId xl) dg
if not $ isDefEdgeType (lType xl)
then return (dg', tars)
else case lookupUniqueNodeByName (target xl) dg of
Just (t, _) -> return (dg', t : tars)
Nothing -> fail $ "required target [" ++ target xl
++ "] was not found in DGraph!"
Nothing -> fail $ "required source [" ++ source xl
++ "] was not found in DGraph!"
-- | deletes a node from dg
deleteNode :: Monad m => DGraph -> NodeName -> m (Node, DGraph)
deleteNode dg nm = let nd = showName nm
in case lookupUniqueNodeByName nd dg of
Just (j, lbl) -> return (j, changeDGH dg $ DeleteNode (j, lbl))
Nothing -> fail $
"required node [" ++ nd ++ "] was not found in DGraph!"