Restructuration et simplification des fonctions d'affichage, de détypage

et d'"externalisation"; standardisation du nom des fonctions d'affichage


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

4 files changed, 79 insertions, 78 deletions

diff --git a/dev/base_include b/dev/base_include
index 55e2c9286..cd837ab6a 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -17,16 +17,16 @@
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
-#install_printer  (* identifier *) prid;;
-#install_printer  (* label *) prlab;;
-#install_printer prmsid;;
-#install_printer prmbid;;
-#install_printer prdir;;
-#install_printer prmp;;
-#install_printer  (* section_path *)  prsp;;
-#install_printer  (* qualid *)  prqualid;;
-#install_printer  (* kernel_name *) prkn;;
-#install_printer  (* constant *) prcon;;
+#install_printer  (* identifier *) ppid;;
+#install_printer  (* label *) pplab;;
+#install_printer  (* mod_self_id *) ppmsid;;
+#install_printer  (* mod_bound_id *) ppmbid;;
+#install_printer  (* dir_path *) ppdir;;
+#install_printer  (* module_path *) ppmp;;
+#install_printer  (* section_path *)  ppsp;;
+#install_printer  (* qualid *)  ppqualid;;
+#install_printer  (* kernel_name *) ppkn;;
+#install_printer  (* constant *) ppcon;;
 #install_printer  (* constr *)  print_pure_constr;; 
 #install_printer  (* patch *) ppripos;;
 #install_printer  (* values *) ppvalues;;
diff --git a/dev/db b/dev/db
index 54e0706cc..751043977 100644
--- a/dev/db
+++ b/dev/db
@@ -1,35 +1,35 @@
 load_printer "gramlib.cma"
 load_printer "printers.cma"
 
-install_printer Top_printers.prid
-install_printer Top_printers.prlab
-install_printer Top_printers.prmsid
-install_printer Top_printers.prmbid
-install_printer Top_printers.prdir
-install_printer Top_printers.prmp
-install_printer Top_printers.prkn
-install_printer Top_printers.prcon
-install_printer Top_printers.prsp
-install_printer Top_printers.prqualid
+install_printer Top_printers.ppid
+install_printer Top_printers.pplab
+install_printer Top_printers.ppmsid
+install_printer Top_printers.ppmbid
+install_printer Top_printers.ppdir
+install_printer Top_printers.ppmp
+install_printer Top_printers.ppkn
+install_printer Top_printers.ppcon
+install_printer Top_printers.ppsp
+install_printer Top_printers.ppqualid
 install_printer Top_printers.ppbigint
 
 install_printer Top_printers.pppattern
-install_printer Top_printers.pprawterm
+install_printer Top_printers.pprawconstr
 
-install_printer Top_printers.ppterm
-install_printer Top_printers.print_uni
-install_printer Top_printers.pp_universes
+install_printer Top_printers.ppconstr
+install_printer Top_printers.ppuni
+install_printer Top_printers.ppuniverses
 install_printer Top_printers.pptype
-install_printer Top_printers.prj
+install_printer Top_printers.ppj
 
-install_printer Top_printers.prgoal
-install_printer Top_printers.prsigmagoal
+install_printer Top_printers.ppgoal
+install_printer Top_printers.ppsigmagoal
 install_printer Top_printers.pproof
-install_printer Top_printers.prevd
-install_printer Top_printers.prclenv
+install_printer Top_printers.ppevd
+install_printer Top_printers.ppclenv
 
 install_printer Top_printers.pptac
-install_printer Top_printers.pr_obj
+install_printer Top_printers.ppobj
 install_printer Top_printers.pploc
                                                   
 
diff --git a/dev/include b/dev/include
index d1b5a717b..563edd042 100644
--- a/dev/include
+++ b/dev/include
@@ -5,26 +5,26 @@
 #use "base_include";;
 
 #install_printer  (* pattern *) pppattern;;
-#install_printer  (* rawconstr *) pprawterm;;
+#install_printer  (* rawconstr *) pprawconstr;;
 
-#install_printer  (* constr *) ppterm;;
-#install_printer  (* constr_substituted *) ppsterm;; 
-#install_printer  (* universe *)  print_uni;;
-#install_printer  (* universes *)  pp_universes;;
-#install_printer  (* type_judgement*) pptype;;
-#install_printer  (* judgement*) prj;;
+#install_printer  (* constr *) ppconstr;;
+#install_printer  (* constr_substituted *) ppsconstr;; 
+#install_printer  (* universe *)  ppuni;;
+#install_printer  (* universes *)  ppuniverses;;
+#install_printer  (* type_judgement *) pptype;;
+#install_printer  (* judgement *) ppj;;
 
-#install_printer  (* goal *)  prgoal;;
-#install_printer  (* sigma goal *)  prsigmagoal;;
+#install_printer  (* goal *)  ppgoal;;
+#install_printer  (* sigma goal *)  ppsigmagoal;;
 #install_printer  (* proof *)  pproof;;
-#install_printer  (* evar_map *)  prevm;;
-#install_printer  (* evar_defs *)  prevd;;
-#install_printer  (* clenv *) prclenv;;
+#install_printer  (* evar_map *)  ppevm;;
+#install_printer  (* evar_defs *)  ppevd;;
+#install_printer  (* clenv *) ppclenv;;
 #install_printer  (* env *) ppenv;;
 
 #install_printer  (* tactic *) pptac;;
