2 bugs: 1) projections pas renommées 2) mutual fixpoints a l'envers

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

3 files changed, 25 insertions, 18 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index abe2394148..811591bd8b 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -35,15 +35,15 @@ end
 
 type updown = { mutable up : Orefset.t ; mutable down : Orefset.t }
 
-let add_down r o = o.down <- Orefset.add r o.down
-let add_up r o = o.up <- Orefset.add r o.up
-let lang_add_type r o = if lang () = Haskell then add_up r o else add_down r o
+let add_down o r = o.down <- Orefset.add r o.down
+let add_up o r = o.up <- Orefset.add r o.up
+let lang_add_type o r = if lang () = Haskell then add_up o r else add_down o r
 
 (*s Get all references used in one [ml_decl] list. *)
 
 let mltype_get_references o t = 
   let rec get_rec = function 
-    | Tglob (r,l) -> lang_add_type r o; List.iter get_rec l 
+    | Tglob (r,l) -> lang_add_type o r; List.iter get_rec l 
     | Tarr (a,b) -> get_rec a; get_rec b 
     | _ -> () 
   in get_rec t
@@ -52,31 +52,38 @@ let ast_get_references o a =
   let rec get_rec a =
     ast_iter get_rec a;
     match a with 
-      | MLglob r -> add_down r o
-      | MLcons (r,_) -> add_up r o
-      | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> add_up r o) v
+      | MLglob r -> add_down o r
+      | MLcons (r,_) -> add_up o r
+      | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> add_up o r) v
       | MLcast (_,t) -> mltype_get_references o t 
       | _ -> ()
   in get_rec a
 
+let ip_of_indref = function 
+  | IndRef ip -> ip 
+  | _ -> assert false
+
 let decl_get_references ld = 
   let o = { up = Orefset.empty ; down = Orefset.empty } in 
   let one_decl = function 
     | Dind (l,_) -> 
 	List.iter (fun (_,r,l) -> 
-		     lang_add_type r o; 
+		     lang_add_type o r; 
+		     (try 
+			List.iter (add_down o) (find_proj (ip_of_indref r))
+		      with Not_found -> ()); 
 		     List.iter (fun (r,l) -> 
-				  add_up r o; 
+				  add_up o r; 
 				  List.iter (mltype_get_references o) l) l) l
-    | Dtype (r,_,t) -> lang_add_type r o; mltype_get_references o t 
+    | Dtype (r,_,t) -> lang_add_type o r; mltype_get_references o t 
     | Dterm (r,a,t) -> 
-	add_down r o; ast_get_references o a; mltype_get_references o t
+	add_down o r; ast_get_references o a; mltype_get_references o t
     | Dfix(rv,c,t) -> 
-	Array.iter (fun r -> add_down r o) rv; 
+	Array.iter (add_down o) rv; 
 	Array.iter (ast_get_references o) c; 
 	Array.iter (mltype_get_references o) t
-    | DcustomTerm (r,_) -> add_down r o
-    | DcustomType (r,_) -> lang_add_type r o
+    | DcustomTerm (r,_) -> add_down o r
+    | DcustomType (r,_) -> lang_add_type o r
   in 
   List.iter one_decl ld; 
   o
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 2a80227f1f..e197515f0c 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -1199,7 +1199,7 @@ and optimize_Dfix prm (r,t,typ) b l =
 		 with Not_found -> Tunknown) v 
 	    in 
 	    let c = 
-	      let gv = Array.map (fun r -> MLglob r) v in 
+	      let gv = Array.init len (fun i -> MLglob v.(len-i-1)) in 
 	      Array.map (gen_subst gv (-len)) c in 
 	    Dfix (v, c, typs) :: (optimize prm l)
 	  else optimize prm l 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 55e53acfa2..7ed6b66eea 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -214,7 +214,7 @@ let rec pp_expr par env args =
     | MLcons (r,args') -> 
 	(try 
 	   let projs = find_proj (kn_of_r r, 0) in 
-	   pp_record (projs, List.map (pp_expr true env []) args')
+	   pp_record_pat (projs, List.map (pp_expr true env []) args')
 	 with Not_found ->
 	   assert (args=[]);
 	   let tuple = pp_tuple (pp_expr true env []) args' in 
@@ -260,7 +260,7 @@ let rec pp_expr par env args =
     | MLmagic a ->
 	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args) 
 	  
-and pp_record (projs, args) =
+and pp_record_pat (projs, args) =
    str "{ " ++
    prlist_with_sep (fun () -> str ";" ++ spc ()) 
      (fun (r,a) -> pp_global r ++ str " =" ++ spc () ++ a)
@@ -272,7 +272,7 @@ and pp_one_pat env (r,ids,t) =
   let expr = pp_expr (expr_needs_par t) env' [] t in 
   try 
     let projs = find_proj (kn_of_r r,0) in 
-    pp_record (projs, List.rev_map pr_id ids), expr
+    pp_record_pat (projs, List.rev_map pr_id ids), expr
   with Not_found -> 
     let args = 
       if ids = [] then (mt ())