Modules dans COQ\!\!\!\!

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

1 files changed, 50 insertions, 38 deletions

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 14e4feff5..93277300b 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -15,11 +15,13 @@ open Nameops
 open Sign
 open Term
 open Declarations
+open Entries
 open Inductive
 open Instantiate
 open Reduction
 open Cooking
 open Typeops
+open Libnames
 open Libobject
 open Lib
 open Nametab
@@ -33,7 +35,11 @@ open Indtypes
 open Nametab
 
 let recalc_sp dir sp =
-  let (_,spid) = repr_path sp in Names.make_path dir spid
+  let (_,spid) = repr_path sp in Libnames.make_path dir spid
+
+let recalc_kn dir kn = 
+  let (mp,_,l) = Names.repr_kn kn in
+    Names.make_kn mp dir l
 
 let rec find_var id = function
   | [] -> false
@@ -93,8 +99,8 @@ let abstract_inductive ids_to_abs hyps inds =
 	 let params' =
 	   List.map 
 	     (function
-		| (Name id,None,p) -> id, LocalAssum p
-		| (Name id,Some p,_) -> id, LocalDef p
+		| (Name id,None,p) -> id, Entries.LocalAssum p
+		| (Name id,Some p,_) -> id, Entries.LocalDef p
 		| (Anonymous,_,_) -> anomaly"Unnamed inductive local variable")
 	     params in
 	 { mind_entry_params = params';
@@ -170,20 +176,21 @@ type opacity = bool
 
 type discharge_operation = 
   | Variable of identifier * section_variable_entry * strength * bool
-  | Constant of section_path * recipe * strength * bool
+  | Constant of identifier * recipe * strength * constant * bool
   | Inductive of mutual_inductive_entry * bool
   | Class of cl_typ * cl_info_typ
   | Struc of inductive * (unit -> struc_typ)
   | Objdef of constant
   | Coercion of coercion_entry
-  | Require of module_reference
+  | Require of library_reference
   | Constraints of Univ.constraints
 
 (* Main function to traverse the library segment and compute the various
    discharge operations. *)
 
-let process_object oldenv dir sec_sp
-  (ops,ids_to_discard,(constl,indl,cstrl as work_alist)) (sp,lobj) =
+let process_object oldenv olddir full_olddir newdir  
+(* {dir -> newdir} {sec_sp -> full_olddir, olddir} *)
+  (ops,ids_to_discard,(constl,indl,cstrl as work_alist)) ((sp,kn),lobj) =
   let tag = object_tag lobj in 
   match tag with
     | "VARIABLE" ->
@@ -222,60 +229,63 @@ let process_object oldenv dir sec_sp
 	  (ops, ids_to_discard, (constl,indl,cstrl))
 	else
 *)
-	let cb = Environ.lookup_constant sp oldenv in
-	let imp = is_implicit_constant sp in
-	let newsp = match stre with
-	  | DischargeAt (d,_) when not (is_dirpath_prefix_of d dir) -> sp
-	  | _ -> recalc_sp dir sp in
+	let kn = Nametab.locate_constant (qualid_of_sp sp) in
+	let lab = label kn in
+	let cb = Environ.lookup_constant kn oldenv in
+	let imp = is_implicit_constant kn in
+	let newkn = (*match stre with (* this did not work anyway...*)
+	  | DischargeAt (d,_) when not (is_dirpath_prefix_of d dir) -> kn
+	  | _ -> *)recalc_kn newdir kn in
         let mods = 
 	  let abs_vars = build_abstract_list cb.const_hyps ids_to_discard in
-	  [ (sp, DO_ABSTRACT(newsp,abs_vars)) ]
+	  [ (kn, DO_ABSTRACT(newkn,abs_vars)) ]
 	in
 	let r = { d_from = cb;
 	          d_modlist = work_alist;
 	          d_abstract = ids_to_discard } in
-	let op = Constant (newsp,r,stre,imp) in
+	let op = Constant (id_of_label lab, r,stre,newkn,imp) in
         (op :: ops, ids_to_discard, (mods@constl, indl, cstrl))
   
     | "INDUCTIVE" ->
-	let mib = Environ.lookup_mind sp oldenv in
-	let newsp = recalc_sp dir sp in
+	let kn = Nametab.locate_mind (qualid_of_sp sp) in
+	let mib = Environ.lookup_mind kn oldenv in
+	let newkn = recalc_kn newdir kn in
 	let imp = is_implicit_args() (* CHANGE *) in
 	let (mie,indmods,cstrmods) = 
-	  process_inductive sp newsp oldenv (ids_to_discard,work_alist) mib in
+	  process_inductive kn newkn oldenv (ids_to_discard,work_alist) mib in
 	((Inductive(mie,imp)) :: ops, ids_to_discard,
 	 (constl,indmods@indl,cstrmods@cstrl))
 
     | "CLASS" -> 
 	let ((cl,clinfo) as x) = outClass lobj in
