Un nom long pour les variables de section qui font classe ou coercion; réorganisation; bugs discharge

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

4 files changed, 129 insertions, 105 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index dd35be0fba..2afe796d4d 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -14,8 +14,8 @@ open Rawterm
 (* usage qque peu general: utilise aussi dans record *)
 
 type cte_typ = 
-  | NAM_Var of identifier
-  | NAM_Constant of section_path
+  | NAM_Section_Variable of variable_path
+  | NAM_Constant of constant_path
   | NAM_Inductive of inductive_path
   | NAM_Constructor of constructor_path
 
@@ -23,18 +23,17 @@ let cte_of_constr c = match kind_of_term c with
   | IsConst (sp,_) -> NAM_Constant sp
   | IsMutInd (ind_sp,_) -> NAM_Inductive ind_sp
   | IsMutConstruct (cstr_cp,_) -> NAM_Constructor cstr_cp
-  | IsVar id -> NAM_Var id
+  | IsVar id -> NAM_Section_Variable (find_section_variable id)
   |  _ -> raise Not_found
 
 type cl_typ = 
   | CL_SORT 
   | CL_FUN
-  | CL_Var of identifier
-  | CL_SP of section_path 
+  | CL_SECVAR of variable_path
+  | CL_CONST of constant_path
   | CL_IND of inductive_path
 
 type cl_info_typ = {
-  cL_STR : string;
   cL_STRE : strength;
   cL_PARAM : int }
 
@@ -98,10 +97,8 @@ let add_new_path x =
 
 let init () =
   cLASSES:= []; 
-  add_new_class1 (CL_FUN,{cL_STR="FUNCLASS";
-			  cL_PARAM=0;cL_STRE=NeverDischarge});
-  add_new_class1 (CL_SORT,{cL_STR="SORTCLASS";
-			   cL_PARAM=0;cL_STRE=NeverDischarge});
+  add_new_class1 (CL_FUN,  { cL_PARAM=0; cL_STRE=NeverDischarge });
+  add_new_class1 (CL_SORT, { cL_PARAM=0; cL_STRE=NeverDischarge });
   cOERCIONS:= [];
   iNHERITANCE_GRAPH:= []
 
@@ -140,7 +137,7 @@ let coe_of_reference = function
   | ConstRef sp -> NAM_Constant sp
   | IndRef sp -> NAM_Inductive sp
   | ConstructRef sp -> NAM_Constructor sp
-  | VarRef sp  -> NAM_Var (basename sp)
+  | VarRef sp  -> NAM_Section_Variable sp
   | EvarRef _ -> raise Not_found
 
 let coercion_params r =
@@ -175,8 +172,8 @@ let (inClass,outClass) =
                     cache_function = cache_class;
                     export_function = (function x -> Some x) })
 
-let add_new_class (cl,s,stre,p) = 
-  Lib.add_anonymous_leaf (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})))
+let add_new_class (cl,stre,p) = 
+  Lib.add_anonymous_leaf (inClass ((cl,{cL_STRE=stre;cL_PARAM=p})))
    
 let _ = 
   Summary.declare_summary "inh_graph"
@@ -191,8 +188,8 @@ let _ =
 
 let constructor_at_head t = 
   let rec aux t' = match kind_of_term t' with
-    | IsVar id -> CL_Var id,0
-    | IsConst (sp,_) -> CL_SP sp,0
+    | IsVar id -> CL_SECVAR (find_section_variable id),0
+    | IsConst (sp,_) -> CL_CONST sp,0
     | IsMutInd (ind_sp,_) -> CL_IND ind_sp,0
     | IsProd (_,_,c) -> CL_FUN,0
     | IsLetIn (_,_,_,c) -> aux c
@@ -221,32 +218,32 @@ let class_of env sigma t =
 
 let class_args_of c = snd (decomp_app c)
 
