Test & correction de la production de code Haskell

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2468 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 124 insertions, 111 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 5e1d4c8086..e56e151c8d 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -22,6 +22,8 @@ open Util
 
 let current_module = ref None
 
+let is_construct = function ConstructRef _ -> true | _ -> false 
+
 let sp_of_r r = match r with 
     | ConstRef sp -> sp
     | IndRef (sp,_) -> sp
@@ -91,9 +93,8 @@ let cache r f =
 module ToplevelParams = struct
   let toplevel = true
   let globals () = Idset.empty
-  let rename_global r = Termops.id_of_global (Global.env()) r
-  let pp_type_global = Printer.pr_global
-  let pp_global = Printer.pr_global
+  let rename_global r _ = Termops.id_of_global (Global.env()) r
+  let pp_global r _ = Printer.pr_global r
 end
 
 (*s Renaming issues for a monolithic extraction. *)
@@ -109,25 +110,16 @@ module MonoParams = struct
     global_ids := Idset.add id' !global_ids; 
     id'
 
-  let rename_type_global r =  
-    cache r
-      (fun r -> 
-	 let id = Termops.id_of_global (Global.env()) r in
-	 rename_global_id (lowercase_id id))
-      
-  let rename_global r = 
+  let rename_global r upper = 
     cache r
       (fun r -> 
 	 let id = Termops.id_of_global (Global.env()) r in
-	 match r with
-	   | ConstructRef _ -> rename_global_id (uppercase_id id)
-	   | _ -> rename_global_id (lowercase_id id))
+	 rename_global_id 
+	   (if upper || (is_construct r) 
+	    then uppercase_id id else lowercase_id id))
       
-  let pp_type_global r = 
-    str (check_ml r (string_of_id (rename_type_global r)))
-      
-  let pp_global r = 
-    str (check_ml r (string_of_id (rename_global r)))
+  let pp_global r upper = 
+    str (check_ml r (string_of_id (rename_global r upper)))
       
 end
 
@@ -153,27 +145,17 @@ module ModularParams = struct
       else id'
     in global_ids := Idset.add id' !global_ids; id'
 
-  let rename_type_global r = 
-    cache r 
-      (fun r ->     
-	 let id = Termops.id_of_global (Global.env()) r in 
-	 rename_global_id r id (lowercase_id id) "coq_")
-
-  let rename_global r =
+  let rename_global r upper =
     cache r 
       (fun r -> 
 	 let id = Termops.id_of_global (Global.env()) r in 
-	 match r with
-	   | ConstructRef _ -> rename_global_id r id (uppercase_id id) "Coq_"
-	   | _ -> rename_global_id r id (lowercase_id id) "coq_")
-
-  let pp_type_global r = 
-    str 
-      (check_ml r ((module_option r)^(string_of_id (rename_type_global r))))
+	 if upper || (is_construct r) then 
+	   rename_global_id r id (uppercase_id id) "Coq_"
+	 else rename_global_id r id (lowercase_id id) "coq_")
 
-  let pp_global r = 
+  let pp_global r upper = 
     str
-      (check_ml r ((module_option r)^(string_of_id (rename_global r))))
+      (check_ml r ((module_option r)^(string_of_id (rename_global r upper))))
 
 end
 
@@ -211,7 +193,8 @@ let extract_to_file f prm decls =
   in
   let cout = open_out f in
   let ft = Pp_control.with_output_to cout in
-  if decls <> [] then pp_with ft (hv 0 (preamble prm));
+  if decls <> [] || prm.lang = "haskell" 
+  then pp_with ft (hv 0 (preamble prm));
   begin 
     try
       List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index ce367c1c2b..6f987696b9 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -287,9 +287,9 @@ let decl_in_m m = function
   | Dtype ([],_) -> false
   | Dcustom (r,_) ->  is_long_module m r
 
-let file_suffix = function
-  | "ocaml" -> ".ml"
-  | "haskell" -> ".hs"
+let module_file_name m = function
+  | "ocaml" -> (String.uncapitalize (string_of_id m)) ^ ".ml"
+  | "haskell" -> (String.capitalize (string_of_id m)) ^ ".hs"
   | _ -> assert false
 
 let _ = 
