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=1.1 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr 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 2076FBC0B for ; Thu, 25 Jan 2007 10:36:57 +0100 (CET) Received: from nz-out-0506.google.com (nz-out-0506.google.com [64.233.162.224]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l0P9awpG030257 for ; Thu, 25 Jan 2007 10:36:59 +0100 Received: by nz-out-0506.google.com with SMTP id l8so427697nzf for ; Thu, 25 Jan 2007 01:36:55 -0800 (PST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; b=olfqRXqIXpID3z17h+xgL5KopNiRNaYsiSb/8uxf0/D6CXcQtdjIHJKDwv2/oEIFa4y2H5334QOft64BO4+/utWFrOzMvCdqaCYrQKE7D6rGrpEsDAnzDyIIR7OAy/RAQTpjPk6EGhENJJA0EEC489xbVnyS+Gcxr+ma4mpPD80= Received: by 10.35.65.17 with SMTP id s17mr3458374pyk.1169717815206; Thu, 25 Jan 2007 01:36:55 -0800 (PST) Received: by 10.35.95.3 with HTTP; Thu, 25 Jan 2007 01:36:55 -0800 (PST) Message-ID: Date: Thu, 25 Jan 2007 10:36:55 +0100 From: "Nicolas Pouillard" Sender: nicolas.pouillard@gmail.com To: "Martin Jambon" Subject: Re: using camlp4 api [WAS: Re: [Caml-list] parsing problem.] Cc: "Pietro Abate" , "ocaml ml" In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <20070123235940.GA32163@pulp.rsise.anu.edu.au> <20070124215329.GA17676@pulp.rsise.anu.edu.au> X-Google-Sender-Auth: 88e74d3089e18b25 X-Miltered: at concorde with ID 45B87A3A.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; camlp:01 parsing:01 ens-lyon:01 camlp:01 parser:01 grammars:01 verbose:01 coq:01 coq:01 parsing:01 syntax:01 nat:01 nat:01 notation:01 2007,:98 On 1/24/07, Martin Jambon wrote: > On Thu, 25 Jan 2007, Pietro Abate wrote: > > > where in the first part there is a grammar definition and in the second part > > the grammar is used to parse the argument of the match statement. > > > > my question: Is it possible to do something similar with camlp4 ? > > > > In the library documentation I can see that this might be possible, but I don't > > quite understand where to start. The first step should be to write a small > > parser to interpret the language definition and then to generate, by using the > > Grammar (extensible grammars) module, other production that extend the current > > grammar to parse the rest of the file. The trick part is that I cannot write (I > > think) and EXTEND statement on the fly (as it should be parsed itself), but I > > have to use the quotation library directly, and this is very verbose... > > > > Did anybody do anything similar ? One small example ? > Yes, Coq is one example but not a small one :) Indeed Coq parsing uses camlp4. And Coq have a syntax extensible on the fly. Coq < Definition myeq (x : nat) (y : nat) := x = y. myeq is defined Coq < Notation "x '=?=' y" := (myeq x y) (at level 70, no associativity). Coq < Check (3 =?= 4). 3 =?= 4 : Prop -- Nicolas Pouillard