Utilisation de noms dans 'Implicit Arguments [...]'

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

6 files changed, 81 insertions, 32 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ec9e88c77..3ebad5ae3 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1674,7 +1674,10 @@ let xlate_vernac =
 	(reference_to_ct_ID id,
 	 match opt_positions with
 	     None -> CT_int_list[]
-	   | Some l -> CT_int_list(List.map (fun x -> CT_int x) l))
+	   | Some l ->
+	       CT_int_list
+	       (List.map (function ExplByPos x -> CT_int x | ExplByName _ ->
+		 xlate_error "TODO: explicit argument by name") l))
   | VernacReserve _ -> xlate_error "TODO: Default Variable Type"
   | VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
   | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
diff --git a/library/impargs.ml b/library/impargs.ml
index f2c37374d..831b34e05 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -20,6 +20,7 @@ open Libobject
 open Lib
 open Nametab
 open Pp
+open Topconstr
 
 (*s Flags governing the computation of implicit arguments *)
 
@@ -208,13 +209,20 @@ let add_free_rels_until strict bound env m pos acc =
 
 (* calcule la liste des arguments implicites *)
 
+let my_concrete_name avoid names t = function
+  | Anonymous -> Anonymous, avoid, Anonymous::names
+  | na -> 
+      let id = Termops.next_name_not_occuring false na avoid names t in
+      Name id, id::avoid, Name id::names
+  
 let compute_implicits_gen strict contextual env t =
-  let rec aux env n names t =
+  let rec aux env avoid n names t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
-      | Prod (x,a,b) ->
+      | Prod (na,a,b) ->
+	  let na',avoid' = Termops.concrete_name false avoid names na b in
 	  add_free_rels_until strict n env a (Hyp (n+1))
-            (aux (push_rel (x,None,a) env) (n+1) (x::names) b)
+            (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
       | _ -> 
 	  let names = List.rev names in
 	  let v = Array.map (fun na -> na,None) (Array.of_list names) in
@@ -222,8 +230,9 @@ let compute_implicits_gen strict contextual env t =
 	  else v
   in 
   match kind_of_term (whd_betadeltaiota env t) with 
-    | Prod (x,a,b) ->
-	let v = aux (push_rel (x,None,a) env) 1 [x] b in
+    | Prod (na,a,b) ->
+	let na',avoid = Termops.concrete_name false [] [] na b in
+	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
 	Array.to_list v
     | _ -> []
 
@@ -435,31 +444,55 @@ let implicits_of_global_out r =
 
 (* Declare manual implicits *)
 
-let check_range n i =
-  if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
+(*
+let check_range n = function
+  | loc,ExplByPos i ->
+      if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
+  | loc,ExplByName id ->
+()
+*)
+
+let rec list_remove a = function
+  | b::l when a = b -> l
+  | b::l -> b::list_remove a l
+  | [] -> raise Not_found
 
+let set_implicit id imp =
+  Some (id,match imp with None -> Manual | Some imp -> imp)
 
 let declare_manual_implicits r l =
   let t = Global.type_of_global r in
   let autoimps = compute_implicits_gen false true (Global.env()) t in
   let n = List.length autoimps in
-  if not (list_distinct l) then error ("Some numbers occur several time");
-  List.iter (check_range n) l;
-  let l = List.sort (-) l in
+  if not (list_distinct l) then 
+    error ("Some parameters are referred more than once");
+(*  List.iter (check_range n) l;*)
+(*  let l = List.sort (-) l in*)
   (* Compare with automatic implicits to recover printing data and names *)
-  let rec merge k = function
-    | [], [] -> []
-    | ((na,imp)::imps, p::l) when k=p ->
-	let id = match na with
-	  | Name id -> id
-	  | _ -> errorlabstrm ""
-	      (str "Cannot set implicit argument number " ++ int p ++
-	      str ": it has no name") in
-	let imp = match imp with None -> (id,Manual) | Some imp -> (id,imp) in
-	Some imp :: merge (k+1) (imps,l)
-    | _::imps, l' -> None :: merge (k+1) (imps,l')
-    | [], _ -> assert false in
-  let l = Impl_manual (merge 1 (autoimps,l)) in
+  let rec merge k l = function
+    | (Name id,imp)::imps ->
+	let l',imp =
+	  try list_remove (ExplByPos k) l, set_implicit id imp
+	  with Not_found ->
+	  try list_remove (ExplByName id) l, set_implicit id imp
+	  with Not_found ->
+	  l, None in
+	imp :: merge (k+1) l' imps
+    | (Anonymous,imp)::imps -> 
+	None :: merge (k+1) l imps
+    | [] when l = [] -> []
+    | _ ->
+	match List.hd l with
+	| ExplByName id ->
+	    error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
+	| ExplByPos i ->
+	    if i<1 or i>n then 
+	      error ("Bad implicit argument number: "^(string_of_int i))
+	    else
+	      errorlabstrm ""
+		(str "Cannot set implicit argument number " ++ int i ++
+		 str ": it has no name") in
+  let l = Impl_manual (merge 1 l autoimps) in
   let (_,oimp_out) = implicits_of_global_gen r in
   let l = l, if !Options.v7_only then oimp_out else l in
   add_anonymous_leaf (in_implicits [r,l])
