Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_basevernac.ml4

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

4 files changed, 143 insertions, 60 deletions

diff --git a/parsing/termast.ml b/parsing/termast.ml
index 8e7cc12af2..3d72f4adcd 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -155,11 +155,13 @@ let rec skip_coercion dest_ref (f,args as app) =
     try
       match dest_ref f with
 	| Some r ->
-	    let n = Classops.coercion_params r in
-	    if n >= List.length args then app
-	    else (* We skip a coercion *)
-	      let _,fargs = list_chop n args in
-	      skip_coercion dest_ref (List.hd fargs,List.tl fargs)
+	    (match Classops.hide_coercion r with
+	       | Some n ->
+		   if n >= List.length args then app
+		   else (* We skip a coercion *)
+		     let _,fargs = list_chop n args in
+	       	     skip_coercion dest_ref (List.hd fargs,List.tl fargs)
+	       | None -> app)
 	| None -> app
     with Not_found -> app
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 710a723e36..0b190db0e8 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -138,9 +138,17 @@ let coe_of_reference = function
   | EvarRef _ -> raise Not_found
   | x -> x
 
-let hide_coercion r =
-  let _,coe_info = coercion_info (coe_of_reference r) in
-  if coe_info.coe_hide then None else Some coe_info.coe_param
+let hide_coercion coe =
+  let _,coe_info = coercion_info coe in
+  if coe_info.coe_hide then Some coe_info.coe_param else None
+
+let set_coercion_visibility b coe =
+  let _,coe_info = coercion_info coe in
+  coe_info.coe_hide <- not b
+
+let is_coercion_visible coe = 
+  let _,coe_info = coercion_info coe in
+  not coe_info.coe_hide
 
 let coercion_params coe_info = coe_info.coe_param
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index fec858a590..4ccf02b1f5 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -2,16 +2,14 @@
 (*i $Id$ i*)
 
 (*i*)
-open Pp
 open Names
 open Term
 open Evd
 open Environ
-open Libobject
 open Declare
-open Rawterm
 (*i*)
 
+(*s This is the type of class kinds *)
 type cl_typ = 
   | CL_SORT 
   | CL_FUN 
@@ -19,64 +17,91 @@ type cl_typ =
   | CL_CONST of constant_path
   | CL_IND of inductive_path
 
+(* This is the type of infos for declared classes *)
 type cl_info_typ = {
-  cL_STRE : strength;
-  cL_PARAM : int }
+  cl_strength : strength;
+  cl_param : int }
 
-type cte_typ = 
-  | NAM_Section_Variable of variable_path
-  | NAM_Constant of constant_path
-  | NAM_Inductive of inductive_path
-  | NAM_Constructor of constructor_path
+(* This is the type of coercion kinds *)
+type coe_typ = global_reference
 
-type coe_typ = cte_typ
+(* This is the type of infos for declared coercions *)
+type coe_info_typ 
 
+(* [cl_index] is the type of class keys *)
+type cl_index
 
-type coe_info_typ = {
-  cOE_VALUE : unsafe_judgment;
-  cOE_STRE : strength;
-  cOE_ISID : bool;
-  cOE_PARAM : int }
+(* [coe_index] is the type of coercion keys *)
+type coe_index
 
-type inheritance_path = int list
+(* This is the type of paths from a class to another *)
+type inheritance_path = coe_index list
 
-val inheritance_graph : unit -> ((int * int) * inheritance_path) list
-val classes : unit -> (int * (cl_typ * cl_info_typ)) list
-val coercions : unit -> (int * (coe_typ * coe_info_typ)) list
+val cte_of_constr : constr -> global_reference
+val coe_of_reference : global_reference -> coe_typ
 
-val cte_of_constr : constr -> cte_typ
-val class_info : cl_typ -> (int * cl_info_typ)
-val class_exists : cl_typ -> bool
-val class_info_from_index : int -> cl_typ * cl_info_typ
-val coercion_exists : coe_typ -> bool
-val coercion_info : coe_typ -> (int * coe_info_typ)
-val coercion_info_from_index : int -> coe_typ * coe_info_typ
+(*s [declare_class] adds a class to the set of declared classes *)
+val declare_class : cl_typ * strength * int -> unit
 
-(* [coercion_params] raises [Not_found] if not a coercion *)
-val coercion_params : global_reference -> int
+(*s Access to classes infos *)
+val class_info : cl_typ -> (cl_index * cl_info_typ)
+val class_exists : cl_typ -> bool
+val class_info_from_index : cl_index -> cl_typ * cl_info_typ
 
+(* [constructor_at_head c] returns the head reference of c and its
+   number of arguments *)
 val constructor_at_head : constr -> cl_typ * int
 
 (* raises [Not_found] if not convertible to a class *)
-val class_of : env -> 'c evar_map -> constr -> constr * int
+val class_of : env -> 'c evar_map -> constr -> constr * cl_index
 
 val class_args_of : constr -> constr list
-val inClass : (cl_typ * cl_info_typ) -> obj
-val outClass : obj -> (cl_typ * cl_info_typ)
-val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> obj
-val outCoercion : obj -> (coe_typ * coe_info_typ) * cl_typ * cl_typ
-val lookup_path_between : (int * int) -> inheritance_path
-val lookup_path_to_fun_from : int -> inheritance_path
-val lookup_path_to_sort_from : int -> inheritance_path
-val coe_value : int -> (unsafe_judgment * bool)
-val stre_of_cl : cl_typ -> strength
-val add_new_class : cl_typ * strength * int -> unit
-val add_new_coercion_in_graph : 
-  (coe_typ * coe_info_typ) * cl_typ * cl_typ -> unit
-val add_coercion_in_graph : int * int * int -> unit
 
