55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Static/History.hs
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederDescription : history treatment for development graphs
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederMaintainer : Christian.Maeder@dfki.de
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederStability : provisional
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederPortability : non-portable(Logic)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maederfunctions to keep the history entries in sync with the actual graph changes
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-}
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maedermodule Static.History
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder ( groupHistory
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , changeDGH
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , changesDGH
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , updateDGOnly
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , flatHistory
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , negateChange
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , getLastChange
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , reverseHistory
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , splitHistory
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , applyProofHistory
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , undoHistStep
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , redoHistStep
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder , undoAllChanges
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder , togglePending
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder , justTogglePending
59f44203d89ff92c042f2e5d3d0d324488250b37Christian Maeder , clearHistory
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder ) where
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maederimport Static.DevGraph
c208973c890b8f993297720fd0247bc7481d4304Christian Maederimport Static.DgUtils
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maederimport qualified Common.Lib.SizedList as SizedList
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maederimport Data.Graph.Inductive.Graph as Graph
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maederimport Data.List
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | add a history item to current history.
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederaddToProofHistoryDG :: HistElem -> DGraph -> DGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederaddToProofHistoryDG x dg =
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder dg { proofHistory = SizedList.cons x $ proofHistory dg }
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | get the old history and the new offset
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedersplitHistory :: DGraph -> DGraph -> (ProofHistory, ProofHistory)
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedersplitHistory oldGraph newGraph = let
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder oldHist = proofHistory oldGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder newHist = proofHistory newGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder diff = SizedList.take (SizedList.size newHist - SizedList.size oldHist)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder newHist
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder in (oldHist, diff)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | reverse the history list
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederreverseHistory :: SizedList.SizedList HistElem -> SizedList.SizedList HistElem
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederreverseHistory = SizedList.reverse . SizedList.map
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder (\ e -> case e of
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder HistElem _ -> e
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder HistGroup r l -> HistGroup r $ reverseHistory l)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | group pushd changes, leave history of old graph unchanged
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedergroupHistory :: DGraph -> DGRule -> DGraph -> DGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedergroupHistory oldGraph rule newGraph = let
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder (oldHist, diff) = splitHistory oldGraph newGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder in if SizedList.null diff then newGraph else
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder newGraph { proofHistory = SizedList.cons (HistGroup rule diff) oldHist }
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | get most recent step
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedergetLastHistElem :: DGraph -> HistElem
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedergetLastHistElem dg = let hist = proofHistory dg in
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder if SizedList.null hist then error "Static.DevGraph.getHistElem"
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder else SizedList.head hist
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | get most recent change
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedergetLastChange :: DGraph -> DGChange
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedergetLastChange dg = case getLastHistElem dg of
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder HistElem c -> c
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder HistGroup _ _ -> error "Static.DevGraph.getLastChange"
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | negate change
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedernegateChange :: DGChange -> DGChange
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedernegateChange change = case change of
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder InsertNode x -> DeleteNode x
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder DeleteNode x -> InsertNode x
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder InsertEdge x -> DeleteEdge x
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder DeleteEdge x -> InsertEdge x
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder SetNodeLab old (node, new) -> SetNodeLab new (node, old)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederflatHistory :: SizedList.SizedList HistElem -> [DGChange]
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederflatHistory h = if SizedList.null h then [] else
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder (case SizedList.head h of
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder HistElem c -> [c]
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder HistGroup _ l -> flatHistory l) ++ flatHistory (SizedList.tail h)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederundoHistStep :: DGraph -> (DGraph, [DGChange])
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederundoHistStep dg = let h = proofHistory dg in
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder if SizedList.null h then (dg, []) else let
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder he = SizedList.head h
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder (ndg, cs) = case he of
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder HistElem c -> let (dg2, nc) = updateDGOnly dg $ negateChange c in
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder (dg2 { proofHistory = SizedList.tail h }, [nc])
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder HistGroup _ l -> let
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder (dg2, ncs) = mapAccumL (\ g _ -> undoHistStep g)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder dg { proofHistory = SizedList.append l $ SizedList.tail h }
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder $ SizedList.toList l
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder in (dg2, concat ncs)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder in (ndg { redoHistory = SizedList.cons he $ redoHistory dg }, cs)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
35365329a925cdcf3a5c7c424303fe3bd3d0601bChristian MaederundoAllChangesAux :: DGraph -> DGraph
35365329a925cdcf3a5c7c424303fe3bd3d0601bChristian MaederundoAllChangesAux dg = let h = proofHistory dg in
35365329a925cdcf3a5c7c424303fe3bd3d0601bChristian Maeder if SizedList.null h then dg else undoAllChangesAux $ fst $ undoHistStep dg
35365329a925cdcf3a5c7c424303fe3bd3d0601bChristian Maeder
d57a083760050f91189fb67b46f2b59f4f628f27Christian MaederundoAllChanges :: DGraph -> DGraph
35365329a925cdcf3a5c7c424303fe3bd3d0601bChristian MaederundoAllChanges dg = let nDg = undoAllChangesAux dg in
35365329a925cdcf3a5c7c424303fe3bd3d0601bChristian Maeder nDg { getNewEdgeId = incEdgeId $ maximum (startEdgeId
35365329a925cdcf3a5c7c424303fe3bd3d0601bChristian Maeder : map (\ (_, _, l) -> dgl_id l) (labEdgesDG nDg)) }
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederredoHistStep :: DGraph -> (DGraph, [DGChange])
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederredoHistStep dg = let h = redoHistory dg in
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder if SizedList.null h then (dg, []) else
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder let he = SizedList.head h
98ddb1db022a8167d2442a6290b12c128bee576fChristian Maeder cs = reverse $ flatHistory $ SizedList.singleton he
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder (ndg, ncs) = updateDGAndChanges dg cs
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder in (ndg { proofHistory = SizedList.cons he $ proofHistory dg
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder , redoHistory = SizedList.tail h }, ncs)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | apply the reversed changes to the graph and add them to the history
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederapplyProofHistory :: SizedList.SizedList HistElem -> DGraph -> DGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederapplyProofHistory l = applyReverseHistory $ reverseHistory l
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederapplyReverseHistory :: SizedList.SizedList HistElem -> DGraph -> DGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederapplyReverseHistory l dg = if SizedList.null l then dg else
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder applyReverseHistory (SizedList.tail l) $ case SizedList.head l of
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder HistElem c -> changeDGH dg c
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder HistGroup r h -> let dg2 = applyReverseHistory h dg in
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder groupHistory dg r dg2
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | change the given DGraph with a list of changes
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederchangesDGH :: DGraph -> [DGChange] -> DGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederchangesDGH = foldl' changeDGH
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | toggle the pending flag of the input edges
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedertogglePending :: DGraph -> [LEdge DGLinkLab] -> DGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaedertogglePending dg = changesDGH dg . concatMap
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder (\ e@(s, t, l) ->
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder [DeleteEdge e, InsertEdge
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder (s, t, l { dglPending = not (dglPending l)})])
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder-- | toggle the pending flag of the input edges (without history change)
d57a083760050f91189fb67b46f2b59f4f628f27Christian MaederjustTogglePending :: DGraph -> [LEdge DGLinkLab] -> DGraph
d57a083760050f91189fb67b46f2b59f4f628f27Christian MaederjustTogglePending = foldl' togglePendFlag
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder
d57a083760050f91189fb67b46f2b59f4f628f27Christian MaedertogglePendFlag :: DGraph -> LEdge DGLinkLab -> DGraph
d57a083760050f91189fb67b46f2b59f4f628f27Christian MaedertogglePendFlag dg (v, _, l) = let
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder (Just (ins, _, sl, outs), rg) = match v $ dgBody dg
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder in dg { dgBody = (ins, v, sl
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder , map (\ (o, t) ->
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder if dgl_id o == dgl_id l
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder then (o { dglPending = not (dglPending o) }, t)
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder else (o, t)) outs) & rg }
d57a083760050f91189fb67b46f2b59f4f628f27Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | forget redo stack
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederclearRedo :: DGraph -> DGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederclearRedo g = g { redoHistory = SizedList.empty }
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
59f44203d89ff92c042f2e5d3d0d324488250b37Christian Maeder-- | forget history
59f44203d89ff92c042f2e5d3d0d324488250b37Christian MaederclearHistory :: DGraph -> DGraph
59f44203d89ff92c042f2e5d3d0d324488250b37Christian MaederclearHistory g = g { proofHistory = SizedList.empty }
59f44203d89ff92c042f2e5d3d0d324488250b37Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | change the given DGraph and the history with the given DGChange.
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederchangeDGH :: DGraph -> DGChange -> DGraph
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederchangeDGH g c = let (ng, nc) = updateDGOnly g c in
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder addToProofHistoryDG (HistElem nc) $ clearRedo ng
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder-- | change the given DGraph with a list of DGChange
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederupdateDGAndChanges :: DGraph -> [DGChange] -> (DGraph, [DGChange])
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederupdateDGAndChanges = mapAccumL updateDGOnly
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder{- | change the given DGraph with given DGChange and return a new DGraph and
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder the processed DGChange as well. -}
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederupdateDGOnly :: DGraph -> DGChange -> (DGraph, DGChange)
55c5e901b5c3466300009135585bc70bd576dcb6Christian MaederupdateDGOnly g c =
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder case c of
66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder InsertNode n -> (insLNodeDG n g, InsertNode n)
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder DeleteNode n@(i, _) -> (delNodeDG i g, DeleteNode n)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder InsertEdge e -> let (newEdge, ng) = insLEdgeDG e g in
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder (ng, InsertEdge newEdge)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder DeleteEdge e -> (delLEdgeDG e g, DeleteEdge e)
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder SetNodeLab _ n -> let (newG, o) = labelNodeDG n g in
66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder (newG, SetNodeLab o n)