Anonymous | Login | Signup for a new account 2015-12-02 07:56 CET
 Main | My View | View Issues | Change Log | Roadmap

View Issue Details  Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005171OCamlOCaml generalpublic2010-10-25 16:472012-09-25 20:07
Reporterbluestorm
Assigned Toprotz
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed
PlatformOSOS Version
Product Version3.12.0
Target VersionFixed in Version3.13.0+dev
Summary0005171: map.ml function `join` does more comparisons than needed
DescriptionI'm under the impression that the `join` function in Map.ml is a bit wasteful regarding the use of user-provided comparison functions :

let rec join l v d r =
match (l, r) with
(Empty, _) -> add v d r
| (_, Empty) -> add v d l
| (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
if lh > rh + 2 then bal ll lv ld (join lr v d r) else
if rh > lh + 2 then bal (join l v d rl) rv rd rr else
create l v d r

The two base cases use the `add` primitive, wich itself uses the `Ord.compare` function to locate the right place for the key `v` in the tree. However, no such comparisons should be needed as we know statically that the key is (in either case) less than or bigger than all keys in the target tree.

I have experimented with the following implementation, which seems to be doing ok (but I'm not familiar with the algorithmic considerations wrt. the balanced trees) :

(* beware : those two functions assume that the added k is *strictly*
smaller (or bigger) than all the present keys in the tree; it
does not test for equality with the current min (or max) key.

Indeed, they are only used during the "join" operation which
respects this precondition.
*)
let rec add_min_binding k v = function
| Empty -> singleton k v
| Node (l, x, d, r, h) ->
bal (add_min_binding k v l) x d r

let rec add_max_binding k v = function
| Empty -> singleton k v
| Node (l, x, d, r, h) ->
bal l x d (add_max_binding k v r)

(* Same as create and bal, but no assumptions are made on the
relative heights of l and r.
*)
let rec join l v d r =
match (l, r) with
(Empty, _) -> add_min_binding v d r
| (_, Empty) -> add_max_binding v d l
| (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
if lh > rh + 2 then bal ll lv ld (join lr v d r) else
if rh > lh + 2 then bal (join l v d rl) rv rd rr else
create l v d r

The advantage of such a modification is that it avoids the use of the user-provided comparison function when unnecessary, which may be arbitrarily costly.
TagsNo tags attached.
Attached Files FMapAVL.v [^] (67,717 bytes) 2010-10-27 12:34
FMapFullAVL.v [^] (25,209 bytes) 2010-10-27 12:34

 Relationships

 Notes pilki (reporter) 2010-10-27 12:35 I added two modifications of the MapAVL library of coq 8.3 including the proposal, proving it correct. protz (manager) 2011-12-23 21:55 This has been enacted. r11955

 Issue History Date Modified Username Field Change 2010-10-25 16:47 bluestorm New Issue 2010-10-27 12:34 pilki File Added: FMapAVL.v 2010-10-27 12:34 pilki File Added: FMapFullAVL.v 2010-10-27 12:35 pilki Note Added: 0005691 2011-05-20 15:01 doligez Status new => acknowledged 2011-12-23 21:55 protz Note Added: 0006525 2011-12-23 21:55 protz Status acknowledged => resolved 2011-12-23 21:55 protz Fixed in Version => 3.13.0+dev 2011-12-23 21:55 protz Resolution open => fixed 2011-12-23 21:55 protz Assigned To => protz 2012-09-25 20:07 xleroy Status resolved => closed