deplacement de Discharge dans toplevel

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

12 files changed, 187 insertions, 39 deletions

diff --git a/.depend b/.depend
index 70c7cba1a7..61f230160b 100644
--- a/.depend
+++ b/.depend
@@ -175,7 +175,7 @@ dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi
 dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx 
 dev/top_printers.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
     kernel/closure.cmi toplevel/command.cmi kernel/constant.cmi \
-    parsing/coqast.cmi library/discharge.cmi parsing/egrammar.cmi \
+    parsing/coqast.cmi toplevel/discharge.cmi parsing/egrammar.cmi \
     tactics/elim.cmi kernel/environ.cmi parsing/esyntax.cmi kernel/evd.cmi \
     kernel/generic.cmi kernel/inductive.cmi parsing/lexer.cmi \
     library/libobject.cmi library/library.cmi toplevel/metasyntax.cmi \
@@ -190,7 +190,7 @@ dev/top_printers.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
     toplevel/vernacinterp.cmi 
 dev/top_printers.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
     kernel/closure.cmx toplevel/command.cmx kernel/constant.cmx \
-    parsing/coqast.cmx library/discharge.cmx parsing/egrammar.cmx \
+    parsing/coqast.cmx toplevel/discharge.cmx parsing/egrammar.cmx \
     tactics/elim.cmx kernel/environ.cmx parsing/esyntax.cmx kernel/evd.cmx \
     kernel/generic.cmx kernel/inductive.cmx parsing/lexer.cmx \
     library/libobject.cmx library/library.cmx toplevel/metasyntax.cmx \
@@ -345,10 +345,6 @@ library/declare.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
     kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
     library/declare.cmi 
-library/discharge.cmo: library/declare.cmi library/lib.cmi \
-    library/discharge.cmi 
-library/discharge.cmx: library/declare.cmx library/lib.cmx \
-    library/discharge.cmi 
 library/global.cmo: kernel/environ.cmi kernel/generic.cmi \
     kernel/inductive.cmi kernel/instantiate.cmi kernel/safe_typing.cmi \
     kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
@@ -843,6 +839,18 @@ toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
     lib/options.cmx lib/pp.cmx parsing/printer.cmx lib/profile.cmx \
     library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
     toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx 
+toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \
+    kernel/constant.cmi library/declare.cmi kernel/evd.cmi kernel/generic.cmi \
+    library/global.cmi kernel/inductive.cmi kernel/instantiate.cmi \
+    library/lib.cmi library/libobject.cmi kernel/names.cmi lib/pp.cmi \
+    pretyping/recordops.cmi kernel/reduction.cmi kernel/term.cmi lib/util.cmi \
+    toplevel/discharge.cmi 
+toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \
+    kernel/constant.cmx library/declare.cmx kernel/evd.cmx kernel/generic.cmx \
+    library/global.cmx kernel/inductive.cmx kernel/instantiate.cmx \
+    library/lib.cmx library/libobject.cmx kernel/names.cmx lib/pp.cmx \
+    pretyping/recordops.cmx kernel/reduction.cmx kernel/term.cmx lib/util.cmx \
+    toplevel/discharge.cmi 
 toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi kernel/inductive.cmi \
     parsing/lexer.cmi lib/options.cmi lib/pp.cmi kernel/type_errors.cmi \
     lib/util.cmi toplevel/errors.cmi 
@@ -915,7 +923,7 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
     toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     toplevel/class.cmi toplevel/command.cmi parsing/coqast.cmi \
-    library/declare.cmi library/discharge.cmi kernel/environ.cmi \
+    library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \
     kernel/evd.cmi parsing/extend.cmi library/global.cmi library/goptions.cmi \
     library/impargs.cmi library/lib.cmi library/libobject.cmi \
     library/library.cmi proofs/macros.cmi toplevel/metasyntax.cmi \
@@ -928,7 +936,7 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
     toplevel/class.cmx toplevel/command.cmx parsing/coqast.cmx \
-    library/declare.cmx library/discharge.cmx kernel/environ.cmx \
+    library/declare.cmx toplevel/discharge.cmx kernel/environ.cmx \
     kernel/evd.cmx parsing/extend.cmx library/global.cmx library/goptions.cmx \
     library/impargs.cmx library/lib.cmx library/libobject.cmx \
     library/library.cmx proofs/macros.cmx toplevel/metasyntax.cmx \
diff --git a/Makefile b/Makefile
index 3362abc8f7..5ab2271c45 100644
--- a/Makefile
+++ b/Makefile
@@ -68,8 +68,7 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
 LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \
 	library/global.cmo library/states.cmo library/library.cmo \
 	library/nametab.cmo library/impargs.cmo library/redinfo.cmo \
