coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Extraction performances

From: Thomas Braibant <thomas.braibant AT gmail.com>
To: coq-club AT inria.fr
Cc: Damien Pous <Damien.Pous AT inria.fr>
Subject: [Coq-Club] Extraction performances
Date: Wed, 6 Jan 2010 21:50:02 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:cc:content-type; b=aTOe7YX17CFFpe/dyYMENx9EN0FgHTKDIAhHpdbmHhQhlW2bdHhZLY1IR2QiukILsT G4YTleA4tMkkKPhruSxYO8ra0Rmh8y7lXmuRcMfeSFg7Y38eFlFOA4oj2owaGF6f8yZO 8D28HhBBSMzuovCgzbvglO2N2JvB0bGAaO/4U=

Hi List,

I have extracted some part of a development (a decision procedure),
that performs intensive calculations with Finite Sets and Finite Maps
on positives. I try to evaluate the performances of this decision
procedure, with respect to its extracted couterpart in OCaml.

I was rather surprised to see that there is almost no efficiency
difference when I replaced the FMaps and FSets on positives (both
Patricia trees with radix-2) with standard OCaml Maps and Sets over
ints. I gather this is somehow because Patricia trees are highly
efficient for positives, and that standard Ocaml Maps must performs
more comparisons, but I am puzzled. Can anyone comment on this ?

Moreover, has someone any kind of implementation in OCaml of the
signature of FMaps and FSets over ints (with some kind of persistent
arrays) I could play with ?

With best regards,
thomas braibant

[Coq-Club] Extraction performances, Thomas Braibant