diff options
Diffstat (limited to 'lib/store.ml')
-rw-r--r-- | lib/store.ml | 91 |
1 files changed, 0 insertions, 91 deletions
diff --git a/lib/store.ml b/lib/store.ml deleted file mode 100644 index a1788f7d..00000000 --- a/lib/store.ml +++ /dev/null @@ -1,91 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(** 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 T = -sig -end - -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 (M : T) : 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 |