From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.3 required=5.0 tests=AWL,MISSING_HEADERS autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id C5BC1BC69 for ; Thu, 25 Oct 2007 16:29:25 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAApFIEfAXQInh2dsb2JhbACOWgIBCAop X-IronPort-AV: E=Sophos;i="4.21,328,1188770400"; d="scan'208";a="5094576" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 25 Oct 2007 16:29:25 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l9PETOgK012001 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 25 Oct 2007 16:29:24 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAApFIEeBrw8Eh2dsb2JhbACOWgIBCAop X-IronPort-AV: E=Sophos;i="4.21,328,1188770400"; d="scan'208";a="18602404" Received: from ext.lri.fr ([129.175.15.4]) by mail4-smtp-sop.national.inria.fr with ESMTP; 25 Oct 2007 16:29:24 +0200 Received: from localhost (localhost [127.0.0.1]) by ext.lri.fr (Postfix) with ESMTP id 30DDAA46AA for ; Thu, 25 Oct 2007 16:29:24 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at lri.fr Received: from ext.lri.fr ([127.0.0.1]) by localhost (ext.lri.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id Ax+nMPwiv5Nd for ; Thu, 25 Oct 2007 16:29:24 +0200 (CEST) Received: from lri4-245.lri.fr (lri4-245 [129.175.4.245]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by ext.lri.fr (Postfix) with ESMTP id 19285A46A9 for ; Thu, 25 Oct 2007 16:29:24 +0200 (CEST) Message-ID: <4720A840.5060603@lri.fr> Date: Thu, 25 Oct 2007 16:29:20 +0200 From: Matthieu Sozeau Organization: LRI User-Agent: Thunderbird 2.0.0.6 (Macintosh/20070728) MIME-Version: 1.0 Cc: caml-list Subject: Re: [Caml-list] Finger trees References: <200710231233.47817.jon@ffconsultancy.com> <471E60B4.8070607@lix.polytechnique.fr> In-Reply-To: <471E60B4.8070607@lix.polytechnique.fr> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 4720A844.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; matthieu:01 matthieu:01 lri:01 coq:01 ocaml:01 lri:01 ocaml:01 cheers:01 icfp:01 reasonnable:01 coq:01 literate:01 recursion:01 bug:01 ocamlfind:01 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