Date: 2014-12-04
Categories: parsing

Parsing examples

My work on P1, E3, P3 and P4 was motivated in part by a desire to have simple tools that I could use in other areas of research. These tools are mostly source-to-source translators. For example, in the past I have had various ad-hoc tools to translate OCaml to LaTeX, or OCaml to HOL, HOL to Lem, Lem to OCaml etc.

The idea is to start making these tools maintainable and not one-off efforts to be used for a particular task then thrown away.

Previous versions of P1 etc have not been engineered well enough to make the resulting tools maintainable or usable. I am hoping to change that by investing more engineering effort into P1 etc.

So I have started a new repository on github https://github.com/tomjridge/example_grammars/ which contains grammars and grammar-based tools that I use.

To reduce grammar maintenance, I have added additional functionality to P1 etc:

OCAMLTYPEXPR -> "'" ?ident?            {{ Tex.tyvar ([x1;x2]|>ss_concat|>c) }}
  | "(" w1=?w? t=TYPEXPR w2=?w? ")"       {{ "("^(Tex.w w1)^t^(Tex.w w2)^")" }}

As a (somewhat largish) example, a grammar for a Lem/OCaml language is https://github.com/tomjridge/example_grammars/blob/master/src/ocaml.cppo Note that this can be used with p1 (for correctness/simplcity) and p4 (for speed). This is possible because p1 and p4 have essentially the same interface. At the moment there is only a single set of actions (to map to LaTeX). I am currently using this to produce typeset Lem code for inclusion in a paper.


Related posts: