separation calcul des implicites et declaration des constantes / inductifs / variables

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

5 files changed, 96 insertions, 61 deletions

diff --git a/library/declare.ml b/library/declare.ml
index cf5abce74f..92af415126 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -54,49 +54,39 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
 	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
 
-let cache_variable (sp,((id,(d,_,_) as vd),imps)) =
+let cache_variable (sp,(id,(d,_,_) as vd)) =
   begin match d with (* Fails if not well-typed *)
     | SectionLocalAssum ty -> Global.push_named_assum (id,ty)
     | SectionLocalDef c -> Global.push_named_def (id,c)
   end;
   Nametab.push id (VarRef sp);
-  if imps then declare_var_implicits sp;
   vartab := Spmap.add sp vd !vartab
 
-let load_variable _ = ()
-
-let open_variable _ = ()
-
-let export_variable x = None
-
 let (in_variable, out_variable) =
   let od = {
     cache_function = cache_variable;
-    load_function = load_variable;
-    open_function = open_variable;
-    export_function = export_variable } in
+    load_function = (fun _ -> ());
+    open_function = (fun _ -> ());
+    export_function = (fun x -> None) }
+  in
   declare_object ("VARIABLE", od)
 
-let out_variable sp = fst (out_variable sp)
-
 let declare_variable id obj =
-  let _ = add_leaf id CCI (in_variable ((id,obj),is_implicit_args())) in
-  ()
+  let sp = add_leaf id CCI (in_variable (id,obj)) in
+  if is_implicit_args() then declare_var_implicits sp
 
 (* Parameters. *)
 
-let cache_parameter (sp,(c,imps)) =
+let cache_parameter (sp,c) =
   Global.add_parameter sp c;
-  Nametab.push (basename sp) (ConstRef sp);
-  if imps then declare_constant_implicits sp
+  Nametab.push (basename sp) (ConstRef sp)
 
-let load_parameter (sp,(_,imps)) =
-  if imps then declare_constant_implicits sp
+let load_parameter _ = ()
 
 let open_parameter (sp,_) =
   Nametab.push (basename sp) (ConstRef sp)
 
-let export_parameter obj = Some obj
+let export_parameter x = Some x
 
 let (in_parameter, out_parameter) =
   let od = {
@@ -108,7 +98,8 @@ let (in_parameter, out_parameter) =
   declare_object ("PARAMETER", od)
 
 let declare_parameter id c =
-  let _ = add_leaf id CCI (in_parameter (c,is_implicit_args())) in ()
+  let sp = add_leaf id CCI (in_parameter c) in 
+  if is_implicit_args() then declare_constant_implicits sp
 
 (* Constants. *)
 
@@ -125,23 +116,21 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.unfreeze_function = (fun ft -> csttab := ft);
 	    Summary.init_function = (fun () -> csttab := Spmap.empty) }
 
-let cache_constant (sp,((cdt,stre),imps)) =
+let cache_constant (sp,(cdt,stre)) =
   begin match cdt with 
     | ConstantEntry ce -> Global.add_constant sp ce
     | ConstantRecipe r -> Global.add_discharged_constant sp r
   end;
   Nametab.push (basename sp) (ConstRef sp);
-  if imps then declare_constant_implicits sp;
   csttab := Spmap.add sp stre !csttab
 
-let load_constant (sp,((ce,stre),imps)) =
-  if imps then declare_constant_implicits sp;
+let load_constant (sp,(ce,stre)) =
   csttab := Spmap.add sp stre !csttab
 
 let open_constant (sp,_) =
   Nametab.push (basename sp) (ConstRef sp)
 
