Ajout Print Canonical Structures

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

11 files changed, 24 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 0c6c19c57c..2c865c8771 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,7 @@ Vernacular commands
 
 - Added "Print Rewrite HintDb" to print the content of a DB used by
   autorewrite (doc TODO)
+- Added "Print Canonical Structures" (doc TODO)
 
 Gallina
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 365c234ae3..f0cdc49aee 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1785,6 +1785,8 @@ let rec xlate_vernac =
 	| PrintCoercions -> CT_print_coercions
 	| PrintCoercionPaths (id1, id2) -> 
 	    CT_print_path (xlate_class id1, xlate_class id2)
+	| PrintCanonicalStructures ->
+	    xlate_error "TODO: Print Canonical Structures"
 	| PrintInspect n -> CT_inspect (CT_int n)
 	| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
 	| PrintLocalContext -> CT_print
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 79b0e26fc1..a8f46a12b1 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -191,6 +191,7 @@ GEXTEND Gram
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
+      | IDENT "Canonical"; IDENT "Structures" -> PrintCanonicalStructures
       | IDENT "Tables" -> PrintTables
       | "Proof"; qid = global -> PrintOpaqueName qid
       | IDENT "Hint" -> PrintHintGoal
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index e920352d1a..5b0350f82e 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -579,6 +579,7 @@ GEXTEND Gram
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
+      | IDENT "Canonical"; IDENT "Structures" -> PrintCanonicalStructures
       | IDENT "Tables" -> PrintTables
 (* Obsolete: was used for cooking V6.3 recipes ??
       | IDENT "Proof"; qid = global -> PrintOpaqueName qid
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index bbbbc31800..50347df033 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -27,6 +27,7 @@ open Printer
 open Printmod
 open Libnames
 open Nametab
+open Recordops
 
 (*********************)
 (** Basic printing   *)
@@ -593,10 +594,10 @@ let print_class i =
   pr_class cl
   
 let print_path ((i,j),p) = 
-  (str"[" ++ 
-     prlist_with_sep pr_semicolon print_coercion_value p ++
-     str"] : " ++ print_class i ++ str" >-> " ++
-     print_class j)
+  hov 2 (
+    str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++
+    str"] : ") ++
+  print_class i ++ str" >-> " ++ print_class j
 
 let _ = Classops.install_path_printer print_path
 
@@ -627,4 +628,9 @@ let print_path_between cls clt =
   in
   print_path ((i,j),p)
 
+let print_canonical_structures () =
+  prlist_with_sep pr_fnl (fun ((r1,r2),o) -> 
+    prterm o.o_DEF ++ str ": " ++ pr_global r1 ++ str " >-> " ++ pr_global r2)
+    (canonical_structures ())
+
 (*************************************************************************)
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 3af935d086..20429cd3d9 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -57,6 +57,7 @@ val print_graph : unit -> std_ppcmds
 val print_classes : unit -> std_ppcmds
 val print_coercions : unit -> std_ppcmds
 val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
+val print_canonical_structures : unit -> std_ppcmds
 
 val inspect : int -> std_ppcmds
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index cc53ae7f3f..cfccdb5e68 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -117,6 +117,8 @@ let subst_obj subst obj =
 let object_table =
   (ref [] : ((global_reference * global_reference) * obj_typ) list ref)
 
+let canonical_structures () = !object_table
+
 let cache_canonical_structure (_,(cst,lo)) =
   List.iter (fun (o,_ as x) ->
     if not (List.mem_assoc o !object_table) then
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 128018d581..7402f74c9a 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -48,3 +48,6 @@ val inStruc : inductive * struc_typ -> obj
 val outStruc : obj -> inductive * struc_typ
 
 val outCanonicalStructure : obj -> constant
+
+val canonical_structures : unit -> 
+  ((global_reference * global_reference) * obj_typ) list
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0389dae68f..f0433f560f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -894,6 +894,7 @@ let vernac_print = function
   | PrintCoercions -> ppnl (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->
       ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
+  | PrintCanonicalStructures -> ppnl (Prettyp.print_canonical_structures ())
   | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ()))
   | PrintUniverses (Some s) -> dump_universes s
   | PrintHint qid -> Auto.print_hint_ref (Nametab.global qid)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 0ab5f8ac9e..db68c779c5 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -51,6 +51,7 @@ type printable =
   | PrintClasses
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
+  | PrintCanonicalStructures
   | PrintUniverses of string option
   | PrintHint of reference
   | PrintHintGoal
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 11a247e502..a039027a22 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -1031,6 +1031,7 @@ let rec pr_vernac = function
 	| PrintClasses -> str"Print Classes"
 	| PrintCoercions -> str"Print Coercions"
 	| PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t
+	| PrintCanonicalStructures -> str"Print Canonical Structures"
 	| PrintTables -> str"Print Tables"
 	| PrintOpaqueName qid -> str"Print Term" ++ spc() ++ pr_reference qid
 	| PrintHintGoal -> str"Print Hint"