- constantes avec recettes

 - discharge en deux temps, avec état remis comme au début de la section
(mais c'est toujours buggé)


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

1 files changed, 115 insertions, 79 deletions

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 84b357c5d..f0a97c218 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -74,7 +74,14 @@ let abstract_constant ids_to_abs hyps (body,typ) =
       let name = Name id in
       let var = snd (hd_sign hyps) in
       let cvar = incast_type var in
-      let body' = mkLambda name cvar (subst_var id body) in
+      let body' = match body with
+	| None -> None
+	| Some { contents = Cooked c } -> 
+	    Some (ref (Cooked (mkLambda name cvar (subst_var id c))))
+	| Some { contents = Recipe f } ->
+	    Some (ref (Recipe 
+			 (fun () -> mkLambda name cvar (subst_var id (f())))))
+      in
       let typ' =
     	{ body = mkProd name cvar (subst_var id typ.body);
 	  typ  = sort_of_product_without_univ var.typ typ.typ } 
@@ -88,29 +95,21 @@ let abstract_constant ids_to_abs hyps (body,typ) =
 
 (* Substitutions. *)
 
-let expmod_constr modlist c =
-  let env = Global.env() in
+let expmod_constr oldenv modlist c =
   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 
+  let simpfun = 
+    if modlist = [] then fun x -> x else nf_betaiota oldenv sigma in
+  let expfun cst = 
     try 
-      constant_value env c
-    with Failure _ -> begin
-      mSGERRNL 
+      constant_value oldenv cst
+    with Failure _ ->
+      let (sp,_) = destConst 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" >];
-      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))
@@ -118,27 +117,34 @@ let expmod_constr modlist 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))
+    | DOP2 (Cast,val_0,typ) -> DOP2 (Cast,simpfun val_0,simpfun typ)
     | _ -> simpfun c'
 
-let expmod_type modlist {body=c;typ=s} = {body=expmod_constr modlist c;typ=s}
+let expmod_type oldenv modlist {body=c;typ=s} = 
+  { body = expmod_constr oldenv modlist c; typ = s }
 
+let expmod_constant_value opaque oldenv modlist = function
+  | None -> None
+  | Some { contents = Cooked c } -> 
+      if opaque then 
+	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 (ids_to_discard,modlist) mib =
+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
   let inds = 
     array_map_to_list
       (fun mip ->
 	 (mip.mind_typename,
-	  expmod_type modlist mip.mind_arity,
+	  expmod_type oldenv modlist mip.mind_arity,
 	  Array.to_list mip.mind_consnames,
-	  under_dlams (expmod_constr modlist) mip.mind_lc))
+	  under_dlams (expmod_constr oldenv modlist) mip.mind_lc))
       mib.mind_packets
   in
   let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in
@@ -162,22 +168,22 @@ let process_inductive osecsp nsecsp (ids_to_discard,modlist) mib =
 
 (* Discharge of constants. *)
 
-let process_constant osecsp nsecsp (ids_to_discard,modlist) cb =
-  let body = global_reference CCI (basename osecsp) in
-  let typ = expmod_type modlist cb.const_type in
+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 (body',typ',modl) = 
     abstract_constant ids_to_discard cb.const_hyps (body,typ)
   in
   let mods = (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) :: modlist in
-  ({ const_entry_body = body'; const_entry_type = Some typ'.body },
-   mods)
+  (body', typ'.body, mods)
 
 
 (* Discharge of the various objects of the environment. *)
 
-let constant_message sp =
+let constant_message id =
   if Options.verbose() then 
-    pPNL [< print_id (basename sp); 'sTR " is discharged." >]
+    pPNL [< print_id id; 'sTR " is discharged." >]
 
 let inductive_message inds =
   if Options.verbose() then 
@@ -189,74 +195,80 @@ let inductive_message inds =
 			   (fun (id,_,_,_) -> print_id id) l;
 			 'sPC; 'sTR "are discharged.">]))
 
