Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant

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

4 files changed, 20 insertions, 77 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 542bd6b946..c87ec0d341 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -110,50 +110,9 @@ let declare_variable id obj =
   if is_implicit_args() then declare_var_implicits id;
   sp
 
-(* Parameters. *)
+(* Globals: constants and parameters *)
 
-let cache_parameter (sp,c) =
-  (if Nametab.exists_cci sp then
-    let (_,id) = repr_path sp in
-    errorlabstrm "cache_parameter" [< pr_id id; 'sTR " already exists" >]);
-  Global.add_parameter sp c;
-  Nametab.push 0 sp (ConstRef sp)
-
-let load_parameter (sp,_) =
-  (if Nametab.exists_cci sp then
-    let (_,id) = repr_path sp in
-    errorlabstrm "cache_parameter" [< pr_id id; 'sTR " already exists" >]);
-  Nametab.push 1 sp (ConstRef sp)
-
-let open_parameter (sp,_) =
-  Nametab.push 0 (restrict_path 0 sp) (ConstRef sp)
-
-(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_parameter_entry = mkProp
-
-let export_parameter c = Some dummy_parameter_entry
-
-let (in_parameter, out_parameter) =
-  let od = {
-    cache_function = cache_parameter;
-    load_function = load_parameter;
-    open_function = open_parameter;
-    export_function = export_parameter } 
-  in
-  declare_object ("PARAMETER", od)
-
-let declare_parameter id c =
-  let sp = add_leaf id (in_parameter c) in 
-  if is_implicit_args() then declare_constant_implicits sp;
-  sp
-
-(* Constants. *)
-
-type constant_declaration_type =
-  | ConstantEntry  of constant_entry
-  | ConstantRecipe of Cooking.recipe
-
-type constant_declaration = constant_declaration_type * strength
+type constant_declaration = global_declaration * strength
 
 let csttab = ref (Spmap.empty : strength Spmap.t)
 
@@ -167,10 +126,7 @@ let cache_constant (sp,(cdt,stre)) =
   (if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
     errorlabstrm "cache_constant" [< pr_id id; 'sTR " already exists" >]);
-  begin match cdt with 
-    | ConstantEntry ce -> Global.add_constant sp ce
-    | ConstantRecipe r -> Global.add_discharged_constant sp r
-  end;
+  Global.add_constant sp cdt;
   (match stre with
     | DischargeAt (dp,n) when not (is_dirpath_prefix_of dp (Lib.cwd ())) ->
         (* Only qualifications including the sections segment from the current
@@ -197,10 +153,7 @@ let open_constant (sp,(_,stre)) =
   Nametab.push n (restrict_path n sp) (ConstRef sp)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = ConstantEntry { 
-  const_entry_body = mkProp;
-  const_entry_type = None;
-  const_entry_opaque = false }
+let dummy_constant_entry = ParameterEntry mkProp
 
 let export_constant (ce,stre) = Some (dummy_constant_entry,stre)
 
@@ -215,11 +168,10 @@ let (in_constant, out_constant) =
 
 let hcons_constant_declaration = function
   | (ConstantEntry ce, stre) ->
-      (ConstantEntry 
-	 { const_entry_body = hcons1_constr ce.const_entry_body;
-	   const_entry_type = option_app hcons1_constr ce.const_entry_type;
-           const_entry_opaque = ce.const_entry_opaque },
-	 stre)
+      (ConstantEntry
+       { const_entry_body = hcons1_constr ce.const_entry_body;
+	 const_entry_type = option_app hcons1_constr ce.const_entry_type;
+         const_entry_opaque = ce.const_entry_opaque }, stre)
   | cd -> cd
 
 let declare_constant id cd =
@@ -228,8 +180,8 @@ let declare_constant id cd =
   if is_implicit_args() then declare_constant_implicits sp;
   sp
 
-let redeclare_constant sp cd =
-  add_absolutely_named_leaf sp (in_constant cd);
+let redeclare_constant sp (cd,stre) =
+  add_absolutely_named_leaf sp (in_constant (GlobalRecipe cd,stre));
   if is_implicit_args() then declare_constant_implicits sp
 
 (* Inductives. *)
@@ -315,9 +267,6 @@ let is_constant sp =
 
 let constant_strength sp = Spmap.find sp !csttab
 
-let constant_or_parameter_strength sp =
-  try constant_strength sp with Not_found -> NeverDischarge
-
 let get_variable id = 
   let (p,(c,ty,cst),str) = Idmap.find id !vartab in
   ((id,c,ty),str)
@@ -431,3 +380,8 @@ let is_global id =
     is_dirpath_prefix_of (dirpath_of_global osp) (Lib.cwd())
   with Not_found -> 
     false
+
+let strength_of_global = function
+  | ConstRef sp -> constant_strength sp
+  | VarRef id -> variable_strength id
+  | IndRef _ | ConstructRef _ -> NeverDischarge 
diff --git a/library/declare.mli b/library/declare.mli
index bb903a9c46..e8da45a57b 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -39,20 +39,14 @@ type variable_declaration = dir_path * section_variable_entry * strength
 
 val declare_variable : variable -> variable_declaration -> section_path
 
-type constant_declaration_type =
-  | ConstantEntry  of constant_entry
-  | ConstantRecipe of Cooking.recipe
-
-type constant_declaration = constant_declaration_type * strength
+type constant_declaration = global_declaration * strength
 
 (* [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
    the full path of the declaration *)
 val declare_constant : identifier -> constant_declaration -> constant
 
-val redeclare_constant : constant -> constant_declaration -> unit
-
-val declare_parameter : identifier -> constr -> constant
+val redeclare_constant : constant -> Cooking.recipe * strength -> unit
 
 (* [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
@@ -69,7 +63,6 @@ val make_strength_2 : unit -> strength
 
 val is_constant : section_path -> bool
 val constant_strength : constant -> strength
-val constant_or_parameter_strength : constant -> strength
 
 val out_variable : Libobject.obj -> identifier * variable_declaration
 val get_variable : variable -> named_declaration * strength
@@ -105,3 +98,5 @@ val global_reference : identifier -> constr
 val construct_reference : Environ.env -> identifier -> constr
 
 val is_global : identifier -> bool
+
+val strength_of_global : global_reference -> strength
diff --git a/library/global.ml b/library/global.ml
index bbb77c8537..b929ad78f0 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -47,10 +47,7 @@ let push_named_def d =
   cst
 let pop_named_decls ids = global_env := pop_named_decls ids !global_env
 
-let add_parameter sp c = global_env := add_parameter sp c !global_env
 let add_constant sp ce = global_env := add_constant sp ce !global_env
-let add_discharged_constant sp r = 
-  global_env := add_discharged_constant sp r !global_env
 let add_mind sp mie = global_env := add_mind sp mie !global_env
 let add_constraints c = global_env := add_constraints c !global_env
 
diff --git a/library/global.mli b/library/global.mli
index f10ab98a5a..48b647c6ab 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,10 +32,7 @@ val push_named_assum : (identifier * types) -> Univ.constraints
 val push_named_def   : (identifier * constr * types option) -> Univ.constraints
 val pop_named_decls  : identifier list -> unit
 
-val add_parameter           : constant -> types -> unit
-val add_constant            : constant -> constant_entry -> unit
-val add_discharged_constant : constant -> Cooking.recipe -> unit
-
+val add_constant    : constant -> global_declaration -> unit
 val add_mind        : mutual_inductive -> mutual_inductive_entry -> unit
 val add_constraints : constraints -> unit