warning message when a qualid to extract can be both a module or a cst

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

4 files changed, 77 insertions, 55 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 2be509954..9a06ed49e 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -255,7 +255,7 @@ let rec record_contents_fstlev struc =
   let addterm mp id = add_ext_mpmem Term mp (modular_rename false id) in
   let addmod mp id = add_ext_mpmem Mod mp (modular_rename true id) in 
   let addfix mp r = 
-    add_ext_mpmem Term mp (modular_rename false (id_of_global r))
+    add_ext_mpmem Term mp (modular_rename false (safe_id_of_global r))
   in
   let f mp = function 
     | (l,SEdecl (Dind (_,ind))) -> 
@@ -327,7 +327,7 @@ let create_modular_renamings struc =
   let add upper r = 
     let mp = modpath_of_r r in 
     let l = mp_create_renaming mp in 
-    let s = modular_rename upper (id_of_global r) in 
+    let s = modular_rename upper (safe_id_of_global r) in 
     add_global_ids (id_of_string s);
     add_renaming r (s::l); 
     begin try 
@@ -378,8 +378,8 @@ let create_mono_renamings struc =
     let mycase = if upper then uppercase_id else lowercase_id in 
     let id = 
       if l = [""] then 
-	next_ident_away (mycase (id_of_global r)) (global_ids_list ())
-      else id_of_string (modular_rename upper (id_of_global r))
+	next_ident_away (mycase (safe_id_of_global r)) (global_ids_list ())
+      else id_of_string (modular_rename upper (safe_id_of_global r))
     in 
     add_global_ids id; 
     add_renaming r ((string_of_id id)::l) 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index a1c3331c6..8eb7a6b4a 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -427,51 +427,55 @@ let init modular =
   reset ();
   if modular && lang () = Scheme then error_scheme ()
 
+(* From a list of [reference], let's retrieve whether they correspond
+   to modules or [global_reference]. Warn the user if both is possible. *)
+
+let rec locate_ref = function
+  | [] -> [],[]
+  | r::l ->
+      let q = snd (qualid_of_reference r) in
+      let mpo = try Some (Nametab.locate_module q) with Not_found -> None
+      and ro = try Some (Nametab.locate q) with Not_found -> None in
+      match mpo, ro with
+	| None, None -> Nametab.error_global_not_found q
+	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
+	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
+	| Some mp, Some r ->
+	    warning_both_mod_and_cst q mp r;
+	    let refs,mps = locate_ref l in refs,mp::mps
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when
     extracting to a file with the command:
     \verb!Extraction "file"! [qualid1] ... [qualidn]. *)
 
-let full_extraction f qualids =
+let full_extr f (refs,mps) =
   init false;
-  let rec find = function
-    | [] -> [],[]
-    | q::l ->
-	let refs,mps = find l in
-	try
-	  let mp = Nametab.locate_module (snd (qualid_of_reference q)) in
-	  if is_modfile mp then error_MPfile_as_mod mp true;
-	  refs,(mp::mps)
-	with Not_found -> (Nametab.global q)::refs, mps
-  in
-  let refs,mps = find qualids in
+  List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
   let struc = optimize_struct refs (mono_environment refs mps) in
   warning_axioms ();
   print_structure_to_file (mono_filename f) struc;
   reset ()
 
+let full_extraction f lr = full_extr f (locate_ref lr)
 
 (*s Simple extraction in the Coq toplevel. The vernacular command
     is \verb!Extraction! [qualid]. *)
 
-let simple_extraction qid =
-  init false;
-  try
-    let mp = Nametab.locate_module (snd (qualid_of_reference qid)) in
-    if is_modfile mp then error_MPfile_as_mod mp true;
-    full_extraction None [qid]
-  with Not_found ->
-    let r = Nametab.global qid in
-    if is_custom r then
-      msgnl (str "User defined extraction:" ++ spc () ++
-	       str (find_custom r) ++ fnl ())
-    else
-      let struc = optimize_struct [r] (mono_environment [r] []) in
-      let d = get_decl_in_structure r struc in
-      warning_axioms ();
-      print_one_decl struc (modpath_of_r r) d;
-      reset ()
+let simple_extraction r = match locate_ref [r] with
+  | ([], [mp]) as p -> full_extr None p
+  | [r],[] ->
+      init false;
+      if is_custom r then
+	msgnl (str "User defined extraction:" ++ spc () ++
+		 str (find_custom r) ++ fnl ())
+      else
+	let struc = optimize_struct [r] (mono_environment [r] []) in
+	let d = get_decl_in_structure r struc in
+	warning_axioms ();
+	print_one_decl struc (modpath_of_r r) d;
+	reset ()
+  | _ -> assert false
 
 
 (*s (Recursive) Extraction of a library. The vernacular command is
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 5bfc3688f..289074b62 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -197,27 +197,33 @@ let reset_tables () =
    WARNING: for inductive objects, an extract_inductive must have been 
    done before. *)
 
