aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-12 16:40:32 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-17 15:05:04 +0100
commit433f0bc4e5110db09c770022b277c419f8b35f64 (patch)
tree12f881fa7bbc72783dc2be9e7df7c39b05a7bbc7
parent5f2f22e7ff5d53e3258affa0e0e41666d5e0691d (diff)
Summary: more surgery functions
API to let one forge a frozen state out of another frozen state plus some frozen bits
-rw-r--r--library/states.ml2
-rw-r--r--library/states.mli2
-rw-r--r--library/summary.ml44
-rw-r--r--library/summary.mli3
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