-let export_constant obj = Some obj
+let export_constant x = Some x
 
 let (in_constant, out_constant) =
   let od = {
@@ -153,8 +142,8 @@ let (in_constant, out_constant) =
   declare_object ("CONSTANT", od)
 
 let declare_constant id cd =
-  let _ = add_leaf id CCI (in_constant (cd,is_implicit_args())) in ()
-
+  let sp = add_leaf id CCI (in_constant cd) in
+  if is_implicit_args() then declare_constant_implicits sp
  
 (* Inductives. *)
 
@@ -173,18 +162,16 @@ let push_inductive_names sp mie =
       0 mie.mind_entry_inds
   in ()
 
-let cache_inductive (sp,(mie,imps)) =
+let cache_inductive (sp,mie) =
   Global.add_mind sp mie;
-  push_inductive_names sp mie;
-  if imps then declare_inductive_implicits sp
+  push_inductive_names sp mie
 
-let load_inductive (sp,(_,imps)) =
-  if imps then declare_inductive_implicits sp
+let load_inductive _ = ()
 
-let open_inductive (sp,(mie,_)) =
+let open_inductive (sp,mie) =
   push_inductive_names sp mie
 
-let export_inductive obj = Some obj
+let export_inductive x = Some x
 
 let (in_inductive, out_inductive) =
   let od = {
@@ -200,11 +187,11 @@ let declare_mind mie =
     | (id,_,_,_)::_ -> id
     | [] -> anomaly "cannot declare an empty list of inductives"
   in
-  let sp = add_leaf id CCI (in_inductive (mie,is_implicit_args())) in
+  let sp = add_leaf id CCI (in_inductive mie) in
+  if is_implicit_args() then declare_inductive_implicits sp;
   sp
 
-
-(* Test and access functions. *)
+(*s Test and access functions. *)
 
 let is_constant sp = 
   try let _ = Global.lookup_constant sp in true with Not_found -> false
diff --git a/library/declare.mli b/library/declare.mli
index e1fb407f30..95aa8be8f6 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -44,7 +44,7 @@ val declare_mind : mutual_inductive_entry -> section_path
 
 val declare_eliminations : section_path -> int -> unit
 
-val out_inductive : Libobject.obj -> mutual_inductive_entry * bool
+val out_inductive : Libobject.obj -> mutual_inductive_entry 
 
 val make_strength : string list -> strength
 val make_strength_0 : unit -> strength
diff --git a/library/impargs.ml b/library/impargs.ml
index 5248bc4a61..e2ec4a4762 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -7,6 +7,8 @@ open Reduction
 open Declarations
 open Environ
 open Inductive
+open Libobject
+open Lib
 
 type implicits =
   | Impl_auto of int list
@@ -43,18 +45,30 @@ let list_of_implicits = function
   | Impl_manual l -> l
   | No_impl -> []
 
-(* Constants. *)
+(*s Constants. *)
 
 let constants_table = ref Spmap.empty
 
-let declare_constant_implicits sp =
+let compute_constant_implicits sp =
   let env = Global.env () in
   let cb = lookup_constant sp env in
-  let imps = auto_implicits env (body_of_type cb.const_type) in
+  auto_implicits env (body_of_type cb.const_type)
+
+let cache_constant_implicits (_,(sp,imps)) = 
   constants_table := Spmap.add sp imps !constants_table
 
-let declare_constant_manual_implicits sp imps =
-  constants_table := Spmap.add sp (Impl_manual imps) !constants_table
+let (in_constant_implicits, _) =
+  let od = {
+    cache_function = cache_constant_implicits;
+    load_function = cache_constant_implicits;
+    open_function = (fun _ -> ());
+    export_function = (fun x -> Some x) }
+  in
+  declare_object ("CONSTANT-IMPLICITS", od)
+
+let declare_constant_implicits sp =
+  let imps = compute_constant_implicits sp in
+  add_anonymous_leaf (in_constant_implicits (sp,imps))
 
 let constant_implicits sp =
   try Spmap.find sp !constants_table with Not_found -> No_impl
@@ -62,14 +76,14 @@ let constant_implicits sp =
 let constant_implicits_list sp =
   list_of_implicits (constant_implicits sp)
 
-(* Inductives and constructors. Their implicit arguments are stored
+(*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
    $i$ are the implicit arguments of the inductive and $v$ the array of 
    implicit arguments of the constructors. *)
 
 let inductives_table = ref Spmap.empty
 
-let declare_inductive_implicits sp =
+let compute_inductive_implicits sp =
   let env = Global.env () in
   let mib = lookup_mind sp env in
   let env_ar = push_rels (mind_arities_context mib) env in
@@ -78,9 +92,24 @@ let declare_inductive_implicits sp =
      Array.map (fun c -> auto_implicits env_ar (body_of_type c))
        (mind_user_lc mip))
   in
-  let imps = Array.map imps_one_inductive mib.mind_packets in
+  Array.map imps_one_inductive mib.mind_packets
+
+let cache_inductive_implicits (_,(sp,imps)) =
   inductives_table := Spmap.add sp imps !inductives_table
-    
+
+let (in_inductive_implicits, _) =
+  let od = {
+    cache_function = cache_inductive_implicits;
+    load_function = cache_inductive_implicits;
+    open_function = (fun _ -> ());
+    export_function = (fun x -> Some x) }
+  in
+  declare_object ("INDUCTIVE-IMPLICITS", od)
+ 
+let declare_inductive_implicits sp =
+  let imps = compute_inductive_implicits sp in
+  add_anonymous_leaf (in_inductive_implicits (sp,imps))
+
 let inductive_implicits (sp,i) =
   try
     let imps = Spmap.find sp !inductives_table in fst imps.(i)
@@ -99,20 +128,35 @@ let constructor_implicits_list constr_sp =
 let inductive_implicits_list ind_sp =
   list_of_implicits (inductive_implicits ind_sp)
 
-(* Variables. *)
+(*s Variables. *)
 
 let var_table = ref Spmap.empty
 
-let declare_var_implicits sp =
+let compute_var_implicits sp =
   let env = Global.env () in
   let (_,ty) = lookup_named (basename sp) env in
-  let imps = auto_implicits env (body_of_type ty) in
+  auto_implicits env (body_of_type ty)
+
+let cache_var_implicits (_,(sp,imps)) =
   var_table := Spmap.add sp imps !var_table
 
+let (in_var_implicits, _) =
+  let od = {
+    cache_function = cache_var_implicits;
+    load_function = cache_var_implicits;
+    open_function = (fun _ -> ());
+    export_function = (fun x -> Some x) }
+  in
+  declare_object ("VARIABLE-IMPLICITS", od)
+
+let declare_var_implicits sp =
+  let imps = compute_var_implicits sp in
+  add_anonymous_leaf (in_var_implicits (sp,imps))
+
 let implicits_of_var sp =
   list_of_implicits (try Spmap.find sp !var_table with Not_found -> No_impl)
 
-(* Tests if declared implicit *)
+(*s Tests if declared implicit *)
 
 let is_implicit_constant sp =
   try let _ = Spmap.find sp !constants_table in true with Not_found -> false
@@ -130,7 +174,7 @@ let implicits_of_global = function
   | ConstructRef csp ->	list_of_implicits (constructor_implicits csp)
   | EvarRef _ -> []
 
-(* Registration as global tables and roolback. *)
+(*s Registration as global tables and rollback. *)
 
 type frozen_t = bool
               * implicits Spmap.t 
diff --git a/library/impargs.mli b/library/impargs.mli
index cbe31a3af2..3da01fe090 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -7,8 +7,8 @@ open Term
 open Inductive
 (*i*)
 
-(* Implicit arguments. Here we store the implicit arguments. Notice that we 
-   are outside the kernel, which knows nothing about implicit arguments. *)
+(*s Implicit arguments. Here we store the implicit arguments. Notice that we 
+    are outside the kernel, which knows nothing about implicit arguments. *)
 
 type implicits =
   | Impl_auto of int list
@@ -22,11 +22,15 @@ val with_implicits : bool -> ('a -> 'b) -> 'a -> 'b
 
 val list_of_implicits : implicits -> int list
 
-val declare_constant_implicits : section_path -> unit
-val declare_constant_manual_implicits : section_path -> int list -> unit
-val constant_implicits : section_path -> implicits
+(*s Computation of implicits (done using the global environment). *)
 
+val declare_var_implicits : section_path -> unit
+val declare_constant_implicits : section_path -> unit
 val declare_inductive_implicits : section_path -> unit
+
+(*s Access to already computed implicits. *)
+
+val constant_implicits : section_path -> implicits
 val inductive_implicits : inductive_path -> implicits
 val constructor_implicits : constructor_path -> implicits
 
@@ -34,7 +38,6 @@ val constructor_implicits_list : constructor_path -> int list
 val inductive_implicits_list : inductive_path -> int list
 val constant_implicits_list : section_path -> int list
 
-val declare_var_implicits : section_path -> unit
 val implicits_of_var : section_path -> int list
 
 val is_implicit_constant : section_path -> bool
@@ -43,6 +46,8 @@ val is_implicit_var : section_path -> bool
 
 val implicits_of_global : global_reference -> int list
 
+(*s Rollback. *)
+
 type frozen_t
 val freeze : unit -> frozen_t
 val unfreeze : frozen_t -> unit
diff --git a/library/lib.ml b/library/lib.ml
index b307ee5f55..7d7e9e2c81 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -201,7 +201,6 @@ type frozen = string option * library_segment
 
 let freeze () = (!module_name, !lib_stk)
 
-(* module_name is not set ? *)
 let unfreeze (mn,stk) =
   module_name := mn;
   lib_stk := stk;