implicites manuels

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

10 files changed, 161 insertions, 54 deletions

diff --git a/CHANGES b/CHANGES
index b5d85ac15..db1ef0b33 100644
--- a/CHANGES
+++ b/CHANGES
@@ -57,6 +57,16 @@ que les 3 primitives), on peut typer avec "constr", "tactic", ou
   Begin Silent -> Set Silent
   End Silent -> Unset Silent.
 
+- Déclaration manuelle des implicites avec
+
+	Implicits ident.
+	Implicits ident [ num num ... num ].
+
+  Petit changement de sémantique : lors de la fermeture d'une section,
+  les implicites sont calculés selon la valeur *courante* de "Implicit 
+  Arguments" et non plus selon la valeur qu'elle avait au moment de la 
+  définition dans la section.
+
 Tactiques
 
 - Langage de tactique
diff --git a/Makefile b/Makefile
index e0768feff..44c2590cb 100644
--- a/Makefile
+++ b/Makefile
@@ -298,8 +298,7 @@ REALSVO=theories/Reals/R_Ifp.vo       theories/Reals/Reals.vo \
 	theories/Reals/Rderiv.vo
 
 THEORIESVO = $(LOGICVO) $(ARITHVO) $(BOOLVO) $(ZARITHVO) $(LISTSVO) \
-             $(SETSVO) $(RELATIONSVO) $(REALSVO)
-# TODO: add $(WELLFOUNDEDVO) 
+             $(SETSVO) $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)
 
 $(THEORIESVO): states/initial.coq
 
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index e8565badd..55f3e9bf0 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -740,6 +740,12 @@ Save.
 (* End properties. *)
 End semi_rings.
 
+Implicits Cons_varlist.
+Implicits Cons_monom.
+Implicits SPconst.
+Implicits SPplus.
+Implicits SPmult.
+
 Section rings.
 
 (* Here the coercion between Ring and Semi-Ring will be useful *)
diff --git a/kernel/names.mli b/kernel/names.mli
index 79f5f0e93..323009011 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -12,7 +12,7 @@ type name = Name of identifier | Anonymous
 
 (* Constructor of an identifier;
    [make_ident] builds an identifier from a string and an optional index; if
-   the string ends by a digit, a "_" is inserted *)
+   the string ends by a digit, a ["_"] is inserted *)
 val make_ident : string -> int option -> identifier
 
 (* Some destructors of an identifier *)
@@ -36,7 +36,7 @@ val next_name_away : name -> identifier list -> identifier
 val next_name_away_with_default : 
   string -> name -> identifier list -> identifier
 
-(*s path_kind is currently degenerated, [FW] is not used *)
+(*s [path_kind] is currently degenerated, [FW] is not used *)
 type path_kind = CCI | FW | OBJ
 
 (* parsing and printing of path kinds *)
@@ -46,7 +46,7 @@ val kind_of_string : string -> path_kind
 (*s Directory paths = section names paths *)
 type dir_path = string list
 
-(* Printing of directory paths as "#module#submodule" *)
+(* Printing of directory paths as ["#module#submodule"] *)
 val string_of_dirpath : dir_path -> string
 
 (*s Section paths *)
@@ -64,12 +64,12 @@ val kind_of_path : section_path -> path_kind
 val sp_of_wd : string list -> section_path
 val wd_of_sp : section_path -> string list
 
-(* Parsing and printing of section path as "#module#id#kind" *)
+(* Parsing and printing of section path as ["#module#id#kind"] *)
 val path_of_string : string -> section_path
 val string_of_path : section_path -> string
 val print_sp : section_path -> std_ppcmds
 
-(*
+(*i
 val string_of_path_mind : section_path -> identifier -> string
 val coerce_path : path_kind -> section_path -> section_path
 val fwsp_of : section_path -> section_path
@@ -79,15 +79,15 @@ val fwsp_of_ccisp : section_path -> section_path
 val ccisp_of_fwsp : section_path -> section_path
 val append_to_path : section_path -> string -> section_path
 
-val sp_ord : section_path -> section_path -> int
 val sp_gt : section_path * section_path -> bool
-*)
+i*)
+val sp_ord : section_path -> section_path -> int
 
 (* [is_dirpath_prefix p1 p2=true] if [p1] is a prefix of or is equal to [p2] *)
 val dirpath_prefix_of : dir_path -> dir_path -> bool
-(*
+(*i
 module Spset : Set.S with type elt = section_path
-*)
+i*)
 module Spmap : Map.S with type key = section_path
 
 (*s Specific paths for declarations *)
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
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index ba584d756..866d09f7d 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -173,7 +173,7 @@ let process_object oldenv dir sec_sp
     | "INDUCTIVE" ->
 	let mib = Environ.lookup_mind sp oldenv in
 	let newsp = recalc_sp dir sp in
-	let imp = is_implicit_inductive_definition sp in
+	let imp = is_implicit_args() (* CHANGE *) in
 	let (mie,indmods,cstrmods) = 
 	  process_inductive sp newsp oldenv (ids_to_discard,work_alist) mib in
 	((Inductive(mie,imp)) :: ops, ids_to_discard,
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f60ecbd3e..e33c9655a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -436,6 +436,21 @@ let _ =
        | [] -> (fun () -> Impargs.make_implicit_args false)
        | _  -> bad_vernac_args "IMPLICIT_ARGS_OFF")
 
+let number_list = 
+  List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list") 
+
+let _ =
+  add "IMPLICITS"
+    (function 
+       | (VARG_STRING "") :: (VARG_IDENTIFIER id) :: l -> 
+	   (fun () -> 
+	      let imps = number_list l in
+	      Impargs.declare_manual_implicits (Nametab.sp_of_id CCI id) imps)
+       | [VARG_STRING "Auto"; VARG_IDENTIFIER id] -> 
+	   (fun () -> 
+	      Impargs.declare_implicits (Nametab.sp_of_id CCI id))
+       | _  -> bad_vernac_args "IMPLICITS")
+
 let _ =
   add "SaveNamed"
     (function 
@@ -588,10 +603,7 @@ let _ =
 let _ =
   add "ExplainProof"
     (function l ->
-       let l = List.map (function 
-			   | (VARG_NUMBER n) -> n 
-                           |   _   -> bad_vernac_args "ExplainProof") l
-       in
+       let l = number_list l in
        fun () ->
          let pts = get_pftreestate() in
          let evc = evc_of_pftreestate pts in
@@ -605,10 +617,7 @@ let _ =
 let _ =
   add "ExplainProofTree"
     (function l ->
-       let l = List.map (function 
-			   | (VARG_NUMBER n) -> n
-			   |   _  -> bad_vernac_args "ExplainProofTree") l
-       in 
+       let l = number_list l in 
        fun () ->
          let pts = get_pftreestate() in
          let evc = evc_of_pftreestate pts in