apres le backtrack precedent, remise de trois points precis et surs

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

3 files changed, 60 insertions, 27 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 0f07658fb7..45181def85 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -261,16 +261,20 @@ module StdParams = struct
     then 
       if (Refset.mem r !must_qualify) || (lang () = Haskell)
       then str (string_of_ren l s)
-      else 
-	if clash_in_contents mp s (decreasing_contents cur_mp) 
-	then str (string_of_ren l s)
-	else str s
+      else
+	try 
+	  if clash_in_contents mp s (decreasing_contents cur_mp) 
+	  then str (string_of_ren l s)
+	  else str s
+	with Not_found -> str (string_of_ren l s)
     else 
       let nl = List.length l in 
       if n = nl && nl < List.length cur_l then (* strict prefix *)
-	if clash_in_contents mp s (decreasing_contents cur_mp) 
-	then error_unqualified_name (string_of_ren l s) (string_of_modlist cur_l)
-	else str s
+	try 
+	  if clash_in_contents mp s (decreasing_contents cur_mp) 
+	  then error_unqualified_name (string_of_ren l s) (string_of_modlist cur_l)
+	  else str s
+	with Not_found -> str (string_of_ren l s)
       else (* [cur_mp] and [mp] are orthogonal *)
 	let l = remove_common cur_l l 
 	in str (string_of_ren l s)
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index ab798eebfc..51cf81c486 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -424,6 +424,30 @@ let extraction_module m =
 	let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in 
 	let l = environment_until (Some dir_m) in 
 	init_env l;
+(* TEMPORARY: make Extraction Module look like Recursive Extraction Module *)
+	let struc = 
+	  let select l (mp,meb) = 
+	        if in_mp v mp then (mp, unpack (extract_meb v true meb)) :: l else l
+	  in List.fold_left select [] (List.rev l)
+	in 
+	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
+	let struc = optimize_struct dummy_prm None struc in 
+	let rec print = function 
+	  | [] -> () 
+	  | (MPfile dir, _) :: l when dir <> dir_m -> print l 
+	  | (MPfile dir, sel) as e :: l -> 
+	      let short_m = snd (split_dirpath dir) in
+	      let f = module_file_name short_m in 
+	      let prm = {modular=true;mod_name=short_m;to_appear=[]} in
+	            print_structure_to_file (Some f) prm [e]; 
+	            print l 
+	  | _ -> assert false
+	in print struc; 
+	reset_tables ()
+
+
+
+(*i
 	let mp,meb = list_last l in 
 	let struc = [mp, unpack (extract_meb v true meb)] in 
 	let extern_decls = 
@@ -435,6 +459,7 @@ let extraction_module m =
 	let struc = optimize_struct prm (Some extern_decls) struc in 
 	print_structure_to_file (Some (module_file_name m)) prm struc; 
 	reset_tables ()
+i*)
 	  
 (*s Recursive Extraction of all the modules [M] depends on. 
   The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index b3038aa4ae..4edc851857 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -185,26 +185,30 @@ let rec extract_type env db j c args =
     | Const kn -> 
 	let kn = long_kn kn in 
 	let r = ConstRef kn in 
-	if is_custom r then Tglob (r,[])
-	else if is_axiom env kn then 
-	  (* There are two kinds of informative axioms here, *)
-	  (* - the types that should be realized via [Extract Constant] *)
-	  (* - the type schemes that are not realizable (yet). *) 
-	  (* TODO: in modular extraction, we should try not to fail here !!! *)
-	  if args = [] then Tglob (r,[]) else error_axiom_scheme r
-	else 
-	  let body = constant_value env kn in 
-	  let mlt1 = extract_type env db j (applist (body, args)) [] in 
-	  (match mlt_env env r with 
-	     | Some mlt ->
-		 if mlt = Tdummy then Tdummy
-		 else 
-		   let s = type_sign env (constant_type env kn) in 
-		   let mlt2 = extract_type_app env db (r,s) args in 
-		   (* ML type abbreviation behave badly with respect to Coq *)
-		   (* reduction. Try to find the shortest correct answer. *) 
-		   if type_eq (mlt_env env) mlt1 mlt2 then mlt2 else mlt1
-	     | None -> mlt1)
+	let cb = lookup_constant kn env in 
+	let typ = cb.const_type in 
+	(match flag_of_type env typ with 
+	   | (Info, TypeScheme) -> 
+	       let mlt = extract_type_app env db (r, type_sign env typ) args in 
+	              (match cb.const_body with 
+			 | None -> mlt
+			 | Some _ when is_custom r -> mlt 
+			 | Some lbody -> 
+			     let newc = applist (Declarations.force lbody, args) in 
+			     let mlt' = extract_type env db j newc [] in 
+			           (* ML type abbreviations interact badly with Coq *)
+			           (* reduction, so [mlt] and [mlt'] might be different: *)
+			           (* The more precise is [mlt'], extracted after reduction *)
+			           (* The shortest is [mlt], which use abbreviations *)
+			           (* If possible, we take [mlt], otherwise [mlt']. *)
+			           if type_eq (mlt_env env) mlt mlt' then mlt else mlt')
+	   | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
+	              (match cb.const_body with 
+			 | None -> Tunknown (* Brutal approximation ... *)
+			 | Some lbody -> 
+			          (* We try to reduce. *)
+			     let newc = applist (Declarations.force lbody, args) in 
+			           extract_type env db j newc []))
     | Ind ((kn,i) as ip) ->
 	let kn = long_kn kn in
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in