From 0f9a7d13714f30a3c1eeee41b6a500370e5c18bb Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 11 Oct 2013 09:10:52 +0000
Subject: Vcs: the gc method returns the set of nodes that were collected

In this way one can post-process them.  Stm can for example cancel
the ongoing jobs related to nodes that are no more there.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16877 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/vcs.ml  | 8 ++++----
 lib/vcs.mli | 7 ++++---
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/lib/vcs.ml b/lib/vcs.ml
index 6668d07483..e2513b1c1e 100644
--- a/lib/vcs.ml
+++ b/lib/vcs.ml
@@ -55,10 +55,10 @@ module type S = sig
   val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
   val get_info : ('k,'e,'info) t -> id -> 'info option
   
-  val gc : ('k,'e,'info) t -> ('k,'e,'info) t
-
   module NodeSet : Set.S with type elt = id
 
+  val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t
+
   val reachable : ('k,'e,'info) t -> id -> NodeSet.t
 
   module Dag : Dag.S with type node = id
@@ -187,7 +187,7 @@ let gc vcs =
   let alive =
     BranchMap.fold (fun b { pos } s -> closure s vcs.dag pos)
       vcs.heads Dag.NodeSet.empty in
-  { vcs with dag =
-      Dag.del_nodes vcs.dag (Dag.NodeSet.diff (Dag.all_nodes vcs.dag) alive) }
+  let dead = Dag.NodeSet.diff (Dag.all_nodes vcs.dag) alive in
+  { vcs with dag = Dag.del_nodes vcs.dag dead }, dead
 
 end
diff --git a/lib/vcs.mli b/lib/vcs.mli
index 72feae5dc4..6c3571a082 100644
--- a/lib/vcs.mli
+++ b/lib/vcs.mli
@@ -70,16 +70,17 @@ module type S = sig
   val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
   val get_info : ('k,'e,'info) t -> id -> 'info option
 
-  val gc : ('k,'e,'info) t -> ('k,'e,'info) t
-
   module NodeSet : Set.S with type elt = id
+  
+  (* Removes all unreachable nodes and returns them *)
+  val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t
 
   val reachable : ('k,'e,'info) t -> id -> NodeSet.t
 
   (* read only dag *)
   module Dag : Dag.S with type node = id
   val dag : ('kind,'diff,'info) t -> ('diff,'info,id) Dag.t
-  
+ 
   val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t
   val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option
   val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t 
-- 
cgit v1.2.3