nouveau discharge fait par le noyau; plus de recettes dans les corps des constantes

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

4 files changed, 53 insertions, 222 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index d51cf629c4..1a236c3ff7 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -33,29 +33,26 @@ let constant_entry_of_com (com,comtypopt) =
   let env = Global.env() in
   match comtypopt with
       None -> 
-	{ const_entry_body = Cooked (interp_constr sigma env com);
+	{ const_entry_body = interp_constr sigma env com;
 	  const_entry_type = None }
     | Some comtyp ->
 	let typ = interp_type sigma env comtyp in
-	{ const_entry_body = Cooked (interp_casted_constr sigma env com typ);
+	{ const_entry_body = interp_casted_constr sigma env com typ;
 	  const_entry_type = Some typ }
 
 let red_constant_entry ce = function
   | None -> ce
   | Some red ->
-      let body = match ce.const_entry_body with
-	| Cooked c -> c
-	| Recipe _ -> assert false
-      in
+      let body = ce.const_entry_body in
       { const_entry_body = 
-	  Cooked (reduction_of_redexp red (Global.env()) Evd.empty body); 
+	  reduction_of_redexp red (Global.env()) Evd.empty body; 
 	const_entry_type = 
 	  ce.const_entry_type }
 
 let definition_body_red ident n com comtypeopt red_option = 
   let ce = constant_entry_of_com (com,comtypeopt) in
   let ce' = red_constant_entry ce red_option in
-  declare_constant ident (ce',n);
+  declare_constant ident (ConstantEntry ce',n);
   if is_verbose() then message ((string_of_id ident) ^ " is defined")
 
 let definition_body ident n com typ = definition_body_red ident n com typ None
@@ -237,13 +234,12 @@ let build_recursive lnameargsardef =
       | fi::lf ->
 	  let ce = 
 	    { const_entry_body =
-		Cooked 
-		  (mkFix ((Array.of_list nvrec,i),
-			  (varrec,List.map (fun id -> Name id) lnamerec,
-			   recvec)));
+		mkFix ((Array.of_list nvrec,i),
+		       (varrec,List.map (fun id -> Name id) lnamerec,
+			recvec));
 	      const_entry_type = None } 
 	  in
-	  declare_constant fi (ce, n);
+	  declare_constant fi (ConstantEntry ce, n);
           declare (i+1) lf
       | _ -> () 
     in 
@@ -256,9 +252,9 @@ let build_recursive lnameargsardef =
   let _ = 
     List.fold_left
       (fun subst (f,def) ->
-	 let ce = { const_entry_body = Cooked (replace_vars subst def);
+	 let ce = { const_entry_body = replace_vars subst def;
 		    const_entry_type = None } in
-	 declare_constant f (ce,n);
+	 declare_constant f (ConstantEntry ce,n);
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst lnamerec)
@@ -308,12 +304,11 @@ let build_corecursive lnameardef =
       | fi::lf ->
 	  let ce = 
 	    { const_entry_body =
-		Cooked 
-		  (mkCoFix (i, (varrec,List.map (fun id -> Name id) lnamerec,
-			      recvec)));
+		mkCoFix (i, (varrec,List.map (fun id -> Name id) lnamerec,
+			     recvec));
 	      const_entry_type = None } 
 	  in
-          declare_constant fi (ce,n);
+          declare_constant fi (ConstantEntry ce,n);
           declare (i+1) lf
       | _        -> () 
     in 
@@ -324,9 +319,9 @@ let build_corecursive lnameardef =
   let _ = 
     List.fold_left
       (fun subst (f,def) ->
-	 let ce = { const_entry_body = Cooked (replace_vars subst def);
+	 let ce = { const_entry_body = replace_vars subst def;
 		    const_entry_type = None } in
-	 declare_constant f (ce,n);
+	 declare_constant f (ConstantEntry ce,n);
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst lnamerec)
@@ -358,8 +353,8 @@ let build_scheme lnamedepindsort =
   let n = NeverDischarge in 
   let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in 
   let rec declare decl fi =
-    let ce = { const_entry_body = Cooked decl; const_entry_type = None } 
-    in declare_constant fi (ce,n)
+    let ce = { const_entry_body = decl; const_entry_type = None } 
+    in declare_constant fi (ConstantEntry ce,n)
   in 
   List.iter2 declare listdecl lrecnames; 
   if is_verbose() then pPNL(recursive_message lrecnames)
@@ -377,7 +372,7 @@ let start_proof_com sopt stre com =
 
 let save_named opacity =
   let id,(const,strength) = Pfedit.cook_proof () in
-  declare_constant id (const,strength);
+  declare_constant id (ConstantEntry const,strength);
   Pfedit.delete_current_proof ();
   if Options.is_verbose() then message ((string_of_id id) ^ " is defined")
 
@@ -385,7 +380,7 @@ let save_anonymous opacity save_ident strength =
   let id,(const,_) = Pfedit.cook_proof () in
   if atompart_of_id id <> "Unnamed_thm" then
     message("Overriding name "^(string_of_id id)^" and using "^save_ident);
-  declare_constant (id_of_string save_ident) (const,strength);
+  declare_constant (id_of_string save_ident) (ConstantEntry const,strength);
   Pfedit.delete_current_proof ();
   if Options.is_verbose() then message (save_ident ^ " is defined")
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 2e64ccab17..b922aa13e7 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -10,6 +10,7 @@ open Declarations
 open Inductive
 open Instantiate
 open Reduction
+open Cooking
 open Typeops
 open Libobject
 open Lib
@@ -22,102 +23,14 @@ open Recordops
 let recalc_sp sp =
   let (_,spid,k) = repr_path sp in Lib.make_path spid k
 
-(* Abstractions. *)
+let build_abstract_list hyps ids_to_discard =
+  map_succeed 
+    (fun id -> 
+       if not (mem_named_context id hyps) then failwith "caugth"; ABSTRACT)
+    ids_to_discard
 
-let whd_all c = whd_betadeltaiota (Global.env()) Evd.empty c
-
-type modification_action = ABSTRACT | ERASE
-
-let interp_modif absfun oper (oper',modif) cl = 
-  let rec interprec = function
-    | ([], cl) -> 
-	(match oper' with
-	   | ConstRef sp -> mkConst (sp,Array.of_list cl)
-	   | ConstructRef sp -> mkMutConstruct (sp,Array.of_list cl)
-	   | IndRef sp -> mkMutInd (sp,Array.of_list cl))
-    | (ERASE::tlm, c::cl) -> interprec (tlm,cl)
-    | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c
-    | _ -> assert false
-  in 
-  interprec (modif,cl)
-
-type 'a modification =
-  | NOT_OCCUR
-  | DO_ABSTRACT of 'a * modification_action list
-  | DO_REPLACE
-
-let modify_opers replfun absfun oper_alist =
-  let failure () =
-    anomalylabstrm "generic__modify_opers"
-      [< 'sTR"An oper which was never supposed to appear has just appeared" ;
-         'sPC ; 'sTR"Either this is in system code, and you need to" ; 'sPC;
-         'sTR"report this error," ; 'sPC ;
-         'sTR"Or you are using a user-written tactic which calls" ; 'sPC ;
-         'sTR"generic__modify_opers, in which case the user-written code" ;
-         'sPC ; 'sTR"is broken - this function is an internal system" ;
-         'sPC ; 'sTR"for internal system use only" >]
-  in
-  let rec substrec c =
-    let op, cl = splay_constr c in
-    let cl' = Array.map substrec cl in
-    match op with
-      (* Hack pour le sp dans l'annotation du Cases *)
-      | OpMutCase (n,(spi,a,b,c,d) as oper) ->
-	  (try
-	     match List.assoc (IndRef spi) oper_alist with
-	       | DO_ABSTRACT (IndRef spi',_) ->
-		   gather_constr (OpMutCase (n,(spi',a,b,c,d)),cl')
-	       | _ -> raise Not_found
-	   with
-	     | Not_found -> gather_constr (op,cl'))
-
-      | OpMutInd spi ->
-	  (try
-	     (match List.assoc (IndRef spi) oper_alist with
-		| NOT_OCCUR -> failure ()
-		| DO_ABSTRACT (oper',modif) ->
-		    if List.length modif > Array.length cl then
-		      anomaly "found a reference with too few args"
-		    else 
-		      interp_modif absfun (IndRef spi) (oper',modif)
-			(Array.to_list cl')
-		| DO_REPLACE -> assert false)
-	   with 
-	     | Not_found -> mkMutInd (spi,cl'))
-
-      | OpMutConstruct spi ->
-	  (try
-	     (match List.assoc (ConstructRef spi) oper_alist with
-		| NOT_OCCUR -> failure ()
-		| DO_ABSTRACT (oper',modif) ->
-		    if List.length modif > Array.length cl then
-		      anomaly "found a reference with too few args"
-		    else 
-		      interp_modif absfun (ConstructRef spi) (oper',modif)
-			(Array.to_list cl')
-		| DO_REPLACE -> assert false)
-	   with 
-	     | Not_found -> mkMutConstruct (spi,cl'))
-
-      | OpConst sp ->
-	  (try
-	     (match List.assoc (ConstRef sp) oper_alist with
-		| NOT_OCCUR -> failure ()
-		| DO_ABSTRACT (oper',modif) ->
-		    if List.length modif > Array.length cl then
-		      anomaly "found a reference with too few args"
-		    else 
-		      interp_modif absfun (ConstRef sp) (oper',modif)
-			(Array.to_list cl')
-		| DO_REPLACE -> substrec (replfun (sp,cl')))
-	   with 
-	     | Not_found -> mkConst (sp,cl'))
-  
-    | _ -> gather_constr (op, cl')
-  in 
-  if oper_alist = [] then fun x -> x else substrec
-
-(**)
+(* Discharge of inductives is done here (while discharge of constants 
+   is done by the kernel for efficiency). *)
 
 let abstract_inductive ids_to_abs hyps inds =
   let abstract_one_var d inds =
@@ -153,72 +66,6 @@ let abstract_inductive ids_to_abs hyps inds =
       inds' in
   (inds'', List.rev revmodl)
 
-let abstract_constant ids_to_abs hyps (body,typ) =
-  let abstract_once ((hyps,body,typ,modl) as sofar) id =
-    match hyps with
-      | [] -> sofar
-      | (hyp,c,t as decl)::rest ->
-    if hyp <> id then sofar
-    else
-      let body' = match body with
-	| None -> None
-	| Some { contents = Cooked c } -> 
-	    Some (ref (Cooked (mkNamedLambda_or_LetIn decl c)))
-	| Some { contents = Recipe f } ->
-	    Some (ref (Recipe (fun () -> mkNamedLambda_or_LetIn decl (f()))))
-      in
-      let typ' = mkNamedProd_or_LetIn decl typ in
-      (rest, body', typ', ABSTRACT::modl)
-  in
-  let (_,body',typ',revmodl) =
-    List.fold_left abstract_once (hyps,body,typ,[]) ids_to_abs in
-  (body',typ', List.rev revmodl)
-
-
-(* Substitutions. *)
-
-let expmod_constr oldenv modlist c =
-  let sigma = Evd.empty in
-  let simpfun = 
-    if modlist = [] then fun x -> x else nf_betaiota oldenv sigma in
-  let expfun cst = 
-    try 
-      constant_value oldenv cst
-    with NotEvaluableConst Opaque ->
-      let (sp,_) = cst in
-      errorlabstrm "expmod_constr"
-	[< '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" >];
-  in
-  let under_casts f c = match kind_of_term c with
-    | IsCast (c,t) -> mkCast (f c,f t)
-    | _ -> f c 
-  in
-  let c' = modify_opers expfun (fun a b -> mkApp (a, [|b|])) modlist c in
-  match kind_of_term c' with
-    | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ)
-    | _ -> simpfun c'
-
-let expmod_type oldenv modlist c =
-  type_app (expmod_constr oldenv modlist) c
-
-let expmod_constant_value opaque oldenv modlist = function
-  | None -> None
-  | Some { contents = Cooked c } -> 
-      if opaque then 
-	(* None *)
-        Some (ref (Recipe (fun () -> expmod_constr oldenv modlist c)))
-      else
-	Some (ref (Cooked (expmod_constr oldenv modlist c)))
-  | Some { contents = Recipe f } -> 
-      Some (ref (Recipe (fun () -> expmod_constr oldenv modlist (f ()))))
-
-
-(* Discharge of inductive types. *)
-
 let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
   assert (Array.length mib.mind_packets > 0);
   let finite = mib.mind_packets.(0).mind_finite in
@@ -250,24 +97,10 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
      mind_entry_inds = inds' },
    modifs)
 
-
-(* Discharge of constants. *)
-
-let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
-  let body = 
-    expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in
-  let typ = expmod_type oldenv modlist cb.const_type in
-  let hyps = map_named_context (expmod_constr oldenv modlist) cb.const_hyps in
-  let (body',typ',modl) = abstract_constant ids_to_discard hyps (body,typ) in
-  let mods = [ (ConstRef osecsp, DO_ABSTRACT(ConstRef nsecsp,modl)) ] in
-  (body', body_of_type typ', mods)
-
-
-(* Discharge of the various objects of the environment. *)
+(* Discharge messages. *)
 
 let constant_message id =
-  if Options.is_verbose() then 
-    pPNL [< print_id id; 'sTR " is discharged." >]
+  if Options.is_verbose() then pPNL [< print_id id; 'sTR " is discharged." >]
 
 let inductive_message inds =
   if Options.is_verbose() then 
@@ -279,16 +112,21 @@ let inductive_message inds =
 			   (fun (id,_,_,_) -> print_id id) l;
 			 'sPC; 'sTR "are discharged.">]))
 
+(* Discharge operations for the various objects of the environment. *)
+
 type discharge_operation = 
   | Variable of identifier * section_variable_entry * strength * bool * bool
   | Parameter of identifier * constr * bool
-  | Constant of identifier * constant_entry * strength * bool
+  | Constant of identifier * recipe * strength * bool
   | Inductive of mutual_inductive_entry * bool
   | Class of cl_typ * cl_info_typ
   | Struc of inductive_path * struc_typ
   | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ) 
               * identifier * int 
 
+(* Main function to traverse the library segment and compute the various
+   discharge operations. *)
+
 let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
   let tag = object_tag lobj in 
   match tag with
@@ -319,17 +157,15 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
 	  let spid = basename sp in
 	  let imp = is_implicit_constant sp in
 	  let newsp = recalc_sp sp in
-	  let (body,typ,mods) = 
-	    process_constant sp newsp oldenv (ids_to_discard,work_alist) cb in
-	  let op = match body with
-	    | None -> 
-		Parameter (spid,typ,imp)
-	    | Some { contents = b } -> 
-		let ce = 
-		  { const_entry_body = b; const_entry_type = Some typ } in
-		Constant (spid,ce,stre,imp)
+	  let mods = 
+	    let modl = build_abstract_list cb.const_hyps ids_to_discard in
+	    [ (ConstRef sp, DO_ABSTRACT(ConstRef newsp,modl)) ] 
 	  in
-          (op::ops, ids_to_discard, mods@work_alist)
+	  let r = { d_from = sp;
+		    d_modlist = work_alist;
+		    d_abstract = ids_to_discard } in
+	  let op = Constant (spid,r,stre,imp) in
+          (op :: ops, ids_to_discard, mods @ work_alist)
   
     | "INDUCTIVE" ->
 	let mib = Environ.lookup_mind sp oldenv in
@@ -337,7 +173,7 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
 	let imp = is_implicit_inductive_definition sp in
 	let (mie,mods) = 
 	  process_inductive sp newsp oldenv (ids_to_discard,work_alist) mib in
-	((Inductive(mie,imp))::ops, ids_to_discard, mods@work_alist)
+	((Inductive(mie,imp)) :: ops, ids_to_discard, mods @ work_alist)
 
     | "CLASS" -> 
 	let ((cl,clinfo) as x) = outClass lobj in
@@ -386,8 +222,8 @@ let process_operation = function
   | Parameter (spid,typ,imp) ->
       with_implicits imp (declare_parameter spid) typ;
       constant_message spid
-  | Constant (spid,ce,stre,imp) ->
-      with_implicits imp (declare_constant spid) (ce,stre);
+  | Constant (spid,r,stre,imp) ->
+      with_implicits imp (declare_constant spid) (ConstantRecipe r,stre);
       constant_message spid
   | Inductive (mie,imp) ->
       let _ = with_implicits imp declare_mind mie in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 559c3f33f5..d377b46e8c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -140,9 +140,9 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
 	   let ok = 
 	     try
 	       let cie =
-		 { const_entry_body = Cooked proj;
+		 { const_entry_body = proj;
 		   const_entry_type = None } in
-	       (declare_constant fi (cie,NeverDischarge); true)
+	       (declare_constant fi (ConstantEntry cie,NeverDischarge); true)
              with Type_errors.TypeError (k,ctx,te) ->
                ((warning_or_error coe 
                    [<'sTR (string_of_id fi); 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index dffccf3f9c..114665bada 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -459,13 +459,13 @@ let _ =
               save_anonymous_remark true (string_of_id id))
        | _ -> bad_vernac_args "SaveAnonymousRmk")
 
-(***
 let _ =
   add "TRANSPARENT"
     (fun id_list () ->
        List.iter 
 	 (function 
-	    | VARG_IDENTIFIER id -> set_transparent id
+	    | VARG_IDENTIFIER id -> 
+		let sp = Nametab.sp_of_id CCI id in Global.set_transparent sp
 	    |   _  -> bad_vernac_args "TRANSPARENT")
 	 id_list)
     
@@ -474,10 +474,10 @@ let _ =
     (fun id_list () ->
        List.iter
 	 (function 
-	    | VARG_IDENTIFIER id -> set_opaque id
+	    | VARG_IDENTIFIER id -> 
+		let sp = Nametab.sp_of_id CCI id in Global.set_opaque sp
 	    |   _  -> bad_vernac_args "OPAQUE")
 	 id_list)
-***)
 
 let _ =
   add "UNDO"