{- |
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 qualified Control.Monad.Fail as Fail
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 :: HetcatsOpts
-> String
-> LibEnv
-> LibName
-> DGraph
-> ResultT IO (LibName, LibEnv)
dgXUpdate opts :: HetcatsOpts
opts xs :: String
xs le :: LibEnv
le ln :: LibName
ln dg :: DGraph
dg = case String -> Maybe Element
forall s. XmlSource s => s -> Maybe Element
parseXMLDoc String
xs of
    Nothing -> String -> ResultT IO (LibName, LibEnv)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "dgXUpdate: cannot parse xupdate file"
    Just diff :: Element
diff -> let
      -- we assume that the diff refers to an unchanged dg..
      dgOld :: DGraph
dgOld = DGraph -> DGraph
undoAllChanges DGraph
dg
      oldLId :: EdgeId
oldLId = DGraph -> EdgeId
getNewEdgeId DGraph
dgOld
      xorig :: Element
xorig = HetcatsOpts -> LibEnv -> LibName -> DGraph -> Element
dGraph HetcatsOpts
opts LibEnv
le LibName
ln DGraph
dgOld
      in HetcatsOpts
-> Element
-> EdgeId
-> Element
-> LibEnv
-> LibName
-> DGraph
-> ResultT IO (LibName, LibEnv)
dgXUpdateMods HetcatsOpts
opts Element
xorig EdgeId
oldLId Element
diff LibEnv
le LibName
ln DGraph
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 :: HetcatsOpts
-> Element
-> EdgeId
-> Element
-> LibEnv
-> LibName
-> DGraph
-> ResultT IO (LibName, LibEnv)
dgXUpdateMods opts :: HetcatsOpts
opts xorig :: Element
xorig oldLId :: EdgeId
oldLId diff :: Element
diff le :: LibEnv
le ln :: LibName
ln dg :: DGraph
dg = do
  -- dg with changes incorporated (diff only) and listing of these changes
  (xml :: Element
xml, chL :: ChangeList
chL) <- Result (Element, ChangeList) -> ResultT IO (Element, ChangeList)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (Element, ChangeList) -> ResultT IO (Element, ChangeList))
-> Result (Element, ChangeList) -> ResultT IO (Element, ChangeList)
forall a b. (a -> b) -> a -> b
$ Element -> Element -> Result (Element, ChangeList)
forall (m :: * -> *).
MonadFail m =>
Element -> Element -> m (Element, ChangeList)
changeXmlMod Element
xorig Element
diff
  IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> String -> String -> IO ()
