From 9fa14555270fa8f2368a7f4df1510bd2937d25ec Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Mon, 6 May 2013 13:40:58 +0000 Subject: States: frozen states can hold closures States.freeze takes ~marshallable:bool, so that (only) when we want to marshal data to disk/network we can ask the freeze functions of the summary to force lazy values. The flag is propagated to Lib and Summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16478 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/summary.ml | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) (limited to 'library/summary.ml') diff --git a/library/summary.ml b/library/summary.ml index 056acd41c..53e9f7002 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -11,7 +11,7 @@ open Errors open Util type 'a summary_declaration = { - freeze_function : unit -> 'a; + freeze_function : bool -> 'a; unfreeze_function : 'a -> unit; init_function : unit -> unit } @@ -20,7 +20,7 @@ let summaries = let internal_declare_summary sumname sdecl = let (infun,outfun) = Dyn.create sumname in - let dyn_freeze () = infun (sdecl.freeze_function()) + let dyn_freeze b = infun (sdecl.freeze_function b) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in let ddecl = { @@ -43,10 +43,18 @@ let declare_summary sumname decl = type frozen = Dyn.t String.Map.t -let freeze_summaries () = +let freeze_summaries ~marshallable = let m = ref String.Map.empty in Hashtbl.iter - (fun id decl -> m := String.Map.add id (decl.freeze_function()) !m) + (fun id decl -> + (* to debug missing Lazy.force + if marshallable then begin + prerr_endline ("begin marshalling " ^ id); + ignore(Marshal.to_string (decl.freeze_function marshallable) []); + prerr_endline ("end marshalling " ^ id); + end; + /debug *) + m := String.Map.add id (decl.freeze_function marshallable) !m) summaries; !m @@ -92,10 +100,10 @@ let unfreeze_summary datas = (** All-in-one reference declaration + registration *) -let ref ~name x = +let ref ?(freeze=fun _ r -> r) ~name x = let r = ref x in declare_summary name - { freeze_function = (fun () -> !r); + { freeze_function = (fun b -> freeze b !r); unfreeze_function = ((:=) r); init_function = (fun () -> r := x) }; r -- cgit v1.2.3