From f4a6a6aaa928e7a6c8d360c45268cb82c020c2dc Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 25 Aug 2013 22:34:08 +0000
Subject: Added a more efficient way to recover the domain of a map.

The extended signature is defined in CMap, and should be compatible
with the old one, except that module arguments have to be explicitely
named. The implementation itself is quite unsafe, as it relies on the
current implementation of OCaml maps, even though that should not be
a problem (it has not changed in ages).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/cMap.ml | 60 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)
 create mode 100644 lib/cMap.ml

(limited to 'lib/cMap.ml')

diff --git a/lib/cMap.ml b/lib/cMap.ml
new file mode 100644
index 0000000000..bf0a337687
--- /dev/null
+++ b/lib/cMap.ml
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+module type OrderedType =
+sig
+  type t
+  val compare : t -> t -> int
+end
+
+module type S = Map.S
+
+module type ExtS =
+sig
+  include Map.S
+  module Set : Set.S with type elt = key
+  val domain : 'a t -> Set.t
+end
+
+module Domain (M : Map.OrderedType) :
+sig
+  val domain : 'a Map.Make(M).t -> Set.Make(M).t
+end =
+struct
+  (** This unsafe module is a way to access to the actual implementations of
+      OCaml sets and maps without reimplementing them ourselves. It is quite
+      dubious that these implementations will ever be changed... Nonetheless,
+      if this happens, we can still implement a less clever version of [domain].
+  *)
+
+  type 'a map = 'a Map.Make(M).t
+  type set = Set.Make(M).t
+
+  type 'a _map =
+  | MEmpty
+  | MNode of 'a map * M.t * 'a * 'a map * int
+
+  type _set =
+  | SEmpty
+  | SNode of set * M.t * set * int
+
+  let rec domain (s : 'a map) : set = match Obj.magic s with
+  | MEmpty -> Obj.magic SEmpty
+  | MNode (l, k, _, r, h) ->
+    Obj.magic (SNode (domain l, k, domain r, h))
+  (** This function is essentially identity, but OCaml current stdlib does not
+      take advantage of the similarity of the two structures, so we introduce
+      this unsafe loophole. *)
+ 
+end
+
+module Make(M : Map.OrderedType) =
+struct
+  include Map.Make(M)
+  include Domain(M)
+end
-- 
cgit v1.2.3