writeVerbFile HetcatsOpts
opts (LibName -> String
libNameToFile LibName
ln String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".xml")
    (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Element -> String
ppTopElement (Element -> String) -> Element -> String
forall a b. (a -> b) -> a -> b
$ Element -> Element
cleanUpElem Element
xml
  XGraph
xgr <- Result XGraph -> ResultT IO XGraph
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result XGraph -> ResultT IO XGraph)
-> Result XGraph -> ResultT IO XGraph
forall a b. (a -> b) -> a -> b
$ Element -> Result XGraph
xGraph Element
xml
  -- the changes will now be incorporated in the so-far unchanged session-dg.
  (dg0 :: DGraph
dg0, chL' :: ChangeList
chL') <- Result (DGraph, ChangeList) -> ResultT IO (DGraph, ChangeList)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (DGraph, ChangeList) -> ResultT IO (DGraph, ChangeList))
-> Result (DGraph, ChangeList) -> ResultT IO (DGraph, ChangeList)
forall a b. (a -> b) -> a -> b
$ DGraph -> ChangeList -> Result (DGraph, ChangeList)
deleteElements DGraph
dg ChangeList
chL
  let newLId :: EdgeId
newLId = EdgeId -> EdgeId -> EdgeId
forall a. Ord a => a -> a -> a
max (XGraph -> EdgeId
nextLinkId XGraph
xgr) (EdgeId -> EdgeId) -> EdgeId -> EdgeId
forall a b. (a -> b) -> a -> b
$ DGraph -> EdgeId
getNewEdgeId DGraph
dg
      -- to anticipate multiple use of link-ids
      dg1 :: DGraph
dg1 = EdgeId -> EdgeId -> DGraph -> DGraph
renumberDGLinks EdgeId
oldLId EdgeId
newLId DGraph
dg0
      dg2 :: DGraph
dg2 = DGraph
dg1 { globalAnnos :: GlobalAnnos
globalAnnos = XGraph -> GlobalAnnos
globAnnos XGraph
xgr
                -- TODO as of now, ALL nodes will be removed from globalEnv!
                , globalEnv :: GlobalEnv
globalEnv = GlobalEnv
forall k a. Map k a
Map.empty }
  (dg3 :: DGraph
dg3, le' :: LibEnv
le', chL'' :: ChangeList
chL'') <- HetcatsOpts
-> XGraph
-> LibEnv
-> DGraph
-> ChangeList
-> ResultT IO (DGraph, LibEnv, ChangeList)
iterateXgBody HetcatsOpts
opts XGraph
xgr LibEnv
le DGraph
dg2 ChangeList
chL'
  -- for any leftover theorem link updates, the respective links are deleted
  DGraph
dgFin <- (DGraph -> DGraph) -> ResultT IO DGraph -> ResultT IO DGraph
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DGraph -> DGraph
clearHistory (ResultT IO DGraph -> ResultT IO DGraph)
-> ResultT IO DGraph -> ResultT IO DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> ChangeList -> ResultT IO DGraph
forall (m :: * -> *).
MonadFail m =>
DGraph -> ChangeList -> m DGraph
deleteLeftoverChanges DGraph
dg3 ChangeList
chL''
  (LibName, LibEnv) -> ResultT IO (LibName, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName
ln, LibEnv -> LibEnv
computeLibEnvTheories (LibEnv -> LibEnv) -> LibEnv -> LibEnv
forall a b. (a -> b) -> a -> b
$ LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
dgFin LibEnv
le')

{- | deletes theorem links from dg that were left-over in changelist.
fails if any other undone changes are found -}
deleteLeftoverChanges :: Fail.MonadFail m => DGraph -> ChangeList -> m DGraph
deleteLeftoverChanges :: DGraph -> ChangeList -> m DGraph
deleteLeftoverChanges dg :: DGraph
dg chL :: ChangeList
chL = let lIds :: [EdgeId]
lIds = Map EdgeId ChangeAction -> [EdgeId]
forall k a. Map k a -> [k]
Map.keys (Map EdgeId ChangeAction -> [EdgeId])
-> Map EdgeId ChangeAction -> [EdgeId]
forall a b. (a -> b) -> a -> b
$ ChangeList -> Map EdgeId ChangeAction
changeLinks ChangeList
chL in do
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ChangeList
emptyChangeList ChangeList -> ChangeList -> Bool
forall a. Eq a => a -> a -> Bool
== ChangeList
chL { changeLinks :: Map EdgeId ChangeAction
changeLinks = Map EdgeId ChangeAction
forall k a. Map k a
Map.empty })
    (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "some changes could not be processed:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ChangeList -> String
forall a. Show a => a -> String
show ChangeList
chL
  (DGraph -> EdgeId -> m DGraph) -> DGraph -> [EdgeId] -> m DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dg' :: DGraph
dg' ei :: EdgeId
ei -> case EdgeId -> DGraph -> [LEdge DGLinkLab]
getDGLinksById EdgeId
ei DGraph
dg' of
    [ledge :: LEdge DGLinkLab
ledge@(_, _, lkLab :: DGLinkLab
lkLab)] | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkType -> Bool
isDefEdge (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lkLab -> DGraph -> m DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return
      (DGraph -> m DGraph) -> DGraph -> m DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> DGChange -> DGraph
changeDGH DGraph
dg' (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
ledge
    _ -> String -> m DGraph
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m DGraph) -> String -> m DGraph
forall a b. (a -> b) -> a -> b
$ "deleteLeftoverChanges: conflict with edge #" String -> String -> String
forall a. [a] -> [a] -> [a]
++ EdgeId -> String
forall a. Show a => a -> String
show EdgeId
ei
    ) DGraph
dg [EdgeId]
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 :: HetcatsOpts
-> XGraph
-> LibEnv
-> DGraph
-> ChangeList
-> ResultT IO (DGraph, LibEnv, ChangeList)
iterateXgBody opts :: HetcatsOpts
opts xgr :: XGraph
xgr lv :: LibEnv
lv dg :: DGraph
dg chL :: ChangeList
chL = let lg :: LogicGraph
lg = LogicGraph
logicGraph in do
  (DGraph, LibEnv, ChangeList)
rs1 <- ((DGraph, LibEnv, ChangeList)
 -> XNode -> ResultT IO (DGraph, LibEnv, ChangeList))
-> (DGraph, LibEnv, ChangeList)
-> [XNode]
-> ResultT IO (DGraph, LibEnv, ChangeList)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HetcatsOpts
-> LogicGraph
-> Maybe G_theory
-> (DGraph, LibEnv, ChangeList)
-> XNode
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkNodeUpdate HetcatsOpts
opts LogicGraph
lg Maybe G_theory
forall a. Maybe a
Nothing) (DGraph
dg, LibEnv
lv, ChangeList
chL) ([XNode] -> ResultT IO (DGraph, LibEnv, ChangeList))
-> [XNode] -> ResultT IO (DGraph, LibEnv, ChangeList)
forall a b. (a -> b) -> a -> b
$ XGraph -> [XNode]
startNodes XGraph
xgr
  (DGraph, LibEnv, ChangeList)
