aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-04 21:46:12 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-04 21:55:31 +0100
commit153d77d00ccbacf22aa5d70ca2c1cacab2749339 (patch)
tree98997d190ad1b45f3096473c1015feae55b64efe /lib
parent0aba678e885fa53fa649de59eb1d06b4af3a847c (diff)
Specializing the Dyn module to each usecase.
Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point.
Diffstat (limited to 'lib')
-rw-r--r--lib/cSig.mli2
-rw-r--r--lib/dyn.ml15
-rw-r--r--lib/dyn.mli6
-rw-r--r--lib/future.ml7
-rw-r--r--lib/future.mli3
5 files changed, 29 insertions, 4 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