module Static.History
( groupHistory
, changeDGH
, changesDGH
, updateDGOnly
, flatHistory
, negateChange
, getLastChange
, reverseHistory
, splitHistory
, applyProofHistory
, undoHistStep
, redoHistStep
, undoAllChanges
, togglePending
, justTogglePending
, clearHistory
) where
import Static.DevGraph
import Static.DgUtils
import qualified Common.Lib.SizedList as SizedList
import Data.Graph.Inductive.Graph as Graph
import Data.List
addToProofHistoryDG :: HistElem -> DGraph -> DGraph
addToProofHistoryDG :: HistElem -> DGraph -> DGraph
addToProofHistoryDG x :: HistElem
x dg :: DGraph
dg =
DGraph
dg { proofHistory :: ProofHistory
proofHistory = HistElem -> ProofHistory -> ProofHistory
forall a. a -> SizedList a -> SizedList a
SizedList.cons HistElem
x (ProofHistory -> ProofHistory) -> ProofHistory -> ProofHistory
forall a b. (a -> b) -> a -> b
$ DGraph -> ProofHistory
proofHistory DGraph
dg }
splitHistory :: DGraph -> DGraph -> (ProofHistory, ProofHistory)
splitHistory :: DGraph -> DGraph -> (ProofHistory, ProofHistory)
splitHistory oldGraph :: DGraph
oldGraph newGraph :: DGraph
newGraph = let
oldHist :: ProofHistory
oldHist = DGraph -> ProofHistory
proofHistory DGraph
oldGraph
newHist :: ProofHistory
newHist = DGraph -> ProofHistory
proofHistory DGraph
newGraph
diff :: ProofHistory
diff = Int -> ProofHistory -> ProofHistory
forall a. Int -> SizedList a -> SizedList a
SizedList.take (ProofHistory -> Int
forall a. SizedList a -> Int
SizedList.size ProofHistory
newHist Int -> Int -> Int
forall a. Num a => a -> a -> a
- ProofHistory -> Int
forall a. SizedList a -> Int
SizedList.size ProofHistory
oldHist)
ProofHistory
newHist
in (ProofHistory
oldHist, ProofHistory
diff)
reverseHistory :: SizedList.SizedList HistElem -> SizedList.SizedList HistElem
reverseHistory :: ProofHistory -> ProofHistory
reverseHistory = ProofHistory -> ProofHistory
forall a. SizedList a -> SizedList a
SizedList.reverse (ProofHistory -> ProofHistory)
-> (ProofHistory -> ProofHistory) -> ProofHistory -> ProofHistory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HistElem -> HistElem) -> ProofHistory -> ProofHistory
forall a b. (a -> b) -> SizedList a -> SizedList b
SizedList.map
(\ e :: HistElem
e -> case HistElem
e of
HistElem _ -> HistElem
e
HistGroup r :: DGRule
r l :: ProofHistory
l -> DGRule -> ProofHistory -> HistElem
HistGroup DGRule
r (ProofHistory -> HistElem) -> ProofHistory -> HistElem
forall a b. (a -> b) -> a -> b
$ ProofHistory -> ProofHistory
reverseHistory ProofHistory
l)
groupHistory :: DGraph -> DGRule -> DGraph -> DGraph
groupHistory :: DGraph -> DGRule -> DGraph -> DGraph
groupHistory oldGraph :: DGraph
oldGraph rule :: DGRule
rule newGraph :: DGraph
newGraph = let
(oldHist :: ProofHistory
oldHist, diff :: ProofHistory
diff) = DGraph -> DGraph -> (ProofHistory, ProofHistory)
splitHistory DGraph
oldGraph DGraph
newGraph
in if ProofHistory -> Bool
forall a. SizedList a -> Bool
SizedList.null ProofHistory
diff then DGraph
newGraph else
DGraph
newGraph { proofHistory :: ProofHistory
proofHistory = HistElem -> ProofHistory -> ProofHistory
forall a. a -> SizedList a -> SizedList a
SizedList.cons (DGRule -> ProofHistory -> HistElem
HistGroup DGRule
rule ProofHistory
diff) ProofHistory
oldHist }
getLastHistElem :: DGraph -> HistElem
getLastHistElem :: DGraph -> HistElem
getLastHistElem dg :: DGraph
dg = let hist :: ProofHistory
hist = DGraph -> ProofHistory
proofHistory DGraph
dg in
if ProofHistory -> Bool
forall a. SizedList a -> Bool
SizedList.null ProofHistory
hist then [Char] -> HistElem
forall a. HasCallStack => [Char] -> a
error "Static.DevGraph.getHistElem"
else ProofHistory -> HistElem
forall a. SizedList a -> a
SizedList.head ProofHistory
hist
getLastChange :: DGraph -> DGChange
getLastChange :: DGraph -> DGChange
getLastChange dg :: DGraph
dg = case DGraph -> HistElem
getLastHistElem DGraph
dg of
HistElem c :: DGChange
c -> DGChange
c
HistGroup _ _ -> [Char] -> DGChange
forall a. HasCallStack => [Char] -> a
error "Static.DevGraph.getLastChange"
negateChange :: DGChange -> DGChange
negateChange :: DGChange -> DGChange
negateChange change :: DGChange
change = case DGChange
change of
InsertNode x :: LNode DGNodeLab
x -> LNode DGNodeLab -> DGChange
DeleteNode LNode DGNodeLab
x
DeleteNode x :: LNode DGNodeLab
x -> LNode DGNodeLab -> DGChange
InsertNode LNode DGNodeLab
x
InsertEdge x :: LEdge DGLinkLab
x -> LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
x
DeleteEdge x :: LEdge DGLinkLab
x -> LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
x
SetNodeLab old :: DGNodeLab
old (node :: Int
node, new :: DGNodeLab
new) -> DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
new (Int
node, DGNodeLab
old)
flatHistory :: SizedList.SizedList HistElem -> [DGChange]
flatHistory :: ProofHistory -> [DGChange]
flatHistory h :: ProofHistory
h = if ProofHistory -> Bool
forall a. SizedList a -> Bool
SizedList.null ProofHistory
h then [] else
(case ProofHistory -> HistElem
forall a. SizedList a -> a
SizedList.head ProofHistory
h of
HistElem c :: DGChange
c -> [DGChange
c]
HistGroup _ l :: ProofHistory
l -> ProofHistory -> [DGChange]
flatHistory ProofHistory
l) [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++ ProofHistory -> [DGChange]
flatHistory (ProofHistory -> ProofHistory
forall a. SizedList a -> SizedList a
SizedList.tail ProofHistory
h)
undoHistStep :: DGraph -> (DGraph, [DGChange])
undoHistStep :: DGraph -> (DGraph, [DGChange])
undoHistStep dg :: DGraph
dg = let h :: ProofHistory
h = DGraph -> ProofHistory
proofHistory DGraph
dg in
if ProofHistory -> Bool
forall a. SizedList a -> Bool
SizedList.null ProofHistory
h then (DGraph
dg, []) else let
he :: HistElem
he = ProofHistory -> HistElem
forall a. SizedList a -> a
SizedList.head ProofHistory
h
(ndg :: DGraph
ndg, cs :: [DGChange]
cs) = case HistElem
he of
HistElem c :: DGChange
c -> let (dg2 :: DGraph
dg2, nc :: DGChange
nc) = DGraph -> DGChange -> (DGraph, DGChange)
updateDGOnly DGraph
dg (DGChange -> (DGraph, DGChange)) -> DGChange -> (DGraph, DGChange)
forall a b. (a -> b) -> a -> b
$ DGChange -> DGChange
negateChange DGChange
c in
(DGraph
dg2 { proofHistory :: ProofHistory
proofHistory = ProofHistory -> ProofHistory
forall a. SizedList a -> SizedList a
SizedList.tail ProofHistory
h }, [DGChange
nc])
HistGroup _ l :: ProofHistory
l -> let
(dg2 :: DGraph
dg2, ncs :: [[DGChange]]
ncs) = (DGraph -> HistElem -> (DGraph, [DGChange]))
-> DGraph -> [HistElem] -> (DGraph, [[DGChange]])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (\ g :: DGraph
g _ -> DGraph -> (DGraph, [DGChange])
undoHistStep DGraph
g)
DGraph
dg { proofHistory :: ProofHistory
proofHistory = ProofHistory -> ProofHistory -> ProofHistory
forall a. SizedList a -> SizedList a -> SizedList a
SizedList.append ProofHistory
l (ProofHistory -> ProofHistory) -> ProofHistory -> ProofHistory
forall a b. (a -> b) -> a -> b
$ ProofHistory -> ProofHistory
forall a. SizedList a -> SizedList a
SizedList.tail ProofHistory
h }
([HistElem] -> (DGraph, [[DGChange]]))
-> [HistElem] -> (DGraph, [[DGChange]])
forall a b. (a -> b) -> a -> b
$ ProofHistory -> [HistElem]
forall a. SizedList a -> [a]
SizedList.toList ProofHistory
l
in (DGraph
dg2, [[DGChange]] -> [DGChange]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[DGChange]]
ncs)
in (DGraph
ndg { redoHistory :: ProofHistory
redoHistory = HistElem -> ProofHistory -> ProofHistory
forall a. a -> SizedList a -> SizedList a
SizedList.cons HistElem
he (ProofHistory -> ProofHistory) -> ProofHistory -> ProofHistory
forall a b. (a -> b) -> a -> b
$ DGraph -> ProofHistory
redoHistory DGraph
dg }, [DGChange]
cs)
undoAllChangesAux :: DGraph -> DGraph
undoAllChangesAux :: DGraph -> DGraph
undoAllChangesAux dg :: DGraph
dg = let h :: ProofHistory
h = DGraph -> ProofHistory
proofHistory DGraph
dg in
if ProofHistory -> Bool
forall a. SizedList a -> Bool
SizedList.null ProofHistory
h then DGraph
dg else DGraph -> DGraph
undoAllChangesAux (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ (DGraph, [DGChange]) -> DGraph
forall a b. (a, b) -> a
fst ((DGraph, [DGChange]) -> DGraph) -> (DGraph, [DGChange]) -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> (DGraph, [DGChange])
undoHistStep DGraph
dg
undoAllChanges :: DGraph -> DGraph
undoAllChanges :: DGraph -> DGraph
undoAllChanges dg :: DGraph
dg = let nDg :: DGraph
nDg = DGraph -> DGraph
undoAllChangesAux DGraph
dg in
DGraph
nDg { getNewEdgeId :: EdgeId
getNewEdgeId = EdgeId -> EdgeId
incEdgeId (EdgeId -> EdgeId) -> EdgeId -> EdgeId
forall a b. (a -> b) -> a -> b
$ [EdgeId] -> EdgeId
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (EdgeId
startEdgeId
EdgeId -> [EdgeId] -> [EdgeId]
forall a. a -> [a] -> [a]
: (LEdge DGLinkLab -> EdgeId) -> [LEdge DGLinkLab] -> [EdgeId]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, l :: DGLinkLab
l) -> DGLinkLab -> EdgeId
dgl_id DGLinkLab
l) (DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
nDg)) }
redoHistStep :: DGraph -> (DGraph, [DGChange])
redoHistStep :: DGraph -> (DGraph, [DGChange])
redoHistStep dg :: DGraph
dg = let h :: ProofHistory
h = DGraph -> ProofHistory
redoHistory DGraph
dg in
if ProofHistory -> Bool
forall a. SizedList a -> Bool
SizedList.null ProofHistory
h then (DGraph
dg, []) else
let he :: HistElem
he = ProofHistory -> HistElem
forall a. SizedList a -> a
SizedList.head ProofHistory
h
cs :: [DGChange]
cs = [DGChange] -> [DGChange]
forall a. [a] -> [a]
reverse ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ ProofHistory -> [DGChange]
flatHistory (ProofHistory -> [DGChange]) -> ProofHistory -> [DGChange]
forall a b. (a -> b) -> a -> b
$ HistElem -> ProofHistory
forall a. a -> SizedList a
SizedList.singleton HistElem
he
(ndg :: DGraph
ndg, ncs :: [DGChange]
ncs) = DGraph -> [DGChange] -> (DGraph, [DGChange])
updateDGAndChanges DGraph
dg [DGChange]
cs
in (DGraph
ndg { proofHistory :: ProofHistory
proofHistory = HistElem -> ProofHistory -> ProofHistory
forall a. a -> SizedList a -> SizedList a
SizedList.cons HistElem
he (ProofHistory -> ProofHistory) -> ProofHistory -> ProofHistory
forall a b. (a -> b) -> a -> b
$ DGraph -> ProofHistory
proofHistory DGraph
dg
, redoHistory :: ProofHistory
redoHistory = ProofHistory -> ProofHistory
forall a. SizedList a -> SizedList a
SizedList.tail ProofHistory
h }, [DGChange]
ncs)
applyProofHistory :: SizedList.SizedList HistElem -> DGraph -> DGraph
applyProofHistory :: ProofHistory -> DGraph -> DGraph
applyProofHistory l :: ProofHistory
l = ProofHistory -> DGraph -> DGraph
applyReverseHistory (ProofHistory -> DGraph -> DGraph)
-> ProofHistory -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ ProofHistory -> ProofHistory
reverseHistory ProofHistory
l
applyReverseHistory :: SizedList.SizedList HistElem -> DGraph -> DGraph
applyReverseHistory :: ProofHistory -> DGraph -> DGraph
applyReverseHistory l :: ProofHistory
l dg :: DGraph
dg = if ProofHistory -> Bool
forall a. SizedList a -> Bool
SizedList.null ProofHistory
l then DGraph
dg else
ProofHistory -> DGraph -> DGraph
applyReverseHistory (ProofHistory -> ProofHistory
forall a. SizedList a -> SizedList a
SizedList.tail ProofHistory
l) (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ case ProofHistory -> HistElem
forall a. SizedList a -> a
SizedList.head ProofHistory
l of
HistElem c :: DGChange
c -> DGraph -> DGChange -> DGraph
changeDGH DGraph
dg DGChange
c
HistGroup r :: DGRule
r h :: ProofHistory
h -> let dg2 :: DGraph
dg2 = ProofHistory -> DGraph -> DGraph
applyReverseHistory ProofHistory
h DGraph
dg in
DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg DGRule
r DGraph
dg2
changesDGH :: DGraph -> [DGChange] -> DGraph
changesDGH :: DGraph -> [DGChange] -> DGraph
changesDGH = (DGraph -> DGChange -> DGraph) -> DGraph -> [DGChange] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' DGraph -> DGChange -> DGraph
changeDGH
togglePending :: DGraph -> [LEdge DGLinkLab] -> DGraph
togglePending :: DGraph -> [LEdge DGLinkLab] -> DGraph
togglePending dg :: DGraph
dg = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg ([DGChange] -> DGraph)
-> ([LEdge DGLinkLab] -> [DGChange]) -> [LEdge DGLinkLab] -> DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LEdge DGLinkLab -> [DGChange]) -> [LEdge DGLinkLab] -> [DGChange]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
(\ e :: LEdge DGLinkLab
e@(s :: Int
s, t :: Int
t, l :: DGLinkLab
l) ->
[LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
e, LEdge DGLinkLab -> DGChange
InsertEdge
(Int
s, Int
t, DGLinkLab
l { dglPending :: Bool
dglPending = Bool -> Bool
not (DGLinkLab -> Bool
dglPending DGLinkLab
l)})])
justTogglePending :: DGraph -> [LEdge DGLinkLab] -> DGraph
justTogglePending :: DGraph -> [LEdge DGLinkLab] -> DGraph
justTogglePending = (DGraph -> LEdge DGLinkLab -> DGraph)
-> DGraph -> [LEdge DGLinkLab] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' DGraph -> LEdge DGLinkLab -> DGraph
togglePendFlag
togglePendFlag :: DGraph -> LEdge DGLinkLab -> DGraph
togglePendFlag :: DGraph -> LEdge DGLinkLab -> DGraph
togglePendFlag dg :: DGraph
dg (v :: Int
v, _, l :: DGLinkLab
l) = let
(Just (ins :: Adj DGLinkLab
ins, _, sl :: DGNodeLab
sl, outs :: Adj DGLinkLab
outs), rg :: Gr DGNodeLab DGLinkLab
rg) = Int
-> Gr DGNodeLab DGLinkLab
-> (Maybe (Adj DGLinkLab, Int, DGNodeLab, Adj DGLinkLab),
Gr DGNodeLab DGLinkLab)
forall (gr :: * -> * -> *) a b.
Graph gr =>
Int -> gr a b -> Decomp gr a b
match Int
v (Gr DGNodeLab DGLinkLab
-> (Maybe (Adj DGLinkLab, Int, DGNodeLab, Adj DGLinkLab),
Gr DGNodeLab DGLinkLab))
-> Gr DGNodeLab DGLinkLab
-> (Maybe (Adj DGLinkLab, Int, DGNodeLab, Adj DGLinkLab),
Gr DGNodeLab DGLinkLab)
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
in DGraph
dg { dgBody :: Gr DGNodeLab DGLinkLab
dgBody = (Adj DGLinkLab
ins, Int
v, DGNodeLab
sl
, ((DGLinkLab, Int) -> (DGLinkLab, Int))
-> Adj DGLinkLab -> Adj DGLinkLab
forall a b. (a -> b) -> [a] -> [b]
map (\ (o :: DGLinkLab
o, t :: Int
t) ->
if DGLinkLab -> EdgeId
dgl_id DGLinkLab
o EdgeId -> EdgeId -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkLab -> EdgeId
dgl_id DGLinkLab
l
then (DGLinkLab
o { dglPending :: Bool
dglPending = Bool -> Bool
not (DGLinkLab -> Bool
dglPending DGLinkLab
o) }, Int
t)
else (DGLinkLab
o, Int
t)) Adj DGLinkLab
outs) (Adj DGLinkLab, Int, DGNodeLab, Adj DGLinkLab)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
Context a b -> gr a b -> gr a b
& Gr DGNodeLab DGLinkLab
rg }
clearRedo :: DGraph -> DGraph
clearRedo :: DGraph -> DGraph
clearRedo g :: DGraph
g = DGraph
g { redoHistory :: ProofHistory
redoHistory = ProofHistory
forall a. SizedList a
SizedList.empty }
clearHistory :: DGraph -> DGraph
clearHistory :: DGraph -> DGraph
clearHistory g :: DGraph
g = DGraph
g { proofHistory :: ProofHistory
proofHistory = ProofHistory
forall a. SizedList a
SizedList.empty }
changeDGH :: DGraph -> DGChange -> DGraph
changeDGH :: DGraph -> DGChange -> DGraph
changeDGH g :: DGraph
g c :: DGChange
c = let (ng :: DGraph
ng, nc :: DGChange
nc) = DGraph -> DGChange -> (DGraph, DGChange)
updateDGOnly DGraph
g DGChange
c in
HistElem -> DGraph -> DGraph
addToProofHistoryDG (DGChange -> HistElem
HistElem DGChange
nc) (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> DGraph
clearRedo DGraph
ng
updateDGAndChanges :: DGraph -> [DGChange] -> (DGraph, [DGChange])
updateDGAndChanges :: DGraph -> [DGChange] -> (DGraph, [DGChange])
updateDGAndChanges = (DGraph -> DGChange -> (DGraph, DGChange))
-> DGraph -> [DGChange] -> (DGraph, [DGChange])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL DGraph -> DGChange -> (DGraph, DGChange)
updateDGOnly
updateDGOnly :: DGraph -> DGChange -> (DGraph, DGChange)
updateDGOnly :: DGraph -> DGChange -> (DGraph, DGChange)
updateDGOnly g :: DGraph
g c :: DGChange
c =
case DGChange
c of
InsertNode n :: LNode DGNodeLab
n -> (LNode DGNodeLab -> DGraph -> DGraph
insLNodeDG LNode DGNodeLab
n DGraph
g, LNode DGNodeLab -> DGChange
InsertNode LNode DGNodeLab
n)
DeleteNode n :: LNode DGNodeLab
n@(i :: Int
i, _) -> (Int -> DGraph -> DGraph
delNodeDG Int
i DGraph
g, LNode DGNodeLab -> DGChange
DeleteNode LNode DGNodeLab
n)
InsertEdge e :: LEdge DGLinkLab
e -> let (newEdge :: LEdge DGLinkLab
newEdge, ng :: DGraph
ng) = LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG LEdge DGLinkLab
e DGraph
g in
(DGraph
ng, LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
newEdge)
DeleteEdge e :: LEdge DGLinkLab
e -> (LEdge DGLinkLab -> DGraph -> DGraph
delLEdgeDG LEdge DGLinkLab
e DGraph
g, LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
e)
SetNodeLab _ n :: LNode DGNodeLab
n -> let (newG :: DGraph
newG, o :: DGNodeLab
o) = LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab)
labelNodeDG LNode DGNodeLab
n DGraph
g in
(DGraph
newG, DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
o LNode DGNodeLab
n)