rs2 <- ((DGraph, LibEnv, ChangeList)
 -> [([XLink], XNode)] -> ResultT IO (DGraph, LibEnv, ChangeList))
-> (DGraph, LibEnv, ChangeList)
-> [[([XLink], XNode)]]
-> ResultT IO (DGraph, LibEnv, ChangeList)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (((DGraph, LibEnv, ChangeList)
 -> ([XLink], XNode) -> ResultT IO (DGraph, LibEnv, ChangeList))
-> (DGraph, LibEnv, ChangeList)
-> [([XLink], XNode)]
-> ResultT IO (DGraph, LibEnv, ChangeList)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HetcatsOpts
-> LogicGraph
-> (DGraph, LibEnv, ChangeList)
-> ([XLink], XNode)
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkXStepUpdate HetcatsOpts
opts LogicGraph
lg)) (DGraph, LibEnv, ChangeList)
rs1 ([[([XLink], XNode)]] -> ResultT IO (DGraph, LibEnv, ChangeList))
-> [[([XLink], XNode)]] -> ResultT IO (DGraph, LibEnv, ChangeList)
forall a b. (a -> b) -> a -> b
$ [[([XLink], XNode)]] -> [[([XLink], XNode)]]
forall a. [a] -> [a]
reverse ([[([XLink], XNode)]] -> [[([XLink], XNode)]])
-> [[([XLink], XNode)]] -> [[([XLink], XNode)]]
forall a b. (a -> b) -> a -> b
$ XGraph -> [[([XLink], XNode)]]
xg_body XGraph
xgr
  LogicGraph
-> (DGraph, LibEnv, ChangeList)
-> [XLink]
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkThmLinkUpdates LogicGraph
lg (DGraph, LibEnv, ChangeList)
rs2 ([XLink] -> ResultT IO (DGraph, LibEnv, ChangeList))
-> [XLink] -> ResultT IO (DGraph, LibEnv, ChangeList)
forall a b. (a -> b) -> a -> b
$ XGraph -> [XLink]
thmLinks XGraph
xgr

-- | apply updates to one branch of the xgraph.
mkXStepUpdate :: HetcatsOpts -> LogicGraph -> (DGraph, LibEnv, ChangeList)
              -> ([XLink], XNode) -> ResultT IO (DGraph, LibEnv, ChangeList)
mkXStepUpdate :: HetcatsOpts
-> LogicGraph
-> (DGraph, LibEnv, ChangeList)
-> ([XLink], XNode)
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkXStepUpdate opts :: HetcatsOpts
opts lg :: LogicGraph
lg (dg :: DGraph
dg, lv :: LibEnv
lv, chL :: ChangeList
chL) (xlks :: [XLink]
xlks, xnd :: XNode
xnd) = let
  -- first, add the req. signature change from ingoing definition links
  sigUpd :: NodeMod
sigUpd = ChangeList -> [XLink] -> NodeMod
getLinkModUnion ChangeList
chL [XLink]
xlks
  chL' :: ChangeList
chL' = if NodeMod
sigUpd NodeMod -> NodeMod -> Bool
forall a. Eq a => a -> a -> Bool
== NodeMod
unMod then ChangeList
chL else ChangeAction -> NodeName -> ChangeList -> ChangeList
updateNodeChange (NodeMod -> ChangeAction
MkUpdate NodeMod
sigUpd)
              (XNode -> NodeName
nodeName XNode
xnd) ChangeList
chL in do
    [(Node, GMorphism, DGLinkType, XLink)]
