Mise en place d'un système optionnel de discharge immédiat; prise en compte des défs locales dans les arguments des inductifs; nettoyage divers

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

5 files changed, 37 insertions, 21 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index e0ae40af6..4d8e5ba2c 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -8,6 +8,7 @@ open Term
 open Inductive
 open Declarations
 open Environ
+open Inductive
 open Lib
 open Classops
 open Declare
@@ -260,18 +261,16 @@ let build_id_coercion idf_opt source =
     | Some c -> c
     | None -> error_not_transparent source in
   let lams,t = Sign.decompose_lam_assum c in
-  let llams = List.length lams in
-  let lams = List.rev lams in
   let val_f =
     it_mkLambda_or_LetIn
       (mkLambda (Name (id_of_string "x"),
-		 applistc vs (rel_list 0 llams),
+		 applistc vs (extended_rel_list 0 lams),
 		 mkRel 1))
        lams
   in
   let typ_f =
     it_mkProd_wo_LetIn
-      (mkProd (Anonymous, applistc vs (rel_list 0 llams), lift 1 t))
+      (mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t))
       lams
   in
   (* juste pour verification *)
@@ -387,7 +386,7 @@ let count_extra_abstractions hyps ids_to_discard =
     List.fold_left
       (fun (hyps,n as sofar) id -> 
 	 match hyps with
-	   | (hyp,None,_)::rest when id = hyp ->(rest, n+1)
+	   | (hyp,None,_)::rest when id = basename hyp ->(rest, n+1)
 	   | _ -> sofar)
       (hyps,0) ids_to_discard
   in n
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 49dd7b887..5a029a0e6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -440,8 +440,11 @@ let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
   strength =
   begin match strength with
     | DischargeAt disch_sp when Lib.is_section_p disch_sp ->
+	(*
 	let c = constr_of_constr_entry const in
 	let _ = declare_variable id (SectionLocalDef c,strength,opacity) in ()
+	*)
+        let _ = declare_constant id (ConstantEntry const,strength,opacity)in ()
     | NeverDischarge | DischargeAt _ ->
         let _ = declare_constant id (ConstantEntry const,strength,opacity)in ()
     | NotDeclare -> apply_tac_not_declare id pft tpo
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index a3c9586a4..42f05a01d 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -23,13 +23,15 @@ open Recordops
 let recalc_sp dir sp =
   let (_,spid,k) = repr_path sp in Names.make_path dir spid k
 
+let rec find_var id = function
+  | [] -> raise Not_found
+  | (sp,b,_)::l -> if basename sp = id then b=None else find_var id l
+
 let build_abstract_list hyps ids_to_discard =
   map_succeed 
     (fun id ->
        try
-	 match lookup_id_value id hyps with
-	   | None -> ABSTRACT
-	   | Some c -> failwith "caugth"
+	 if find_var id hyps then ABSTRACT else failwith "caugth"
        with Not_found -> failwith "caugth")
     ids_to_discard
 
@@ -110,7 +112,8 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
 	  Array.to_list lc))
       mib.mind_packets
   in
-  let hyps' = map_named_context (expmod_constr oldenv modlist) mib.mind_hyps in
+  let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) mib.mind_hyps in
+  let hyps' = map_named_context (expmod_constr oldenv modlist) hyps in
   let (inds',modl) = abstract_inductive ids_to_discard hyps' inds in
   let lmodif_one_mind i = 
     let nbc = Array.length (mind_nth_type_packet mib i).mind_consnames in 
@@ -355,15 +358,21 @@ let close_section _ s =
   let newdir = dirpath sec_sp in
   let olddir = wd_of_sp sec_sp in
   let (ops,ids,_) = 
-    List.fold_left 
-      (process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
-  in 
+    if Options.immediate_discharge then ([],[],([],[],[]))
+    else
+      List.fold_left 
+	(process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
+  in
+  let ids = last_section_hyps olddir in
   Global.pop_named_decls ids;
   Summary.unfreeze_lost_summaries fs;
   let mc = segment_contents decls in
-  add_anonymous_leaf (in_end_section (sec_sp,mc)); 
-  List.iter process_operation (List.rev ops) 
+  add_anonymous_leaf (in_end_section (sec_sp,mc));
+  if Options.immediate_discharge then ()
+  else
+    List.iter process_operation (List.rev ops)
 
 let save_module_to s f =
   Library.save_module_to segment_contents s f
 
+
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 91d65a5f9..f24051fd1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -77,8 +77,13 @@ let warning_or_error coe err =
   pPNL (hOV 0 [< 'sTR"Warning: "; st >])
 
 (* We build projections *)
-let declare_projections structref coers paramdecls fields =
-  let r = constr_of_reference Evd.empty (Global.env()) structref in
+let declare_projections indsp coers fields =
+  let mispec = Global.lookup_mind_specif (indsp,[||]) in
+  let paramdecls = Inductive.mis_params_ctxt mispec in
+  let paramdecls = 
+    List.map (fun (na,b,t) -> match na with Name id -> (id,b,t) | _ -> assert false)
+      paramdecls in
+  let r = constr_of_reference Evd.empty (Global.env()) (IndRef indsp) in
   let paramargs = List.rev (List.map (fun (id,_,_) -> mkVar id) paramdecls) in
   let rp = applist (r, paramargs) in
   let x = Environ.named_hd (Global.env()) r Anonymous in
@@ -107,6 +112,7 @@ let declare_projections structref coers paramdecls fields =
 	     it_mkNamedLambda_or_LetIn (mkLambda (x, rp, body)) paramdecls in
 	   let name = 
 	     try
+	       let proj = instantiate_inductive_section_params proj indsp in
 	       let cie = { const_entry_body = proj; const_entry_type = None} in
 	       let sp =
 		 declare_constant fi (ConstantEntry cie,NeverDischarge,false)
@@ -122,7 +128,7 @@ let declare_projections structref coers paramdecls fields =
 		 let constr_fi =
 		   constr_of_reference Evd.empty (Global.env()) refi in
 		 if coe then begin
-		   let cl = Class.class_of_ref structref in
+		   let cl = Class.class_of_ref (IndRef indsp) in
 		   Class.try_add_new_coercion_with_source 
 		     refi NeverDischarge cl
 		 end;
@@ -163,13 +169,13 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
       mind_entry_typename = idstruc;
       mind_entry_arity = mkSort s;
       mind_entry_consnames = [idbuild];
-     mind_entry_lc = [type_constructor] } in
+      mind_entry_lc = [type_constructor] } in
   let mie =
     { mind_entry_finite = true;
       mind_entry_inds = [mie_ind] } in
   let sp = declare_mutual_with_eliminations mie in
   let rsp = (sp,0) in (* This is ind path of idstruc *)
-  let sp_projs = declare_projections (IndRef rsp) coers params fields in
+  let sp_projs = declare_projections rsp coers fields in
   let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
   if is_coe then Class.try_add_new_coercion build NeverDischarge;
   Recordops.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index ac2c6836e..b678cc3e5 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -12,8 +12,7 @@ open Sign
    [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  global_reference -> bool list -> 
-    named_context -> named_context -> constant_path option list
+  inductive_path -> bool list -> named_context -> constant_path option list
 
 val definition_structure :
    bool * identifier * (identifier * Coqast.t) list *