-#install_printer  (* object *) pr_obj;;
-#install_printer  (* global_reference *) prglobal;;
+#install_printer  (* object *) ppobj;;
+#install_printer  (* global_reference *) ppglobal;;
 
 #install_printer  (* fconstr *) ppfconstr;;
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4bf879e85..f4f17c1d7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -29,31 +29,32 @@ open Evd
 let _ = Constrextern.print_evar_arguments := true
 
 (* name printers *)
-let prid id = pp (pr_id id)
-let prlab l = pp (pr_lab l)
-let prmsid msid = pp (str (debug_string_of_msid msid))
-let prmbid mbid = pp (str (debug_string_of_mbid mbid))
-let prdir dir = pp (pr_dirpath dir)
-let prmp mp = pp(str (string_of_mp mp))
-let prcon con = pp(pr_con con)
-let prkn kn = pp(pr_kn kn)
-let prsp sp = pp(pr_sp sp)
-let prqualid qid = pp(pr_qualid qid)
+let ppid id = pp (pr_id id)
+let pplab l = pp (pr_lab l)
+let ppmsid msid = pp (str (debug_string_of_msid msid))
+let ppmbid mbid = pp (str (debug_string_of_mbid mbid))
+let ppdir dir = pp (pr_dirpath dir)
+let ppmp mp = pp(str (string_of_mp mp))
+let ppcon con = pp(pr_con con)
+let ppkn kn = pp(pr_kn kn)
+let ppsp sp = pp(pr_sp sp)
+let ppqualid qid = pp(pr_qualid qid)
 
 (* term printers *)
-let ppterm x = pp(Termops.print_constr x)
-let ppsterm x = ppterm (Declarations.force x)
-let ppterm_univ x = Constrextern.with_universes ppterm x
-let pprawterm = (fun x -> pp(pr_rawterm x))
-let pppattern = (fun x -> pp(pr_pattern x))
-let pptype = (fun x -> pp(prtype x))
-let ppfconstr c = ppterm (Closure.term_of_fconstr c)
+let ppconstr x = pp(Termops.print_constr x)
+let ppterm = ppconstr
+let ppsconstr x = ppconstr (Declarations.force x)
+let ppconstr_univ x = Constrextern.with_universes ppconstr x
+let pprawconstr = (fun x -> pp(pr_lrawconstr x))
+let pppattern = (fun x -> pp(pr_constr_pattern x))
+let pptype = (fun x -> pp(pr_ltype x))
+let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
 let ppbigint n = pp (Bigint.pr_bigint n);;
 
 let pP s = pp (hov 0 s)
 
-let safe_prglobal = function 
+let safe_pr_global = function 
   | ConstRef kn -> pp (str "CONSTREF(" ++ pr_con kn ++ str ")")
   | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
 			  int i ++ str ")")
@@ -61,23 +62,23 @@ let safe_prglobal = function
 				      int i ++ str "," ++ int j ++ str ")")
   | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")")
 
-let prglobal x = try pp(pr_global x) with _ -> safe_prglobal x
+let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x
 
-let prconst (sp,j) =
-    pp (str"#" ++ pr_kn sp ++ str"=" ++ prterm j.uj_val)
+let ppconst (sp,j) =
+    pp (str"#" ++ pr_kn sp ++ str"=" ++ pr_lconstr j.uj_val)
 
-let prvar ((id,a)) =
-    pp (str"#" ++ pr_id id ++ str":" ++ prterm a)
+let ppvar ((id,a)) =
+    pp (str"#" ++ pr_id id ++ str":" ++ pr_lconstr a)
 
-let genprj f j = let (c,t) = f j in (c ++ str " : " ++ t)
+let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
 
-let prj j = pp (genprj prjudge j)
+let ppj j = pp (genppj pr_ljudge j)
 
 (* proof printers *)
-let prevm evd = pp(pr_evar_map evd)
-let prevd evd = pp(pr_evar_defs evd)
-let prclenv clenv = pp(pr_clenv clenv)
-let prgoal g = pp(db_pr_goal g)
+let ppevm evd = pp(pr_evar_map evd)
+let ppevd evd = pp(pr_evar_defs evd)
+let ppclenv clenv = pp(pr_clenv clenv)
+let ppgoal g = pp(db_pr_goal g)
 
 let pr_gls gls =
   hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
@@ -88,14 +89,14 @@ let pr_glls glls =
   hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
          prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
 
-let prsigmagoal g = pp(pr_goal (sig_it g))
+let ppsigmagoal g = pp(pr_goal (sig_it g))
 let prgls gls = pp(pr_gls gls)
 let prglls glls = pp(pr_glls glls)
 let pproof p = pp(print_proof Evd.empty empty_named_context p)
 
-let print_uni u = (pp (pr_uni u))
+let ppuni u = pp(pr_uni u)
 
-let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]")
+let ppuniverses u = pp (str"[" ++ pr_universes u ++ str"]")
 
 let ppenv e = pp
   (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++
@@ -103,7 +104,7 @@ let ppenv e = pp
 
 let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x))
 
-let pr_obj obj = Format.print_string (Libobject.object_tag obj)
+let ppobj obj = Format.print_string (Libobject.object_tag obj)
 
 let cnt = ref 0
 
@@ -300,7 +301,7 @@ let print_pure_constr csr =
 	print_string (Printexc.to_string e);print_flush ();
 	raise e
 
-let ppfconstr c = ppterm (Closure.term_of_fconstr c)
+let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
 let pploc x = let (l,r) = unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"