mrs <- (XLink -> ResultT IO (Node, GMorphism, DGLinkType, XLink))
-> [XLink] -> ResultT IO [(Node, GMorphism, DGLinkType, XLink)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (LogicGraph
-> DGraph
-> XLink
-> ResultT IO (Node, GMorphism, DGLinkType, XLink)
getTypeAndMorphism LogicGraph
lg DGraph
dg) [XLink]
xlks
    G_sign lid :: lid
lid sg :: ExtSign sign symbol
sg sId :: SigId
sId <- LogicGraph
-> DGraph
-> [(Node, GMorphism, DGLinkType, XLink)]
-> ResultT IO G_sign
getSigForXNode LogicGraph
lg DGraph
dg [(Node, GMorphism, DGLinkType, XLink)]
mrs
    (DGraph, LibEnv, ChangeList)
rs1 <- HetcatsOpts
-> LogicGraph
-> Maybe G_theory
-> (DGraph, LibEnv, ChangeList)
-> XNode
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkNodeUpdate HetcatsOpts
opts LogicGraph
lg (G_theory -> Maybe G_theory
forall a. a -> Maybe a
Just (G_theory -> Maybe G_theory) -> G_theory -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
sg SigId
sId)
        (DGraph
dg, LibEnv
lv, ChangeList
chL') XNode
xnd
    ((DGraph, LibEnv, ChangeList)
 -> (Node, GMorphism, DGLinkType, XLink)
 -> ResultT IO (DGraph, LibEnv, ChangeList))
-> (DGraph, LibEnv, ChangeList)
-> [(Node, GMorphism, DGLinkType, XLink)]
-> ResultT IO (DGraph, LibEnv, ChangeList)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LogicGraph
-> (DGraph, LibEnv, ChangeList)
-> (Node, GMorphism, DGLinkType, XLink)
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkLinkUpdate LogicGraph
lg) (DGraph, LibEnv, ChangeList)
rs1 [(Node, GMorphism, DGLinkType, XLink)]
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 :: ChangeList -> [XLink] -> NodeMod
getLinkModUnion chL :: ChangeList
chL = (XLink -> NodeMod -> NodeMod) -> NodeMod -> [XLink] -> NodeMod
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ xl :: XLink
xl ->
  case EdgeId -> Map EdgeId ChangeAction -> Maybe ChangeAction
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (XLink -> EdgeId
edgeId XLink
xl) (Map EdgeId ChangeAction -> Maybe ChangeAction)
-> Map EdgeId ChangeAction -> Maybe ChangeAction
forall a b. (a -> b) -> a -> b
$ ChangeList -> Map EdgeId ChangeAction
changeLinks ChangeList
chL of
    -- TODO: Cons symMod was chosen only to ensure updating of adjacent nodes.
    Just MkInsert -> NodeMod -> NodeMod -> NodeMod
mergeNodeMod NodeMod
symMod
    Just (MkUpdate nmod :: NodeMod
nmod) -> NodeMod -> NodeMod -> NodeMod
mergeNodeMod NodeMod
nmod
    Nothing -> NodeMod -> NodeMod
forall a. a -> a
id ) NodeMod
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 :: HetcatsOpts
-> LogicGraph
-> Maybe G_theory
-> (DGraph, LibEnv, ChangeList)
-> XNode
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkNodeUpdate opts :: HetcatsOpts
opts lg :: LogicGraph
lg mGt :: Maybe G_theory
mGt (dg :: DGraph
dg, lv :: LibEnv
lv, chL :: ChangeList
chL) xnd :: XNode
xnd = let
  nm :: NodeName
nm = XNode -> NodeName
nodeName XNode
xnd
  nd :: String
nd = NodeName -> String
showName NodeName
nm in case NodeName -> ChangeList -> Maybe (ChangeAction, ChangeList)
retrieveNodeChange NodeName
nm ChangeList
chL of
    -- no change required, move on
    Nothing -> (DGraph, LibEnv, ChangeList)
