55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{- |

881f43de18aeae879886be203cd32e90051799c0Till MossakowskiModule : ./Static/ApplyChanges.hs

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : apply xupdate changes to a development graph

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiCopyright : (c) Christian Maeder, DFKI GmbH 2010

881f43de18aeae879886be203cd32e90051799c0Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Christian.Maeder@dfki.de

881f43de18aeae879886be203cd32e90051799c0Till MossakowskiStability : provisional

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederPortability : non-portable(Grothendieck)

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederadjust development graph according to xupdate information

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski-}

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskimodule Static.ApplyChanges (dgXUpdateMods, dgXUpdate) where

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederimport Static.ComputeTheory

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport Static.DevGraph

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederimport Static.DgUtils

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederimport Static.FromXml

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederimport Static.GTheory

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederimport Static.History (undoAllChanges, changeDGH, clearHistory)

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederimport Static.ToXml

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederimport Static.XGraph

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport Static.XSimplePath

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Driver.Options

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport Driver.ReadFn (libNameToFile)

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport Driver.WriteFn (writeVerbFile)

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport Comorphisms.LogicGraph (logicGraph)

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport Common.LibName

81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maederimport Common.ResultT

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport Common.Result

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport Common.XUpdate

a64026be6c3fd217259aab4ee0a5934192255e88mscodescu

a64026be6c3fd217259aab4ee0a5934192255e88mscodescuimport Logic.Grothendieck

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport Control.Monad

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederimport Control.Monad.Trans (lift)

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederimport Data.Graph.Inductive.Graph (Node, match, lab)

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederimport qualified Data.List as List (nub)

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederimport qualified Data.Set as Set

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederimport qualified Data.Map as Map

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederimport Text.XML.Light hiding (Node)

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder{- incorporate a previous session (diff) upon an exising dgraph. The structure

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maederis as follows:

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder - roll back the current dg to it's initial state

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder - apply diff to initial dg

a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowski - create xgraph from dg'

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder - incorporate changes into current dg; the xgraph serves for structuring.

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederNOTE: The data-type NodeMod holds information about the changes upon a node.

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederHowever, with the current usage, a Boolean value would do since the module only

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederknows update or don't-update. We kept the NodeMod-approach since proper usage

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettichof the NodeMod data type might allow more precise updating.

fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder

2bbf88585fe313af8585da0288880310cc1b027dChristian MaederNOTE(2): If any element changes, ALL elements that lie underneath in terms of

a64026be6c3fd217259aab4ee0a5934192255e88mscodescusignature-hierachy will receive updating as well (even if two subsequent

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederchanges would lead to an unchanged signature further down). -}

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder-- | recieves diff as a string and current dg and prepares those for processing

da955132262baab309a50fdffe228c9efe68251dCui JiandgXUpdate :: HetcatsOpts -> String -> LibEnv -> LibName -> DGraph

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski -> ResultT IO (LibName, LibEnv)

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederdgXUpdate opts xs le ln dg = case parseXMLDoc xs of

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder Nothing -> fail "dgXUpdate: cannot parse xupdate file"

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski Just diff -> let

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder -- we assume that the diff refers to an unchanged dg..

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder dgOld = undoAllChanges dg

eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder oldLId = getNewEdgeId dgOld

d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder xorig = dGraph opts le ln dgOld

d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in dgXUpdateMods opts xorig oldLId diff le ln dg

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder{- | updates a dgraph partially in accordance with changelist data from a .diff

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederapplication. an xgraph is created and used as a guideline for signature-

2bbf88585fe313af8585da0288880310cc1b027dChristian Maederhierachy and for retrieving required new data. -}

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederdgXUpdateMods :: HetcatsOpts -> Element -> EdgeId -> Element -> LibEnv

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder -> LibName -> DGraph -> ResultT IO (LibName, LibEnv)

fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian MaederdgXUpdateMods opts xorig oldLId diff le ln dg = do

fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder -- dg with changes incorporated (diff only) and listing of these changes

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder (xml, chL) <- liftR $ changeXmlMod xorig diff

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder lift $ writeVerbFile opts (libNameToFile ln ++ ".xml")

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder $ ppTopElement $ cleanUpElem xml

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder xgr <- liftR $ xGraph xml

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder -- the changes will now be incorporated in the so-far unchanged session-dg.

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder (dg0, chL') <- liftR $ deleteElements dg chL

fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder let newLId = max (nextLinkId xgr) $ getNewEdgeId dg

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder -- to anticipate multiple use of link-ids

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder dg1 = renumberDGLinks oldLId newLId dg0

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder dg2 = dg1 { globalAnnos = globAnnos xgr

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder -- TODO as of now, ALL nodes will be removed from globalEnv!

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder , globalEnv = Map.empty }

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder (dg3, le', chL'') <- iterateXgBody opts xgr le dg2 chL'

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder -- for any leftover theorem link updates, the respective links are deleted

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich dgFin <- fmap clearHistory $ deleteLeftoverChanges dg3 chL''

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich 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!"