Re: using camlp4 api [WAS: Re: [Caml-list] parsing problem.]

["Nicolas Pouillard" <nicolas.pouillard@inria.fr>]

On 1/24/07, Martin Jambon <martin.jambon@ens-lyon.org> 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