[wg-camlp4] My uses of syntax extension

[Harrison, John R]

I'm currently using camlp5 for syntax extensions. I never switched to
the new camlp4. It was introduced with minimal discussion and hardly
any useful documentation, while even things that were trivial in
camlp5 seemed complicated, so I never made the effort.

I think one of my applications (item 2 below) is very unusual, so
perhaps it will be a useful, or at least amusing, outlier in any list
people accumulate of current uses of syntax extension.

1. In the code for my book (http://www.cl.cam.ac.uk/~jrh13/atp/) I use
   items entered in <<quotations>>, which I simply want to treat as a
   string to get passed to my parser. This is essentially trivial in
   camlp5, though I think it is less so in camlp4.

   let quotexpander s =
     .... "default_parser \""^(String.escaped s)^"\"";;

   Quotation.add "" (Quotation.ExStr (fun x -> quotexpander));;

2. For the HOL Light prover (http://code.google.com/p/hol-light/),
   backward compatibility with other HOLs (where ML is used not only
   as the implementation language but also as the toplevel) dictates
   that I do various things to make OCaml look like old-style ML:

       * Add some alphanumeric infixes like "o" and "THEN"

       * Use "it" as the default binding for the previous expression
         (actually, I would prefer the toplevel to do this anyway).

       * Use quotations, but within the characters `....` not <<...>>

       * Completely change the OCaml lexical conventions so that
         all-uppercase words like INST and REWRITE_TAC are treated as
         ordinary identifiers.

   The subversion of the lexical conventions is the most tiresome
   aspect. (It also needs to be switchable in order to allow easy
   interfacing with more conventional OCaml code.) In camlp5, I do
   this by copying and editing the existing lexer, which makes it
   very brittle and necessitates frequent changes as camlp5's
   internals evolve. I would very much like a better solution.

John.