-let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) =
+type discharge_operation = 
+  | Variable of identifier * constr * strength * bool
+  | Parameter of identifier * constr
+  | Constant of identifier * constant_entry * strength
+  | Inductive of mutual_inductive_entry
+  | Class of cl_typ * cl_info_typ
+  | Struc of section_path * struc_typ
+  | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ) 
+              * identifier * int 
+
+let process_object oldenv sec_sp (ops,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
+	  (ops,id::ids_to_discard,work_alist)
+	else
+	  let expmod_a = expmod_constr oldenv work_alist a.body in
+	  (Variable (id,expmod_a,stre,sticky) :: ops,
+           ids_to_discard,work_alist)
 
     | "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
+	  (ops, ids_to_discard, (Const sp, DO_REPLACE) :: work_alist)
+	else
+	  let cb = Environ.lookup_constant sp oldenv in
 	  let spid = basename sp in
 	  let newsp = recalc_sp sp in
-	  let (ce,mods) = 
-	    process_constant sp newsp (ids_to_discard,work_alist) cb in
-	  declare_constant spid (ce,stre);
-	  constant_message sp;
-          (ids_to_discard,mods@work_alist)
-	end
+	  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)
+	    | Some { contents = b } -> 
+		let ce = 
+		  { const_entry_body = b; const_entry_type = Some typ } in
+		Constant (spid,ce,stre)
+	  in
+          (op::ops, ids_to_discard, mods@work_alist)
   
     | "INDUCTIVE" ->
-	let mib = Global.lookup_mind sp in
+	let mib = Environ.lookup_mind sp oldenv in
 	let newsp = recalc_sp sp in
 	let (mie,mods) = 
-	  process_inductive sp newsp (ids_to_discard,work_alist) mib in
-	let _ = declare_mind mie in
-	inductive_message mie.mind_entry_inds;
-        (ids_to_discard,mods@work_alist)
+	  process_inductive sp newsp oldenv (ids_to_discard,work_alist) mib in
+        ((Inductive mie)::ops, ids_to_discard, mods@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
+	  (ops,ids_to_discard,work_alist)
+	else
+	  let (y1,y2) = process_class sec_sp x in
+          ((Class (y1,y2))::ops, ids_to_discard, work_alist)
 	  
     | "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
+	  (ops,ids_to_discard,work_alist)
+        else
+	  let (y,idf,ps) = process_coercion sec_sp x in
+          ((Coercion (y,idf,ps))::ops, ids_to_discard, work_alist)
                     
     | "STRUCTURE" ->
 	let (sp,info) = outStruc lobj in
 	let newsp = recalc_sp sp in
-	let mib = Global.lookup_mind (ccisp_of newsp) in
+	let mib = Environ.lookup_mind newsp oldenv 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)
+	  { s_CONST = info.s_CONST;
+	    s_PARAM = mib.mind_nparams;
+	    s_PROJ = List.map (option_app recalc_sp) info.s_PROJ } in
+	((Struc (newsp,strobj))::ops, ids_to_discard, work_alist)
 
     (***TODO
     | "OBJDEF1" -> 
@@ -266,14 +278,38 @@ let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) =
         (ids_to_discard,work_alist)
     ***)
 
-    | _ -> 
-	(ids_to_discard,work_alist)
+    | _ -> (ops,ids_to_discard,work_alist)
 
-let process_item sec_sp acc = function
-  | (sp,Leaf lobj) -> process_object sec_sp acc (sp,lobj)
+let process_item oldenv sec_sp acc = function
+  | (sp,Leaf lobj) -> process_object oldenv sec_sp acc (sp,lobj)
   | (_,_) -> acc
 
+let process_operation = function
+  | Variable (id,expmod_a,stre,sticky) ->
+      declare_variable id (expmod_a,stre,sticky)
+  | Parameter (spid,typ) ->
+      declare_parameter spid typ;
+      constant_message spid
+  | Constant (spid,ce,stre) ->
+      declare_constant spid (ce,stre);
+      constant_message spid
+  | Inductive mie ->
+      let _ = declare_mind mie in
+      inductive_message mie.mind_entry_inds
+  | Class (y1,y2) ->
+      Lib.add_anonymous_leaf (inClass (y1,y2))
+  | Struc (newsp,strobj) ->
+      Lib.add_anonymous_leaf (inStruc (newsp,strobj))
+  | Coercion ((_,_,clt) as y,idf,ps) ->
+      Lib.add_anonymous_leaf (inCoercion y); 
+      coercion_syntax idf ps clt
+
 let close_section _ s = 
-  let (sec_sp,decls) = close_section s in
-  let _ = List.fold_left (process_item sec_sp) ([],[]) decls in 
-  ()
+  let oldenv = Global.env() in
+  let (sec_sp,decls,frozen) = close_section s in
+  let (ops,_,_) = 
+    List.fold_left (process_item oldenv sec_sp) ([],[],[]) decls in 
+  Summary.unfreeze_summaries frozen;
+  List.iter process_operation (List.rev ops)
+
+