@@ -298,8 +298,7 @@ let _ =
        | [VARG_STRING lang; VARG_IDENTIFIER m] ->
 	   (fun () -> 
 	      let dir_m = module_of_id m in 
-	      let f = (String.uncapitalize (string_of_id m))
-		       ^ (file_suffix lang) in
+	      let f = module_file_name m lang in
 	      let prm = {lang=lang;
 			 toplevel=false;
 			 mod_name= Some m;
@@ -333,8 +332,7 @@ let _ =
 	      Dirset.iter 
 		(fun m ->
 		   let short_m = snd (split_dirpath m) in
-		   let f = (String.uncapitalize (string_of_id short_m))
-			   ^ (file_suffix lang) in
+		   let f = module_file_name short_m lang in 
 		   let prm = {lang=lang;
 			      toplevel=false;
 			      mod_name= Some short_m;
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 7b2e4c9d7c..7f6821eb87 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -783,6 +783,7 @@ and extract_constant sp =
 
 and eta_expanse ec typ = match ec with 
   | Emlterm (MLlam _) -> ec
+  | Emlterm (MLfix _) -> ec 
   | Emlterm a -> 
       (match extract_type (Global.env()) typ with 
 	 | Tmltype (Tarr _, _) -> 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 213e758190..0dcf58916a 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -37,18 +37,24 @@ let preamble prm =
     | Some m -> String.capitalize (string_of_id m) 
   in 
   (str "module " ++ str m ++ str " where" ++ fnl () ++ fnl () ++
-     str "type Prop = ()" ++ fnl () ++
-     str "prop = ()" ++ fnl () ++ fnl () ++
-     str "type Arity = ()" ++ fnl () ++
-     str "arity = ()" ++ fnl () ++ fnl ())
+     str "type Prop = Unit.Unit" ++ fnl () ++
+     str "prop = Unit.unit" ++ fnl () ++ fnl () ++
+     str "type Arity = Unit.Unit" ++ fnl () ++
+     str "arity = Unit.unit" ++ fnl () ++ fnl ())
+
+let pp_abst = function
+  | [] -> (mt ())
+  | l  -> (str "\\" ++
+             prlist_with_sep (fun () -> (str " ")) pr_id l ++
+             str " ->" ++ spc ())
 
 (*s The pretty-printing functor. *)
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_type_global = P.pp_type_global
-let pp_global = P.pp_global
-let rename_global = P.rename_global
+let pp_type_global r = P.pp_global r true
+let pp_global r = P.pp_global r false
+let rename_global r = P.rename_global r false
 
 let pr_lower_id id = pr_id (lowercase_id id)
 
@@ -57,9 +63,9 @@ let empty_env () = [], P.globals()
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let rec pp_type par t =
+let rec pp_type par ren t =
   let rec pp_rec par = function
-    | Tvar id -> pr_lower_id id (* TODO: possible clash with Haskell kw *)
+    | Tvar id -> pr_id (try Idmap.find id ren with _ -> id)
     | Tapp l ->
 	(match collapse_type_app l with
 	   | [] -> assert false
@@ -67,19 +73,15 @@ let rec pp_type par t =
 	   | t::l -> 
 	       (open_par par ++
 		  pp_rec false t ++ spc () ++
-		  prlist_with_sep (fun () -> (spc ())) (pp_type true) l ++ 
+		  prlist_with_sep (fun () -> (spc ())) (pp_type true ren) l ++ 
 		  close_par par))
     | Tarr (t1,t2) ->
 	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
 	   pp_rec false t2 ++ close_par par)
-    | Tglob r -> 
-	pp_type_global r
-    | Texn s -> 
-	(str ("() -- " ^ s) ++ fnl ())
-    | Tprop ->
-	str "Prop"
-    | Tarity ->
-	str "Arity"
+    | Tglob r -> pp_type_global r
+    | Texn s -> (str ("() -- " ^ s) ++ fnl ())
+    | Tprop -> str "Prop"
+    | Tarity -> str "Arity"
   in 
   hov 0 (pp_rec par t)
 
@@ -120,8 +122,9 @@ let rec pp_expr par env args =
 	let par2 = not par' && expr_needs_par a2 in
 	apply 
 	  (hov 0 (open_par par' ++
-		  hov 2 (str "let " ++ pr_id (List.hd i) ++ str " =" ++ spc ()
-			 ++ pp_expr false env [] a1 ++ spc () ++ str "in") 
+		  hov 2 (str "let" ++ spc () ++ pr_id (List.hd i) ++ 
+			 str " = " ++ pp_expr false env [] a1 ++ spc () ++ 
+			 str "in") 
 		  ++ spc () ++ pp_expr par2 env' [] a2 ++ close_par par'))
     | MLglob r -> 
 	apply (pp_global r)
@@ -147,14 +150,17 @@ let rec pp_expr par env args =
       	pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
     | MLexn s -> 
 	(* An [MLexn] may be applied, but I don't really care *)
-	(open_par par ++ str "error" ++ spc () ++ qs s ++ close_par par)
+	(open_par par ++ str "Prelude.error" ++ spc () ++ 
+	 qs s ++ close_par par)
     | MLprop ->
 	assert (args=[]); str "prop"
     | MLarity ->
 	assert (args=[]); str "arity"
     | MLcast (a,t) ->
+	let tvars = get_tvars t in 
+	let _,ren = rename_tvars keywords tvars in 
 	(open_par true ++ pp_expr false env args a ++ spc () ++ str "::" ++ 
-	 spc () ++ pp_type false t ++ close_par true)
+	 spc () ++ pp_type false ren t ++ close_par true)
     | MLmagic a ->
 	(open_par true ++ str "Obj.magic" ++ spc () ++ 
 	 pp_expr false env args a ++ close_par true)
@@ -179,24 +185,24 @@ and pp_pat env pv =
 
 and pp_fix par env in_p (ids,bl) args =
   (open_par par ++ 
-     v 0 (str "let { " ++
-	    prvect_with_sep
-      	      (fun () -> (str "; " ++ fnl ()))
-	      (fun (fi,ti) -> pp_function env (pr_id fi) ti)
-	      (array_map2 (fun id b -> (id,b)) ids bl) ++
-	    str " }" ++fnl () ++
-	    match in_p with
-	      | Some j -> 
-      		  hov 2 (str "in " ++ pr_id ids.(j) ++
-			   if args <> [] then
-			     (str " " ++ 
-				prlist_with_sep (fun () -> (str " "))
-				  (fun s -> s) args)
-			   else
-			     (mt ()))
-	      | None -> 
-		  (mt ())) ++
-     close_par par)
+   v 0  
+     (v 2 (str "let" ++ fnl () ++
+	   prvect_with_sep fnl 
+	  (fun (fi,ti) -> pp_function env (pr_id fi) ti) 
+	     (array_map2 (fun a b -> a,b) ids bl)) ++ 
+      fnl () ++ 
+      (match in_p with
+	 | Some j -> 
+      	     hov 2 (str "in " ++ pr_id ids.(j) ++
+		    if args <> [] then
+		      (str " " ++ 
+		       prlist_with_sep (fun () -> (str " "))
+		      (fun s -> s) args)
+		    else
+		      (mt ()))
+	 | None -> 
+	     (mt ()))) ++
+   close_par par)
 
 and pp_function env f t =
   let bl,t' = collect_lams t in
@@ -210,18 +216,19 @@ let pp_ast a = hov 0 (pp_expr false (empty_env ()) [] a)
 (*s Pretty-printing of inductive types declaration. *)
 
 let pp_one_inductive (pl,name,cl) =
+  let pl,ren = rename_tvars keywords pl in
   let pp_constructor (id,l) =
     (pp_global id ++
        match l with
          | [] -> (mt ()) 
 	 | _  -> (str " " ++
       	       	    prlist_with_sep 
-		      (fun () -> (str " ")) (pp_type true) l))
+		      (fun () -> (str " ")) (pp_type true ren) l))
   in
   (str (if cl = [] then "type " else "data ") ++ 
      pp_type_global name ++ str " " ++
      prlist_with_sep (fun () -> (str " ")) pr_lower_id pl ++
-     if pl = [] then (mt ()) else (str " ") ++
+     (if pl = [] then (mt ()) else (str " ")) ++
      (v 0 (str "= " ++
 	       prlist_with_sep (fun () -> (fnl () ++ str "  | "))
                  pp_constructor cl)))
