Lazy manuelles dans le code

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

10 files changed, 52 insertions, 25 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index eb37adbd3c..7c3b8e60f0 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 -> Lazy.force_val body
+      | Some body -> Declarations.force body
       | None -> assert false
   in
   let c' = modify_opers expfun modlist c in
@@ -141,11 +141,12 @@ let abstract_constant ids_to_abs hyps (body,typ) =
   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'))
+	Some (Declarations.from_val
+		(let body = Declarations.force l_body in
+		 let (_,body') = 
+		   List.fold_left abstract_once_body (hyps,body) ids_to_abs
+		 in
+		   body'))
   in
     (body',typ')
 
@@ -154,7 +155,9 @@ let cook_constant env r =
   let typ = expmod_type r.d_modlist cb.const_type in
   let body = 
     option_app 
-      (fun lconstr -> lazy (expmod_constr r.d_modlist (Lazy.force_val lconstr))) 
+      (fun lconstr -> 
+	 Declarations.from_val 
+	   (expmod_constr r.d_modlist (Declarations.force lconstr))) 
       cb.const_body
   in
   let hyps =
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 1787478b9d..b54189ba64 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 Lazy.t option * constr * constraints * bool
+  env -> recipe -> constr_substituted option * constr * constraints * bool
 
 (*s Utility functions used in module [Discharge]. *)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index d3c7681c09..e6dd40c8a3 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -21,9 +21,30 @@ open Sign
 
 (*s Constants (internal representation) (Definition/Axiom) *)
 
+type subst_internal = 
+  | Constr of constr 
+  | LazyConstr of substitution * constr
+
+type constr_substituted = subst_internal ref
+
+let from_val c = ref (Constr c)
+
+let force cs = match !cs with
+    Constr c -> c
+  | LazyConstr (subst,c) -> 
+      let c' = subst_mps subst c in
+	cs := Constr c';
+	c'
+
+let subst_constr_subst subst cs = match !cs with
+    Constr c -> ref (LazyConstr (subst,c))
+  | LazyConstr (subst',c) -> 
+      let subst'' = join subst' subst in
+	ref (LazyConstr (subst'',c))
+
 type constant_body = {
   const_hyps : section_context; (* New: younger hyp at top *)
-  const_body : constr Lazy.t option;
+  const_body : constr_substituted option;
   const_type : types;
   const_constraints : constraints;
   const_opaque : bool }
@@ -88,12 +109,9 @@ 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 (lazy_subst sub) cb.const_body;
+  { const_body = option_app (subst_constr_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 715a83a4af..a40b65f6b9 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -21,9 +21,15 @@ open Sign
 
 (*s Constants (Definition/Axiom) *)
 
+type constr_substituted
+
+val from_val : constr -> constr_substituted
+val force : constr_substituted -> constr
+val subst_constr_subst : substitution -> constr_substituted -> constr_substituted
+
 type constant_body = {
   const_hyps : section_context; (* New: younger hyp at top *)
-  const_body : constr Lazy.t option;
+  const_body : constr_substituted option;
   const_type : types;
   const_constraints : constraints;
   const_opaque : bool }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index dd9a72bd1d..e4b1af8fed 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 l_body -> Lazy.force_val l_body
+    | Some l_body -> Declarations.force 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 b8399ab321..ba4dcf0b7f 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -92,13 +92,13 @@ and merge_with env mtb with_decl =
 		      in
 			SPBconst {cb with 
 				    const_body = 
-				      Some (Lazy.lazy_from_val j.uj_val);
+				      Some (Declarations.from_val j.uj_val);
 				    const_constraints = cst}
 		  | Some b -> 
-		      let cst1 = Reduction.conv env' c (Lazy.force_val b) in 
+		      let cst1 = Reduction.conv env' c (Declarations.force b) in 
 		      let cst = Constraint.union cb.const_constraints cst1 in
 			SPBconst {cb with 
-				    const_body = Some (Lazy.lazy_from_val c);
+				    const_body = Some (Declarations.from_val c);
 				    const_constraints = cst}
 	      end	
 	| With_Module (id, mp) ->
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 40a0e84c52..758bf21596 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -165,7 +165,7 @@ let strengthen_const env mp l cb = match cb.const_body with
   | Some _ -> cb
   | None -> {cb with const_body = 
 	       let const = mkConst (make_kn mp empty_dirpath l) in 
-		 Some (Lazy.lazy_from_val const)
+		 Some (Declarations.from_val const)
 	    }
 
 let strengthen_mind env mp l mib = match mib.mind_equiv with
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 70faa24b4a..663c6b6958 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -121,8 +121,8 @@ type global_declaration =
 let hcons_constant_body cb =
   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))
+    | Some l_constr -> let constr = Declarations.force l_constr in
+	Some (Declarations.from_val (hcons1_constr constr))
   in
     { cb with
 	const_body = body;
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6e20ceeb4c..0e24da5876 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -161,9 +161,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
     match cb2.const_body with
       | None -> cst
       | Some lc2 ->
-	  let c2 = Lazy.force_val lc2 in
+	  let c2 = Declarations.force lc2 in
 	  let c1 = match cb1.const_body with
-	    | Some c1 -> Lazy.force_val c1
+	    | Some lc1 -> Declarations.force lc1
 	    | 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 aabefe6bf2..1145ee94b0 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 (Lazy.lazy_from_val j.uj_val), typ, cst, c.const_entry_opaque
+      Some (Declarations.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
@@ -91,7 +91,7 @@ let build_constant_declaration env (body,typ,cst,op) =
     | None -> global_vars_set env typ
     | Some b ->
         Idset.union 
-	  (global_vars_set env (Lazy.force_val b)) 
+	  (global_vars_set env (Declarations.force b)) 
 	  (global_vars_set env typ) 
   in
   let hyps = keep_hyps env ids in