From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 4E019BC75 for ; Thu, 24 Feb 2005 22:45:58 +0100 (CET) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j1OLjvFL018940 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=NO) for ; Thu, 24 Feb 2005 22:45:58 +0100 Received: from localhost (localhost [127.0.0.1]) by ext.lri.fr (Postfix) with ESMTP id CCA3419E947; Thu, 24 Feb 2005 22:45:57 +0100 (CET) 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 28128-04; Thu, 24 Feb 2005 22:45:57 +0100 (CET) Received: from acces.lri.fr (acces [129.175.15.6]) (using TLSv1 with cipher EDH-RSA-DES-CBC3-SHA (168/168 bits)) (No client certificate requested) by ext.lri.fr (Postfix) with ESMTP id B98F919E929; Thu, 24 Feb 2005 22:45:57 +0100 (CET) Date: Thu, 24 Feb 2005 22:45:52 +0100 (CET) From: Pierre Letouzey To: David Monniaux Cc: Coq , caml-list Subject: Re: [Coq-Club] camlp4 rewrites In-Reply-To: <421E3AEC.2080200@ens.fr> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Virus-Scanned: by amavisd-new at lri.fr X-Miltered: at nez-perce with ID 421E4B15.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; letouzey:01 letouzey:01 lri:01 rewrites:01 monniaux:01 wrote:01 coq:01 ocaml:01 infix:01 coq:01 ocaml:01 bug:01 mistaken:01 datatype:01 reused:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: Hello David, On Thu, 24 Feb 2005, David Monniaux wrote: > I'm currently playing with Coq and extraction, and I'm having the > following problems: > * Since the list constructor of standard OCaml (infix ::) is not (yet) > usable as a prefix ( :: ), I cannot just tell Coq to extract lists to > OCaml lists. (Future OCaml versions will allow prefix ( :: ), I'm told.) Yes, Yves Bertot has come long ago with the same problem, and I remember having submitted a feature-wish to the Ocaml team. > * OCaml compiles match e with true -> x1 | false -> x2 less efficiently > than if e then x1 else x2 (bug report filed, but not fixed so far). > > Unless I'm greatly mistaken, this can be fixed by a mere syntactic > transformation using Camlp4. I suppose I'm not the first person to have > encountered these problems... So has anybody done the necessary Camlp4 > scripts? :-) > Indeed, I've got such a camlp4 translator. I do not advertize it much, because it's not very robust. In particular, if you have defined your own customized "list" datatype or reused any of the Coq standard library names, that will lead to problems. Nevertheless, in normal situation, it will do what you expect. The script (containing instructions) is: http://www.lri.fr/~letouzey/download/pp_extract.ml In particular, there is a portion to uncomment if you want the sumbool type (left|right) to be translated to boolean and hence take advantage of "if ... then ... else" syntax. Cheers, Pierre