diff options
Diffstat (limited to 'clib/store.ml')
-rw-r--r-- | clib/store.ml | 89 |
1 files changed, 89 insertions, 0 deletions
diff --git a/clib/store.ml b/clib/store.ml new file mode 100644 index 00000000..1469358c --- /dev/null +++ b/clib/store.ml @@ -0,0 +1,89 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module implements an "untyped store", in this particular case + we see it as an extensible record whose fields are left + unspecified. ***) + +(** We use a dynamic "name" allocator. But if we needed to serialise + stores, we might want something static to avoid troubles with + plugins order. *) + +module type S = +sig + type t + type 'a field + val empty : t + val set : t -> 'a field -> 'a -> t + val get : t -> 'a field -> 'a option + val remove : t -> 'a field -> t + val merge : t -> t -> t + val field : unit -> 'a field +end + +module Make () : S = +struct + + let next = + let count = ref 0 in fun () -> + let n = !count in + incr count; + n + + type t = Obj.t option array + (** Store are represented as arrays. For small values, which is typicial, + is slightly quicker than other implementations. *) + +type 'a field = int + +let allocate len : t = Array.make len None + +let empty : t = [||] + +let set (s : t) (i : 'a field) (v : 'a) : t = + let len = Array.length s in + let nlen = if i < len then len else succ i in + let () = assert (0 <= i) in + let ans = allocate nlen in + Array.blit s 0 ans 0 len; + Array.unsafe_set ans i (Some (Obj.repr v)); + ans + +let get (s : t) (i : 'a field) : 'a option = + let len = Array.length s in + if len <= i then None + else Obj.magic (Array.unsafe_get s i) + +let remove (s : t) (i : 'a field) = + let len = Array.length s in + let () = assert (0 <= i) in + let ans = allocate len in + Array.blit s 0 ans 0 len; + if i < len then Array.unsafe_set ans i None; + ans + +let merge (s1 : t) (s2 : t) : t = + let len1 = Array.length s1 in + let len2 = Array.length s2 in + let nlen = if len1 < len2 then len2 else len1 in + let ans = allocate nlen in + (** Important: No more allocation from here. *) + Array.blit s2 0 ans 0 len2; + for i = 0 to pred len1 do + let v = Array.unsafe_get s1 i in + match v with + | None -> () + | Some _ -> Array.unsafe_set ans i v + done; + ans + +let field () = next () + +end |