-> ResultT IO (DGraph, LibEnv, ChangeList)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg, LibEnv
lv, ChangeList
chL)
    -- make insertion using DGChange.InsertNode object
    Just (MkInsert, chL' :: ChangeList
chL') -> let n :: Node
n = DGraph -> Node
getNewNodeDG DGraph
dg in do
      (lbl :: DGNodeLab
lbl, lv' :: LibEnv
lv') <- HetcatsOpts
-> LogicGraph
-> Maybe G_theory
-> XNode
-> (DGraph, LibEnv)
-> ResultT IO (DGNodeLab, LibEnv)
generateNodeLab HetcatsOpts
opts LogicGraph
lg Maybe G_theory
mGt XNode
xnd (DGraph
dg, LibEnv
lv)
      let dg' :: DGraph
dg' = DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab -> DGChange
InsertNode (Node
n, DGNodeLab
lbl)
      (DGraph, LibEnv, ChangeList)
-> ResultT IO (DGraph, LibEnv, ChangeList)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg', LibEnv
lv', ChangeList
chL')
    -- make update using DGChange.SetNodeLab object
    Just (MkUpdate nmod :: NodeMod
nmod, chL' :: ChangeList
chL') -> do
      (lbl :: DGNodeLab
lbl, lv' :: LibEnv
lv') <- HetcatsOpts
-> LogicGraph
-> Maybe G_theory
-> XNode
-> (DGraph, LibEnv)
-> ResultT IO (DGNodeLab, LibEnv)
generateNodeLab HetcatsOpts
opts LogicGraph
lg Maybe G_theory
mGt XNode
xnd (DGraph
dg, LibEnv
lv)
      (n :: Node
n, lblOrig :: DGNodeLab
lblOrig) <- case String -> DGraph -> Maybe (LNode DGNodeLab)
lookupUniqueNodeByName String
nd DGraph
dg of
        Just ndOrig :: LNode DGNodeLab
ndOrig -> LNode DGNodeLab -> ResultT IO (LNode DGNodeLab)
forall (m :: * -> *) a. Monad m => a -> m a
return LNode DGNodeLab
ndOrig
        Nothing -> String -> ResultT IO (LNode DGNodeLab)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> ResultT IO (LNode DGNodeLab))
-> String -> ResultT IO (LNode DGNodeLab)
forall a b. (a -> b) -> a -> b
$ "node [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nd String -> String -> String
forall a. [a] -> [a] -> [a]
++ "] was not found in dg, but was"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ " marked for updating"
      let dg' :: DGraph
dg' = DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
lblOrig (Node
n, DGNodeLab
lbl)
      -- all adjacent links need to get their morphism updated
      (DGraph, LibEnv, ChangeList)
-> ResultT IO (DGraph, LibEnv, ChangeList)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg', LibEnv
lv', DGraph -> Node -> NodeMod -> ChangeList -> ChangeList
markLinkUpdates DGraph
dg' Node
n NodeMod
nmod ChangeList
chL')

-- | mark all links adjacent to a node as update-pending
markLinkUpdates :: DGraph -> Node -> NodeMod -> ChangeList -> ChangeList
markLinkUpdates :: DGraph -> Node -> NodeMod -> ChangeList -> ChangeList
markLinkUpdates dg :: DGraph
dg t :: Node
t nmod :: NodeMod
nmod chL :: ChangeList
chL = let
  (Just (ins :: Adj DGLinkLab
ins, _, _, outs :: Adj DGLinkLab
outs), _) = Node
-> Gr DGNodeLab DGLinkLab
-> (Maybe (Adj DGLinkLab, Node, DGNodeLab, Adj DGLinkLab),
    Gr DGNodeLab DGLinkLab)
forall (gr :: * -> * -> *) a b.
Graph gr =>
Node -> gr a b -> Decomp gr a b
match Node
t (Gr DGNodeLab DGLinkLab
 -> (Maybe (Adj DGLinkLab, Node, DGNodeLab, Adj DGLinkLab),
     Gr DGNodeLab DGLinkLab))
-> Gr DGNodeLab DGLinkLab
-> (Maybe (Adj DGLinkLab, Node, DGNodeLab, Adj DGLinkLab),
    Gr DGNodeLab DGLinkLab)
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
  in ((DGLinkLab, Node) -> ChangeList -> ChangeList)
-> ChangeList -> Adj DGLinkLab -> ChangeList
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (ChangeAction -> EdgeId -> ChangeList -> ChangeList
updateLinkChange (NodeMod -> ChangeAction
MkUpdate NodeMod
nmod) (EdgeId -> ChangeList -> ChangeList)
-> ((DGLinkLab, Node) -> EdgeId)
-> (DGLinkLab, Node)
-> ChangeList
-> ChangeList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> EdgeId
dgl_id (DGLinkLab -> EdgeId)
-> ((DGLinkLab, Node) -> DGLinkLab) -> (DGLinkLab, Node) -> EdgeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DGLinkLab, Node) -> DGLinkLab
forall a b. (a, b) -> a
fst) ChangeList
chL
     (Adj DGLinkLab -> ChangeList) -> Adj DGLinkLab -> ChangeList
forall a b. (a -> b) -> a -> b
$ Adj DGLinkLab
ins Adj DGLinkLab -> Adj DGLinkLab -> Adj DGLinkLab
forall a. [a] -> [a] -> [a]
++ Adj DGLinkLab
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 :: LogicGraph
-> (DGraph, LibEnv, ChangeList)
-> (Node, GMorphism, DGLinkType, XLink)
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkLinkUpdate lg :: LogicGraph
lg (dg :: DGraph
dg, lv :: LibEnv
lv, chL :: ChangeList
chL) (i :: Node
i, mr :: GMorphism
mr, tp :: DGLinkType
tp, xl :: XLink
xl) = let ei :: EdgeId
ei = XLink -> EdgeId
edgeId XLink
xl in
  case EdgeId -> ChangeList -> Maybe (ChangeAction, ChangeList)
retrieveLinkChange EdgeId
ei ChangeList
chL of
    Nothing -> (DGraph, LibEnv, ChangeList)
-> ResultT IO (DGraph, LibEnv, ChangeList)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg, LibEnv
lv, ChangeList
chL)
    Just (chA :: ChangeAction
chA, chL' :: ChangeList
chL') -> do
      (j :: Node
j, gs :: G_sign
gs) <- String -> DGraph -> ResultT IO (Node, G_sign)
signOfNode (XLink -> String
target XLink
xl) DGraph
dg
      DGLinkLab
lkLab <- LogicGraph
-> XLink
-> GMorphism
-> G_sign
-> DGLinkType
-> ResultT IO DGLinkLab
finalizeLink LogicGraph
lg XLink
xl GMorphism
mr G_sign
gs DGLinkType
tp
      -- if updating an existing link, the old one is deleted from dg first
      DGraph
dg' <- if ChangeAction
chA ChangeAction -> ChangeAction -> Bool
forall a. Eq a => a -> a -> Bool
== ChangeAction
MkInsert then DGraph -> ResultT IO DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg else
        (LEdge DGLinkLab -> DGraph)
-> ResultT IO (LEdge DGLinkLab) -> ResultT IO DGraph
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph)
-> (LEdge DGLinkLab -> DGChange) -> LEdge DGLinkLab -> DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LEdge DGLinkLab -> DGChange
DeleteEdge) (ResultT IO (LEdge DGLinkLab) -> ResultT IO DGraph)
-> ResultT IO (LEdge DGLinkLab) -> ResultT IO DGraph
forall a b. (a -> b) -> a -> b
$ Node -> EdgeId -> DGraph -> ResultT IO (LEdge DGLinkLab)
forall (m :: * -> *).
MonadFail m =>
Node -> EdgeId -> DGraph -> m (LEdge DGLinkLab)
lookupUniqueLink Node
i EdgeId
ei DGraph
dg
      (DGraph, LibEnv, ChangeList)
