Déplacement non-affichage des coercions dans termast

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

5 files changed, 59 insertions, 81 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 792a66fe9..5f2557f1c 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -10,19 +10,21 @@ open Libobject
 open Declare
 open Term
 open Generic
+open Rawterm
 
 (* usage qque peu general: utilise aussi dans record *)
 
 type cte_typ = 
   | NAM_Var of identifier
-  | NAM_SP of section_path
-  | NAM_Construct of constructor_path
+  | NAM_Constant of section_path
+  | NAM_Inductive of inductive_path
+  | NAM_Constructor of constructor_path
 
 let cte_of_constr = function  
-  | DOPN(Const sp,_) -> NAM_SP sp
-  | DOPN(MutInd (sp,_),_) -> NAM_SP sp
+  | DOPN(Const sp,_) -> NAM_Constant sp
+  | DOPN(MutInd ind_sp,_) -> NAM_Inductive ind_sp
+  | DOPN(MutConstruct cstr_cp,_) -> NAM_Constructor cstr_cp
   | VAR id -> NAM_Var id
-  | DOPN(MutConstruct cstr_cp,_) -> NAM_Construct cstr_cp
   |  _ -> raise Not_found
 
 type cl_typ = 
@@ -95,7 +97,7 @@ let add_new_coercion (coe,s) =
 let add_new_path x =
   iNHERITANCE_GRAPH := x::(!iNHERITANCE_GRAPH)
 
-let init () = 
+let init () =
   cLASSES:= []; 
   add_new_class1 (CL_FUN,{cL_STR="FUNCLASS";
 			  cL_PARAM=0;cL_STRE=NeverDischarge});
@@ -135,6 +137,17 @@ let coercion_exists coe =
   try let _ = coercion_info coe in true
   with Not_found -> false
 
+let coe_of_reference = function
+  | RConst (sp,l) -> NAM_Constant sp
+  | RInd (ind_sp,l) -> NAM_Inductive ind_sp
+  | RConstruct (cstr_sp,l) -> NAM_Constructor cstr_sp
+  | RVar id  -> NAM_Var id
+  | _ -> raise Not_found
+
+let coercion_params r =
+  let _,coe_info = coercion_info (coe_of_reference r) in
+  coe_info.cOE_PARAM
+
 (* coercion_info_from_index : int -> coe_typ * coe_info_typ *)
 
 let coercion_info_from_index i = 
@@ -176,14 +189,13 @@ let _ =
 
 let constructor_at_head t = 
   let rec aux t' = match t' with
-    | (DOPN(Const sp,_)) -> CL_SP sp,0
-    | (DOPN(MutInd (sp,i),_)) -> CL_IND (sp,i),0
-    | (VAR(id)) -> CL_Var id,0
-    | (DOP2(Cast,c,_)) -> aux (collapse_appl c)
-    | (DOPN(AppL,cl)) -> 
-	let c,_ = aux (array_hd cl) in c,Array.length(cl)-1
+    | VAR id -> CL_Var id,0
+    | DOPN(Const sp,_) -> CL_SP sp,0
+    | DOPN(MutInd ind_sp,_) -> CL_IND ind_sp,0
     | DOP2(Prod,_,DLAM(_,c)) -> CL_FUN,0
     | DOP0(Sort(_)) -> CL_SORT,0
+    | DOP2(Cast,c,_) -> aux (collapse_appl c)
+    | DOPN(AppL,cl) -> let c,_ = aux (array_hd cl) in c,Array.length(cl)-1
     |  _ -> raise Not_found
   in 
   aux (collapse_appl t)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index fe7fb437d..5aa8b7aaf 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -9,6 +9,7 @@ open Evd
 open Environ
 open Libobject
 open Declare
+open Rawterm
 (*i*)
 
 type cl_typ = 
