aboutsummaryrefslogtreecommitdiff
path: root/lib/fset.ml
diff options
context:
space:
mode:
authorppedrot2012-11-08 17:11:59 +0000
committerppedrot2012-11-08 17:11:59 +0000
commitb0b1710ba631f3a3a3faad6e955ef703c67cb967 (patch)
tree9d35a8681cda8fa2dc968535371739684425d673 /lib/fset.ml
parentbafb198e539998a4a64b2045a7e85125890f196e (diff)
Monomorphized a lot of equalities over OCaml integers, thanks to
the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/fset.ml')
-rw-r--r--lib/fset.ml16
1 files changed, 8 insertions, 8 deletions
diff --git a/lib/fset.ml b/lib/fset.ml
index 567feaa75c..c93ce535d1 100644
--- a/lib/fset.ml
+++ b/lib/fset.ml
@@ -93,7 +93,7 @@ struct
(Empty, None, Empty)
| Node(l, v, r, _) ->
let c = X.compare x v in
- if c = 0 then (l, Some v, r)
+ if Int.equal c 0 then (l, Some v, r)
else if c < 0 then
let (ll, vl, rl) = split x l in (ll, vl, join rl v r)
else
@@ -109,13 +109,13 @@ struct
Empty -> false
| Node(l, v, r, _) ->
let c = X.compare x v in
- c = 0 || mem x (if c < 0 then l else r)
+ Int.equal c 0 || mem x (if c < 0 then l else r)
let rec add x = function
Empty -> Node(Empty, x, Empty, 1)
| Node(l, v, r, _) as t ->
let c = X.compare x v in
- if c = 0 then t else
+ if Int.equal c 0 then t else
if c < 0 then bal (add x l) v r else bal l v (add x r)
let singleton x = Node(Empty, x, Empty, 1)
@@ -124,7 +124,7 @@ struct
Empty -> Empty
| Node(l, v, r, _) ->
let c = X.compare x v in
- if c = 0 then merge l r else
+ if Int.equal c 0 then merge l r else
if c < 0 then bal (remove x l) v r else bal l v (remove x r)
let rec union s1 s2 =
@@ -133,12 +133,12 @@ struct
| (t1, Empty) -> t1
| (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
if h1 >= h2 then
- if h2 = 1 then add v2 s1 else begin
+ if Int.equal h2 1 then add v2 s1 else begin
let (l2, _, r2) = split v1 s2 in
join (union l1 l2) v1 (union r1 r2)
end
else
- if h1 = 1 then add v1 s2 else begin
+ if Int.equal h1 1 then add v1 s2 else begin
let (l1, _, r1) = split v2 s1 in
join (union l1 l2) v2 (union r1 r2)
end
@@ -184,7 +184,7 @@ struct
compare_aux [s1] [s2]
let equal s1 s2 =
- compare s1 s2 = 0
+ Int.equal (compare s1 s2) 0
let rec subset s1 s2 =
match (s1, s2) with
@@ -194,7 +194,7 @@ struct
false
| Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) ->
let c = X.compare v1 v2 in
- if c = 0 then
+ if Int.equal c 0 then
subset l1 l2 && subset r1 r2
else if c < 0 then
subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2