changement type_var et signature

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

9 files changed, 269 insertions, 129 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 2b50f00267..7a0ecd887c 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -12,4 +12,6 @@ Grammar vernac vernac : ast :=
   extr_constr [ "Extraction" constrarg($c) "." ] -> 
               [(Extraction $c)]
 | extr_list   [ "Extraction" "-r" ne_qualidarg_list($l) "." ] ->
-              [(ExtractionList ($LIST $l))].
+              [(ExtractionRec ($LIST $l))]
+| extr_list   [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] ->
+              [(ExtractionFile $f ($LIST $l))].
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 4fc2dc79f4..3cfee3a9bb 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -127,6 +127,7 @@ let extract_env rl =
 (*s Registration of vernac commands for extraction. *)
 
 module ToplevelParams = struct
+  let rename_global r = Names.id_of_string (Global.string_of_global r)
   let pp_type_global = Printer.pr_global
   let pp_global = Printer.pr_global
 end
@@ -164,9 +165,19 @@ let reference_of_varg = function
   | VARG_QUALID q -> Nametab.locate q
   | _ -> assert false
 
+let decl_of_vargl vl =
+  let rl = List.map reference_of_varg vl in
+  List.map extract_declaration (extract_env rl)
+
 let _ = 
-  vinterp_add "ExtractionList"
+  vinterp_add "ExtractionRec"
     (fun vl () ->
-       let rl = List.map reference_of_varg vl in
-       let rl' = extract_env rl in
-       List.iter (fun r -> mSGNL (pp_decl (extract_declaration r))) rl')
+       let rl' = decl_of_vargl vl in
+       List.iter (fun d -> mSGNL (pp_decl d)) rl')
+
+let _ = 
+  vinterp_add "ExtractionFile"
+    (function 
+       | VARG_STRING f :: vl ->
+	   (fun () -> Ocaml.extract_to_file f (decl_of_vargl vl))
+       | _ -> assert false)
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index 041bb44ca9..ba083df77a 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -1,4 +1,3 @@
 
-open Term
+(*s This module declares the extraction commands. *)
 
-val extract_env : global_reference list -> global_reference list
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index d3b65e03f6..47b68c7b57 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -40,14 +40,23 @@ open Closure
    after instanciation, which is rather [Varity]
    \end{itemize} *)
 
-type type_var = Varity | Vprop | Vdefault
+type info = Logic | Info
+
+type arity = Arity | NotArity
+
+type type_var = info * arity
+
+let logic_arity = (Logic, Arity)
+let info_arity = (Info, Arity)
+let logic = (Logic, NotArity)
+let default = (Info, NotArity)
 
 type signature = (type_var * identifier) list
 
 (* When dealing with CIC contexts, we maintain corresponding contexts 
    made of [type_var] *)
 