diff --git a/library/impargs.mli b/library/impargs.mli
index 83ca8dfb9..1ee82c384 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -54,7 +54,8 @@ val declare_mib_implicits : mutual_inductive -> unit
 val declare_implicits : global_reference -> unit
 
 (* Manual declaration of which arguments are expected implicit *)
-val declare_manual_implicits : global_reference -> int list -> unit
+val declare_manual_implicits : global_reference -> 
+  Topconstr.explicitation list -> unit
 
 (* Get implicit arguments *)
 val is_implicit_constant : constant -> implicits_flags
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 4c096964d..cca57911b 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -436,8 +436,9 @@ GEXTEND Gram
 	   VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
 *)
       | IDENT "Implicit"; IDENT "Arguments"; qid = global; 
-           pos = OPT [ "["; l = LIST0 natural; "]" -> l ] ->
-	  VernacDeclareImplicits (qid,pos)
+         pos = OPT [ "["; l = LIST0 ident; "]" -> l ] ->
+	   let pos = option_app (List.map (fun id -> ExplByName id)) pos in
+	   VernacDeclareImplicits (qid,pos)
 
       | IDENT "Implicit"; ["Type" | "Types"];
 	   idl = LIST1 ident; ":"; c = lconstr -> VernacReserve (idl,c)
@@ -681,7 +682,7 @@ GEXTEND Gram
          "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
 
      | IDENT "Infix"; local = locality; (*a = entry_prec; n = OPT natural; *)
-	 op = STRING; p = global;
+	 op = STRING; ":="; p = global; 
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
          let (a,n,b) = Metasyntax.interp_infix_modifiers None None modl in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 3d5068304..d142f1d87 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -234,7 +234,7 @@ type vernac_expr =
   | VernacHintDestruct of locality_flag *
       identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr
   | VernacSyntacticDefinition of identifier * constr_expr * int option
-  | VernacDeclareImplicits of reference * int list option
+  | VernacDeclareImplicits of reference * explicitation list option
   | VernacReserve of identifier list * constr_expr
   | VernacSetOpacity of opacity_flag * reference list
   | VernacUnsetOption of Goptions.option_name
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 81818bb08..0e5e1c99d 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -169,6 +169,10 @@ let pr_search a b pr_p = match a with
 
 let pr_locality local = if local then str "Local " else str ""
 
+let pr_explanation imps = function
+  | ExplByPos n -> pr_id (Impargs.name_of_implicit (List.nth imps (n-1)))
+  | ExplByName id -> pr_id id
+
 let pr_class_rawexpr = function
   | FunClass -> str"Funclass"
   | SortClass -> str"Sortclass"
@@ -555,7 +559,7 @@ let rec pr_vernac = function
 	    (match a with None -> [] | Some a -> [SetAssoc a]),s
         | None -> [],s in
       hov 0 (hov 0 (str"Infix " ++ pr_locality local
-      ++ qsnew s ++ spc() ++ pr_reference q) ++
+      ++ qsnew s ++ str " :=" ++ spc() ++ pr_reference q) ++
       pr_syntax_modifiers mv8 ++
       (match sn with
     | None -> mt()
@@ -971,8 +975,11 @@ pr_vbinders bl ++ spc())
   | VernacDeclareImplicits (q,None) ->
       hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
   | VernacDeclareImplicits (q,Some l) ->
+      let r = Nametab.global q in
+      Impargs.declare_manual_implicits r l;
+      let imps = Impargs.implicits_of_global r in
       hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++
-             str"[" ++ prlist_with_sep sep int l ++ str"]")
+             str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]")
   | VernacReserve (idl,c) ->
       hov 1 (str"Implicit Type" ++
         str (if List.length idl > 1 then "s " else " ") ++
@@ -1100,7 +1107,11 @@ let pr_vernac = function
       (* Obsolete modules *)
       List.mem (string_of_id r)
 	["Refine"; "Inv"; "Equality"; "EAuto"; "AutoRewrite"; "EqDecide"; 
-         "Xml"; "Extraction"; "Tauto"; "Setoid_replace";"Elimdep"] -> mt()
+         "Xml"; "Extraction"; "Tauto"; "Setoid_replace";"Elimdep";
+	 "DatatypesSyntax"; "LogicSyntax"; "Logic_TypeSyntax";
+	 "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"] ->
+      warning ("Forgetting obsolete module "^(string_of_id r));
+      mt()
   | VernacSyntax _  | VernacGrammar _ as x -> pr_vernac x
   | x -> pr_vernac x ++ sep_end ()