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

9 files changed, 259 insertions, 70 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
new file mode 100644
index 000000000..58fc1795b
--- /dev/null
+++ b/kernel/cooking.ml
@@ -0,0 +1,158 @@
+
+(*i $Id$ i*)
+
+open Pp
+open Util
+open Names
+open Term
+open Sign
+open Declarations
+open Instantiate
+open Environ
+open Reduction
+
+(*s Cooking the constants. *)
+
+type modification_action = ABSTRACT | ERASE
+
+type 'a modification =
+  | NOT_OCCUR
+  | DO_ABSTRACT of 'a * modification_action list
+  | DO_REPLACE
+
+type work_alist = (global_reference * global_reference modification) list
+
+type recipe = {
+  d_from : section_path;
+  d_abstract : identifier list;
+  d_modlist : (global_reference * global_reference modification) list }
+
+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)
+
+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) ->
+		    assert (List.length modif <= Array.length cl);
+		    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) ->
+		    assert (List.length modif <= Array.length cl);
+		    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) ->
+		    assert (List.length modif <= Array.length cl);
+		    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
+
+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 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 abstract_constant ids_to_abs hyps (body,typ) =
+  let abstract_once ((hyps,body,typ) 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 c -> Some (mkNamedLambda_or_LetIn decl c)
+	    in
+	    let typ' = mkNamedProd_or_LetIn decl typ in
+	    (rest, body', typ')
+  in
+  let (_,body',typ') =
+    List.fold_left abstract_once (hyps,body,typ) ids_to_abs in
+  (body',typ')
+
+let cook_constant env r =
+  let cb = lookup_constant r.d_from env in
+  let typ = expmod_type env r.d_modlist cb.const_type in
+  let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
+  let hyps = map_named_context (expmod_constr env r.d_modlist) cb.const_hyps in
+  abstract_constant r.d_abstract hyps (body,typ)
+
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
new file mode 100644
index 000000000..7d1bc3988
--- /dev/null
+++ b/kernel/cooking.mli
@@ -0,0 +1,32 @@
+
+(*i $Id$ i*)
+
+open Names
+open Term
+open Declarations
+open Environ
+
+(*s Cooking the constants. *)
+
+type modification_action = ABSTRACT | ERASE
+
+type 'a modification =
+  | NOT_OCCUR
+  | DO_ABSTRACT of 'a * modification_action list
+  | DO_REPLACE
+
+type work_alist = (global_reference * global_reference modification) list
+
+type recipe = {
+  d_from : section_path;
+  d_abstract : identifier list;
+  d_modlist : work_alist }
+
+val cook_constant : env -> recipe -> constr option * constr
+
+(*s Utility functions used in module [Discharge]. *)
+
+val expmod_constr : env -> work_alist -> constr -> constr
+val expmod_type : env -> work_alist -> types -> types
+
+
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ff80c338f..96eef5700 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -8,15 +8,9 @@ open Sign
 
 (* Constant entries *)
 
-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 : constant_value option;
+  const_body : constr option;
   const_type : types;
   const_hyps : named_context;
   const_constraints : constraints;
@@ -27,12 +21,8 @@ let is_defined cb =
 
 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_body : constr;
   const_entry_type : constr option }
 
 (* Inductive entries *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3be72f3fd..3e7d8a9bd 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -13,15 +13,9 @@ open Sign
 
 (*s Constants (internal representation) (Definition/Axiom) *)
 
-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 : constant_value option;
+  const_body : constr option;
   const_type : types;
   const_hyps : named_context; (* New: younger hyp at top *)
   const_constraints : constraints;
@@ -31,12 +25,10 @@ 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 : lazy_constant_value;
+  const_entry_body : constr;
   const_entry_type : constr option }
 
 (*s Inductive types (internal representation). *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 00e6d66f6..2613199ff 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -310,6 +310,16 @@ let evaluable_constant env k =
   with Not_found -> 
     false
 
+(*s Opaque / Transparent switching *)
+
+let set_opaque env sp =
+  let cb = lookup_constant sp env in
+  cb.const_opaque <- true
+
+let set_transparent env sp =
+  let cb = lookup_constant sp env in
+  cb.const_opaque <- false
+
 (*s Modules (i.e. compiled environments). *)
 
 type compiled_env = {
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c4a5e4659..84f384759 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -144,6 +144,11 @@ val prod_create : env -> types * constr -> constr
 val defined_constant : env -> constant -> bool
 val evaluable_constant : env -> constant -> bool
 
+(*s Opaque / Transparent switching *)
+
+val set_opaque : env -> section_path -> unit
+val set_transparent : env -> section_path -> unit
+
 (*s Modules. *)
 
 type compiled_env
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index f99ccb0c4..7f6f1258b 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -41,15 +41,12 @@ exception NotEvaluableConst of const_evaluation_result
 
 let constant_value env (sp,args) =
   let cb = lookup_constant sp env in
-  if cb.const_opaque then raise (NotEvaluableConst Opaque) else
-  if not (is_defined cb) then raise (NotEvaluableConst NoBody) else
+  if cb.const_opaque then raise (NotEvaluableConst Opaque);
   match cb.const_body with
-    | Some v -> 
-	let body = cook_constant v in
+    | Some body -> 
         instantiate_constr cb.const_hyps body (Array.to_list args)
     | None ->
-	anomalylabstrm "termenv__constant_value"
-	  [< 'sTR "a defined constant with no body." >]
+	raise (NotEvaluableConst NoBody)
 
 let constant_opt_value env cst =
   try Some (constant_value env cst)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 48d9ad184..db2f57d67 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -270,6 +270,20 @@ let push_rels_with_univ vars env =
 
 (* Insertion of constants and parameters in environment. *)
 
+let add_parameter sp t env =
+  let (jt,cst) = safe_infer 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 = None;
+    const_type = assumption_of_judgment env' Evd.empty jt;
+    const_hyps = keep_hyps ids (named_context env);
+    const_constraints = cst;
+    const_opaque = false } 
+  in
+  Environ.add_constant sp cb env'
+
 let add_constant_with_value sp body typ env =
   let (jb,cst) = safe_infer env body in
   let env' = add_constraints cst env in
@@ -296,7 +310,7 @@ let add_constant_with_value sp body typ env =
   in
   let cb = { 
     const_kind = kind_of_path sp;
-    const_body = Some (ref (Cooked body));
+    const_body = Some body;
     const_type = ty;
     const_hyps = keep_hyps ids (named_context env);
     const_constraints = Constraint.union cst cst';
@@ -304,41 +318,29 @@ let add_constant_with_value sp body typ env =
   in
   add_constant sp cb env''
 
-let add_lazy_constant sp f t env =
-  let (jt,cst) = safe_infer 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 ids (named_context env);
-    const_constraints = cst;
-    const_opaque = false } 
-  in
-  add_constant sp cb env'
+let add_discharged_constant sp r env =
+  let (body,typ) = Cooking.cook_constant env r in
+  match body with
+    | None -> 
+	add_parameter sp typ env
+    | Some c -> 
+	let (jtyp,cst) = safe_infer env typ in
+	let env' = add_constraints cst env in
+	let ids = 
+	  Idset.union (global_vars_set c) 
+	    (global_vars_set (body_of_type jtyp.uj_type))
+	in
+	let cb = { const_kind = kind_of_path sp;
+		   const_body = body;
+		   const_type = assumption_of_judgment env' Evd.empty jtyp;
+		   const_hyps = keep_hyps ids (named_context env);
+		   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_infer 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 = None;
-    const_type = assumption_of_judgment env' Evd.empty jt;
-    const_hyps = keep_hyps ids (named_context env);
-    const_constraints = cst;
-    const_opaque = false } 
-  in
-  Environ.add_constant sp cb env'
+  add_constant_with_value sp ce.const_entry_body ce.const_entry_type env
 
 (* Insertion of inductive types. *)
 
@@ -462,6 +464,9 @@ let rec pop_named_decls idl env =
     | [] -> env
     | id::l -> pop_named_decls l (Environ.pop_named_decl id env)
 
+let set_opaque = Environ.set_opaque
+let set_transparent = Environ.set_transparent
+
 let export = export
 let import = import
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 89e3fbbb7..011d0e414 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -31,13 +31,13 @@ val push_named_assum :
 val push_named_def :
   identifier * 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_constant : 
+  section_path -> constant_entry -> safe_environment -> safe_environment
+val add_discharged_constant : 
+  section_path -> Cooking.recipe -> safe_environment -> safe_environment
+
 val add_mind : 
   section_path -> mutual_inductive_entry -> safe_environment 
     -> safe_environment
@@ -46,13 +46,13 @@ val add_constraints : constraints -> safe_environment -> safe_environment
 val pop_named_decls : identifier list -> safe_environment -> safe_environment
 
 val lookup_named : identifier -> safe_environment -> constr option * types
-(*i
-val lookup_rel : int -> safe_environment -> name * types
-i*)
 val lookup_constant : section_path -> safe_environment -> constant_body
 val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
 val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
 
+val set_opaque : safe_environment -> section_path -> unit
+val set_transparent : safe_environment -> section_path -> unit
+
 val export : safe_environment -> string -> compiled_env
 val import : compiled_env -> safe_environment -> safe_environment