From 433f0bc4e5110db09c770022b277c419f8b35f64 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Fri, 12 Dec 2014 16:40:32 +0100
Subject: Summary: more surgery functions

API to let one forge a frozen state out of another frozen state
plus some frozen bits
---
 library/states.ml   |  2 ++
 library/states.mli  |  2 ++
 library/summary.ml  | 44 ++++++++++++++++++++++++++++++--------------
 library/summary.mli |  3 +++
 4 files changed, 37 insertions(+), 14 deletions(-)

diff --git a/library/states.ml b/library/states.ml
index 200b14517..de03ca7c0 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -11,6 +11,8 @@ open System
 
 type state = Lib.frozen * Summary.frozen
 
+let summary_of_state = snd
+
 let freeze ~marshallable =
   (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
 
diff --git a/library/states.mli b/library/states.mli
index fae1bfc02..f2aab78c9 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -20,6 +20,8 @@ type state
 val freeze : marshallable:Summary.marshallable -> state
 val unfreeze : state -> unit
 
+val summary_of_state : state -> Summary.frozen
+
 (** {6 Rollback } *)
 
 (** [with_state_protection f x] applies [f] to [x] and restores the
diff --git a/library/summary.ml b/library/summary.ml
index 7a0064a1f..a44721606 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -123,21 +123,22 @@ let nop () = ()
 
 type frozen_bits = (int * Dyn.t) list
 
+let ids_of_string_list complement ids =
+  if not complement then List.map String.hash ids
+  else
+    let fold accu id =
+      let id = String.hash id in
+      Int.Set.remove id accu
+    in
+    let ids = List.fold_left fold !all_declared_summaries ids in
+    Int.Set.elements ids
+
 let freeze_summary ~marshallable ?(complement=false) ids =
-  let ids =
-    if not complement then List.map String.hash ids
-    else
-      let fold accu id =
-        let id = String.hash id in
-        Int.Set.remove id accu
-      in
-      let ids = List.fold_left fold !all_declared_summaries ids in
-      Int.Set.elements ids
-  in
-    List.map (fun id ->
-      let (_, summary) = Int.Map.find id !summaries in
-      id, summary.freeze_function marshallable)
-    ids
+  let ids = ids_of_string_list complement ids in
+  List.map (fun id ->
+    let (_, summary) = Int.Map.find id !summaries in
+    id, summary.freeze_function marshallable)
+  ids
 
 let unfreeze_summary datas =
   List.iter
@@ -150,6 +151,21 @@ let unfreeze_summary datas =
         iraise e)
   datas
 
+let surgery_summary { summaries; ml_module } bits =
+  let summaries = List.map (fun (id, _ as orig) ->
+      try id, List.assoc id bits
+      with Not_found -> orig)
+    summaries in
+  { summaries; ml_module }
+
+let project_summary { summaries; ml_module } ?(complement=false) ids =
+  let ids = ids_of_string_list complement ids in
+  List.filter (fun (id, _) -> List.mem id ids) summaries
+
+let pointer_equal l1 l2 =
+  CList.for_all2eq
+    (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2
+
 (** All-in-one reference declaration + registration *)
 
 let ref ?(freeze=fun _ r -> r) ~name x =
diff --git a/library/summary.mli b/library/summary.mli
index 1ce09e12c..1dcb1d5f5 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -68,3 +68,6 @@ type frozen_bits
 val freeze_summary :
   marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
 val unfreeze_summary : frozen_bits -> unit
+val surgery_summary : frozen -> frozen_bits -> frozen
+val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits
+val pointer_equal : frozen_bits -> frozen_bits -> bool
-- 
cgit v1.2.3