Lazy experimentale temporaire...

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

10 files changed, 61 insertions, 24 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 616be45f1..eb37adbd3 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -107,7 +107,7 @@ let expmod_constr modlist c =
         str"and then require that theorems which use them" ++ spc () ++
         str"be transparent");
     match cb.const_body with
-      | Some body -> body
+      | Some body -> Lazy.force_val body
       | None -> assert false
   in
   let c' = modify_opers expfun modlist c in
@@ -119,23 +119,44 @@ let expmod_type modlist c =
   type_app (expmod_constr modlist) c
 
 let abstract_constant ids_to_abs hyps (body,typ) =
-  let abstract_once ((hyps,body,typ) as sofar) id =
+  let abstract_once_typ ((hyps,typ) as sofar) id =
     match hyps with
       | (hyp,c,t as decl)::rest when hyp = id ->
-	  let body' = option_app (mkNamedLambda_or_LetIn decl) body in
 	  let typ' = mkNamedProd_wo_LetIn decl typ in
-	  (rest, body', typ')
+	  (rest, typ')
       | _ -> 
 	  sofar
   in
-  let (_,body',typ') =
-    List.fold_left abstract_once (hyps,body,typ) ids_to_abs in
-  (body',typ')
+  let abstract_once_body ((hyps,body) as sofar) id =
+    match hyps with
+      | (hyp,c,t as decl)::rest when hyp = id ->
+	  let body' = mkNamedLambda_or_LetIn decl body in
+	  (rest, body')
+      | _ -> 
+	  sofar
+  in
+  let (_,typ') =
+    List.fold_left abstract_once_typ (hyps,typ) ids_to_abs 
+  in
+  let body' = match body with
+      None -> None
+    | Some l_body -> 
+	Some (lazy (let body = Lazy.force_val l_body in
+		    let (_,body') = 
+		      List.fold_left abstract_once_body (hyps,body) ids_to_abs
+		    in
+		      body'))
+  in
+    (body',typ')
 
 let cook_constant env r =
   let cb = r.d_from in
   let typ = expmod_type r.d_modlist cb.const_type in
-  let body = option_app (expmod_constr r.d_modlist) cb.const_body in
+  let body = 
+    option_app 
+      (fun lconstr -> lazy (expmod_constr r.d_modlist (Lazy.force_val lconstr))) 
+      cb.const_body
+  in
   let hyps =
     Sign.fold_named_context
       (fun d ctxt ->
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 3cd03fc9a..1787478b9 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -32,7 +32,7 @@ type recipe = {
   d_modlist : work_list }
 
 val cook_constant :
-  env -> recipe -> constr option * constr * constraints * bool
+  env -> recipe -> constr Lazy.t option * constr * constraints * bool
 
 (*s Utility functions used in module [Discharge]. *)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 05989bc82..d3c7681c0 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -23,7 +23,7 @@ open Sign
 
 type constant_body = {
   const_hyps : section_context; (* New: younger hyp at top *)
-  const_body : constr option;
+  const_body : constr Lazy.t option;
   const_type : types;
   const_constraints : constraints;
   const_opaque : bool }
@@ -88,9 +88,12 @@ type mutual_inductive_body = {
   mind_equiv : kernel_name option
  }
 
+let lazy_subst sub l_constr = 
+  lazy (subst_mps sub (Lazy.force_val l_constr))
+
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 let subst_const_body sub cb = 
-  { const_body = option_app (Term.subst_mps sub) cb.const_body;
+  { const_body = option_app (lazy_subst sub) cb.const_body;
     const_type = type_app (Term.subst_mps sub) cb.const_type;
     const_hyps = (assert (cb.const_hyps=[]); []);
     const_constraints = cb.const_constraints;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index eeec64875..715a83a4a 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -23,7 +23,7 @@ open Sign
 
 type constant_body = {
   const_hyps : section_context; (* New: younger hyp at top *)
-  const_body : constr option;
+  const_body : constr Lazy.t option;
   const_type : types;
   const_constraints : constraints;
   const_opaque : bool }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 6449c183f..dd9a72bd1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -141,7 +141,7 @@ let constant_value env kn =
   let cb = lookup_constant kn env in
   if cb.const_opaque then raise (NotEvaluableConst Opaque);
   match cb.const_body with
-    | Some body -> body
+    | Some l_body -> Lazy.force_val l_body
     | None -> raise (NotEvaluableConst NoBody)
 
 let constant_opt_value env cst =
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 0fb79376a..b8399ab32 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -91,13 +91,14 @@ and merge_with env mtb with_decl =
 			  cst2
 		      in
 			SPBconst {cb with 
-				    const_body = Some j.uj_val;
+				    const_body = 
+				      Some (Lazy.lazy_from_val j.uj_val);
 				    const_constraints = cst}
 		  | Some b -> 
-		      let cst1 = Reduction.conv env' c b in 
+		      let cst1 = Reduction.conv env' c (Lazy.force_val b) in 
 		      let cst = Constraint.union cb.const_constraints cst1 in
 			SPBconst {cb with 
-				    const_body = Some c;
+				    const_body = Some (Lazy.lazy_from_val c);
 				    const_constraints = cst}
 	      end	
 	| With_Module (id, mp) ->
diff --git a/kernel/modops.ml b/kernel/modops.ml
index d4338f0fb..40a0e84c5 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -163,7 +163,10 @@ and add_module mp mb env =
 
 let strengthen_const env mp l cb = match cb.const_body with
   | Some _ -> cb
-  | None -> {cb with const_body = Some (mkConst (make_kn mp empty_dirpath l))}
+  | None -> {cb with const_body = 
+	       let const = mkConst (make_kn mp empty_dirpath l) in 
+		 Some (Lazy.lazy_from_val const)
+	    }
 
 let strengthen_mind env mp l mib = match mib.mind_equiv with
   | Some _ -> mib
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d8a00d7b7..70faa24b4 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -119,9 +119,14 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 let hcons_constant_body cb =
-  { cb with
-    const_body = option_app hcons1_constr cb.const_body;
-    const_type = hcons1_constr cb.const_type }
+  let body = match cb.const_body with
+      None -> None
+    | Some l_constr -> let constr = Lazy.force_val l_constr in
+	Some (Lazy.lazy_from_val (hcons1_constr constr))
+  in
+    { cb with
+	const_body = body;
+	const_type = hcons1_constr cb.const_type }
 
 let add_constant dir l decl senv =
   check_label l senv.labset;
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2a81ebee0..6e20ceeb4 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -160,9 +160,10 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
     let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in
     match cb2.const_body with
       | None -> cst
-      | Some c2 ->
+      | Some lc2 ->
+	  let c2 = Lazy.force_val lc2 in
 	  let c1 = match cb1.const_body with
-	    | Some c1 -> c1
+	    | Some c1 -> Lazy.force_val c1
 	    | None -> mkConst (make_kn (MPself msid1) empty_dirpath l)
 	  in
 	    check_conv cst conv env c1 c2
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 1abe65c20..aabefe6bf 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -81,7 +81,7 @@ let infer_declaration env dcl =
   | DefinitionEntry c ->
       let (j,cst) = infer env c.const_entry_body in
       let (typ,cst) = constrain_type env j cst c.const_entry_type in
-      Some j.uj_val, typ, cst, c.const_entry_opaque
+      Some (Lazy.lazy_from_val j.uj_val), typ, cst, c.const_entry_opaque
   | ParameterEntry t ->
       let (j,cst) = infer env t in
       None, Typeops.assumption_of_judgment env j, cst, false
@@ -90,7 +90,10 @@ let build_constant_declaration env (body,typ,cst,op) =
   let ids = match body with 
     | None -> global_vars_set env typ
     | Some b ->
-        Idset.union (global_vars_set env b) (global_vars_set env typ) in
+        Idset.union 
+	  (global_vars_set env (Lazy.force_val b)) 
+	  (global_vars_set env typ) 
+  in
   let hyps = keep_hyps env ids in
     { const_body = body;
       const_type = typ;