-> ResultT IO (DGraph, LibEnv, ChangeList)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> DGChange -> DGraph
changeDGH DGraph
dg' (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
InsertEdge (Node
i, Node
j, DGLinkLab
lkLab), LibEnv
lv, ChangeList
chL')

-- | updates any necessary ThmLinks
mkThmLinkUpdates :: LogicGraph -> (DGraph, LibEnv, ChangeList) -> [XLink]
                 -> ResultT IO (DGraph, LibEnv, ChangeList)
mkThmLinkUpdates :: LogicGraph
-> (DGraph, LibEnv, ChangeList)
-> [XLink]
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkThmLinkUpdates lg :: LogicGraph
lg (dg :: DGraph
dg, lv :: LibEnv
lv, chL :: ChangeList
chL) xlks :: [XLink]
xlks = do
  [(Node, GMorphism, DGLinkType, XLink)]
mrs <- (XLink -> ResultT IO (Node, GMorphism, DGLinkType, XLink))
-> [XLink] -> ResultT IO [(Node, GMorphism, DGLinkType, XLink)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (LogicGraph
-> DGraph
-> XLink
-> ResultT IO (Node, GMorphism, DGLinkType, XLink)
getTypeAndMorphism LogicGraph
lg DGraph
dg) [XLink]
xlks
  ((DGraph, LibEnv, ChangeList)
 -> (Node, GMorphism, DGLinkType, XLink)
 -> ResultT IO (DGraph, LibEnv, ChangeList))
-> (DGraph, LibEnv, ChangeList)
-> [(Node, GMorphism, DGLinkType, XLink)]
-> ResultT IO (DGraph, LibEnv, ChangeList)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LogicGraph
-> (DGraph, LibEnv, ChangeList)
-> (Node, GMorphism, DGLinkType, XLink)
-> ResultT IO (DGraph, LibEnv, ChangeList)
mkLinkUpdate LogicGraph
lg) (DGraph
dg, LibEnv
lv, ChangeList
chL) [(Node, GMorphism, DGLinkType, XLink)]
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 :: DGraph -> ChangeList -> Result (DGraph, ChangeList)
deleteElements dg :: DGraph
dg chL :: ChangeList
chL = do
  (dg1 :: DGraph
dg1, targets :: [Node]
targets) <- ((DGraph, [Node]) -> XLink -> Result (DGraph, [Node]))
-> (DGraph, [Node]) -> [XLink] -> Result (DGraph, [Node])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (DGraph, [Node]) -> XLink -> Result (DGraph, [Node])
forall (m :: * -> *).
MonadFail m =>
(DGraph, [Node]) -> XLink -> m (DGraph, [Node])
deleteLinkAux (DGraph
dg, []) ([XLink] -> Result (DGraph, [Node]))
-> [XLink] -> Result (DGraph, [Node])
forall a b. (a -> b) -> a -> b
$ Set XLink -> [XLink]
forall a. Set a -> [a]
Set.toList (Set XLink -> [XLink]) -> Set XLink -> [XLink]
forall a b. (a -> b) -> a -> b
$ ChangeList -> Set XLink
deleteLinks ChangeList
chL
  DGraph