@@ -237,11 +244,16 @@ let pp_decl = function
   | Dtype (i, _) -> 
       hov 0 (pp_inductive i)
   | Dabbrev (r, l, t) ->
+      let l,ren = rename_tvars keywords l in
       hov 0 (str "type " ++ pp_type_global r ++ spc () ++ 
-	       prlist_with_sep (fun () -> (str " ")) pr_lower_id l ++
-	       if l <> [] then (str " ") else (mt ()) ++ str "=" ++ spc () ++
-	       pp_type false t ++ fnl ())
-  | Dglob (r, MLfix (i,ids,defs)) ->
+	       prlist_with_sep (fun () -> (str " ")) pr_id l ++
+	       (if l <> [] then (str " ") else (mt ())) ++ str "=" ++ spc () ++
+	       pp_type false ren t ++ fnl ())
+  | Dglob (r, MLfix (_,[|_|],[|def|])) ->
+      let id = rename_global r in
+      let env' = [id], P.globals() in
+      (pp_function  env' (pr_id id) def ++ fnl ())
+(*  | Dglob (r, MLfix (i,ids,defs)) ->
       let env = empty_env () in
       let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       (prlist_with_sep (fun () -> (fnl ()))
@@ -253,14 +265,14 @@ let pp_decl = function
 	 if id <> idi then
 	   (fnl () ++ pr_id id ++ str " = " ++ pr_id idi ++ fnl ())
 	 else
-	   (mt ()))
+	   (mt ())) *)
   | Dglob (r, a) ->
       hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl ())
   | Dcustom (r,s) -> 
       hov 0  (pp_global r ++ str " =" ++ 
 		spc () ++ str s ++ fnl ())
 
