camlp4 rewrites

camlp4 rewrites

[David Monniaux]

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? :-)

Re: [Coq-Club] camlp4 rewrites

[Pierre Letouzey]

Hello David,

On Thu, 24 Feb 2005, David Monniaux wrote:

> 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.)

Yes, Yves Bertot has come long ago with the same problem, and I remember 
having submitted a feature-wish to the Ocaml team.

> * 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? :-)
>

Indeed, I've got such a camlp4 translator. I do not advertize it much, 
because it's not very robust. In particular, if you have defined your own 
customized "list" datatype or reused any of the Coq standard library 
names, that will lead to problems. Nevertheless, in normal situation, it 
will do what you expect. The script (containing instructions) is:

http://www.lri.fr/~letouzey/download/pp_extract.ml

In particular, there is a portion to uncomment if you want the sumbool 
type (left|right) to be translated to boolean and hence take advantage
of "if ... then ... else" syntax.

Cheers,

Pierre

Re: [Caml-list] camlp4 rewrites

[Martin Jambon]

On Thu, 24 Feb 2005, David Monniaux wrote:

> 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? :-)

The following should solve your problem #2 (I just wrote as an exercise
for myself :-)
It works by overriding (partially) the regular syntax of OCaml (which
might not be the syntax of Coq, I don't know Coq). If anyone
has a better solution, please tell me.
The general solution however seems to work only on the AST. Any
comments or suggestions?


(* File pa_matchbool.ml
   Compilation:
     ocamlc -c -I +camlp4 -pp 'camlp4o pa_extend.cmo q_MLast.cmo -loc loc' \
        pa_matchbool.ml
   Test:
     camlp4o -I . pr_o.cmo pa_matchbool.cmo test_matchbool.ml \
        -o test_matchbool.ppo
*)
let expand_match loc e l =
  match l with
      [ <:patt< True >>, None, e1;
	(<:patt< False >> | <:patt< _ >>), None, e2 ]
    | [ <:patt< False >>, None, e2;
	(<:patt< True >> | <:patt< _ >>), None, e1 ] ->

	true, <:expr< if $e$ then $e1$ else $e2$ >>

    | _ -> false, <:expr< match $e$ with [ $list:l$ ] >>

let expand_function loc l =
  match expand_match loc <:expr< __matchbool >> l with
      true, e -> <:expr< fun __matchbool -> $e$ >>
    | false, _ -> <:expr< fun [ $list:l$ ] >>


let match_case = Grammar.Entry.create Pcaml.gram "match_case";;

EXTEND
  GLOBAL: match_case;

  Pcaml.expr: LEVEL "expr1" [
    [ "match"; e = Pcaml.expr; "with";
	OPT "|"; cases = LIST1 match_case SEP "|" ->
	  snd (expand_match loc e cases)
    | "function";
	OPT "|"; cases = LIST1 match_case SEP "|" ->
	  expand_function loc cases ]
  ];

  match_case: [
    [ x1 = Pcaml.patt;
      w = OPT [ "when"; e = Pcaml.expr -> e ]; "->";
      x2 = Pcaml.expr -> (x1, w, x2) ]
  ];
END;;



Martin

--
Martin Jambon, PhD
Researcher in Structural Bioinformatics since the 20th Century
The Burnham Institute http://www.burnham.org
San Diego, California