-type extraction_context = type_var list
+type extraction_context = bool list
 
 (* The [type_extraction_result] is the result of the [extract_type] function
    that extracts a CIC object into an ML type. It is either: 
@@ -85,11 +94,6 @@ let whd_betaiotalet = clos_norm_flags (UNIFORM, red_add betaiota_red ZETA)
 
 (* Translation between [Type_extraction_result] and [type_var]. *)
 
-let v_of_t = function
-  | Tprop -> Vprop
-  | Tarity -> Varity
-  | Tmltype _ -> Vdefault
-
 type lamprod = Lam | Prod
 
 (* FIXME: to be moved somewhere else *)
@@ -104,11 +108,12 @@ let id_of_name = function
   | Anonymous -> id_of_string "x"
   | Name id   -> id
 
-(* This function [params_of_sign] extracts the type parameters ('a in Caml)
+(* This function [params_of_sign] extracts the type parameters (['a] in Caml)
    from a signature. *)
 
 let params_of_sign = 
-  List.fold_left (fun l v -> match v with Varity,id -> id :: l | _ -> l) []
+  List.fold_left 
+    (fun l v -> match v with (Info,Arity),id -> id :: l | _ -> l) []
 
 (* [get_arity c] returns [Some s] if [c] is an arity of sort [s], 
    and [None] otherwise. *)
@@ -151,10 +156,16 @@ let is_non_info_term env c =
 (* The next function transforms a type [t] into a [type_var] flag. *)
 
 let v_of_arity env t = match get_arity env t with
-  | Some (Prop Null) -> Vprop
-  | Some _ -> Varity 
-  | _ -> if (is_non_info_type env t) then Vprop else Vdefault
+  | Some (Prop Null) -> logic_arity
+  | Some _ -> info_arity
+  | _ -> if is_non_info_type env t then logic else default
       
+let rec nb_params_to_keep env = function
+  | [] -> 0
+  | (n,t) :: l ->
+      let v = v_of_arity env t in
+      let env' = push_rel (n,None,t) env in
+      (nb_params_to_keep env' l) + (if snd v = NotArity then 1 else 0)
 
 (* The next function transforms an arity into a signature. It is used 
    for example with the types of inductive definitions, which are known
@@ -176,6 +187,7 @@ let rec signature_of_arity env c = match kind_of_term c with
    of inductive definitions. *)
 
 let rec list_of_ml_arrows = function
+  | Tarr (Miniml.Tprop, b) -> list_of_ml_arrows b
   | Tarr (a, b) -> a :: list_of_ml_arrows b
   | t -> []
 
@@ -185,9 +197,9 @@ let rec list_of_ml_arrows = function
 	
 let renum_db ctx n = 
   let rec renum = function
-    | (1, Vdefault :: _) -> 1
-    | (n, Vdefault :: s) -> succ (renum (pred n, s))
-    | (n,        _ :: s) -> renum (pred n, s)
+    | (1, true  :: _) -> 1
+    | (n, true  :: s) -> succ (renum (pred n, s))
+    | (n, false :: s) -> renum (pred n, s)
     | _ -> assert false
   in
   renum (n, ctx)
@@ -197,15 +209,16 @@ let renum_db ctx n =
 let push_many_rels env binders =  
     List.fold_left (fun e (f,t) -> push_rel (f,None,t) e) env binders
 
-let rec push_many_rels_ctx env ctx = function
+let rec push_many_rels_ctx keep_prop env ctx = function
   | (fi,ti) :: l -> 
-      push_many_rels_ctx 
-	(push_rel (fi,None,ti) env) ((v_of_arity env ti)::ctx) l
+      let v = v_of_arity env ti in
+      let keep = (v = default) || (keep_prop && v = logic) in
+      push_many_rels_ctx keep_prop (push_rel (fi,None,ti) env) (keep :: ctx) l
   | [] ->
       (env, ctx)
 
 let fix_environment env ctx fl tl =
-  push_many_rels_ctx env ctx (List.combine fl (Array.to_list tl))
+  push_many_rels_ctx true env ctx (List.combine fl (Array.to_list tl))
 
 (* Test for the application of a constructor *)
 
@@ -303,9 +316,6 @@ let rec extract_type env c =
 	  Tprop 
       | Some _ -> 
 	  (match (kind_of_term (whd_betaiotalet env Evd.empty c)) with
-	    | IsSort (Prop Null) ->
-		assert (args = []); (* A sort can't be applied. *)
-		Tprop 
 	    | IsSort _ ->
 		assert (args = []); (* A sort can't be applied. *)
 		Tarity 
@@ -364,20 +374,26 @@ let rec extract_type env c =
     let id = id_of_name n in (* FIXME: capture problem *)
     let env' = push_rel (n,None,t) env in
     let tag = v_of_arity env t in
-    if tag = Vdefault && flag = Prod then
-      (match extract_rec env fl t [] with
-	 | Tprop | Tarity -> assert false 
-	       (* Cf. relation between [extract_type] and [v_of_arity] *)
-	 | Tmltype (mlt,_,fl') -> 
-	     (match extract_rec env' fl' d [] with 
-		| Tmltype (mld, sign, fl'') -> 
-		    Tmltype (Tarr(mlt,mld), (tag,id)::sign, fl'')
-		| et -> et))
-    else
-      (match extract_rec env' fl d [] with 
-	 | Tmltype (mld, sign, fl'') ->
-	     Tmltype (mld, (tag,id)::sign, fl'')
-	 | et -> et)
+    match tag,flag with
+      | (_, Arity), _ | _, Lam ->
+	  (match extract_rec env' fl d [] with 
+	     | Tmltype (mld, sign, fl'') -> Tmltype (mld, (tag,id)::sign, fl'')
+	     | et -> et)
+      | (Logic, NotArity), Prod ->
+	  (match extract_rec env' fl d [] with 
+	     | Tmltype (mld, sign, fl'') ->
+		 Tmltype (Tarr (Miniml.Tprop, mld), (tag,id)::sign, fl'')
+	     | et -> et)
+      | (Info, NotArity), Prod ->
+	  (match extract_rec env fl t [] with
+	     | Tprop | Tarity -> 
+		assert false 
+		(* Cf. relation between [extract_type] and [v_of_arity] *)
+	     | Tmltype (mlt,_,fl') -> 
+		 (match extract_rec env' fl' d [] with 
+		    | Tmltype (mld, sign, fl'') -> 
+			Tmltype (Tarr(mlt,mld), (tag,id)::sign, fl'')
+		    | et -> et))
 
  (* Auxiliary function dealing with type application. 
     Precondition: [r] is of type an arity. *)
@@ -391,8 +407,8 @@ let rec extract_type env c =
     let (mlargs,fl') = 
       List.fold_right 
 	(fun (v,a) ((args,fl) as acc) -> match v with
-	   | (Vdefault | Vprop), _ -> acc
-	   | Varity,_ -> match extract_rec env fl a [] with
+	   | (_, NotArity), _ -> acc
+	   | (_, Arity), _ -> match extract_rec env fl a [] with
 	       | Tarity -> (Miniml.Tarity :: args, fl) 
   	         (* we pass a dummy type [arity] as argument *)
 	       | Tprop -> (Miniml.Tprop :: args, fl)
@@ -425,33 +441,40 @@ and extract_term_with_type env ctx c t =
 	let id = id_of_name n in
 	let v = v_of_arity env t in 
 	let env' = push_rel (n,None,t) env in
-	let ctx' = v :: ctx in
+	let ctx' = (snd v = NotArity) :: ctx in
 	let d' = extract_term env' ctx' d in 
 	(* If [d] was of type an arity, [c] too would be so *)
 	(match v with
-	   | Varity -> d'
-	   | Vprop | Vdefault -> match d' with
+	   | _,Arity -> d'
+	   | _,NotArity -> match d' with
 	       | Rmlterm a -> Rmlterm (MLlam (id, a))
 	       | Rprop -> assert false (* Cf. rem. above *))
     | IsRel n ->
 	(* TODO : magic or not *) 
-	(match List.nth ctx (pred n) with
-	   | Varity -> assert false (* Cf. precondition *)
-	   | Vprop -> assert false
-	   | Vdefault -> Rmlterm (MLrel (renum_db ctx n))) 
+	Rmlterm (MLrel (renum_db ctx n))
     | IsApp (f,a) ->
+	let nargs = Array.length a in
 	let tyf = Typing.type_of env Evd.empty f in
 	let tyf = 
-	  if nb_prod tyf >= Array.length a then 
+	  if nb_prod tyf >= nargs then 
 	    tyf 
 	  else 
 	    whd_betadeltaiota env Evd.empty tyf 
 	in
-	(match extract_type env tyf with
-	   | Tmltype (_,s,_) -> 
-	       extract_app env ctx (f,tyf,s) (Array.to_list a) 
-	   | Tarity -> assert false (* Cf. precondition *)
-	   | Tprop -> assert false)
+	let nbp = nb_prod tyf in
+	if nbp >= nargs then 
+	  (match extract_type env tyf with
+	     | Tmltype (_,s,_) -> 
+		 extract_app env ctx (f,tyf,s) (Array.to_list a) 
+	     | Tarity -> assert false (* Cf. precondition *)
+	     | Tprop -> assert false)
+	else begin
+	  Format.printf "%d/%d " nbp nargs; Format.print_flush ();
+	  let c' = 
+	    mkApp (mkApp (f, Array.sub a 0 nbp), Array.sub a nbp (nargs-nbp))
+	  in
+	  extract_term_with_type env ctx c' t
+	end
     | IsConst (sp,_) ->
 	Rmlterm (MLglob (ConstRef sp))
     | IsMutConstruct (cp,_) ->
@@ -460,7 +483,7 @@ and extract_term_with_type env ctx c t =
 	let rec abstract rels i = function
 	  | [] -> 
 	      MLcons (ConstructRef cp, List.length rels, List.rev rels)
-	  | (Vdefault,id) :: l -> 
+	  | ((Info,NotArity),id) :: l -> 
 	      MLlam (id, abstract (MLrel (ns - i) :: rels) (succ i) l)
 	  | (_,id) :: l ->
 	      MLlam (id, abstract rels (succ i) l)
@@ -470,7 +493,7 @@ and extract_term_with_type env ctx c t =
 	let extract_branch_aux j b = 	  
 	  let (binders,e) = decompose_lam_eta ni.(j) env b in
 	  let binders = List.rev binders in
-	  let (env',ctx') = push_many_rels_ctx env ctx binders in
+	  let (env',ctx') = push_many_rels_ctx false env ctx binders in
 	  (* Some patological cases need an [extract_constr] here 
 	     rather than an [extract_term]. See exemples in 
 	     [test_extraction.v] *)
@@ -489,7 +512,7 @@ and extract_term_with_type env ctx c t =
 	  let ids = 
 	    List.fold_right 
 	      (fun ((v,_),(n,_)) acc ->
-		 if v = Vdefault then (id_of_name n :: acc) else acc)
+		 if v = default then (id_of_name n :: acc) else acc)
 	      (List.combine s binders) []
 	  in
 	  (ConstructRef cp, ids, e')
@@ -514,18 +537,17 @@ and extract_term_with_type env ctx c t =
     | IsLetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in
 	let env' = push_rel (n,Some c1,t1) env in
-	(match get_arity env t1 with
-	   | Some (Prop Null) -> 
-	       extract_term env' (Vprop::ctx) c2
-	   | Some _ ->
-	       extract_term env' (Varity::ctx) c2
-	   | None -> 
+	let tag = v_of_arity env t1 in
+	(match tag with
+	   | (Info, NotArity) -> 
 	       let c1' = extract_term_with_type env ctx c1 t1 in
-	       let c2' = extract_term env' (Vdefault::ctx) c2 in
+	       let c2' = extract_term env' (true :: ctx) c2 in
 	       (* If [c2] was of type an arity, [c] too would be so *)
 	       (match (c1',c2') with
 		  | (Rmlterm a1,Rmlterm a2) -> Rmlterm (MLletin (id,a1,a2))
-		  | _ -> assert false (* Cf. rem. above *)))
+		  | _ -> assert false (* Cf. rem. above *))
+	   | _ ->
+	       extract_term env' (false :: ctx) c2)
     | IsCast (c, _) ->
 	extract_term_with_type env ctx c t
     | IsMutInd _ | IsProd _ | IsSort _ | IsVar _ 
@@ -539,9 +561,9 @@ and extract_app env ctx (f,tyf,sf) args =
   let mlargs = 
     List.fold_right 
       (fun (v,a) args -> match v with
-	 | Varity,_ -> args
-	 | Vprop,_ -> MLprop :: args
-	 | Vdefault,_ ->  
+	 | (_,Arity), _ -> args
+	 | (Logic,NotArity), _ -> MLprop :: args
+	 | (Info,NotArity), _ ->  
 	     (* We can't trust the tag [Vdefault], we use [extract_constr] *)
 	     match extract_constr env ctx a with 
 	       | Emltype _ -> MLarity :: args
@@ -635,13 +657,15 @@ and extract_mib sp =
 		  let t = mis_constructor_type (succ j) mis in
 		  let nparams = mis_nparams mis in 
 		  let (binders, t) = decompose_prod_n nparams t in
-		  let env = push_many_rels genv (List.rev binders) in
+		  let binders = List.rev binders in
+		  let nparams' = nb_params_to_keep genv binders in
+		  let env = push_many_rels genv binders in
 		  match extract_type env t with
 		    | Tarity | Tprop -> assert false
 		    | Tmltype (mlt, s, f) -> 
 			let l = list_of_ml_arrows mlt in
 			let cp = (ip,succ j) in
-			add_constructor_extraction cp (Cml (l,s,nparams));
+			add_constructor_extraction cp (Cml (l,s,nparams'));
 			f @ fl)
 	       ib.mind_nf_lc fl)
 	mib.mind_packets []
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index b54a7b9abb..c218f9c318 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -15,11 +15,15 @@ open Environ
 
 (*s Result of an extraction. *)
 
-type type_var = Varity | Vprop | Vdefault
+type info = Logic | Info
+
+type arity = Arity | NotArity
+
+type type_var = info * arity
 
 type signature = (type_var * identifier) list
 
-type extraction_context = type_var list
+type extraction_context = bool list
 
 type extraction_result =
   | Emltype of ml_type * signature * identifier list
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index bb11adaaba..1699486562 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -39,7 +39,7 @@ type ml_ast =
   | MLglob  of global_reference
   | MLcons  of global_reference * int * ml_ast list
   | MLcase  of ml_ast * (global_reference * identifier list * ml_ast) array
-  | MLfix   of int * (identifier list) * (ml_ast list)
+  | MLfix   of int * identifier list * ml_ast list
   | MLexn   of identifier
   | MLprop
   | MLarity
@@ -50,7 +50,7 @@ type ml_ast =
 
 type ml_decl = 
   | Dtype   of ml_ind list
-  | Dabbrev of global_reference * (identifier list) * ml_type
+  | Dabbrev of global_reference * identifier list * ml_type
   | Dglob   of global_reference * ml_ast
 
 (*s Pretty-printing of MiniML in a given concrete syntax is parameterized
@@ -59,6 +59,7 @@ type ml_decl =
     functions to print types, terms and declarations. *)
 
 module type Mlpp_param = sig
+  val rename_global : global_reference -> identifier
   val pp_type_global : global_reference -> std_ppcmds
   val pp_global : global_reference -> std_ppcmds
 end
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index ee501ba2f9..86217971f5 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -46,7 +46,58 @@ let space_if = function true -> [< 'sTR " " >] | false -> [< >]
 
 let sec_space_if = function true -> [< 'sPC >] | false -> [< >]
 
-(* collect_lambda MLlam(id1,...MLlam(idn,t)...) = [id1;...;idn],t *)
+(*s Ocaml renaming issues. *)
+
+let ocaml_keywords =     
+  List.fold_right (fun s -> Idset.add (id_of_string s))
+  [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
+    "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
+    "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
+    "inherit"; "initializer"; "lazy"; "let"; "match"; "method";
+    "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
+    "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
+    "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
+    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ] 
+  Idset.empty
+
+let current_ids = ref ocaml_keywords
+
+let rec rename_id id avoid = 
+  if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
+
+let rename_global id = 
+  let id' = rename_id id !current_ids in
+  current_ids := Idset.add id' !current_ids; 
+  id'
+
+let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
+let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
+
+let rename_lower_global id = rename_global (lowercase_id id)
+let rename_upper_global id = rename_global (uppercase_id id)
+
+(*s de Bruijn environments for programs *)
+
+type env = identifier list * Idset.t
+
+let rec rename_vars avoid = function
+  | [] -> 
+      [], avoid
+  | id :: idl ->
+      let id' = rename_id (lowercase_id id) avoid in
+      let (idl', avoid') = rename_vars (Idset.add id' avoid) idl in
+      (id' :: idl', avoid')
+
+let push_vars ids (db,avoid) =
+  let ids',avoid' = rename_vars avoid ids in
+  ids', (ids' @ db, avoid')
+
+let empty_env () = ([], !current_ids)
+
+let get_db_name n (db,_) = List.nth db (pred n)
+
+(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
+    the list [id1;...;idn] and the term [t]. *)
 
 let collect_lambda = 
   let rec collect acc = function
@@ -55,17 +106,11 @@ let collect_lambda =
   in 
   collect []
 
-let rec rename_bvars avoid = function
-  | [] -> []
-  | id :: idl ->
-      let v = next_ident_away id avoid in 
-      v :: (rename_bvars (v::avoid) idl)
-
 let abst = function
   | [] -> [< >]
-  | l  -> [< 'sTR "fun " ;
+  | l  -> [< 'sTR "fun ";
              prlist_with_sep (fun  ()-> [< 'sTR " " >]) pr_id l;
-             'sTR " ->" ; 'sPC >]
+             'sTR " ->"; 'sPC >]
 
 let pr_binding = function
   | [] -> [< >]
@@ -115,24 +160,24 @@ let rec pp_expr par env args =
   in
   function
     | MLrel n -> 
-	apply (pr_id (List.nth env (pred n)))
+	apply (pr_id (get_db_name n env))
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
     | MLlam _ as a -> 
       	let fl,a' = collect_lambda a in
-	let fl = rename_bvars env fl in
-	let st = [< abst (List.rev fl); pp_expr false (fl @ env) [] a' >] in
+	let fl,env' = push_vars fl env in
+	let st = [< abst (List.rev fl); pp_expr false env' [] a' >] in
 	if args = [] then
           [< open_par par; st; close_par par >]
         else
           apply [< 'sTR "("; st; 'sTR ")" >]
     | MLletin (id,a1,a2) ->
-	let id' = rename_bvars env [id] in
+	let id',env' = push_vars [id] env in
 	hOV 0 [< hOV 2 [< 'sTR "let "; pr_id (List.hd id'); 'sTR " ="; 'sPC;
 			  pp_expr false env [] a1; 'sPC; 'sTR "in" >];
 		 'sPC;
-		 pp_expr false (id' @ env) [] a2 >] 
+		 pp_expr false env' [] a2 >] 
     | MLglob r -> 
 	apply (P.pp_global r)
     | MLcons (r,_,[]) ->
@@ -149,8 +194,9 @@ let rec pp_expr par env args =
       	     v 0 [< 'sTR "match "; pp_expr false env [] t; 'sTR " with";
 		    'fNL; 'sTR "  "; pp_pat env pv >];
 	     if args <> [] then [< 'sTR ")" >] else close_par par >]
-    | MLfix (i,idl,al) ->
-      	pp_fix par env true (i,idl,al) args
+    | MLfix (i,ids,defs) ->
+	let ids',env' = push_vars ids env in
+      	pp_fix par env' (Some i) (ids',defs) args
     | MLexn id -> 
 	[< open_par par; 'sTR "failwith"; 'sPC; 
 	   'qS (string_of_id id); close_par par >]
@@ -167,7 +213,7 @@ let rec pp_expr par env args =
 
 and pp_pat env pv = 
   let pp_one_pat (name,ids,t) =
-    let ids = rename_bvars env ids in
+    let ids,env' = push_vars (List.rev ids) env in
     let par = match t with
       | MLlam _  -> true
       | MLcase _ -> true
@@ -176,35 +222,39 @@ and pp_pat env pv =
     hOV 2 [< P.pp_global name;
 	     begin match ids with 
 	       | [] -> [< >]
-	       | _  -> [< 'sTR " "; pp_boxed_tuple pr_id ids >]
+	       | _  -> [< 'sTR " "; pp_boxed_tuple pr_id (List.rev ids) >]
 	     end;
-	     'sTR " ->"; 'sPC; pp_expr par (List.rev ids @ env) [] t >]
+	     'sTR " ->"; 'sPC; pp_expr par env' [] t >]
   in 
   [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) pp_one_pat pv >]
 
-and pp_fix par env in_p (j,fid,bl) args =
-  let env' = (List.rev fid) @ env in
+(*s names of the functions ([ids]) are already pushed in [env],
+    and passed here just for convenience. *)
+
+and pp_fix par env in_p (ids,bl) args =
   [< open_par par; 
      v 0 [< 'sTR "let rec " ;
 	    prlist_with_sep
       	      (fun () -> [< 'fNL; 'sTR "and " >])
-	      (fun (fi,ti) -> pp_function env' (pr_id fi) ti)
-	      (List.combine fid bl) ;
-	    'fNL ;
-	    if in_p then 
-      	      hOV 2 [< 'sTR "in "; pr_id (List.nth fid j);
-                       if args <> [] then
-			 [< 'sTR " "; prlist_with_sep (fun () -> [<'sTR " ">])
-                              (fun s -> s) args >]
-                       else [< >]
-      		    >]
-	    else 
-	      [< >] >];
+	      (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+	      (List.combine ids bl);
+	    'fNL;
+	    match in_p with
+	      | Some j -> 
+      		  hOV 2 [< 'sTR "in "; pr_id (List.nth ids j);
+			   if args <> [] then
+			     [< 'sTR " "; 
+				prlist_with_sep (fun () -> [<'sTR " ">])
+				  (fun s -> s) args >]
+			   else
+			     [< >] >]
+	      | None -> 
+		  [< >] >];
      close_par par >]
 
 and pp_function env f t =
   let bl,t' = collect_lambda t in
-  let bl = rename_bvars env bl in
+  let bl,env' = push_vars bl env in
   let is_function pv =
     let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in
     not (List.exists (fun (k,t0) -> Mlutil.occurs (k+1) t0) ktl)
@@ -214,18 +264,18 @@ and pp_function env f t =
 	if is_function pv then
 	  [< f; pr_binding (List.rev (List.tl bl)) ;
        	     'sTR " = function"; 'fNL;
-	     v 0 [< 'sTR "  "; pp_pat (bl @ env) pv >] >]
+	     v 0 [< 'sTR "  "; pp_pat env' pv >] >]
 	else
           [< f; pr_binding (List.rev bl); 
              'sTR " = match ";
 	     pr_id (List.hd bl); 'sTR " with"; 'fNL;
-	     v 0 [< 'sTR "  "; pp_pat (bl @ env) pv >] >]
+	     v 0 [< 'sTR "  "; pp_pat env' pv >] >]
 	  
     | _ -> [< f; pr_binding (List.rev bl);
 	      'sTR " ="; 'fNL; 'sTR "  ";
-	      hOV 2 (pp_expr false (bl @ env) [] t') >]
+	      hOV 2 (pp_expr false env' [] t') >]
 	
-let pp_ast a = hOV 0 (pp_expr false [] [] a)
+let pp_ast a = hOV 0 (pp_expr false (empty_env ()) [] a)
 
 (*s Pretty-printing of inductive types declaration. *)
 
@@ -249,11 +299,13 @@ let pp_one_inductive (pl,name,cl) =
 let pp_inductive il =
   [< 'sTR "type " ;
      prlist_with_sep 
-       (fun () -> [< 'fNL ; 'sTR "and " >])
+       (fun () -> [< 'fNL; 'sTR "and " >])
        (fun i -> pp_one_inductive i)
        il;
      'fNL >]
 
+(*s Pretty-printing of a declaration. *)
+
 let pp_decl = function
   | Dtype [] -> 
       [< >]
@@ -262,16 +314,19 @@ let pp_decl = function
   | Dabbrev (r, l, t) ->
       hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; 
 	       P.pp_type_global r; 'sPC; 'sTR "="; 'sPC; pp_type t; 'fNL >]
-  | Dglob (r, MLfix (n,idl,l)) ->
-      let id' = List.nth idl n in
-      if true then (* TODO id = id' *)
-	[<  hOV 2 (pp_fix false [] false (n,idl,l) []) >]
-      else
-	[< 'sTR "let "; P.pp_global r; 'sTR " ="; 'fNL;
-	   v 0 [< 'sTR "  "; 
-		  hOV 2 (pp_fix false [] true (n,idl,l) []); 'fNL >] >]
+  | Dglob (r, MLfix (_,[_],[def])) ->
+      let id = P.rename_global r in
+      let env' = ([id], !current_ids) in
+      [<  hOV 2 (pp_fix false env' None ([id],[def]) []) >]
+  | Dglob (r, MLfix (n,ids,defs)) ->
+      let ids',env' = push_vars ids (empty_env ()) in
+      [< 'sTR "let "; P.pp_global r; 'sTR " ="; 'fNL;
+	 v 0 [< 'sTR "  "; 
+		hOV 2 (pp_fix false env' (Some n) (ids',defs) []); 
+		'fNL >] >]
   | Dglob (r, a) ->
-      hOV 0 [< 'sTR "let "; pp_function [] (P.pp_global r) a; 'fNL >]
+      hOV 0 [< 'sTR "let "; 
+	       pp_function (empty_env ()) (P.pp_global r) a; 'fNL >]
 
 end
 
@@ -279,12 +334,49 @@ end
 
 module OcamlParams = struct
 
-let pp_type_global r = failwith "todo" 
+let renamings = Hashtbl.create 97
 
-let pp_global r = failwith "todo"
+let cache r f = 
+  try Hashtbl.find renamings r 
+  with Not_found -> let id = f r in Hashtbl.add renamings r id; id
+
+let rename_type_global r =  
+  cache r
+    (fun r -> 
+       let id = Environ.id_of_global (Global.env()) r in
+       rename_lower_global id)
+
+let pp_type_global r = pr_id (rename_type_global r)
+
+let rename_global r = 
+  cache r
+    (fun r -> 
+       let id = Environ.id_of_global (Global.env()) r in
+       match r with
+	 | ConstructRef _ -> rename_upper_global id
+	 | _ -> rename_lower_global id)
+
+let pp_global r = pr_id (rename_global r)
 
 end
 
 (*s The ocaml pretty-printing module. *)
 
 module Pp = Make(OcamlParams)
+
+let ocaml_preamble () =
+  [< 'sTR "type prop = Prop"; 'fNL; 'fNL;
+     'sTR "type arity = Arity"; 'fNL; 'fNL >]
+
+let extract_to_file f decls =
+  let cout = open_out f in
+  let ft = Pp_control.with_output_to cout in
+  pP_with ft (hV 0 (ocaml_preamble ()));
+  begin 
+    try
+      List.iter (fun d -> mSGNL_with ft (Pp.pp_decl d)) decls
+    with e ->
+      pp_flush_with ft (); close_out cout; raise e
+  end;
+  pp_flush_with ft ();
+  close_out cout
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 6a2834bb7d..2760585d18 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -16,5 +16,6 @@ open Miniml
 
 module Make : functor(P : Mlpp_param) -> Mlpp
 
-module Pp : Mlpp
+val extract_to_file : string -> ml_decl list -> unit
+
 
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 3d3fb10e7d..251d63bba3 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -129,3 +129,9 @@ Extraction eq.
 Extraction eq_rec.
 
 (* mutual fixpoints on many sorts ? *)
+
+  (* TODO *)
+
+(* example with more arguments that given by the type *)
+
+Extraction (nat_rec [n:nat]nat->nat [n:nat]O [n:nat][f:nat->nat]f O O).