Arnaud Spiwack a écrit :
> There's at least been a Coq implementation (proven correct if I'm not 
> mistaken). Thus extractible into OCaml in a probably idiomatic way. I 
> don't know if the library is self contained or just a small proof-of 
> concept, though.
>
> http://www.lri.fr/~sozeau/research/russell/fingertrees.fr.html
>
>
> Arnaud Spiwack
>
> Jon Harrop a écrit :
>> I'm just perusing the multitude of tree data structures out there and 
>> was wondering if anyone has a finger tree implementation written in 
>> OCaml?
>>
>> Cheers,
Indeed, this is a certified implementation of Finger Trees, it's just 
not ready for release yet. I'm actually working on a version using 
modules which extracts to efficient OCaml code (e.g. ropes built on top 
of them permit to run the ICFP simulator in reasonnable time). So, the 
basic extracted code works well but I haven't finished building a 
certified implementation of the ropes which I want to release with it. 
In the meantime you can try this extracted version:

http://www.lri.fr/~sozeau/res/fingertrees-0.1.tgz

Some random notes:
- No documentation / beautifying of the ocaml sources, look at the Coq 
literate code for that, available from the webpage:
http://www.lri.fr/~sozeau/research/russell/fingertrees.en.html
- Uses a bit of Obj.magic for polymorphic recursion
- Some artifacts of extraction make it a bit slower than it could be 
(useless beta-redexes)
- Should still be bug free even at 0.1 !
- Uses ocamlfind for installation
- Released under the LGPL
- It will get polished soon...

Cheers,

-- 
Matthieu Sozeau
http://www.lri.fr/~sozeau