aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorppedrot2012-10-29 13:02:23 +0000
committerppedrot2012-10-29 13:02:23 +0000
commit278517722988d040cb8da822e319d723670ac519 (patch)
tree92316184aec004570c6567f0d585167e47dd52ae /lib
parent0699ef2ffba984e7b7552787894b142dd924f66a (diff)
Removed many calls to OCaml generic equality. This was done by
writing our own comparison functions, and enforcing monomorphization in many places. This should be more efficient, btw. Still a work in progress. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml8
-rw-r--r--lib/hashcons.ml3
-rw-r--r--lib/hashset.ml2
-rw-r--r--lib/util.ml18
4 files changed, 24 insertions, 7 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 2b10125a0e..4ec3787931 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -101,7 +101,13 @@ let print_hyps_limit () = !print_hyps_limit
(* A list of the areas of the system where "unsafe" operation
* has been requested *)
-module Stringset = Set.Make(struct type t = string let compare = compare end)
+module StringOrd =
+struct
+ type t = string
+ let compare (x : t) (y : t) = String.compare x y
+end
+
+module Stringset = Set.Make(StringOrd)
let unsafe_set = ref Stringset.empty
let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 8daeec9444..745169dc08 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -132,8 +132,7 @@ module Hstring = Make(
type t = string
type u = unit
let hashcons () s =(* incr accesstr;*) s
- let equal s1 s2 =(* incr comparaisonstr;
- if*) s1=s2(* then (incr successtr; true) else false*)
+ let equal (s1 : t) (s2 : t) = s1 = s2
let hash = Hashtbl.hash
end)
diff --git a/lib/hashset.ml b/lib/hashset.ml
index fd3d1a554f..6f62e1a90e 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -79,6 +79,8 @@ module Make (E : EqType) =
if i >= Weak.length b then accu else
count_bucket (i+1) b (accu + (if Weak.check b i then 1 else 0))
+ let min x y = if x - y < 0 then x else y
+
let next_sz n = min (3 * n / 2 + 3) Sys.max_array_length
let prev_sz n = ((n - 3) * 2 + 2) / 3
diff --git a/lib/util.ml b/lib/util.ml
index af3b13fa7d..6a0ba470a9 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -137,9 +137,14 @@ let subst_command_placeholder s t =
done;
Buffer.contents buff
-module Stringset = Set.Make(struct type t = string let compare (x:t) (y:t) = compare x y end)
+module StringOrd =
+struct
+ type t = string
+ external compare : string -> string -> int = "caml_string_compare"
+end
-module Stringmap = Map.Make(struct type t = string let compare (x:t) (y:t) = compare x y end)
+module Stringset = Set.Make(StringOrd)
+module Stringmap = Map.Make(StringOrd)
(* Lists *)
@@ -202,9 +207,14 @@ let delayed_force f = f ()
type ('a,'b) union = Inl of 'a | Inr of 'b
-module Intset = Set.Make(struct type t = int let compare (x:t) (y:t) = compare x y end)
+module IntOrd =
+struct
+ type t = int
+ external compare : int -> int -> int = "caml_int_compare"
+end
-module Intmap = Map.Make(struct type t = int let compare (x:t) (y:t) = compare x y end)
+module Intset = Set.Make(IntOrd)
+module Intmap = Map.Make(IntOrd)
(*s interruption *)