-        library/indrec.cmo library/declare.cmo library/discharge.cmo \
-        library/goptions.cmo
+        library/indrec.cmo library/declare.cmo library/goptions.cmo
 
 PRETYPING=pretyping/tacred.cmo pretyping/pretype_errors.cmo \
           pretyping/retyping.cmo pretyping/typing.cmo \
@@ -99,6 +98,7 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
 
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
          toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \
+         toplevel/discharge.cmo \
          toplevel/vernacentries.cmo toplevel/vernac.cmo toplevel/mltop.cmo \
 	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo \
          toplevel/usage.cmo toplevel/coqinit.cmo toplevel/coqtop.cmo
diff --git a/library/declare.ml b/library/declare.ml
index c756d6169f..b0ec976326 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -101,7 +101,7 @@ let declare_parameter id c =
  
 (* Constants. *)
 
-type constant_declaration = constant_entry * strength * bool
+type constant_declaration = constant_entry * strength
 
 let csttab = ref (Spmap.empty : constant_declaration Spmap.t)
 
@@ -110,13 +110,13 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
 	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
 
-let cache_constant (sp,((ce,_,_) as cd)) =
+let cache_constant (sp,((ce,_) as cd)) =
   Global.add_constant sp ce;
   Nametab.push (basename sp) sp;
   declare_constant_implicits sp;
   csttab := Spmap.add sp cd !csttab
 
-let load_constant (sp,((ce,_,_) as cd)) =
+let load_constant (sp,((ce,_) as cd)) =
   declare_constant_implicits sp;
   csttab := Spmap.add sp cd !csttab
 
@@ -184,7 +184,7 @@ let is_constant sp =
   try let _ = Global.lookup_constant sp in true with Not_found -> false
 
 let constant_strength sp = 
-  let (_,stre,_) = Spmap.find sp !csttab in stre
+  let (_,stre) = Spmap.find sp !csttab in stre
 
 let is_variable id = 
   let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab
@@ -294,8 +294,7 @@ let declare_eliminations sp i =
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
     declare_constant (id_of_string na)
-      ({ const_entry_body = c; const_entry_type = None },
-       NeverDischarge, false);
+      ({ const_entry_body = c; const_entry_type = None }, NeverDischarge);
     pPNL [< 'sTR na; 'sTR " is defined" >]
   in
   let env = Global.env () in
diff --git a/library/declare.mli b/library/declare.mli
index f5c2dff07c..15722dbc0a 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -23,7 +23,7 @@ type strength =
 type variable_declaration = constr * strength * bool
 val declare_variable : identifier -> variable_declaration -> unit
 
-type constant_declaration = constant_entry * strength * bool
+type constant_declaration = constant_entry * strength
 val declare_constant : identifier -> constant_declaration -> unit
 
 val declare_parameter : identifier -> constr -> unit
diff --git a/library/discharge.ml b/library/discharge.ml
deleted file mode 100644
index 17a70b2095..0000000000
--- a/library/discharge.ml
+++ /dev/null
@@ -1,6 +0,0 @@
-
-(* $Id$ *)
-
-open Declare
-
-let close_section _ s = Lib.close_section s
diff --git a/library/lib.ml b/library/lib.ml
index b9964a87f9..457a27f6e2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -132,7 +132,8 @@ let close_section s =
   lib_stk := before;
   add_entry sp (ClosedSection (s,after));
   add_frozen_state ();
-  pop_path_prefix ()
+  pop_path_prefix ();
+  (sp,after)
 
 (* The following function exports the whole library segment, that will be 
    saved as a module. Objects are presented in chronological order, and
diff --git a/library/lib.mli b/library/lib.mli
index 56bbcd59cf..3d87abe4db 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -34,7 +34,7 @@ val contents_after : section_path option -> library_segment
 (*s Opening and closing a section. *)
 
 val open_section : string -> section_path
-val close_section : string -> unit
+val close_section : string -> section_path * library_segment
 
 val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> string list
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6e6114f901..12f53c685d 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -175,8 +175,7 @@ let save_named opacity =
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in 
   declare_constant (id_of_string ident)
-    ({ const_entry_body = pfterm; const_entry_type = Some concl },
-      strength, opacity);
+    ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength);
   del_proof ident;
   message(ident ^ " is defined")
     
@@ -188,13 +187,11 @@ let save_anonymous opacity save_ident n =
   let pfterm = extract_pftreestate pfs in 
   if ident = "Unnamed_thm" then
     declare_constant (id_of_string save_ident)
