Prise en compte des noms qualifiés dans certaines commandes

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

5 files changed, 71 insertions, 54 deletions

diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 7300f126b..e59e37e64 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -19,7 +19,7 @@ open Printer
 let print_basename sp =
   let (_,id,k) = repr_path sp in
   try 
-    if sp = Nametab.sp_of_id k id then 
+    if is_visible sp id then 
       string_of_id id
     else 
       (string_of_id id)^"."^(string_of_kind k)
@@ -27,18 +27,6 @@ let print_basename sp =
     warning "Undeclared constants in print_name";
     string_of_path sp
 
-(*
-let print_basename_mind sp mindid =
-  let (_,id,k) = repr_path sp in
-  try 
-    if sp = Nametab.sp_of_id k id then  
-      string_of_id mindid
-    else 
-      (string_of_id mindid)^"."^(string_of_kind k)
-  with Not_found ->
-    warning "Undeclared constants in print_name";
-    string_of_path_mind sp mindid
-*)
 let print_closed_sections = ref false
 
 let print_typed_value_in_env env (trm,typ) =
@@ -186,8 +174,8 @@ let print_mutual sp mib =
              implicit_args_msg sp mipv >])
 
 let print_section_variable sp =
-  let ((id,_,_) as d,_,_) = get_variable sp in
-  let l = implicits_of_var id in
+  let (d,_,_) = get_variable sp in
+  let l = implicits_of_var sp in
   [< print_named_decl d; print_impl_args l; 'fNL >]
 
 let print_body = function
@@ -228,6 +216,15 @@ let print_inductive sp =
     hOV 0 [< 'sTR"Fw inductive definition "; 
 	     'sTR (print_basename sp); 'fNL >]
 
+let print_syntactic_def with_values sep sp =
+  let id = basename sp in
+  [< 'sTR" Syntax Macro "; 
+     print_id id ; 'sTR sep;  
+     if with_values then 
+       let c = Syntax_def.search_syntactic_definition sp in 
+       [< pr_rawterm c >]
+     else [<>]; 'fNL >]
+
 let print_leaf_entry with_values sep (sp,lobj) =
   let tag = object_tag lobj in
   match (sp,tag) with
@@ -242,13 +239,7 @@ let print_leaf_entry with_values sep (sp,lobj) =
     | (_,"GRAMMAR") -> 
 	[< 'sTR" Grammar Marker"; 'fNL >]
     | (_,"SYNTAXCONSTANT") -> 
-	let id = basename sp in
-        [< 'sTR" Syntax Macro "; 
-      	   print_id id ; 'sTR sep;  
-           if with_values then 
-             let c = Syntax_def.search_syntactic_definition id in 
-	     [< pr_rawterm c >]
-           else [<>]; 'fNL >]
+	print_syntactic_def with_values sep sp
     | (_,"PPSYNTAX") -> 
 	[< 'sTR" Syntax Marker"; 'fNL >]
     | (_,"TOKEN") -> 
@@ -268,8 +259,9 @@ let rec print_library_entry with_values ent =
 	[< print_leaf_entry with_values sep (sp,lobj) >]
     | (_,Lib.OpenedSection str) -> 
         [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >]
-    | (_,Lib.ClosedSection (str,_)) -> 
-        [< 'sTR(" >>>>>>> Closed Section " ^ str); 'fNL >]
+    | (sp,Lib.ClosedSection _) -> 
+        [< 'sTR(" >>>>>>> Closed Section " ^ (string_of_id (basename sp)));
+	   'fNL >]
     | (_,Lib.Module str) ->
 	[< 'sTR(" >>>>>>> Module " ^ str); 'fNL >]
     | (_,Lib.FrozenState _) ->
@@ -321,10 +313,10 @@ let print_constructors fn env_ar mip =
     mip.mind_consnames (mind_user_lc mip)
   in ()
 
-let crible (fn : string -> env -> constr -> unit) name =
+let crible (fn : string -> env -> constr -> unit) ref =
   let env = Global.env () in
   let imported = Library.opened_modules() in
-  let const = global_reference CCI name in 
+  let const = constr_of_reference Evd.empty env ref in 
   let rec crible_rec = function
     | (spopt,Lib.Leaf lobj)::rest ->
 	(match (spopt,object_tag lobj) with
@@ -364,12 +356,13 @@ let crible (fn : string -> env -> constr -> unit) name =
   try 
     crible_rec (Lib.contents_after None)
   with Not_found -> 
-    error ((string_of_id name) ^ " not declared")
+    errorlabstrm "search"
+      [< pr_global_reference env ref; 'sPC; 'sTR "not declared" >]
 
-let print_crible name =
+let search_by_head ref =
   crible (fun str ass_name constr -> 
             let pc = prterm_env ass_name constr in
-            mSG[<'sTR str; 'sTR":"; pc; 'fNL >]) name
+            mSG[<'sTR str; 'sTR":"; pc; 'fNL >]) ref
 
 let read_sec_context sec =
   let rec get_cxt in_cxt = function
@@ -414,13 +407,18 @@ let print_name name =
       | ConstRef sp -> print_constant true " = " sp
       | IndRef (sp,_) -> print_inductive sp
       | ConstructRef ((sp,_),_) -> print_inductive sp
+      | VarRef sp -> print_section_variable sp
+      | EvarRef n -> [< 'sTR "?"; 'iNT n; 'fNL >]
   with Not_found -> 
-  try
+  try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let (c,typ) = Global.lookup_named name in 
-    [< print_named_decl (name,c,typ);
-       try print_impl_args (implicits_of_var name)
-       with _ -> [<>] >]
-  with Not_found -> error (str ^ " not a defined object")
+    [< print_named_decl (name,c,typ) >]
+  with Not_found ->
+  try
+    let sp = Syntax_def.locate_syntactic_definition (make_path [] name CCI) in
+    print_syntactic_def true " = " sp
+  with Not_found ->
+    error (str ^ " not a defined object")
 
 let print_opaque_name name = 
   let sigma = Evd.empty in
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index 811e663de..946965c6d 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -22,7 +22,6 @@ val print_context : bool -> Lib.library_segment -> std_ppcmds
 val print_library_entry : bool -> (section_path * Lib.node) -> std_ppcmds
 val print_full_context : unit -> std_ppcmds
 val print_full_context_typ : unit -> std_ppcmds
-val print_crible : identifier -> unit
 val print_sec_context : string -> std_ppcmds
 val print_sec_context_typ : string -> std_ppcmds
 val print_val : env -> unsafe_judgment -> std_ppcmds
@@ -48,7 +47,8 @@ val print_coercions : unit -> std_ppcmds
 val print_path_between : identifier -> identifier -> std_ppcmds
 
 
-val crible : (string -> env -> constr -> unit) -> identifier ->
+val search_by_head : global_reference -> unit
+val crible : (string -> env -> constr -> unit) -> global_reference ->
   unit
 val inspect : int -> std_ppcmds
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7f584a4b9..780ef6dc3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -112,11 +112,18 @@ let locate_file f =
     mSG (hOV 0 [< 'sTR"Can't find file"; 'sPC; 'sTR f; 'sPC;
 		  'sTR"on loadpath"; 'fNL >])
 
-let locate_id id =
+let locate_sp sp =
   try
-    mSG [< 'sTR (string_of_path (Nametab.sp_of_id CCI id)); 'fNL >]
+    let ref = Nametab.locate sp in
+    mSG
+      [< 'sTR (string_of_path (sp_of_global (Global.env()) ref)); 'fNL >]
   with Not_found -> 
-    error ((string_of_id id) ^ " not a defined object")
+  try
+    mSG
+      [< 'sTR (string_of_path (Syntax_def.locate_syntactic_definition sp));
+	 'fNL >]
+  with Not_found ->
+    error ((string_of_path sp) ^ " not a defined object")
 
 let print_loadpath () =
   let l = get_load_path () in
@@ -150,7 +157,7 @@ let _ =
 let _ = 
   add "Locate"
     (function 
-       | [VARG_IDENTIFIER id] -> (fun () -> locate_id id)
+       | [VARG_QUALID sp] -> (fun () -> locate_sp sp)
        | _  -> bad_vernac_args "Locate")
 
 (* For compatibility *)
@@ -282,9 +289,9 @@ let _ =
   add "WriteModule"
     (function 
        | [VARG_IDENTIFIER id] ->
-	   fun () -> let m = string_of_id id in Library.save_module_to m m
+	   fun () -> let m = string_of_id id in Discharge.save_module_to m m
        | [VARG_IDENTIFIER id; VARG_STRING f] ->
-	   fun () -> Library.save_module_to (string_of_id id) f
+	   fun () -> Discharge.save_module_to (string_of_id id) f
        | _ -> bad_vernac_args "WriteModule")
 
 let _ =
@@ -465,8 +472,7 @@ let _ =
     (fun id_list () ->
        List.iter 
 	 (function 
-	    | VARG_IDENTIFIER id -> 
-		let sp = Nametab.sp_of_id CCI id in Global.set_transparent sp
+	    | VARG_CONSTANT sp -> Global.set_transparent sp
 	    |   _  -> bad_vernac_args "TRANSPARENT")
 	 id_list)
     
@@ -475,8 +481,7 @@ let _ =
     (fun id_list () ->
        List.iter
 	 (function 
-	    | VARG_IDENTIFIER id -> 
-		let sp = Nametab.sp_of_id CCI id in Global.set_opaque sp
+	    | VARG_CONSTANT sp -> Global.set_opaque sp
 	    |   _  -> bad_vernac_args "OPAQUE")
 	 id_list)
 
@@ -864,7 +869,13 @@ let _ =
 let _ =
   add "SEARCH"
     (function 
-       | [VARG_IDENTIFIER id] -> (fun () -> print_crible id)
+       | [VARG_QUALID q] ->
+	   (fun () ->
+	      let ref =
+		try Nametab.locate q
+		with Not_found ->
+		  Pretype_errors.error_global_not_found_loc loc q
+	      in search_by_head ref)
        | _ -> bad_vernac_args "SEARCH")
 
 let _ =
@@ -1230,20 +1241,17 @@ let _ =
 let _ =
   add "INFIX"
     (function
-       | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING inf; 
-          VARG_IDENTIFIER pref] ->
+       | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING inf; VARG_QUALID pref] ->
            (fun () ->
-              Metasyntax.add_infix
-               	(Extend.gram_assoc assoc) n inf (string_of_id pref))
+	      Metasyntax.add_infix (Extend.gram_assoc assoc) n inf pref)
        | _ -> bad_vernac_args "INFIX")
 
 let _ =
   add "DISTFIX"
     (function
-       | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING s; VARG_IDENTIFIER f] ->
+       | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING s; VARG_QUALID pref] ->
            (fun () ->
-              Metasyntax.add_distfix
-               	(Extend.gram_assoc assoc) n s (string_of_id f))
+              Metasyntax.add_distfix (Extend.gram_assoc assoc) n s pref)
        | _ -> bad_vernac_args "DISTFIX")
 
 let _ =
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 602818ccd..fd41ae5d2 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -24,6 +24,8 @@ type vernac_arg =
   | VARG_NUMBER of int
   | VARG_NUMBERLIST of int list
   | VARG_IDENTIFIER of identifier
+  | VARG_QUALID of section_path
+  | VARG_CONSTANT of constant_path
   | VCALL of string * vernac_arg list
   | VARG_CONSTR of Coqast.t
   | VARG_CONSTRLIST of Coqast.t list
@@ -77,6 +79,13 @@ let rec cvt_varg ast =
         VCALL (na,List.map cvt_varg l)
 
     | Nvar(_,s) -> VARG_IDENTIFIER (id_of_string s)
+    | Node(loc,"QUALIDARG",p) -> VARG_QUALID (Astterm.interp_qualid p)
+    | Node(loc,"QUALIDCONSTARG",p) ->
+	let q = Astterm.interp_qualid p in
+	let sp =
+	  try Nametab.locate_constant q
+	  with Not_found -> Pretype_errors.error_global_not_found_loc loc q
+	in VARG_CONSTANT sp
     | Str(_,s) -> VARG_STRING s
     | Num(_,n) -> VARG_NUMBER n
     | Node(_,"NONE",[]) -> VARG_UNIT
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 0a5ccb9aa..a83e452eb 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -20,6 +20,8 @@ type vernac_arg =
   | VARG_NUMBER of int
   | VARG_NUMBERLIST of int list
   | VARG_IDENTIFIER of identifier
+  | VARG_QUALID of section_path
+  | VARG_CONSTANT of constant_path
   | VCALL of string * vernac_arg list
   | VARG_CONSTR of Coqast.t
   | VARG_CONSTRLIST of Coqast.t list