- 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

5 files changed, 59 insertions, 13 deletions

diff --git a/kernel/constant.ml b/kernel/constant.ml
index c93d486fa..dda7274af 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -7,13 +7,15 @@ open Generic
 open Term
 open Sign
 
-type constant_entry = {
-  const_entry_body : constr;
-  const_entry_type : constr option }
+type lazy_constant_value =
+  | Cooked of constr
+  | Recipe of (unit -> constr)
+
+type constant_value = lazy_constant_value ref
 
 type constant_body = {
   const_kind : path_kind;
-  const_body : constr option;
+  const_body : constant_value option;
   const_type : typed_type;
   const_hyps : typed_type signature;
   const_constraints : constraints;
@@ -23,3 +25,12 @@ let is_defined cb =
   match cb.const_body with Some _ -> true | _ -> false
 
 let is_opaque cb = cb.const_opaque
+
+let cook_constant = function
+  | { contents = Cooked c } -> c
+  | { contents = Recipe f } as v -> let c = f () in v := Cooked c; c
+
+type constant_entry = {
+  const_entry_body : lazy_constant_value;
+  const_entry_type : constr option }
+
diff --git a/kernel/constant.mli b/kernel/constant.mli
index 800f95811..c24280c40 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -10,9 +10,15 @@ open Sign
 
 (* Constants (internal representation). *)
 
+type lazy_constant_value =
+  | Cooked of constr
+  | Recipe of (unit -> constr)
+
+type constant_value = lazy_constant_value ref
+
 type constant_body = {
   const_kind : path_kind;
-  const_body : constr option;
+  const_body : constant_value option;
   const_type : typed_type;
   const_hyps : typed_type signature;
   const_constraints : constraints;
@@ -22,9 +28,11 @@ val is_defined : constant_body -> bool
 
 val is_opaque : constant_body -> bool
 
+val cook_constant : constant_value -> constr
+
 (*s Constant declaration. *)
 
 type constant_entry= {
-  const_entry_body : constr;
+  const_entry_body : lazy_constant_value;
   const_entry_type : constr option }
 
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index f3634eac5..e2afdb2a7 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -43,7 +43,8 @@ let constant_value env k =
   let cb = lookup_constant sp env in
   if not cb.const_opaque & defined_constant env k then
     match cb.const_body with
-      | Some body -> 
+      | Some v -> 
+	  let body = cook_constant v in
           instantiate_constr 
 	    (ids_of_sign cb.const_hyps) body (Array.to_list args)
       | None -> 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index efa860fa2..a4cde0371 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -262,11 +262,11 @@ let push_rels vars env =
 
 (* Insertion of constants and parameters in environment. *)
 
-let add_constant sp ce env =
-  let (jb,cst) = safe_machine env ce.const_entry_body in
+let add_constant_with_value sp body typ env =
+  let (jb,cst) = safe_machine env body in
   let env' = add_constraints cst env in
   let (env'',ty,cst') = 
-    match ce.const_entry_type with
+    match typ with
       | None -> 
 	  env', typed_type_of_judgment env' Evd.empty jb, Constraint.empty
       | Some ty -> 
@@ -281,11 +281,11 @@ let add_constant sp ce env =
 	    error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
   in
   let ids = 
-    Idset.union (global_vars_set ce.const_entry_body) (global_vars_set ty.body)
+    Idset.union (global_vars_set body) (global_vars_set ty.body)
   in
   let cb = { 
     const_kind = kind_of_path sp;
-    const_body = Some ce.const_entry_body;
+    const_body = Some (ref (Cooked body));
     const_type = ty;
     const_hyps = keep_hyps (var_context env) ids;
     const_constraints = Constraint.union cst cst';
@@ -293,6 +293,28 @@ let add_constant sp ce env =
   in
   add_constant sp cb env''
 
+let add_lazy_constant sp f t env =
+  let (jt,cst) = safe_machine env t in
+  let env' = add_constraints cst env in
+  let ids = global_vars_set jt.uj_val in
+  let cb = {
+    const_kind = kind_of_path sp;
+    const_body = Some (ref (Recipe f));
+    const_type = assumption_of_judgment env' Evd.empty jt;
+    const_hyps = keep_hyps (var_context env) ids;
+    const_constraints = cst;
+    const_opaque = false } 
+  in
+  add_constant sp cb env'
+
+let add_constant sp ce env =
+  match ce.const_entry_body with
+    | Cooked c -> add_constant_with_value sp c ce.const_entry_type env
+    | Recipe f -> 
+	(match ce.const_entry_type with
+	   | Some typ -> add_lazy_constant sp f typ env
+	   | None -> error "you cannot declare a lazy constant without type")
+
 let add_parameter sp t env =
   let (jt,cst) = safe_machine env t in
   let env' = add_constraints cst env in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index eae3f77df..314796ee6 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -30,10 +30,14 @@ val push_var : identifier * constr -> safe_environment -> safe_environment
 val push_rel : name * constr -> safe_environment -> safe_environment
 val add_constant : 
   section_path -> constant_entry -> safe_environment -> safe_environment
+val add_lazy_constant : 
+  section_path -> (unit -> constr) -> constr -> safe_environment 
+    -> safe_environment
 val add_parameter :
   section_path -> constr -> safe_environment -> safe_environment
 val add_mind : 
-  section_path -> mutual_inductive_entry -> safe_environment -> safe_environment
+  section_path -> mutual_inductive_entry -> safe_environment 
+    -> safe_environment
 val add_constraints : constraints -> safe_environment -> safe_environment
 
 val lookup_var : identifier -> safe_environment -> name * typed_type