-      ({ const_entry_body = pfterm; const_entry_type = Some concl },
-       strength, opacity)
+      ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength)
   else begin
     message("Overriding name " ^ ident ^ " and using " ^ save_ident);
     declare_constant (id_of_string save_ident)
-      ({ const_entry_body = pfterm; const_entry_type = Some concl },
-       strength, opacity)
+      ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength)
   end;
   del_proof ident;
   message(save_ident ^ " is defined")
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 35e8e5b87a..d4cd6fec6c 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -290,7 +290,7 @@ let build_id_coercion idf_opt ids =
                         (string_of_cl (fst (constructor_at_head t)))) 
   in
   let constr_entry = {const_entry_body = constr_f; const_entry_type = None } in
-  declare_constant idf (constr_entry,NeverDischarge,false);
+  declare_constant idf (constr_entry,NeverDischarge);
   idf
 
 let coercion_syntax_entry id n =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 217acdb0a1..882033919d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -40,7 +40,7 @@ let constant_entry_of_com com =
 
 let definition_body ident n com = 
   let ce = constant_entry_of_com com in
-  declare_constant ident (ce,n,false)
+  declare_constant ident (ce,n)
 
 let red_constant_entry ce = function
   | None -> ce
@@ -53,7 +53,7 @@ let red_constant_entry ce = function
 let definition_body_red ident n com red_option = 
   let ce = constant_entry_of_com com in
   let ce' = red_constant_entry ce red_option in
