From 9a9a8ab4c2a07aa8faa04f50d6250930220b5be5 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 12 May 2013 15:33:27 +0000
Subject: 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
---
 lib/clib.mllib |  1 +
 lib/hook.ml    | 32 ++++++++++++++++++++++++++++++++
 lib/hook.mli   | 27 +++++++++++++++++++++++++++
 3 files changed, 60 insertions(+)
 create mode 100644 lib/hook.ml
 create mode 100644 lib/hook.mli

(limited to 'lib')

diff --git a/lib/clib.mllib b/lib/clib.mllib
index 022a14ac36..70e083de92 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 0000000000..ee468269f7
--- /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 0000000000..3a11ac2175
--- /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. *)
-- 
cgit v1.2.3