-	if (match clinfo.cl_strength with DischargeAt (sp,_) -> sp = sec_sp | _ -> false) then 
+	if (match clinfo.cl_strength with DischargeAt (dp,_) -> dp = full_olddir | _ -> false) then 
 	  (ops,ids_to_discard,work_alist)
 	else
-	  let (y1,y2) = process_class sec_sp ids_to_discard x in
+	  let (y1,y2) = process_class olddir ids_to_discard x in
           ((Class (y1,y2))::ops, ids_to_discard, work_alist)
 	  
     | "COERCION" -> 
 	let (((_,coeinfo),_,_)as x) = outCoercion lobj in
-	if (match coercion_strength coeinfo with DischargeAt (sp,_) -> sp = sec_sp | _ -> false) then 
+	if (match coercion_strength coeinfo with DischargeAt (dp,_) -> dp = full_olddir | _ -> false) then 
 	  (ops,ids_to_discard,work_alist)
         else
-	  let y = process_coercion sec_sp ids_to_discard x in
+	  let y = process_coercion olddir ids_to_discard x in
           ((Coercion y)::ops, ids_to_discard, work_alist)
                     
     | "STRUCTURE" ->
-	let ((sp,i),info) = outStruc lobj in
-	let newsp = recalc_sp dir sp in
+	let ((kn,i),info) = outStruc lobj in
+	let newkn = recalc_kn newdir kn in
 	let strobj () =
-	  let mib = Environ.lookup_mind newsp (Global.env ()) in
+	  let mib = Environ.lookup_mind newkn (Global.env ()) in
 	  { s_CONST = info.s_CONST;
 	    s_PARAM = mib.mind_packets.(0).mind_nparams;
-	    s_PROJ = List.map (option_app (recalc_sp dir)) info.s_PROJ } in
-	((Struc ((newsp,i),strobj))::ops, ids_to_discard, work_alist)
+	    s_PROJ = List.map (option_app (fun kn -> recalc_kn newdir kn)) info.s_PROJ } in
+	((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist)
 
     | "OBJDEF1" -> 
-	let sp = outObjDef1 lobj in
-	let new_sp = recalc_sp dir sp in
-        ((Objdef new_sp)::ops, ids_to_discard, work_alist)
+	let kn = outObjDef1 lobj in
+	let new_kn = recalc_kn newdir kn in
+        ((Objdef new_kn)::ops, ids_to_discard, work_alist)
 
     | "REQUIRE" -> 
 	let c = out_require lobj in
@@ -283,8 +293,9 @@ let process_object oldenv dir sec_sp
 
     | _ -> (ops,ids_to_discard,work_alist)
 
-let process_item oldenv dir sec_sp acc = function
-  | (sp,Leaf lobj) -> process_object oldenv dir sec_sp acc (sp,lobj)
+let process_item oldenv olddir full_olddir newdir acc = function
+  | (sp,Leaf lobj) -> 
+      process_object oldenv olddir full_olddir newdir  acc (sp,lobj)
   | (_,_) -> acc
 
 let process_operation = function
@@ -293,9 +304,9 @@ let process_operation = function
       let _ =
         with_implicits imp (declare_variable id) (Lib.cwd(),expmod_a,stre) in
       ()
-  | Constant (sp,r,stre,imp) ->
-      with_implicits imp (redeclare_constant sp) (r,stre);
-      constant_message (basename sp)
+  | Constant (id,r,stre,kn,imp) ->
+      with_implicits imp (redeclare_constant id) (r,stre);
+      constant_message id
   | Inductive (mie,imp) ->
       let _ = with_implicits imp declare_mind mie in
       inductive_message mie.mind_entry_inds
@@ -306,7 +317,7 @@ let process_operation = function
   | Objdef newsp ->
       begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end
   | Coercion y -> add_new_coercion y
-  | Require y -> reload_module y
+  | Require y -> reload_library y
   | Constraints y -> Global.add_constraints y
 
 let catch_not_found f x =
@@ -317,13 +328,14 @@ let catch_not_found f x =
 
 let close_section _ s = 
   let oldenv = Global.env() in
-  let olddir,decls,fs = close_section false s in
+  let prefix,decls,fs = close_section false s in
+  let full_olddir, (_,olddir) = prefix in
   let newdir = fst (split_dirpath olddir) in
   let (ops,ids,_) = 
     List.fold_left 
-      (process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
+      (process_item oldenv olddir full_olddir newdir) ([],[],([],[],[])) decls 
   in
   let ids = last_section_hyps olddir in
   Summary.unfreeze_lost_summaries fs;
   catch_not_found (List.iter process_operation) (List.rev ops);
-  Nametab.push_section olddir
+  Nametab.push_dir (Until 1) full_olddir (DirClosedSection full_olddir)