dg2 <- (DGraph -> NodeName -> Result DGraph)
-> DGraph -> [NodeName] -> Result DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dg' :: DGraph
dg' -> ((Node, DGraph) -> DGraph)
-> Result (Node, DGraph) -> Result DGraph
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Node, DGraph) -> DGraph
forall a b. (a, b) -> b
snd (Result (Node, DGraph) -> Result DGraph)
-> (NodeName -> Result (Node, DGraph)) -> NodeName -> Result DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> NodeName -> Result (Node, DGraph)
forall (m :: * -> *).
MonadFail m =>
DGraph -> NodeName -> m (Node, DGraph)
deleteNode DGraph
dg') DGraph
dg1 ([NodeName] -> Result DGraph) -> [NodeName] -> Result DGraph
forall a b. (a -> b) -> a -> b
$ Set NodeName -> [NodeName]
forall a. Set a -> [a]
Set.toList
          (Set NodeName -> [NodeName]) -> Set NodeName -> [NodeName]
forall a b. (a -> b) -> a -> b
$ ChangeList -> Set NodeName
deleteNodes ChangeList
chL
  {- after deletion, all still-existing nodes which lost ingoing definition
  links must be marked for updating. -}
  ChangeList
chL' <- (ChangeList -> Node -> Result ChangeList)
-> ChangeList -> [Node] -> Result ChangeList
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((Node -> ChangeList -> Result ChangeList)
-> ChangeList -> Node -> Result ChangeList
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Node -> ChangeList -> Result ChangeList)
 -> ChangeList -> Node -> Result ChangeList)
-> (Node -> ChangeList -> Result ChangeList)
-> ChangeList
-> Node
-> Result ChangeList
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> ChangeList -> Result ChangeList
forall (m :: * -> *).
MonadFail m =>
DGraph -> Node -> ChangeList -> m ChangeList
markNodeUpdates DGraph
dg2) ChangeList
chL ([Node] -> Result ChangeList) -> [Node] -> Result ChangeList
forall a b. (a -> b) -> a -> b
$ [Node] -> [Node]
forall a. Eq a => [a] -> [a]
List.nub [Node]
targets
  (DGraph, ChangeList) -> Result (DGraph, ChangeList)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg2, ChangeList
chL' { deleteNodes :: Set NodeName
deleteNodes = Set NodeName
forall a. Set a
Set.empty, deleteLinks :: Set XLink
deleteLinks = Set XLink
forall a. Set a
Set.empty })

