implicites manuels

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

4 files changed, 117 insertions, 34 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 92af41512..b90dc2215 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -188,7 +188,7 @@ let declare_mind mie =
     | [] -> anomaly "cannot declare an empty list of inductives"
   in
   let sp = add_leaf id CCI (in_inductive mie) in
-  if is_implicit_args() then declare_inductive_implicits sp;
+  if is_implicit_args() then declare_mib_implicits sp;
   sp
 
 (*s Test and access functions. *)
diff --git a/library/impargs.ml b/library/impargs.ml
index e2ec4a476..cf2d09d61 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -81,9 +81,53 @@ let constant_implicits_list sp =
    $i$ are the implicit arguments of the inductive and $v$ the array of 
    implicit arguments of the constructors. *)
 
-let inductives_table = ref Spmap.empty
+module Inductive_path = struct
+  type t = inductive_path
+  let compare (spx,ix) (spy,iy) = 
+    let c = ix - iy in if c = 0 then sp_ord spx spy else c
+end
 
-let compute_inductive_implicits sp =
+module Indmap = Map.Make(Inductive_path)
+
+let inductives_table = ref Indmap.empty
+
+module Construtor_path = struct
+  type t = constructor_path
+  let compare (indx,ix) (indy,iy) = 
+    let c = ix - iy in if c = 0 then Inductive_path.compare indx indy else c
+end
+
+module Constrmap = Map.Make(Construtor_path)
+
+let inductives_table = ref Indmap.empty
+
+let constructors_table = ref Constrmap.empty
+
+let cache_inductive_implicits (_,(indp,imps)) =
+  inductives_table := Indmap.add indp 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 cache_constructor_implicits (_,(consp,imps)) =
+  constructors_table := Constrmap.add consp imps !constructors_table
+
+let (in_constructor_implicits, _) =
+  let od = {
+    cache_function = cache_constructor_implicits;
+    load_function = cache_constructor_implicits;
+    open_function = (fun _ -> ());
+    export_function = (fun x -> Some x) }
+  in
+  declare_object ("CONSTRUCTOR-IMPLICITS", od)
+
+let compute_mib_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
@@ -94,33 +138,35 @@ let compute_inductive_implicits sp =
   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 cache_mib_implicits (_,(sp,mibimps)) =
+  Array.iteri
+    (fun i (imps,v) ->
+       let indp = (sp,i) in
+       inductives_table := Indmap.add indp imps !inductives_table;
+       Array.iteri 
+	 (fun j imps ->
+	    constructors_table := 
+	      Constrmap.add (indp,succ j) imps !constructors_table) v)
+    mibimps
+
+let (in_mib_implicits, _) =
   let od = {
-    cache_function = cache_inductive_implicits;
-    load_function = cache_inductive_implicits;
+    cache_function = cache_mib_implicits;
+    load_function = cache_mib_implicits;
     open_function = (fun _ -> ());
     export_function = (fun x -> Some x) }
   in
