diff options
| -rw-r--r-- | checker/check.mllib | 2 | ||||
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 1 | ||||
| -rw-r--r-- | lib/clib.mllib | 1 | ||||
| -rw-r--r-- | lib/hook.ml | 32 | ||||
| -rw-r--r-- | lib/hook.mli | 27 |
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. *) |