-  declare_constant ident (ce',n,false)
+  declare_constant ident (ce',n)
 
 let syntax_definition ident com =
   let c = raw_constr_of_com Evd.empty (Global.context()) com in 
@@ -236,7 +236,7 @@ let build_recursive lnameargsardef =
 	  let ce = { const_entry_body = 
 		       mkFixDlam (Array.of_list nvrec) i varrec recvec;
 		     const_entry_type = None } in
-	  declare_constant fi (ce, n, false);
+	  declare_constant fi (ce, n);
           declare (i+1) lf
       | _ -> () 
     in 
@@ -251,7 +251,7 @@ let build_recursive lnameargsardef =
       (fun subst (f,def) ->
 	 let ce = { const_entry_body = Generic.replace_vars subst def;
 		    const_entry_type = None } in
-	 declare_constant f (ce,n,false);
+	 declare_constant f (ce,n);
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst lnamerec)
@@ -300,7 +300,7 @@ let build_corecursive lnameardef =
 	  let ce = { const_entry_body = 
 		       mkCoFixDlam i (Array.of_list larrec) recvec;
 		     const_entry_type = None } in
-          declare_constant fi (ce,n,false);
+          declare_constant fi (ce,n);
           declare (i+1) lf
       | _        -> () 
     in 
@@ -314,7 +314,7 @@ let build_corecursive lnameardef =
       (fun subst (f,def) ->
 	 let ce = { const_entry_body = Generic.replace_vars subst def;
 		    const_entry_type = None } in
-	 declare_constant f (ce,n,false);
+	 declare_constant f (ce,n);
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst lnamerec)
@@ -338,7 +338,7 @@ let build_scheme lnamedepindsort =
     | fi::lf -> 
 	let ce = 
 	  { const_entry_body = listdecl.(i); const_entry_type = None } in
-	declare_constant fi (ce,n,false);
+	declare_constant fi (ce,n);
         declare (i+1) lf
     | _        -> ()
   in 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
new file mode 100644
index 0000000000..bd605b53eb
--- /dev/null
+++ b/toplevel/discharge.ml
@@ -0,0 +1,149 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Constant
+open Inductive
+open Instantiate
+open Reduction
+open Libobject
+open Lib
+open Declare
+open Classops
+open Class
+open Recordops
+
+let recalc_sp sp =
+  let (_,spid,k) = repr_path sp in Lib.make_path spid k
+
+let expmod_constr modlist c =
+  let env = Global.env() in
+  let sigma = Evd.empty in
+  let simpfun = if modlist = [] then fun x -> x else nf_betaiota env sigma in
+  let expfun c = 
+    let (sp,_) = destConst c in 
+    try 
+      constant_value env c
+    with Failure _ -> begin
+      mSGERRNL 
+	[< 'sTR"Cannot unfold the value of " ;
+           'sTR(string_of_path sp) ; 'sPC;
+           'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
+           'sTR"and then require that theorems which use them"; 'sPC;
+           'sTR"be transparent" >];
+      let cb = Global.lookup_constant sp in
+      cb.const_opaque <- false;
+      (try
+         let v = constant_value env c in 
+	 cb.const_opaque <- true; 
+	 v
+       with _ -> anomaly "expmod_constr")
+    end
+  in
+  let under_casts f = function
+    | DOP2(Cast,c,t) -> (DOP2(Cast,f c,f t))
+    | c -> f c 
+  in
+  let c' = modify_opers expfun (fun a b -> mkAppL [|a; b|]) modlist c in
+  match c' with
+    | DOP2(Cast,val_0,typ) -> DOP2(Cast,simpfun val_0,simpfun typ)
+    | DOP2(XTRA "IND",c,DLAMV(na,lc)) ->
+	DOP2(XTRA "IND",under_casts simpfun c,
+             DLAMV(na,Array.map (under_casts simpfun) lc))
+    | _ -> simpfun c'
+
+let expmod_type modlist {body=c;typ=s} = {body=expmod_constr modlist c;typ=s}
+
+let process_constant (ids_to_discard,work_alist) cb =
+  failwith "todo"
+
+let process_inductive (ids_to_discard,work_alist) mib =
+  failwith "todo"
+
+let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) =
+  let tag = object_tag lobj in 
+  match tag with
+    | "VARIABLE" ->
+	let (id,a,stre,sticky) = out_variable sp in
+	if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then
+	  (id::ids_to_discard,work_alist)
+	else begin
+	  let expmod_a = expmod_constr work_alist a.body in
+	  declare_variable id (expmod_a,stre,sticky);
+          (ids_to_discard,work_alist)
+	end
+	  
+    | "CONSTANT" ->
+	let stre = constant_strength sp in
+	if stre = (DischargeAt sec_sp) then
+	  (ids_to_discard, (Const sp, DO_REPLACE) :: work_alist)
+	else begin
+	  let cb = Global.lookup_constant sp in
+	  let ((_,spid,spk)) = repr_path sp in
+	  let ce = process_constant (ids_to_discard,work_alist) cb in
+	  declare_constant spid (ce,stre);
+          (ids_to_discard,work_alist)
+	end
+	  
+    | "INDUCTIVE" ->
+	let mib = Global.lookup_mind sp in
+	let ((_,spid,spk)) = repr_path sp in
+	let mie = process_inductive (ids_to_discard,work_alist) mib in
+	let _ = declare_mind mie in
+        (ids_to_discard,work_alist)
+
+    | "CLASS" -> 
+	let ((cl,clinfo) as x) = outClass lobj in
+	if clinfo.cL_STRE = (DischargeAt sec_sp) then 
+	  (ids_to_discard,work_alist)
+	else begin 
+	  let y = process_class sec_sp x in
+          Lib.add_anonymous_leaf (inClass y);
+          (ids_to_discard,work_alist)
+	end
+	  
+    | "COERCION" -> 
+	let (((_,coeinfo),_,_)as x) = outCoercion lobj in
+        if coeinfo.cOE_STRE = (DischargeAt sec_sp) then 
+	  (ids_to_discard,work_alist)
+        else begin 
+	  let ((_,_,clt) as y),idf,ps = process_coercion sec_sp x in
+          Lib.add_anonymous_leaf (inCoercion y); 
+          coercion_syntax idf ps clt;
+          (ids_to_discard,work_alist)
+	end
+                    
+    | "STRUCTURE" ->
+	let (sp,info) = outStruc lobj in
+	let newsp = recalc_sp sp in
+	let mib = Global.lookup_mind (ccisp_of newsp) in
+	let strobj =
+	  { s_CONST= info.s_CONST;
+	    s_PARAM= mib.mind_nparams;
+	    s_PROJ= List.map (option_app recalc_sp) info.s_PROJ} in
+	Lib.add_anonymous_leaf (inStruc (newsp,strobj));
+	(ids_to_discard,work_alist)
+
+    (***TODO
+    | "OBJDEF1" -> 
+	let sp = outObjDef1 lobj in
+        let ((_,spid,_)) = repr_path sp in
+        begin try objdef_declare spid with _ -> () end;
+        (ids_to_discard,work_alist)
+    ***)
+
+    | _ -> 
+	(ids_to_discard,work_alist)
+
+let process_item sec_sp acc = function
+  | (sp,Leaf lobj) -> process_object sec_sp acc (sp,lobj)
+  | (_,_) -> acc
+
+let close_section _ s = 
+  let (sec_sp,decls) = close_section s in
+  let _ = List.fold_left (process_item sec_sp) ([],[]) decls in 
+  ()
diff --git a/library/discharge.mli b/toplevel/discharge.mli
index 34b8bd1c7f..34b8bd1c7f 100644
--- a/library/discharge.mli
+++ b/toplevel/discharge.mli