From 80aba8d52c650ef8e4ada694c20bf12c15849694 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 8 Aug 2013 18:52:47 +0000 Subject: enhance marshallable option for freeze (minor TODO in safe_typing) It can be: `Yes Full data, in a state that can be marshalled `No Full data, good for Undo only `Shallow Partial data, marshallable, good for slave processes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16682 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/summary.mli | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'library/summary.mli') diff --git a/library/summary.mli b/library/summary.mli index 698034ad6..38d5fc7e8 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -9,10 +9,15 @@ (** This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system. *) +type marshallable = + [ `Yes (* Full data will be marshalled to disk *) + | `No (* Full data will be store in memory, e.g. for Undo *) + | `Shallow ] (* Only part of the data will be marshalled to a slave process *) + type 'a summary_declaration = { (** freeze_function [true] is for marshalling to disk. * e.g. lazy must be forced *) - freeze_function : bool -> 'a; + freeze_function : marshallable -> 'a; unfreeze_function : 'a -> unit; init_function : unit -> unit } @@ -35,7 +40,7 @@ val declare_summary : string -> 'a summary_declaration -> unit The [init_function] restores the reference to its initial value. The [freeze_function] can be overridden *) -val ref : ?freeze:(bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref +val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref (** For global tables registered statically before the end of coqtop launch, the following empty [init_function] could be used. *) @@ -47,7 +52,7 @@ val nop : unit -> unit type frozen -val freeze_summaries : marshallable:bool -> frozen +val freeze_summaries : marshallable:marshallable -> frozen val unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit @@ -55,5 +60,5 @@ val init_summaries : unit -> unit type frozen_bits val freeze_summary : - marshallable:bool -> ?complement:bool -> string list -> frozen_bits + marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits val unfreeze_summary : frozen_bits -> unit -- cgit v1.2.3