+val strength_of_cl : cl_typ -> strength
+
+(*s [declare_coercion] adds a coercion in the graph of coercion paths *)
+val declare_coercion : 
+  coe_typ -> value:unsafe_judgment -> strength:strength -> isid:bool ->
+      src:cl_typ -> target:cl_typ -> params:int -> unit
+
+(*s Access to coercions infos *)
+val coercion_exists : coe_typ -> bool
+val coercion_info_from_index : coe_index -> coe_typ * coe_info_typ
+
+val coercion_value : coe_index -> (unsafe_judgment * bool)
+
+(*s This is for printing purpose *)
+
+(* [hide_coercion] returns the number of params to skip if the coercion must
+   be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
+val hide_coercion : coe_typ -> int option
+
+val set_coercion_visibility : bool -> coe_typ -> unit
+val is_coercion_visible : coe_typ -> bool
+
+(*s Lookup functions for coercion paths *)
+val lookup_path_between : (cl_index * cl_index) -> inheritance_path
+val lookup_path_to_fun_from : cl_index -> inheritance_path
+val lookup_path_to_sort_from : cl_index -> inheritance_path
+
+(*i Pour le discharge *)
+open Libobject
+val inClass : (cl_typ * cl_info_typ) -> Libobject.obj
+val outClass : Libobject.obj -> (cl_typ * cl_info_typ)
+val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> Libobject.obj
+val outCoercion : Libobject.obj -> (coe_typ * coe_info_typ) * cl_typ * cl_typ
+val coercion_strength : coe_info_typ -> strength
+(*i*)
+
+(*i Crade *)
+open Pp
 val install_path_printer : 
-  ((int * int) * inheritance_path -> std_ppcmds) -> unit
+  ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit
+(*i*)
 
 (* This is for printing purpose *)
 val string_of_class : cl_typ -> string
+val get_coercion_value : coe_info_typ -> constr
+val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
+val classes : unit -> (int * (cl_typ * cl_info_typ)) list
+val coercions : unit -> (int * (coe_typ * coe_info_typ)) list
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 96fbd375d8..d8389ac05a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -472,29 +472,77 @@ let _ =
 		message "Implicit arguments mode is unset")
        | _  -> bad_vernac_args "IMPLICIT_ARGS_OFF")
 
-let _ =          
+let coercion_of_qualid loc qid =
+  let ref = global loc qid in
+  let coe = Classops.coe_of_reference ref in
+  if not (Classops.coercion_exists coe) then
+    errorlabstrm "try_add_coercion" 
+      [< Printer.pr_global ref; 'sTR" is not a coercion" >];
+  coe
+
+let _ =
   add "PRINTING_COERCIONS_ON"
     (function 
        | [] -> (fun () -> Termast.print_coercions := true)
-       | _  -> bad_vernac_args "PRINTING_COERCIONS_ON")
+       | l ->
+	   let ql =
+	     List.map 
+	       (function
+		  | VARG_QUALID qid -> qid
+		  | _ ->  bad_vernac_args "PRINTING_COERCIONS_ON") l in
+	   (fun () ->
+	      List.iter
+		(fun qid ->
+		   Classops.set_coercion_visibility true
+		     (coercion_of_qualid dummy_loc qid))
+		ql))
 
 let _ =
   add "PRINTING_COERCIONS_OFF"
     (function 
        | [] -> (fun () -> Termast.print_coercions := false)
-       | _  -> bad_vernac_args "PRINTING_COERCIONS_OFF")
+       | l -> 
+	   let ql =
+	     List.map 
+	       (function
+		  | VARG_QUALID qid -> qid
+		  | _ ->  bad_vernac_args "PRINTING_COERCIONS_OFF") l in
+	   (fun () ->
+	      List.iter
+		(fun qid ->
+		   Classops.set_coercion_visibility false 
+		     (coercion_of_qualid dummy_loc qid))
+		ql))
 
 let _ =
   add "TEST_PRINTING_COERCIONS"
     (function 
        | [] ->
-	   (fun () ->
-	      if !(Termast.print_coercions) = true then
+           (fun () ->
+              if !(Termast.print_coercions) = true then
 		message "Printing of coercions is set"
-	      else 
+              else 
 		message "Printing of coercions is unset")
-       | _  -> bad_vernac_args "TEST_PRINTING_COERCIONS")
-
+       | l -> 
+	   let ql =
+	     List.map 
+	       (function
+		  | VARG_QUALID qid -> qid
+		  | _  -> bad_vernac_args "TEST_PRINTING_COERCIONS") l in
+	   (fun () ->
+              List.iter
+		(fun qid ->
+		   let coe = coercion_of_qualid dummy_loc qid in
+	           if Classops.is_coercion_visible coe then
+		     message
+		       ("Printing of coercion "^(string_of_qualid qid)^
+			" is set")
+		   else 
+		     message 
+		       ("Printing of coercion "^(string_of_qualid qid)^
+			" is unset"))
+		ql))
+    
 let number_list = 
   List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list")