Extraction Implicits: can accept argument names instead of just positions

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

3 files changed, 39 insertions, 5 deletions

diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index b2256c471..18828241c 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -14,6 +14,10 @@ open Vernacexpr
 open Pcoq
 open Genarg
 open Pp
+open Names
+open Nameops
+open Table
+open Extract_env
 
 let pr_mlname _ _ _ s = spc () ++ qs s
 
@@ -24,8 +28,16 @@ ARGUMENT EXTEND mlname
 | [ string(s) ] -> [ s ]
 END
 
-open Table
-open Extract_env
+let pr_int_or_id _ _ _ = function
+  | ArgInt i -> int i
+  | ArgId id -> pr_id id
+
+ARGUMENT EXTEND int_or_id
+  TYPED AS int_or_id
+  PRINTED BY pr_int_or_id
+| [ preident(id) ] -> [ ArgId (id_of_string id) ]
+| [ integer(i) ] -> [ ArgInt i ]
+END
 
 let pr_language = function
   | Ocaml -> str "Ocaml"
@@ -91,7 +103,7 @@ END
 
 VERNAC COMMAND EXTEND ExtractionImplicit
 (* Custom implicit arguments of some csts/inds/constructors *)
-| [ "Extraction" "Implicit" global(r) "[" integer_list(l) "]" ]
+| [ "Extraction" "Implicit" global(r) "[" int_or_id_list(l) "]" ]
   -> [ extraction_implicit r l ]
 END
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 3cac73998..a380654c6 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -537,13 +537,32 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 (*s Extraction Implicit *)
 
+type int_or_id = ArgInt of int | ArgId of identifier
+
 let implicits_table = ref Refmap.empty
 
 let implicits_of_global r =
  try Refmap.find r !implicits_table with Not_found -> []
 
 let add_implicits r l =
-  implicits_table := Refmap.add r l !implicits_table
+  let typ = Global.type_of_global r in
+  let rels,_ =
+    decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in
+  let names = List.rev_map fst rels in
+  let n = List.length names in
+  let check = function
+    | ArgInt i ->
+	if 1 <= i && i <= n then i
+	else err (int i ++ str " is not a valid argument number for " ++
+		  safe_pr_global r)
+    | ArgId id ->
+	(try list_index (Name id) names
+	 with Not_found ->
+	   err (str "No argument " ++ pr_id id ++ str " for " ++
+		safe_pr_global r))
+  in
+  let l' = List.map check l in
+  implicits_table := Refmap.add r l' !implicits_table
 
 (* Registration of operations for rollback. *)
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 04d90b881..b215e373e 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -149,7 +149,10 @@ val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
 val extract_inductive :
   reference -> string -> string list -> string option -> unit
-val extraction_implicit : reference -> int list -> unit
+
+
+type int_or_id = ArgInt of int | ArgId of identifier
+val extraction_implicit : reference -> int_or_id list -> unit
 
 (*s Table of blacklisted filenames *)