diff options
| -rw-r--r-- | lib/cSig.mli | 2 | ||||
| -rw-r--r-- | lib/dyn.ml | 15 | ||||
| -rw-r--r-- | lib/dyn.mli | 6 | ||||
| -rw-r--r-- | lib/future.ml | 7 | ||||
| -rw-r--r-- | lib/future.mli | 3 | ||||
| -rw-r--r-- | library/libobject.ml | 4 | ||||
| -rw-r--r-- | library/libobject.mli | 4 | ||||
| -rw-r--r-- | library/summary.ml | 4 | ||||
| -rw-r--r-- | library/summary.mli | 4 | ||||
| -rw-r--r-- | stm/stm.ml | 5 |
10 files changed, 47 insertions, 7 deletions
diff --git a/lib/cSig.mli b/lib/cSig.mli index 2a8bda293..4463e8d9c 100644 --- a/lib/cSig.mli +++ b/lib/cSig.mli @@ -45,3 +45,5 @@ sig end (** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml documentation for more information. *) + +module type EmptyS = sig end diff --git a/lib/dyn.ml b/lib/dyn.ml index 056b68731..60167ef1b 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -9,6 +9,19 @@ open Errors open Pp +module type S = +sig +type t + +val create : string -> ('a -> t) * (t -> 'a) +val tag : t -> string +val has_tag : t -> string -> bool +val pointer_equal : t -> t -> bool +val dump : unit -> (int * string) list +end + +module Make(M : CSig.EmptyS) = +struct (* Dynamics, programmed with DANGER !!! *) type t = int * Obj.t @@ -48,3 +61,5 @@ let tag (s,_) = let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2 let dump () = Int.Map.bindings !dyntab + +end
\ No newline at end of file diff --git a/lib/dyn.mli b/lib/dyn.mli index cac912aca..55c4f0ce8 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -8,6 +8,8 @@ (** Dynamics. Use with extreme care. Not for kids. *) +module type S = +sig type t val create : string -> ('a -> t) * (t -> 'a) @@ -15,3 +17,7 @@ val tag : t -> string val has_tag : t -> string -> bool val pointer_equal : t -> t -> bool val dump : unit -> (int * string) list +end + +(** FIXME: use OCaml 4.02 generative functors when available *) +module Make(M : CSig.EmptyS) : S diff --git a/lib/future.ml b/lib/future.ml index 78a158264..b6012ed20 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -7,8 +7,9 @@ (************************************************************************) (* To deal with side effects we have to save/restore the system state *) -let freeze = ref (fun () -> assert false : unit -> Dyn.t) -let unfreeze = ref (fun _ -> () : Dyn.t -> unit) +type freeze +let freeze = ref (fun () -> assert false : unit -> freeze) +let unfreeze = ref (fun _ -> () : freeze -> unit) let set_freeze f g = freeze := f; unfreeze := g let not_ready_msg = ref (fun name -> @@ -58,7 +59,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat and 'a comp = | Delegated of (unit -> unit) | Closure of (unit -> 'a) - | Val of 'a * Dyn.t option + | Val of 'a * freeze option | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = diff --git a/lib/future.mli b/lib/future.mli index adc15e49c..29b71b70a 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -157,10 +157,11 @@ val transactify : ('a -> 'b) -> 'a -> 'b (** Debug: print a computation given an inner printing function. *) val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds +type freeze (* These functions are needed to get rid of side effects. Thy are set for the outermos layer of the system, since they have to deal with the whole system state. *) -val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit +val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit diff --git a/library/libobject.ml b/library/libobject.ml index 85c830ea2..c63875907 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -9,6 +9,8 @@ open Libnames open Pp +module Dyn = Dyn.Make(struct end) + (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one wants to work with restricted Coq programs that have only parts of @@ -158,3 +160,5 @@ let discharge_object ((_,lobj) as node) = let rebuild_object lobj = apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj + +let dump = Dyn.dump diff --git a/library/libobject.mli b/library/libobject.mli index 099381897..e49f3fd5c 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -109,3 +109,7 @@ val classify_object : obj -> obj substitutivity val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj val relax : bool -> unit + +(** {6 Debug} *) + +val dump : unit -> (int * string) list diff --git a/library/summary.ml b/library/summary.ml index 8e2abbf15..6ef4e131c 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -10,6 +10,8 @@ open Pp open Errors open Util +module Dyn = Dyn.Make(struct end) + type marshallable = [ `Yes | `No | `Shallow ] type 'a summary_declaration = { freeze_function : marshallable -> 'a; @@ -176,3 +178,5 @@ let ref ?(freeze=fun _ r -> r) ~name x = unfreeze_function = ((:=) r); init_function = (fun () -> r := x) }; r + +let dump = Dyn.dump diff --git a/library/summary.mli b/library/summary.mli index 48c9390d0..a35113fd2 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -71,3 +71,7 @@ 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 + +(** {6 Debug} *) + +val dump : unit -> (int * string) list diff --git a/stm/stm.ml b/stm/stm.ml index 623629745..ea669b159 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -631,10 +631,9 @@ end = struct (* {{{ *) States.unfreeze system; Proof_global.unfreeze proof (* hack to make futures functional *) - let in_t, out_t = Dyn.create "state4future" let () = Future.set_freeze - (fun () -> in_t (freeze_global_state `No, !cur_id)) - (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i) + (fun () -> Obj.magic (freeze_global_state `No, !cur_id)) + (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i) type frozen_state = state type proof_part = |