-let id_of_global = function 
+let safe_id_of_global = function 
   | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
   | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
   | ConstructRef ((kn,i),j) -> 
       (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
   | _ -> assert false
 
-let pr_global r = 
- try Printer.pr_global r 
- with _ -> pr_id (id_of_global r)
+let safe_pr_global r =
+ try Printer.pr_global r
+ with _ -> pr_id (safe_id_of_global r)
 
 (* idem, but with qualification, and only for constants. *)
 
-let pr_long_global r = 
-  try Printer.pr_global r 
+let safe_pr_long_global r =
+  try Printer.pr_global r
   with _ -> match r with
-    | ConstRef kn -> 
-	let mp,_,l = repr_con kn in 
+    | ConstRef kn ->
+	let mp,_,l = repr_con kn in
 	str ((string_of_mp mp)^"."^(string_of_label l))
     | _ -> assert false
 
+let pr_long_mp mp =
+  let lid = repr_dirpath (Nametab.dir_of_mp mp) in
+  str (String.concat "." (List.map string_of_id (List.rev lid)))
+
+let pr_long_global ref = pr_sp (Nametab.sp_of_global ref)
+
 (*S Warning and Error messages. *)
 
 let err s = errorlabstrm "Extraction" s
@@ -229,7 +235,7 @@ let warning_axioms () =
     let s = if List.length info_axioms = 1 then "axiom" else "axioms" in 
     msg_warning 
       (str ("The following "^s^" must be realized in the extracted code:")
-       ++ hov 1 (spc () ++ prlist_with_sep spc pr_global info_axioms) 
+       ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
        ++ str "." ++ fnl ())
   end;
   let log_axioms = Refset.elements !log_axioms in 
@@ -239,15 +245,27 @@ let warning_axioms () =
     in 
     msg_warning
       (str ("The following logical "^s^" encountered:") ++
-       hov 1 (spc () ++ prlist_with_sep spc pr_global log_axioms ++ str ".\n") ++
+       hov 1
+         (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
+       ++
        str "Having invalid logical axiom in the environment when extracting" ++
        spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
        fnl ())
   end
 
+let warning_both_mod_and_cst q mp r =
+ msg_warning
+   (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
+    str "do you mean module " ++
+    pr_long_mp mp ++
+    str " or object " ++
+    pr_long_global r ++ str " ?" ++ fnl () ++
+    str "First choice is assumed, for the second one please use " ++
+    str "fully qualified name." ++ fnl ())
+
 let error_axiom_scheme r i = 
   err (str "The type scheme axiom " ++ spc () ++
-       pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
+       safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
        str " type variable(s).") 
 
 let check_inside_module () = 
@@ -265,10 +283,10 @@ let check_inside_section () =
 	 str "Close it and try again.")
 
 let error_constant r = 
-  err (pr_global r ++ str " is not a constant.") 
+  err (safe_pr_global r ++ str " is not a constant.") 
 
 let error_inductive r = 
-  err (pr_global r ++ spc () ++ str "is not an inductive type.")
+  err (safe_pr_global r ++ spc () ++ str "is not an inductive type.")
 
 let error_nb_cons () = 
   err (str "Not the right number of constructors.")
@@ -284,7 +302,7 @@ let error_scheme () =
   err (str "No Scheme modular extraction available yet.")
 
 let error_not_visible r = 
-  err (pr_global r ++ str " is not directly visible.\n" ++
+  err (safe_pr_global r ++ str " is not directly visible.\n" ++
        str "For example, it may be inside an applied functor." ++
        str "Use Recursive Extraction to get the whole environment.")
 
@@ -296,9 +314,9 @@ let error_MPfile_as_mod mp b =
 	    "Monolithic Extraction cannot deal with this situation.\n"^
 	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
-let error_record r = 
-  err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++
-       str "To help extraction, please use an explicit name.") 
+let error_record r =
+  err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
+       fnl () ++ str "To help extraction, please use an explicit name.")
 
 let check_loaded_modfile mp = match base_mp mp with 
   | MPfile dp -> if not (Library.library_is_loaded dp) then 
@@ -481,11 +499,11 @@ let print_extraction_inline () =
     (str "Extraction Inline:" ++ fnl () ++ 
      Refset.fold
        (fun r p -> 
-	  (p ++ str "  " ++ pr_long_global r ++ fnl ())) i' (mt ()) ++
+	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
      str "Extraction NoInline:" ++ fnl () ++ 
      Refset.fold
        (fun r p -> 
-	  (p ++ str "  " ++ pr_long_global r ++ fnl ())) n (mt ()))
+	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
 
 (* Reset part *)
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index c65c2edfe..628e035bb 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -13,13 +13,13 @@ open Libnames
 open Miniml
 open Declarations
 
-val id_of_global : global_reference -> identifier
-val pr_long_global : global_reference -> Pp.std_ppcmds
-
+val safe_id_of_global : global_reference -> identifier
 
 (*s Warning and Error messages. *)
 
 val warning_axioms : unit -> unit
+val warning_both_mod_and_cst :
+ qualid -> module_path -> global_reference -> unit
 val error_axiom_scheme : global_reference -> int -> 'a
 val error_constant : global_reference -> 'a
 val error_inductive : global_reference -> 'a