Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;

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

6 files changed, 38 insertions, 71 deletions

diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 6f2011eb89..0d420736a3 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -16,16 +16,7 @@ open Impargs
 open Libobject
 open Printer
 
-let print_basename sp =
-  let (_,id,k) = repr_path sp in
-  try 
-    if is_visible sp id then 
-      string_of_id id
-    else 
-      (string_of_id id)^"."^(string_of_kind k)
-  with Not_found -> 
-    warning "Undeclared constants in print_name";
-    string_of_path sp
+let print_basename sp = pr_global (ConstRef sp)
 
 let print_closed_sections = ref false
 
@@ -74,7 +65,7 @@ let implicit_args_id id l =
   if l = [] then 
     [<>]
   else 
-    [< 'sTR"For "; print_id id; 'sTR": "; print_impl_args l ; 'fNL >]
+    [< 'sTR"For "; pr_id id; 'sTR": "; print_impl_args l ; 'fNL >]
 
 let implicit_args_msg sp mipv = 
   [< prvecti
@@ -102,7 +93,7 @@ let print_mutual sp mib =
   let arities = Array.map (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mipv in
   let env_ar = push_rels lpars env in
   let pr_constructor (id,c) =
-    [< print_id id; 'sTR " : "; prterm_env env_ar c >] in
+    [< pr_id id; 'sTR " : "; prterm_env env_ar c >] in
   let print_constructors mis =
     let (_,lC) = mis_type_mconstructs mis in
     let lidC =
@@ -126,7 +117,7 @@ let print_mutual sp mib =
 		      (body_of_type (mis_user_arity mis)) in
       (hOV 0
          [< (hOV 0
-	       [< print_id (mis_typename mis) ; 'bRK(1,2); params;
+	       [< pr_id (mis_typename mis) ; 'bRK(1,2); params;
 	          'sTR ": "; prterm_env env_ar arity; 'sTR " :=" >]);
             'bRK(1,2); print_constructors mis >]) 
   in 
@@ -136,7 +127,7 @@ let print_mutual sp mib =
     let (_,arity) = decomp_n_prod env evd nparams
 		      (body_of_type (mis_user_arity mis0)) in 
     let sfinite = if mis_finite mis0 then "Inductive " else "CoInductive " in
-    (hOV 0 [< 'sTR sfinite ; print_id (mis_typename mis0);
+    (hOV 0 [< 'sTR sfinite ; pr_id (mis_typename mis0);
               if nparams = 0 then 
 		[<>] 
               else 
@@ -194,10 +185,10 @@ let print_constant with_values sep sp =
     hOV 0 [< (match val_0 with 
 		| None -> 
 		    [< 'sTR"*** [ "; 
-		       'sTR (print_basename sp);  
+		       print_basename sp;  
 		       'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >]
 		| _ -> 
-		    [< 'sTR(print_basename sp) ; 
+		    [< print_basename sp; 
 		       'sTR sep; 'cUT ;
 		       if with_values then 
 			 print_typed_body (val_0,typ) 
@@ -206,7 +197,7 @@ let print_constant with_values sep sp =
 	     print_impl_args (list_of_implicits l); 'fNL >]
   else
     hOV 0 [< 'sTR"Fw constant " ; 
-	     'sTR (print_basename sp) ; 'fNL>]
+	     print_basename sp ; 'fNL>]
 
 let print_inductive sp =
   let mib = Global.lookup_mind sp in
@@ -214,12 +205,12 @@ let print_inductive sp =
     [< print_mutual sp mib; 'fNL >]
   else
     hOV 0 [< 'sTR"Fw inductive definition "; 
-	     'sTR (print_basename sp); 'fNL >]
+	     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;  
+     pr_id id ; 'sTR sep;  
      if with_values then 
        let c = Syntax_def.search_syntactic_definition sp in 
        [< pr_rawterm c >]
@@ -309,11 +300,12 @@ let list_filter_vec f vec =
 
 let print_constructors fn env_ar mip = 
   let _ =
-    array_map2 (fun id c -> fn (string_of_id id) env_ar (body_of_type c))
+    array_map2 (fun id c -> fn (pr_id id) (* il faudrait qualifier... *)
+		    env_ar (body_of_type c))
     mip.mind_consnames (mind_user_lc mip)
   in ()
 
-let crible (fn : string -> env -> constr -> unit) ref =
+let crible (fn : std_ppcmds -> env -> constr -> unit) ref =
   let env = Global.env () in
   let imported = Library.opened_modules() in
   let const = constr_of_reference Evd.empty env ref in 
@@ -323,12 +315,12 @@ let crible (fn : string -> env -> constr -> unit) ref =
 	   | (_,"VARIABLE") ->
 	       let ((idc,_,typ),_,_) = get_variable spopt in 
                if (head_const (body_of_type typ)) = const then  
-                 fn (string_of_id idc) env (body_of_type typ);
+                 fn (pr_id idc) env (body_of_type typ);
                crible_rec rest
 	   | (sp,("CONSTANT"|"PARAMETER")) ->
 	       let {const_type=typ} = Global.lookup_constant sp in
                if (head_const (body_of_type typ)) = const then
-                 fn (print_basename sp) env (body_of_type typ);
+                 fn (pr_global (ConstRef sp)) env (body_of_type typ);
                crible_rec rest
 	   | (sp,"INDUCTIVE") -> 
                let mib = Global.lookup_mind sp in 
@@ -357,12 +349,12 @@ let crible (fn : string -> env -> constr -> unit) ref =
     crible_rec (Lib.contents_after None)
   with Not_found -> 
     errorlabstrm "search"
-      [< pr_global_reference env ref; 'sPC; 'sTR "not declared" >]
+      [< pr_global ref; 'sPC; 'sTR "not declared" >]
 
 let search_by_head ref =
-  crible (fun str ass_name constr -> 
+  crible (fun pname ass_name constr -> 
             let pc = prterm_env ass_name constr in
-            mSG[<'sTR str; 'sTR":"; pc; 'fNL >]) ref
+            mSG[< pname; 'sTR":"; pc; 'fNL >]) ref
 
 let read_sec_context sec =
   let rec get_cxt in_cxt = function
@@ -466,7 +458,7 @@ let print_local_context () =
                let {const_body=val_0;const_type=typ} = 
 		 Global.lookup_constant sp in
                [< print_last_const rest;
-                  'sTR(print_basename sp) ;'sTR" = ";
+                  print_basename sp ;'sTR" = ";
                   print_typed_body (val_0,typ) >]
            | "INDUCTIVE" -> 
                let mib = Global.lookup_mind sp in 
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index 64e2cb1094..0c792094bd 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -15,7 +15,6 @@ open Environ
 
 val assumptions_for_print : name list -> names_context
 
-val print_basename : section_path -> string
 val print_closed_sections : bool ref
 val print_impl_args : int list -> std_ppcmds
 val print_context : bool -> Lib.library_segment -> std_ppcmds
@@ -48,6 +47,6 @@ val print_path_between : identifier -> identifier -> std_ppcmds
 
 
 val search_by_head : global_reference -> unit
-val crible : (string -> env -> constr -> unit) -> global_reference -> unit
+val crible : (std_ppcmds -> env -> constr -> unit) -> global_reference -> unit
 val inspect : int -> std_ppcmds
 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index ff4713f794..7ee8cbfa5e 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -20,36 +20,21 @@ let section_path sl s =
   let sl = List.rev sl in
   make_path (List.tl sl) (id_of_string (List.hd sl)) (kind_of_string s)
 
-(*
-let pr_global k oper =
-  let id = id_of_global oper in
-  [< 'sTR (string_of_id id) >]
-*)
-
-let is_visible sp id =
-  match Nametab.sp_of_id CCI id with
-    | VarRef sp' -> sp' = sp
-    | ConstRef sp' -> sp' = sp
-    | IndRef (sp',_) -> dirpath sp' = dirpath sp
-    | ConstructRef ((sp',_),_) -> dirpath sp' = dirpath sp
-    | EvarRef _ -> anomaly "is_visible: should not occur"
-  
-let pr_qualified_path sp id =
-  if is_visible sp id then [<'sTR(string_of_id id)>]
-  else [<'sTR(string_of_path (make_path (dirpath sp) id (kind_of_path sp)))>]
+let pr_global ref =
+  [< 'sTR (string_of_qualid (Nametab.qualid_of_global ref)) >]
 
 let global_const_name sp =
-  try pr_qualified_path sp (basename sp)
+  try pr_global (ConstRef sp)
   with Not_found -> (* May happen in debug *)
     [< 'sTR ("CONST("^(string_of_path sp)^")") >]
 
 let global_ind_name (sp,tyi) =
-  try pr_qualified_path sp (Global.id_of_global (IndRef (sp,tyi)))
+  try pr_global (IndRef (sp,tyi))
   with Not_found -> (* May happen in debug *)
     [< 'sTR ("IND("^(string_of_path sp)^","^(string_of_int tyi)^")") >]
 
 let global_constr_name ((sp,tyi),i) =
-  try pr_qualified_path sp (Global.id_of_global (ConstructRef ((sp,tyi),i)))
+  try pr_global (ConstructRef ((sp,tyi),i))
   with Not_found -> (* May happen in debug *)
     [< 'sTR ("CONSTRUCT("^(string_of_path sp)^","^(string_of_int tyi)
 		  ^","^(string_of_int i)^")") >]
@@ -133,8 +118,8 @@ let pr_ref_label = function (* On triche sur le contexte *)
   | ConstNode sp -> pr_constant (Global.env()) (sp,[||])
   | IndNode sp -> pr_inductive (Global.env()) (sp,[||])
   | CstrNode sp -> pr_constructor (Global.env()) (sp,[||])
-  | VarNode id -> print_id id
-  | SectionVarNode sp -> print_id (basename sp)
+  | VarNode id -> pr_id id
+  | SectionVarNode sp -> pr_id (basename sp)
 
 let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
 let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
@@ -151,13 +136,13 @@ and default_tacpr = function
     | Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
     | Node(_,"CONST",[Path(_,sl,s)]) ->
 	let sp = section_path sl s in
-	pr_qualified_path sp (basename (section_path sl s))
+	pr_global (ConstRef (section_path sl s))
     | Node(_,"MUTIND",[Path(_,sl,s); Num(_,tyi)]) ->
 	let sp = section_path sl s in
-	pr_qualified_path sp (Global.id_of_global (IndRef (sp,tyi)))
+	pr_global (IndRef (sp,tyi))
     | Node(_,"MUTCONSTRUCT",[Path(_,sl,s); Num(_,tyi); Num(_,i)]) ->
 	let sp = section_path sl s in
-	pr_qualified_path sp (Global.id_of_global (ConstructRef ((sp,tyi),i)))
+	pr_global (ConstructRef ((sp,tyi),i))
 
     (* This should be tactics *)
     | Node(_,s,[]) -> [< 'sTR s >]
@@ -170,7 +155,7 @@ let pr_var_decl env (id,c,typ) =
     | None ->  [<  >]
     | Some c ->  [< 'sTR" := "; prterm_env env c >] in
   let ptyp = [< 'sTR" : "; prtype_env env typ >] in
-  [< print_id id ; hOV 0 [< pbody; ptyp >] >]
+  [< pr_id id ; hOV 0 [< pbody; ptyp >] >]
 
 let pr_rel_decl env (na,c,typ) =
   let pbody = match c with
@@ -179,7 +164,7 @@ let pr_rel_decl env (na,c,typ) =
   let ptyp = prtype_env env typ in
   match na with
     | Anonymous -> [< 'sTR"<>" ; 'sPC; pbody; 'sTR" :"; 'sPC; ptyp >]
-    | Name id -> [< print_id id ; 'sPC; pbody; 'sTR" :"; 'sPC; ptyp >]
+    | Name id -> [< pr_id id ; 'sPC; pbody; 'sTR" :"; 'sPC; ptyp >]
 
 
 (* Prints out an "env" in a nice format.  We print out the
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 1c53def26d..cbc70a2f48 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -30,7 +30,7 @@ val pr_constant     : env -> constant -> std_ppcmds
 val pr_existential  : env -> existential -> std_ppcmds
 val pr_constructor  : env -> constructor -> std_ppcmds
 val pr_inductive    : env -> inductive -> std_ppcmds
-val pr_global_reference : env -> global_reference -> std_ppcmds
+val pr_global       : global_reference -> std_ppcmds
 val pr_ref_label    : constr_label -> std_ppcmds
 val pr_pattern      : constr_pattern -> std_ppcmds
 val pr_pattern_env  : names_context -> constr_pattern -> std_ppcmds
@@ -52,8 +52,6 @@ val fprterm         : constr -> std_ppcmds
 val fprtype_env     : env -> types -> std_ppcmds
 val fprtype         : types -> std_ppcmds
 
-val is_visible      : section_path -> identifier -> bool
-
 (* For compatibility *)
 val fterm0          : env -> constr -> std_ppcmds
 (*i*)
diff --git a/parsing/termast.ml b/parsing/termast.ml
index f7c1a88d1c..7025bfde44 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -54,18 +54,6 @@ let with_coercions f = with_option print_coercions f
 (**********************************************************************)
 (* conversion of references                                           *)
 
-(*
-let ids_of_rctxt ctxt =
-  Array.to_list
-    (Array.map
-       (function
-	  | RRef (_,RVar id) -> id
-	  | _ ->
-       error
-       "Termast: arbitrary substitution of references not yet implemented")
-     ctxt)
-*)
-
 let ids_of_ctxt ctxt =
   Array.to_list
     (Array.map
@@ -116,6 +104,10 @@ let ast_of_ref pr r =
   | VarRef sp -> ast_of_ident (basename sp)
   | EvarRef ev -> ast_of_existential_ref pr (ev,ctxt)
 
+let ast_of_qualid p =
+  let dir, s = repr_qualid p in
+  let args = List.map nvar (dir@[s]) in
+  ope ("QUALID", args)
 
 (**********************************************************************)
 (* conversion of patterns                                             *)
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 1674ed9fe1..e47f81e622 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -31,6 +31,7 @@ val ast_of_existential  : env -> existential -> Coqast.t
 val ast_of_constructor  : env -> constructor -> Coqast.t
 val ast_of_inductive    : env -> inductive -> Coqast.t
 val ast_of_ref          : ('a -> Coqast.t) -> global_reference -> Coqast.t
+val ast_of_qualid       : qualid -> Coqast.t
 
 (* For debugging *)
 val print_implicits : bool ref