remoteCounter: backup/restore

When you resume the compilation of a .vi file, you want to
avoid collisions on fresh names.

1 files changed, 19 insertions, 3 deletions

diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index e0e2d5cbc..bec46901f 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -9,8 +9,16 @@
 type 'a getter = unit -> 'a
 type 'a installer = ('a getter) -> unit
 
-let new_counter a ~incr ~build =
-  let data = ref a in
+type remote_counters_status = (string * Obj.t) list
+
+let counters : remote_counters_status ref = ref []
+
+let (!!) x = !(!x)
+
+let new_counter ~name a ~incr ~build =
+  assert(not (List.mem_assoc name !counters));
+  let data = ref (ref a) in
+  counters := (name, Obj.repr data) :: !counters;
   let m = Mutex.create () in
   let mk_thsafe_getter f () =
     (* - slaves must use a remote counter getter, not this one! *)
@@ -22,7 +30,7 @@ let new_counter a ~incr ~build =
     | _ -> ());
     Mutex.lock m; let x = f () in Mutex.unlock m;
     build x in
-  let getter = ref (mk_thsafe_getter (fun () -> data := incr !data; !data)) in
+  let getter = ref(mk_thsafe_getter (fun () -> !data := incr !!data; !!data)) in
   let installer f =
     (match !Flags.async_proofs_mode with
     | Flags.APoff | Flags.APonLazy | Flags.APonParallel 0 -> 
@@ -31,3 +39,11 @@ let new_counter a ~incr ~build =
     getter := f in
   (fun () -> !getter ()), installer
 
+let backup () = !counters
+
+let restore l =
+  List.iter (fun (name, data) ->
+    assert(List.mem_assoc name !counters);
+    let dataref = Obj.obj (List.assoc name !counters) in
+    !dataref := !!(Obj.obj data))
+  l