The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

A month ago, there was a discussion about how to produce
pretty extracted ocaml code for Coq, and in particular how to
use the ocaml list syntax ([] and ::). At first I was thinking of
integrating that syntax within my own ocaml pretty-printer
contrib/extraction/ocaml.ml. But that would have made uglier
a file that is already not very pretty. Then I remembered a
suggestion made by Francois-Rene Rideau concerning Camlp4.

So I finally made a post-extraction pretty-printer using Camlp4,
that replace Coq list/prod/bool(+sumbool optionaly) by their ocaml
counterparts.

You can find the source of this small tool enclosed with this mail.
Installation & Usage notes are at the beginning of this file.
Please have also a look at the CAVEAT: this tool isn't perfect, and
some name clashes may occur. And of course, since my skills in Camlp4
are very recent & limited, there might still be some grammar bugs.

Pierre Letouzey
(***********************************************************)
(*****                pp_extract.ml                   ******)
(***********************************************************)

(* The goal of this file is to enhance readability of 
   Ocaml source files automatically extracted from Coq.
   To this purpose, we propose here to replace a few extracted 
   datatypes by their well-known predefined equivalents in Ocaml:
   
    -  lists
    -  pairs
    -  booleans 
    -  sumbool (Left/Right)
  
   Notice than the sumbool part is commented out by default, 
   since systematically replacing sumbool by boolean is quite 
   a matter of taste. Some may find that clearer, some others not. 
   Uncomment that zone or not according to your taste.

   For each datatype, 
     - we put its name in a list in order to get rid of its definition
   like "type 'a list = Nil | Cons of 'a * 'a list" (see the ast filter 
   at the end of this file. 
     - we put some grammar rules to replace datatype constructors/name
   by its ocaml equivalents.
   
   A special remark concerning booleans: all
   "match ... with True -> ... | False -> ... " constructions
   become "if ... then ... else ...". If you find that unsatisfactory,
   just comment out the last grammar rule of the bool part.

  INSTALLATION: 
  ocamlc -pp "camlp4o pa_extend.cmo q_MLast.cmo" -I +camlp4 -c pp_extract.ml
  mkcamlp4 pa_o.cmo pr_o.cmo ./pp_extract.cmo -o pp_extract
  
  USAGE: 
  ./pp_extract -cip my_ugly_extracted_file.ml -o my_beautiful_output.ml
   
  (the -cip tries to keep the few comments put by the extraction) 

  CAVEAT: 
  This tool is purely syntactic. Do not expect too much of it. 
  In particular name clashes are to be expected if not used carefully.
  For example if you have Coq streams in your files, the "Cons" will 
  become a "::" 

  Pierre Letouzey
  LRI Orsay
  Remarks/feedbacks/bug reports: 
letouzey AT lri.fr

*)
   

open Pcaml
open MLast

let removed_defs = ref ([]: string list)

(* list *)

let _ = removed_defs := "list" :: !removed_defs

EXTEND
  expr: BEFORE "simple"
    [[ UIDENT "Cons" -> let c = "::" in <:expr< $uid:c$ >> ]
    |[ UIDENT "Nil" -> <:expr< [] >> ]];
  patt: BEFORE "simple"
    [[ UIDENT "Cons" -> let c = "::" in <:patt< $uid:c$ >> ]
    |[ UIDENT "Nil" -> <:patt< [] >> ]];
END

(* pairs *)

let _ = removed_defs := "prod" :: !removed_defs

EXTEND
  expr: BEFORE "simple"
    [[ UIDENT "Pair" ; a = expr -> <:expr<$a$>> ]];
  patt: BEFORE "simple" 
    [[ UIDENT "Pair" ; a = patt -> <:patt<$a$>> ]];
  ctyp: LEVEL "simple"
    [[ "("; a = SELF; "," ; tl = LIST1 ctyp SEP ","; ")"; LIDENT "prod" -> 
         let b = List.hd tl in <:ctyp< ($a$ * $b$) >> ]];
END

(* bool *)

let _ = removed_defs := "bool" :: !removed_defs

EXTEND
  expr: BEFORE "simple"
    [[ UIDENT "True" -> <:expr< True >> ]
    |[ UIDENT "False" -> <:expr< False >> ]];
  patt: BEFORE "simple"
    [[ UIDENT "True" -> <:patt< True >> ]
    |[ UIDENT "False" -> <:patt< False >> ]];
  expr: LEVEL "expr1" 
    [[ "match"; e = SELF; "with"; 
       OPT "|"; UIDENT "True"; "->"; e1 = expr; 
       "|"; UIDENT "False"; "->"; e2 = expr -> 
         <:expr< if $e$ then $e1$ else $e2$ >> ]];
END


(* sumbool *)
(*
let _ = removed_defs := "sumbool" :: !removed_defs

EXTEND
  expr: BEFORE "simple"
    [[ UIDENT "Left" -> <:expr< True >> ]
    |[ UIDENT "Right" -> <:expr< False >> ]];
  patt: BEFORE "simple"  
    [[ UIDENT "Left" -> <:patt< True >> ]
    |[ UIDENT "Right" -> <:patt< False >> ]];
  ctyp: BEFORE "simple"
    [[ LIDENT "sumbool" -> <:ctyp< bool >> ]];
  expr: LEVEL "expr1" 
    [[ "match"; e = SELF; "with"; 
       OPT "|"; UIDENT "Left"; "->"; e1 = expr; 
       "|"; UIDENT "Right"; "->"; e2 = expr -> 
         <:expr< if $e$ then $e1$ else $e2$ >> ]];
END
*)

(* the filter functions, used to removed obsolete type definitions from file 
*) 

let new_loc loc = function 
  | None -> loc 
  | Some pos -> pos, snd loc

let rec filter_str_item op = function 
  | [] -> [] 
  | (StTyp (_,[(_,s),_,_,_]),(deb,_)) :: l when List.mem s !removed_defs ->
      filter_str_item (Some deb) l 
  | (ast,loc) :: l -> (ast, new_loc loc op) :: (filter_str_item None l)

let rec filter_sig_item op = function 
  | [] -> [] 
  | (SgTyp (_,[(_,s),_,_,_]),(deb,_)) :: l when List.mem s !removed_defs ->
      filter_sig_item (Some deb) l 
  | (ast,loc) :: l -> (ast, new_loc loc op) :: (filter_sig_item None l)
                        
let _ = 
  let p_sig = !print_interf and p_str = !print_implem in 
  print_interf := (fun l -> p_sig (filter_sig_item None l)); 
  print_implem := (fun l -> p_str (filter_str_item None l))