-(* verfications pour l'ajout d'une classe *)
-
-let fully_applied id p p1 =
-  if p <> p1 then  errorlabstrm "fully_applied" 
-    [< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
-
-let rec arity_sort a = match kind_of_term a with
-  | IsSort (Prop _ | Type _) -> 0
-  | IsProd (_,_,c) -> (arity_sort c) +1
-  | IsLetIn (_,_,_,c) -> arity_sort c    (* Utile ?? *)
-  | IsCast (c,_) -> arity_sort c
-  | _ -> raise Not_found
-
 let stre_of_cl = function 
-  | CL_SP sp ->
-      if is_constant sp then constant_or_parameter_strength sp
-      else NeverDischarge
-  | CL_Var id -> 
-      variable_strength (make_qualid [] (string_of_id id))
+  | CL_CONST sp -> constant_or_parameter_strength sp
+  | CL_SECVAR sp -> variable_strength sp
   | _ -> NeverDischarge
 
+let string_of_class = function
+  | CL_FUN -> "FUNCLASS"
+  | CL_SORT -> "SORTCLASS" 
+  | CL_CONST sp -> string_of_qualid (Global.qualid_of_global (ConstRef sp))
+  | CL_IND sp -> string_of_qualid (Global.qualid_of_global (IndRef sp))
+  | CL_SECVAR sp -> string_of_qualid (Global.qualid_of_global (VarRef sp))
+
 (* coe_value : int -> Term.constr * bool *)
 
 let coe_value i = 
-  let (_,{cOE_VALUE=v;cOE_ISID=b}) = coercion_info_from_index i in
-  v,b
+  let (coe,{cOE_VALUE=_;cOE_ISID=b}) = coercion_info_from_index i in
+  let env = Global.env () in
+  let v = match coe with 
+    | NAM_Section_Variable sp -> constr_of_reference Evd.empty env (VarRef sp)
+    | NAM_Constant sp -> constr_of_reference Evd.empty env (ConstRef sp)
+    | NAM_Constructor ((sp,i),j) ->
+	constr_of_reference Evd.empty env (ConstructRef ((sp,i),j))
+    | NAM_Inductive (sp,i) ->
+	constr_of_reference Evd.empty env (IndRef (sp,i)) in
+  let j = Retyping.get_judgment_of env Evd.empty v in
+  (j,b)
 
 (* pretty-print functions are now in Pretty *)
 (* rajouter une coercion dans le graphe *)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 19f8a77cd6..fec858a590 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -15,18 +15,17 @@ open Rawterm
 type cl_typ = 
   | CL_SORT 
   | CL_FUN 
-  | CL_Var of identifier 
-  | CL_SP of section_path
+  | CL_SECVAR of variable_path
+  | CL_CONST of constant_path
   | CL_IND of inductive_path
 
 type cl_info_typ = {
-  cL_STR : string;
   cL_STRE : strength;
   cL_PARAM : int }
 
 type cte_typ = 
-  | NAM_Var of identifier 
-  | NAM_Constant of section_path
+  | NAM_Section_Variable of variable_path
+  | NAM_Constant of constant_path
   | NAM_Inductive of inductive_path
   | NAM_Constructor of constructor_path
 
@@ -70,13 +69,14 @@ 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 arity_sort : constr -> int
-val fully_applied : identifier -> int -> int -> unit
 val stre_of_cl : cl_typ -> strength
-val add_new_class : (cl_typ * string * strength * int) -> unit
+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 install_path_printer : 
   ((int * int) * inheritance_path -> std_ppcmds) -> unit
+
+(* This is for printing purpose *)
+val string_of_class : cl_typ -> string
diff --git a/toplevel/class.ml b/toplevel/class.ml
index e133c87ea7..56077f36e5 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -35,64 +35,70 @@ let id_of_varid c = match kind_of_term c with
   | IsVar id -> id
   | _ -> anomaly "class__id_of_varid"
 
-let stre_of_VAR c =
-  variable_strength (make_qualid [] (string_of_id (destVar c)))
-
 (* lf liste des variable dont depend la coercion f
    lc liste des variable dont depend la classe source *)
 
 let rec stre_unif_cond = function
   | ([],[]) -> NeverDischarge
-  | (v::l,[]) -> stre_of_VAR v
-  | ([],v::l) -> stre_of_VAR v
+  | (v::l,[]) -> variable_strength v
+  | ([],v::l) -> variable_strength v
   | (v1::l1,v2::l2) ->
       if v1=v2 then 
 	stre_unif_cond (l1,l2)
       else
-	let stre1 = (stre_of_VAR v1)
-	and stre2 = (stre_of_VAR v2) in 
+	let stre1 = (variable_strength v1)
+	and stre2 = (variable_strength v2) in 
 	stre_max (stre1,stre2)
 
 let stre_of_coe = function
   | NAM_Constant sp -> constant_or_parameter_strength sp
-  | NAM_Var id -> variable_strength (make_qualid [] (string_of_id id))
+  | NAM_Section_Variable sp -> variable_strength sp
   | NAM_Inductive _ | NAM_Constructor _ -> NeverDischarge 
+
+(* verfications pour l'ajout d'une classe *)
+
+let rec arity_sort a = match kind_of_term a with
+  | IsSort (Prop _ | Type _) -> 0
+  | IsProd (_,_,c) -> (arity_sort c) +1
+  | IsLetIn (_,_,_,c) -> arity_sort c    (* Utile ?? *)
+  | IsCast (c,_) -> arity_sort c
+  | _ -> raise Not_found
+
+let check_fully_applied cl p p1 =
+  if p <> p1 then  errorlabstrm "fully_applied" 
+    [< 'sTR"Wrong number of parameters for ";'sTR(string_of_class cl) >]
 	
 (* try_add_class : Names.identifier ->
   Term.constr -> (cl_typ * int) option -> bool -> int * Libobject.strength *)
 
-let try_add_class id v clpopt streopt check_exist = 
-  let env = Global.env () in
-  let t = Retyping.get_type_of env Evd.empty v in
-  let p1 =
-    try 
-      arity_sort t 
-    with Not_found -> 
-      errorlabstrm "try_add_class" 
-        [< 'sTR "Type of "; 'sTR (string_of_id id);
-           'sTR " does not end with a sort" >] 
-  in
-  let cl,p =
-    match clpopt with
-      | None -> let (cl,_)=constructor_at_head v in (cl,p1)
-      | Some (cl,p2) -> (fully_applied id p2 p1;cl,p1) 
-  in
+let try_add_class v (cl,p) streopt check_exist = 
   if check_exist & class_exists cl then
     errorlabstrm "try_add_new_class" 
-      [< 'sTR (string_of_id id) ; 'sTR " is already a class" >];
+      [< 'sTR (string_of_class cl) ; 'sTR " is already a class" >];
   let stre' = stre_of_cl cl in 
   let stre = match streopt with
     | Some stre -> stre_max (stre,stre')
     | None -> stre'
   in
-  add_new_class (cl,(string_of_id id),stre,p);
+  add_new_class (cl,stre,p);
   stre
 
 (* try_add_new_class : Names.identifier -> unit *)
 
 let try_add_new_class id stre =
   let v = global_reference CCI id in
-  let _ = try_add_class id v None (Some stre) true in () 
+  let env = Global.env () in
+  let t = Retyping.get_type_of env Evd.empty v in
+  let p1 =
+    try 
+      arity_sort t 
+    with Not_found -> 
+      errorlabstrm "try_add_class" 
+        [< 'sTR "Type of "; 'sTR (string_of_id id);
+           'sTR " does not end with a sort" >] 
+  in
+  let cl = fst (constructor_at_head v) in
+  let _ = try_add_class v (cl,p1) (Some stre) true in () 
 
 (* check_class : Names.identifier ->
   Term.constr -> cl_typ -> int -> int * Libobject.strength *)
@@ -100,14 +106,21 @@ let try_add_new_class id stre =
 let check_class id v cl p =
   try 
     let _,clinfo = class_info cl in
-    if p = clinfo.cL_PARAM then 
-      clinfo.cL_STRE
-    else 
-      errorlabstrm "fully_applied" 
-	[< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
+    check_fully_applied cl p clinfo.cL_PARAM;
+    clinfo.cL_STRE
   with Not_found -> 
-    try_add_class id v (Some (cl,p)) None false
-
+    let env = Global.env () in
+    let t = Retyping.get_type_of env Evd.empty v in
+    let p1 =
+      try 
+	arity_sort t 
+      with Not_found -> 
+	errorlabstrm "try_add_class" 
+          [< 'sTR "Type of "; 'sTR (string_of_id id);
+             'sTR " does not end with a sort" >] 
+    in
+    check_fully_applied cl p p1;
+    try_add_class v (cl,p1) None false
 
 (* decomposition de constr vers coe_typ *)
 
@@ -117,15 +130,19 @@ let coe_of_reference t =
     | 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
+    | IsVar id  ->
+	let sp =
+	  try find_section_variable id 
+	  with Not_found -> anomaly "Not a reference"
+	in [],NAM_Section_Variable sp
     |  _ -> anomaly "Not a reference"
 
 let constructor_at_head1 t = 
   let rec aux t' =
     match kind_of_term t' with
-      | IsConst (sp,l) -> t',[],(Array.to_list l),CL_SP sp,0
+      | IsConst (sp,l) -> t',[],(Array.to_list l),CL_CONST sp,0
       | IsMutInd (ind_sp,l) -> t',[],(Array.to_list l),CL_IND ind_sp,0
-      | IsVar id -> t',[],[],CL_Var id,0
+      | IsVar id -> t',[],[],CL_SECVAR (find_section_variable id),0
       | IsCast (c,_) -> aux c
       | IsApp(f,args) -> 
 	  let t',_,l,c,_ = aux f in t',Array.to_list args,l,c,Array.length args
@@ -150,20 +167,11 @@ let uniform_cond nargs lt =
 let id_of_cl  = function
   | CL_FUN -> (id_of_string "FUNCLASS")
   | CL_SORT -> (id_of_string "SORTCLASS") 
-  | CL_SP sp -> (basename sp)
+  | CL_CONST sp -> (basename sp)
   | CL_IND (sp,i) ->
       (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename
-  | CL_Var id -> id 
+  | CL_SECVAR sp -> (basename sp)
 	
-let string_of_cl  = function
-  | CL_FUN -> "FUNCLASS"
-  | CL_SORT -> "SORTCLASS" 
-  | CL_SP sp -> string_of_id (basename sp)
-  | CL_IND (sp,i) ->
-      string_of_id
-	(mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename
-  | CL_Var id -> string_of_id id 
-
 (* 
 lp est la liste (inverse'e) des arguments de la coercion
 ids est le nom de la classe source
@@ -258,7 +266,7 @@ let build_id_coercion idf_opt ids =
       | Some(idf) -> idf
       | None ->
 	  id_of_string ("Id_"^(string_of_id ids)^"_"^
-                        (string_of_cl (fst (constructor_at_head t)))) 
+                        (string_of_class (fst (constructor_at_head t)))) 
   in
   let constr_entry = 
     { const_entry_body = val_f; const_entry_type = None } in
@@ -367,42 +375,61 @@ let try_add_new_coercion_record id stre source =
 
 (* fonctions pour le discharge: plutot sale *)
 
+let count_extra_abstractions hyps ids_to_discard =
+  let _,n =
+    List.fold_left
+      (fun (hyps,n as sofar) id -> 
+	 match hyps with
+	   | (hyp,None,_)::rest when id = hyp ->(rest, n+1)
+	   | _ -> sofar)
+      (hyps,0) ids_to_discard
+  in n
+
 let defined_in_sec sp sec_sp = dirpath sp = sec_sp
 
-let process_class sec_sp ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) as x ) =
-  let env = Global.env () in
+let process_class sec_sp ids_to_discard x =
+  let (cl,{cL_STRE=stre; cL_PARAM=p}) = x in
+(*  let env = Global.env () in*)
   match cl with 
-    | CL_Var id -> x
-    | CL_SP sp -> 
+    | CL_SECVAR _ -> x
+    | CL_CONST sp -> 
         if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
-          let newsp = Lib.make_path spid CCI in 
+          let newsp = Lib.make_path spid CCI in
+	  let hyps = (Global.lookup_constant sp).const_hyps in
+	  let n = count_extra_abstractions hyps ids_to_discard in
+(*
           let v = global_reference CCI spid in
           let t = Retyping.get_type_of env Evd.empty v in
           let p = arity_sort t in
-          (CL_SP newsp,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})
+*)
+          (CL_CONST newsp,{cL_STRE=stre;cL_PARAM=p+n})
         else 
 	  x
     | CL_IND (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 hyps = (Global.lookup_mind sp).mind_hyps in
+	  let n = count_extra_abstractions hyps ids_to_discard in
+(*
           let v = global_reference CCI spid in
           let t = Retyping.get_type_of env Evd.empty v in
           let p = arity_sort t in
-          (CL_IND (newsp,i),{cL_STR=s;cL_STRE=stre;cL_PARAM=p})
+*)
+          (CL_IND (newsp,i),{cL_STRE=stre;cL_PARAM=p+n})
         else 
 	  x
     | _ -> anomaly "process_class" 
 
 let process_cl sec_sp cl =
   match cl with
-    | CL_Var id -> CL_Var id 
-    | CL_SP sp ->
+    | CL_SECVAR id -> cl
+    | CL_CONST sp ->
 	if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
           let newsp = Lib.make_path spid CCI in 
-          CL_SP newsp
+          CL_CONST newsp
         else 
 	  cl
     | CL_IND (sp,i) ->
@@ -418,9 +445,8 @@ let process_cl sec_sp cl =
 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)
+    | NAM_Section_Variable _ -> ((coe,coeinfo),s1,t1)
     | NAM_Constant sp -> 
 	if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 8c8a647848..f8aada5f56 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -18,7 +18,8 @@ val try_add_new_coercion_with_target : identifier -> strength ->
 
 val try_add_new_class : identifier -> strength -> unit
 val process_class :
-  dir_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ)
+  dir_path -> identifier list -> 
+    (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ)
 val process_coercion :
   dir_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> 
     (coe_typ * coe_info_typ) * cl_typ * cl_typ