-  declare_object ("INDUCTIVE-IMPLICITS", od)
+  declare_object ("MIB-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)
-  with Not_found -> 
-    No_impl
-
-let constructor_implicits ((sp,i),j) =
-  try
-    let imps = Spmap.find sp !inductives_table in (snd imps.(i)).(pred j)
-  with Not_found -> 
-    No_impl
+let declare_mib_implicits sp =
+  let imps = compute_mib_implicits sp in
+  add_anonymous_leaf (in_mib_implicits (sp,imps))
+
+let inductive_implicits indp =
+  try Indmap.find indp !inductives_table with Not_found -> No_impl
+
+let constructor_implicits consp =
+  try Constrmap.find consp !constructors_table with Not_found -> No_impl
 
 let constructor_implicits_list constr_sp = 
   list_of_implicits (constructor_implicits constr_sp)
@@ -156,13 +202,43 @@ let declare_var_implicits sp =
 let implicits_of_var sp =
   list_of_implicits (try Spmap.find sp !var_table with Not_found -> No_impl)
 
+(*s Implicits of a global reference. *)
+
+let declare_implicits = function
+  | VarRef sp -> 
+      declare_var_implicits sp
+  | ConstRef sp -> 
+      declare_constant_implicits sp
+  | IndRef ((sp,i) as indp) -> 
+      let mib_imps = compute_mib_implicits sp in
+      let imps = fst mib_imps.(i) in
+      add_anonymous_leaf (in_inductive_implicits (indp, imps))
+  | ConstructRef (((sp,i),j) as consp) -> 
+      let mib_imps = compute_mib_implicits sp in
+      let imps = (snd mib_imps.(i)).(j-1) in
+      add_anonymous_leaf (in_constructor_implicits (consp, imps))
+  | EvarRef _ -> assert false
+
+let declare_manual_implicits r l = match r with
+  | VarRef sp -> 
+      add_anonymous_leaf (in_var_implicits (sp,Impl_manual l))
+  | ConstRef sp ->
+      add_anonymous_leaf (in_constant_implicits (sp,Impl_manual l))
+  | IndRef indp ->
+      add_anonymous_leaf (in_inductive_implicits (indp,Impl_manual l))
+  | ConstructRef consp -> 
+      add_anonymous_leaf (in_constructor_implicits (consp,Impl_manual l))
+  | EvarRef _ -> 
+      assert false
+
 (*s Tests if declared implicit *)
 
 let is_implicit_constant sp =
   try let _ = Spmap.find sp !constants_table in true with Not_found -> false
 
-let is_implicit_inductive_definition sp =
-  try let _ = Spmap.find sp !inductives_table in true with Not_found -> false
+let is_implicit_inductive_definition indp =
+  try let _ = Indmap.find indp !inductives_table in true 
+  with Not_found -> false
 
 let is_implicit_var sp =
   try let _ = Spmap.find sp !var_table in true with Not_found -> false
@@ -178,21 +254,25 @@ let implicits_of_global = function
 
 type frozen_t = bool
               * implicits Spmap.t 
-              * (implicits * implicits array) array Spmap.t 
+              * implicits Indmap.t 
+	      * implicits Constrmap.t
               * implicits Spmap.t
 
 let init () =
   constants_table := Spmap.empty;
-  inductives_table := Spmap.empty;
+  inductives_table := Indmap.empty;
+  constructors_table := Constrmap.empty;
   var_table := Spmap.empty
 
 let freeze () =
-  (!implicit_args, !constants_table, !inductives_table, !var_table)
+  (!implicit_args, !constants_table, !inductives_table, 
+   !constructors_table, !var_table)
 
-let unfreeze (imps,ct,it,vt) =
+let unfreeze (imps,ct,it,const,vt) =
   implicit_args := imps;
   constants_table := ct;
   inductives_table := it;
+  constructors_table := const;
   var_table := vt
 
 let _ = 
diff --git a/library/impargs.mli b/library/impargs.mli
index 3da01fe09..e97a0a41e 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -26,7 +26,10 @@ val list_of_implicits : implicits -> int list
 
 val declare_var_implicits : section_path -> unit
 val declare_constant_implicits : section_path -> unit
-val declare_inductive_implicits : section_path -> unit
+val declare_mib_implicits : section_path -> unit
+
+val declare_implicits : global_reference -> unit
+val declare_manual_implicits : global_reference -> int list -> unit
 
 (*s Access to already computed implicits. *)
 
@@ -41,7 +44,7 @@ val constant_implicits_list : section_path -> int list
 val implicits_of_var : section_path -> int list
 
 val is_implicit_constant : section_path -> bool
-val is_implicit_inductive_definition : section_path -> bool
+val is_implicit_inductive_definition : inductive_path -> bool
 val is_implicit_var : section_path -> bool
 
 val implicits_of_global : global_reference -> int list
diff --git a/library/nametab.mli b/library/nametab.mli
index 2b0e4dd52..68e272740 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -21,7 +21,7 @@ val push_module : string -> module_contents -> unit
 
 val sp_of_id : path_kind -> identifier -> global_reference
 
-(* This returns the section_path of a constant or fails with Not_found *)
+(* This returns the section path of a constant or fails with [Not_found] *)
 val constant_sp_of_id : identifier -> section_path
 
 val locate : section_path -> global_reference