The Coq mailing list

[Martin Jambon <martin_jambon AT emailuser.net>]

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