Extraction: an experimental command to get rid of some cst/constructor arguments

 The command : Extraction Implicit foo [1 3].
 will tell the extraction to consider fst and third arg of foo as implicit,
 and remove them, unless a final occur-check after extraction shows they
 are still there. Here, foo can be a inductive constructor or a global
 constant.

 This allow typicaly to extract vectors into usual list :-)

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

1 files changed, 42 insertions, 0 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 36ba0cd7d..8ac6545bb 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -321,6 +321,15 @@ let error_record r =
   err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
        fnl () ++ str "To help extraction, please use an explicit name.")
 
+let error_non_implicit r n oid =
+  let name = match oid with
+    | None -> mt ()
+    | Some id -> str "(" ++ pr_name id ++ str ") "
+  in
+  err (str ("The "^(ordinal n)^" argument ") ++ name ++ str "of " ++
+       safe_pr_global r ++ str " still occurs after extraction." ++
+       fnl () ++ str "Please check the Extraction Implicit declarations.")
+
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp -> if not (Library.library_is_loaded dp) then
       let mp1 = (fst(Lib.current_prefix())) in
@@ -522,6 +531,39 @@ let (reset_inline,_) =
 
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
+(*s Extraction Implicit *)
+
+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
+
+(* Registration of operations for rollback. *)
+
+let (implicit_extraction,_) =
+  declare_object
+    {(default_object "Extraction Implicit") with
+       cache_function = (fun (_,(r,l)) -> add_implicits r l);
+       load_function = (fun _ (_,(r,l)) -> add_implicits r l);
+       classify_function = (fun o -> Substitute o);
+       subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l))
+    }
+
+let _ = declare_summary "Extraction Implicit"
+	  { freeze_function = (fun () -> !implicits_table);
+	    unfreeze_function = ((:=) implicits_table);
+	    init_function = (fun () -> implicits_table := Refmap.empty) }
+
+(* Grammar entries. *)
+
+let extraction_implicit r l =
+  check_inside_section ();
+  Lib.add_anonymous_leaf (implicit_extraction (Nametab.global r,l))
+
+
 (*s Extraction Blacklist of filenames not to use while extracting *)
 
 let blacklist_table = ref Idset.empty