From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 6917ABC75 for ; Thu, 24 Feb 2005 21:39:01 +0100 (CET) Received: from postfix3-2.free.fr (postfix3-2.free.fr [213.228.0.169]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j1OKb1W5014779 for ; Thu, 24 Feb 2005 21:39:01 +0100 Received: from picsou.chatons.dyndns.org (unknown [82.225.77.14]) by postfix3-2.free.fr (Postfix) with ESMTP id 45B02C129; Thu, 24 Feb 2005 21:37:01 +0100 (CET) Received: from ens.fr (localhost.localdomain [127.0.0.1]) by picsou.chatons.dyndns.org (Postfix) with ESMTP id 1298317979; Thu, 24 Feb 2005 21:37:01 +0100 (CET) Message-ID: <421E3AEC.2080200@ens.fr> Date: Thu, 24 Feb 2005 21:37:00 +0100 From: David Monniaux User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.4.1) Gecko/20031114 X-Accept-Language: fr-fr, fr, en-us, en-gb, en, es-es, es MIME-Version: 1.0 To: coq-club@pauillac.inria.fr, caml-list Subject: camlp4 rewrites X-Enigmail-Version: 0.76.8.0 X-Enigmail-Supports: pgp-inline, pgp-mime Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; monniaux:01 monniaux:01 rewrites:01 coq:01 ocaml:01 infix:01 coq:01 ocaml:01 bug:01 mistaken:01 ...:98 syntactic:01 constructor:01 usable:01 compiles: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: 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.) * 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? :-)