-let pp_type = pp_type false
+let pp_type = pp_type false Idmap.empty
 
 end
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 54a230881c..f4fef3df1f 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -70,9 +70,9 @@ type extraction_params =
 module type Mlpp_param = sig
   val toplevel : bool
   val globals : unit -> Idset.t
-  val rename_global : global_reference -> identifier
-  val pp_type_global : global_reference -> std_ppcmds
-  val pp_global : global_reference -> std_ppcmds
+      (* the bool arg is: should we rename in uppercase or not ? *)
+  val rename_global : global_reference -> bool -> identifier
+  val pp_global : global_reference -> bool -> std_ppcmds
 end
 
 module type Mlpp = sig
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 5656a42850..26c88726e7 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -28,6 +28,17 @@ exception Impossible
 let anonymous = id_of_string "x"
 let prop_name = id_of_string "_"
 
+(*s Get all type variables from a ML type *)
+
+let get_tvars t = 
+  let rec get_rec s = function 
+  | Tvar i -> Idset.add i s
+  | Tapp l -> List.fold_left get_rec s l 
+  | Tarr (a,b) -> get_rec (get_rec s a) b
+  | a -> s
+  in Idset.elements (get_rec Idset.empty t)
+
+
 (*s In an ML type, update the arguments to all inductive types [(sp,_)] *)  
 
 let rec update_args sp vl = function  
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 6ce52c055f..abec7a65dc 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -31,6 +31,8 @@ val anonym_lams : ml_ast -> int -> ml_ast
 (*s Utility functions over ML types. [update_args sp vl t] puts [vl]
    as arguments behind every inductive types [(sp,_)]. *)
 