-- | look for given node in dg and mark as update-pending in changelist
markNodeUpdates :: Fail.MonadFail m => DGraph -> Node -> ChangeList -> m ChangeList
markNodeUpdates :: DGraph -> Node -> ChangeList -> m ChangeList
markNodeUpdates dg :: DGraph
dg trg :: Node
trg = case Gr DGNodeLab DGLinkLab -> Node -> Maybe DGNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
lab (DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg) Node
trg of
  Nothing -> ChangeList -> m ChangeList
forall (m :: * -> *) a. Monad m => a -> m a
return
  -- TODO: symMod was chosen to ensure updating, it does not always apply.
  Just lbl :: DGNodeLab
lbl -> ChangeList -> m ChangeList
forall (m :: * -> *) a. Monad m => a -> m a
return (ChangeList -> m ChangeList)
-> (ChangeList -> ChangeList) -> ChangeList -> m ChangeList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChangeAction -> NodeName -> ChangeList -> ChangeList
updateNodeChange (NodeMod -> ChangeAction
MkUpdate NodeMod
symMod) (DGNodeLab -> NodeName
dgn_name DGNodeLab
lbl)

-- | deletes a link from dg and returns (def)links target id additionally
deleteLinkAux :: Fail.MonadFail m => (DGraph, [Node]) -> XLink -> m (DGraph, [Node])
deleteLinkAux :: (DGraph, [Node]) -> XLink -> m (DGraph, [Node])
deleteLinkAux (dg :: DGraph
dg, tars :: [Node]
tars) xl :: XLink
xl = case String -> DGraph -> Maybe (LNode DGNodeLab)
lookupUniqueNodeByName (XLink -> String
source XLink
xl) DGraph
dg of
  Just (s :: Node
s, _) -> do
    DGraph
dg' <- (LEdge DGLinkLab -> DGraph) -> m (LEdge DGLinkLab) -> m DGraph
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph)
-> (LEdge DGLinkLab -> DGChange) -> LEdge DGLinkLab -> DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LEdge DGLinkLab -> DGChange
DeleteEdge)
        (m (LEdge DGLinkLab) -> m DGraph)
-> m (LEdge DGLinkLab) -> m DGraph
forall a b. (a -> b) -> a -> b
$ Node -> EdgeId -> DGraph -> m (LEdge DGLinkLab)
forall (m :: * -> *).
MonadFail m =>
Node -> EdgeId -> DGraph -> m (LEdge DGLinkLab)
lookupUniqueLink Node
s (XLink -> EdgeId
edgeId XLink
xl) DGraph
dg
    if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isDefEdgeType (XLink -> DGEdgeType
lType XLink
xl)
      then (DGraph, [Node]) -> m (DGraph, [Node])
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg', [Node]
tars)
      else case String -> DGraph -> Maybe (LNode DGNodeLab)
lookupUniqueNodeByName (XLink -> String
target XLink
xl) DGraph
dg of
        Just (t :: Node
t, _) -> (DGraph, [Node]) -> m (DGraph, [Node])
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg', Node
t Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
tars)
        Nothing -> String -> m (DGraph, [Node])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (DGraph, [Node])) -> String -> m (DGraph, [Node])
forall a b. (a -> b) -> a -> b
$ "required target [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ XLink -> String
target XLink
xl
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ "] was not found in DGraph!"
  Nothing -> String -> m (DGraph, [Node])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (DGraph, [Node])) -> String -> m (DGraph, [Node])
forall a b. (a -> b) -> a -> b
$ "required source [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ XLink -> String
source XLink
xl
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ "] was not found in DGraph!"

-- | deletes a node from dg
deleteNode :: Fail.MonadFail m => DGraph -> NodeName -> m (Node, DGraph)
deleteNode :: DGraph -> NodeName -> m (Node, DGraph)
deleteNode dg :: DGraph
dg nm :: NodeName
nm = let nd :: String
nd = NodeName -> String
showName NodeName
nm
  in case String -> DGraph -> Maybe (LNode DGNodeLab)
lookupUniqueNodeByName String
nd DGraph
dg of
      Just (j :: Node
j, lbl :: DGNodeLab
lbl) -> (Node, DGraph) -> m (Node, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node
j, DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab -> DGChange
DeleteNode (Node
j, DGNodeLab
lbl))
      Nothing -> String -> m (Node, DGraph)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (Node, DGraph)) -> String -> m (Node, DGraph)
forall a b. (a -> b) -> a -> b
$
        "required node [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nd String -> String -> String
forall a. [a] -> [a] -> [a]
++ "] was not found in DGraph!"