@@ -25,8 +26,9 @@ type cl_info_typ = {
 
 type cte_typ = 
   | NAM_Var of identifier 
-  | NAM_SP of section_path 
-  | NAM_Construct of constructor_path
+  | NAM_Constant of section_path
+  | NAM_Inductive of inductive_path
+  | NAM_Constructor of constructor_path
 
 type coe_typ = cte_typ
 
@@ -50,6 +52,7 @@ 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
+val coercion_params : reference -> int (* raise Not_found if not a coercion *)
 val constructor_at_head : constr -> cl_typ * int
 val class_of : env -> 'c evar_map -> constr -> constr * int
 val class_args_of : constr -> constr list
diff --git a/toplevel/class.ml b/toplevel/class.ml
index f8b84b7b6..2262d0083 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -53,12 +53,9 @@ let rec stre_unif_cond = function
 	stre_max (stre1,stre2)
 
 let stre_of_coe = function
-  | NAM_SP sp ->
-      (match global_operator sp (basename sp) with
-	 | Const sp, _ -> constant_strength sp
-	 | _ -> NeverDischarge)
+  | NAM_Constant sp -> constant_strength sp
   | NAM_Var id -> variable_strength id
-  | _ -> NeverDischarge
+  | NAM_Inductive _ | NAM_Constructor _ -> NeverDischarge 
 	
 (* try_add_class : Names.identifier ->
   Term.constr -> (cl_typ * int) option -> bool -> int * Libobject.strength *)
@@ -113,18 +110,14 @@ let check_class id v cl p =
 
 (* decomposition de constr vers coe_typ *)
 
-let coe_constructor_at_head t = 
-  let rec aux t' =
-    match kind_of_term t' with
-      | IsConst (sp,l) -> (Array.to_list l),NAM_SP sp
-      | IsMutInd ((sp,_),l) -> (Array.to_list l),NAM_SP sp
-      | IsVar id  -> [],NAM_Var id
-      | IsCast (c,_) -> aux c
-      | IsMutConstruct (cstr_sp,l) -> (Array.to_list l),NAM_Construct cstr_sp
-      | IsAppL(f,args) -> aux f
-      |  _ -> raise Not_found
-  in 
-  aux (collapse_appl t)
+(* t provient de global_reference donc pas de Cast, pas de AppL *)
+let coe_of_reference t = 
+  match kind_of_term t with
+    | IsConst (sp,l) -> (Array.to_list l),NAM_Constant sp
+    | IsMutInd (ind_sp,l) -> (Array.to_list l),NAM_Inductive ind_sp
+    | IsMutConstruct (cstr_sp,l) -> (Array.to_list l),NAM_Constructor cstr_sp
+    | IsVar id  -> [],NAM_Var id
+    |  _ -> anomaly "Not a reference"
 
 let constructor_at_head1 t = 
   let rec aux t' =
@@ -294,47 +287,12 @@ let build_id_coercion idf_opt ids =
   declare_constant idf (constr_entry,NeverDischarge);
   idf
 
-let coercion_syntax_entry id n =
-  let args = (String.concat " " (list_tabulate (fun _ -> "$_") n)) ^ " $c" in
-  let str = "level 10: " ^ (string_of_id id) ^
-            " [ <<(" ^ (string_of_id id) ^ " " ^ args ^ ")>> ]" ^
-            " -> [ (APPLIST $c):E ]"
-  in
-  try
-    let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in
-    Metasyntax.add_syntax_obj "constr" [se]
-  with Stdpp.Exc_located _ -> 
-    anomaly ("ill-formed syntax entry: "^str)
-
-let fun_coercion_syntax_entry id n =
-  let args =
-    if n<0 then anomaly "fun_coercion_syntax_entry";
-    String.concat " " (list_tabulate (fun _ -> "$_") n) ^ " $c ($LIST $l)" 
-  in
-  let str = "level 10: " ^ ((string_of_id id)^"1") ^
-            " [ (APPLIST " ^ (string_of_id id) ^ " " ^ args ^ ") ] "  ^
-      	    "-> [ (APPLIST $c ($LIST $l)):E ]"
-  in
-  try
-    let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in
-    Metasyntax.add_syntax_obj "constr" [se]
-  with Stdpp.Exc_located _ -> 
-    anomaly ("ill-formed syntax entry: "^str)
-
-let coercion_syntax idf ps clt =
-  match clt with
-    | CL_FUN -> 
-	fun_coercion_syntax_entry idf ps;
-	coercion_syntax_entry idf ps
-    | _ -> coercion_syntax_entry idf ps
-
 let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps =
   add_anonymous_leaf
     (inCoercion
        ((coef,
 	 {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}),
-	cls,clt));
-  coercion_syntax idf ps clt
+	cls,clt))
 
 (* 
 nom de la fonction coercion
@@ -353,7 +311,7 @@ let try_add_new_coercion_core idf stre source target isid =
   let t = Retyping.get_type_of env Evd.empty v in
   let k = Retyping.get_type_of env Evd.empty t in
   let vj = {uj_val=v; uj_type=t; uj_kind = k} in
-  let f_vardep,coef = coe_constructor_at_head v in
+  let f_vardep,coef = coe_of_reference v in
   if coercion_exists coef then
     errorlabstrm "try_add_coercion" 
       [< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >];
@@ -400,7 +358,10 @@ let try_add_new_coercion_core idf stre source target isid =
   let stres = check_class ids vs cls ps in
   let stret = check_class idt vt clt pt in
   let stref = stre_of_coe coef in
+(* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ?
   let streunif = stre_unif_cond (s_vardep,f_vardep) in
+ *)
+  let streunif = NeverDischarge in
   let stre' = stre_max4 stres stret stref streunif in
   (* if (stre=NeverDischarge) & (stre'<>NeverDischarge)
      then errorlabstrm "try_add_coercion" 
@@ -480,28 +441,34 @@ let process_cl sec_sp cl =
 	  cl
     | _ -> cl
 
+(* Pour le discharge *)
 let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
   let s1= process_cl sec_sp s in
   let t1 = process_cl sec_sp t in
   let p = (snd (class_info s1)).cL_PARAM in
   match coe with 
     | NAM_Var id -> ((coe,coeinfo),s1,t1),id,p
-    | NAM_SP sp -> 
+    | NAM_Constant sp -> 
+	if defined_in_sec sp sec_sp then
+	  let ((_,spid,spk)) = repr_path sp in
+	  let newsp = Lib.make_path spid CCI in
+	  ((NAM_Constant newsp,coeinfo),s1,t1),spid,p
+	else
+	  ((coe,coeinfo),s1,t1),basename sp,p
+    | NAM_Inductive (sp,i) -> 
 	if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
 	  let newsp = Lib.make_path spid CCI in
-	  let v = global_reference CCI spid in
-	  ((NAM_SP newsp,coeinfo),s1,t1),spid,p
-	else 
+	  ((NAM_Inductive (newsp,i),coeinfo),s1,t1),spid,p
+	else
 	  ((coe,coeinfo),s1,t1),basename sp,p
-    | NAM_Construct ((sp,i),j) -> 
+    | NAM_Constructor ((sp,i),j) -> 
 	if defined_in_sec sp sec_sp then 
 	  let ((_,spid,spk)) = repr_path sp in
 	  let newsp = Lib.make_path spid CCI in
 	  let id = Global.id_of_global (MutConstruct((newsp,i),j)) in
-	  let v = global_reference CCI id in
-          (((NAM_Construct ((newsp,i),j)),coeinfo),s1,t1),id,p
-	else 
+          (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1),id,p
+	else
 	  ((coe,coeinfo),s1,t1),
 	  Global.id_of_global (MutConstruct((sp,i),j)),
 	  p
diff --git a/toplevel/class.mli b/toplevel/class.mli
index f916db079..f82821554 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -24,6 +24,3 @@ val process_coercion :
     ((coe_typ * coe_info_typ) * cl_typ * cl_typ) * identifier * int 
 
 val defined_in_sec : section_path -> section_path -> bool
-val coercion_syntax : identifier -> int -> cl_typ -> unit
-val fun_coercion_syntax_entry : identifier -> int -> unit
-val coercion_syntax_entry : identifier -> int -> unit
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index f13890228..2942e7e5a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -301,8 +301,7 @@ let process_operation = function
   | Struc (newsp,strobj) ->
       Lib.add_anonymous_leaf (inStruc (newsp,strobj))
   | Coercion ((_,_,clt) as y,idf,ps) ->
-      Lib.add_anonymous_leaf (inCoercion y); 
-      coercion_syntax idf ps clt
+      Lib.add_anonymous_leaf (inCoercion y) 
 
 let close_section _ s = 
   let oldenv = Global.env() in