aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-06-10 17:43:38 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-06-10 17:43:38 +0000
commit5ec6f9c21e446b869a11320b69bfdd51f204c691 (patch)
tree206a5e235067d464323df959aa44f063db97e743 /plugins/extraction
parent28013761c65dd011c6b5fd3990fe28be4cd4b621 (diff)
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
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/g_extraction.ml418
-rw-r--r--plugins/extraction/table.ml21
-rw-r--r--plugins/extraction/table.mli5
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 *)