diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-12 16:40:32 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 15:05:04 +0100 |
commit | 433f0bc4e5110db09c770022b277c419f8b35f64 (patch) | |
tree | 12f881fa7bbc72783dc2be9e7df7c39b05a7bbc7 | |
parent | 5f2f22e7ff5d53e3258affa0e0e41666d5e0691d (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.ml | 2 | ||||
-rw-r--r-- | library/states.mli | 2 | ||||
-rw-r--r-- | library/summary.ml | 44 | ||||
-rw-r--r-- | 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 |