+val get_tvars : ml_type -> identifier list
+
 val update_args : section_path -> ml_type list -> ml_type -> ml_type
 
 val clear_singletons : unit -> unit
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index da562ab52e..c191317578 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -93,6 +93,10 @@ let rec rename_vars avoid = function
       let (idl', avoid') = rename_vars (Idset.add id' avoid) idl in
       (id' :: idl', avoid')
 
+let rename_tvars avoid l = 
+  let l',_ = rename_vars avoid l in 
+  l', List.fold_left2 (fun m i i' -> Idmap.add i i' m) Idmap.empty l l'
+
 let push_vars ids (db,avoid) =
   let ids',avoid' = rename_vars avoid ids in
   ids', (ids' @ db, avoid')
@@ -123,19 +127,18 @@ let preamble _ =
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_type_global = P.pp_type_global 
-let pp_global = P.pp_global
-let rename_global = P.rename_global
+let pp_type_global r = P.pp_global r false
+let pp_global r = P.pp_global r false
+let rename_global r = P.rename_global r false 
 
 let empty_env () = [], P.globals()
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let rec pp_type par t =
+let rec pp_type par ren t =
   let rec pp_rec par = function
-    | Tvar id -> 
-	pp_tvar id
+    | Tvar id -> pp_tvar (try Idmap.find id ren with _ -> id)
     | Tapp l ->
 	(match collapse_type_app l with
 	   | [] -> assert false
@@ -146,14 +149,10 @@ let rec pp_type par t =
     | Tarr (t1,t2) ->
 	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
 	   pp_rec false t2 ++ close_par par)
-    | Tglob r -> 
-	pp_type_global r
-    | Texn s -> 
-	str ("unit (* " ^ s ^ " *)")
-    | Tprop ->
-	str "prop"
-    | Tarity ->
-	str "arity"
+    | Tglob r -> pp_type_global r
+    | Texn s -> str ("unit (* " ^ s ^ " *)")
+    | Tprop -> str "prop"
+    | Tarity -> str "arity"
   in 
   hov 0 (pp_rec par t)
 
@@ -252,8 +251,10 @@ let rec pp_expr par env args =
     | MLarity ->
 	assert (args=[]); str "arity"
     | MLcast (a,t) ->
+	let tvars = get_tvars t in 
+	let _,ren = rename_tvars keywords tvars in 
 	(open_par true ++ pp_expr false env args a ++ spc () ++ str ":" ++ 
-	 spc () ++ pp_type false t ++ close_par true)
+	 spc () ++ pp_type false ren t ++ close_par true)
     | MLmagic a ->
 	(open_par true ++ str "Obj.magic" ++ spc () ++ 
 	 pp_expr false env args a ++ close_par true)
@@ -327,13 +328,14 @@ let pp_parameters l =
   (pp_tuple pp_tvar l ++ space_if (l<>[]))
 
 let pp_one_ind prefix (pl,name,cl) =
+  let pl,ren = rename_tvars keywords pl in 
   let pp_constructor (id,l) =
     (pp_global id ++
        match l with
          | [] -> (mt ()) 
 	 | _  -> (str " of " ++
       	       	    prlist_with_sep 
-		      (fun () -> (spc () ++ str "* ")) (pp_type true) l))
+		      (fun () -> (spc () ++ str "* ")) (pp_type true ren) l))
   in
   (pp_parameters pl ++ str prefix ++ pp_type_global name ++ str " =" ++ 
      (fnl () ++
@@ -347,6 +349,7 @@ let pp_ind il =
    ++ fnl ())
 
 let pp_coind_preamble (pl,name,_) = 
+  let pl,_ = rename_tvars keywords pl in
   (pp_parameters pl ++ pp_type_global name ++ str " = " ++ 
     pp_parameters pl ++ str "__" ++ pp_type_global name ++ str " Lazy.t")
 
@@ -374,9 +377,10 @@ let pp_decl = function
       end else 
 	hov 0 (pp_ind i)
   | Dabbrev (r, l, t) ->
+      let l,ren = rename_tvars keywords l in 
       hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
 	       pp_type_global r ++ spc () ++ str "=" ++ spc () ++ 
-	       pp_type false  t ++ fnl ())
+	       pp_type false ren t ++ fnl ())
   | Dglob (r, MLfix (_,[|_|],[|def|])) ->
       let id = rename_global r in
       let env' = [id], P.globals() in
@@ -388,7 +392,7 @@ let pp_decl = function
       hov 0 (str "let " ++ pp_global r ++ 
 	       str " =" ++ spc () ++ str s ++ fnl ())
 
-let pp_type = pp_type false
+let pp_type = pp_type false Idmap.empty
 
 end
 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 6cabfb7b7b..6a797d15b6 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -35,6 +35,8 @@ val uppercase_id : identifier -> identifier
 type env = identifier list * Idset.t
 
 val rename_vars: Idset.t -> identifier list -> env
+val rename_tvars: 
+  Idset.t -> identifier list -> identifier list * identifier Idmap.t
 val push_vars : identifier list -> env -> identifier list * env
 val get_db_name : int -> env -> identifier