Added a generic notion of hook. Hooks are functions to be set

exactly once at runtime, often to reduce the mutual dependency of
modules. This module permits to track them more easily.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16509 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 64 insertions, 0 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index 48c629009..cd858000a 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,4 +1,6 @@
 Coq_config
+
+Hook
 Int
 Option
 Store
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 01b44f148..e7c3b1a1b 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -1,5 +1,6 @@
 Coq_config
 
+Hook
 Int
 Option
 Store
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index bdfbbf515..818d220b8 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -1,5 +1,6 @@
 Coq_config
 
+Hook
 Int
 Option
 Store
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 022a14ac3..70e083de9 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -1,5 +1,6 @@
 Coq_config
 
+Hook
 Int
 Option
 Store
diff --git a/lib/hook.ml b/lib/hook.ml
new file mode 100644
index 000000000..ee468269f
--- /dev/null
+++ b/lib/hook.ml
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type 'a content =
+| Unset
+| Default of 'a
+| Set of 'a
+
+type 'a t = 'a content ref
+
+type 'a value = 'a t
+
+let get (hook : 'a value) = match !hook with
+| Unset -> assert false
+| Default data | Set data -> data
+
+let set (hook : 'a t) data = match !hook with
+| Unset | Default _ -> hook := Set data
+| Set _ -> assert false
+
+let make ?default () =
+  let data = match default with
+  | None -> Unset
+  | Some data -> Default data
+  in
+  let ans = ref data in
+  (ans, ans)
diff --git a/lib/hook.mli b/lib/hook.mli
new file mode 100644
index 000000000..3a11ac217
--- /dev/null
+++ b/lib/hook.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module centralizes the notions of hooks. Hooks are pointers that are to
+    be set at runtime exactly once. *)
+
+type 'a t
+(** The type of hooks containing ['a]. Hooks can only be set. *)
+
+type 'a value
+(** The content part of a hook. *)
+
+val make : ?default:'a -> unit -> ('a value * 'a t)
+(** Create a new hook together with a way to retrieve its runtime value. *)
+
+val get : 'a value -> 'a
+(** Access the content of a hook. If it was not set yet, try to recover the
+    default value if there is one.
+    @raise Assert_failure if undefined. *)
+
+val set : 'a t -> 'a -> unit
+(** Register a hook. Assertion failure if already registered. *)