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

7 files changed, 118 insertions, 19 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e7b5f31fc..69090bdd2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -146,6 +146,19 @@ let rec no_final_keeps = function
   | [] -> []
   | k :: s -> let s' = k :: no_final_keeps s in if s' = [Keep] then [] else s'
 
+(* Enriching a signature with implicit information *)
+
+let sign_with_implicits r s =
+  let implicits = implicits_of_global r in
+  let rec add_impl i = function
+    | [] -> []
+    | sign::s ->
+	let sign' =
+	  if sign = Keep && List.mem i implicits then Kill Kother else sign
+	in sign' :: add_impl (succ i) s
+  in
+  add_impl 1 s
+
 (*S Management of type variable contexts. *)
 
 (* A De Bruijn variable context (db) is a context for translating Coq [Rel]
@@ -459,13 +472,12 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     i
 
 (*s [extract_type_cons] extracts the type of an inductive
-  constructor toward the corresponding list of ML types. *)
+  constructor toward the corresponding list of ML types.
 
-(* \begin{itemize}
-   \item [db] is a context for translating Coq [Rel] into ML type [Tvar]
-   \item [dbmap] is a translation map (produced by a call to [parse_in_args])
-   \item [i] is the rank of the current product (initially [params_nb+1])
-   \end{itemize} *)
+   - [db] is a context for translating Coq [Rel] into ML type [Tvar]
+   - [dbmap] is a translation map (produced by a call to [parse_in_args])
+   - [i] is the rank of the current product (initially [params_nb+1])
+*)
 
 and extract_type_cons env db dbmap c i =
   match kind_of_term (whd_betadeltaiota env none c) with
@@ -505,6 +517,7 @@ and expand env = type_expand (mlt_env env)
 and type2signature env = type_to_signature (mlt_env env)
 let type2sign env = type_to_sign (mlt_env env)
 let type_expunge env = type_expunge (mlt_env env)
+let type_expunge_from_sign env = type_expunge_from_sign (mlt_env env)
 
 (*s Extraction of the type of a constant. *)
 
@@ -636,6 +649,7 @@ and extract_cst_app env mle mlt kn args =
   let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
   (* Now, the extraction of the arguments. *)
   let s_full = type2signature env (snd schema) in
+  let s_full = sign_with_implicits (ConstRef kn) s_full in
   let s = no_final_keeps s_full in
   let ls = List.length s in
   let la = List.length args in
@@ -694,6 +708,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let type_cons = instantiation (nb_tvars, type_cons) in
   (* Then, the usual variables [s], [ls], [la], ... *)
   let s = List.map (type2sign env) types in
+  let s = sign_with_implicits (ConstructRef cp) s in
   let ls = List.length s in
   let la = List.length args in
   assert (la <= ls + params_nb);
@@ -760,16 +775,23 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
       let a = extract_term env mle type_head c [] in
       (* The extraction of each branch. *)
       let extract_branch i =
+	let r = ConstructRef (ip,i+1) in
 	(* The types of the arguments of the corresponding constructor. *)
 	let f t = type_subst_vect metas (expand env t) in
 	let l = List.map f oi.ip_types.(i) in
 	(* the corresponding signature *)
 	let s = List.map (type2sign env) oi.ip_types.(i) in
+	let s = sign_with_implicits r s in
 	(* Extraction of the branch (in functional form). *)
 	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
 	(* We suppress dummy arguments according to signature. *)
-	let ids,e = case_expunge s e in
-	(ConstructRef (ip,i+1), List.rev ids, e)
+	try
+	  let ids,e = case_expunge s e in
+	  (r, List.rev ids, e)
+	with Occurs i ->
+	  let n = List.length s in
+	  assert ((0<i) && (i <= n));
+	  error_non_implicit r (n-i+1) None
       in
       if mi.ind_info = Singleton then
 	begin
@@ -819,6 +841,8 @@ let extract_std_constant env kn body typ =
   (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
   let l,t' = type_decomp (expand env (var2var' t)) in
   let s = List.map (type2sign env) l in
+  (* Check for user-declared implicit information *)
+  let s = sign_with_implicits (ConstRef kn) s in
   (* Decomposing the top level lambdas of [body].
      If there isn't enough, it's ok, as long as remaining args
      aren't to be pruned (and initial lambdas aren't to be all
@@ -849,7 +873,11 @@ let extract_std_constant env kn body typ =
   (* The real extraction: *)
   let e = extract_term env mle t' c [] in
   (* Expunging term and type from dummy lambdas. *)
-  term_expunge s (ids,e), type_expunge env t
+  try
+    term_expunge s (ids,e), type_expunge_from_sign env s t
+  with Occurs i ->
+    assert ((0 < i) && (i <= n));
+    error_non_implicit (ConstRef kn) (n-i+1) (Some (fst (List.nth rels (i-1))))
 
 let extract_fixpoint env vkn (fi,ti,ci) =
   let n = Array.length vkn in
@@ -934,9 +962,18 @@ let extract_with_type env cb =
 let extract_inductive env kn =
   let ind = extract_ind env kn in
   add_recursors env kn;
-  let f l = List.filter (fun t -> not (isDummy (expand env t))) l in
+  let f i j l =
+    let implicits = implicits_of_global (ConstructRef ((kn,i),j+1)) in
+    let rec filter i = function
+      | [] -> []
+      | t::l ->
+	  let l' = filter (succ i) l in
+	  if isDummy (expand env t) || List.mem i implicits then l'
+	  else t::l'
+    in filter 1 l
+  in
   let packets =
-    Array.map (fun p -> { p with ip_types = Array.map f p.ip_types })
+    Array.mapi (fun i p -> { p with ip_types = Array.mapi (f i) p.ip_types })
       ind.ind_packets
   in { ind with ind_packets = packets }
 
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 60a2e91a2..f8354f52e 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -89,6 +89,12 @@ VERNAC COMMAND EXTEND ResetExtractionInline
   -> [ reset_extraction_inline () ]
 END
 
+VERNAC COMMAND EXTEND ExtractionImplicit
+(* Custom implicit arguments of some csts/inds/constructors *)
+| [ "Extraction" "Implicit" global(r) "[" integer_list(l) "]" ]
+  -> [ extraction_implicit r l ]
+END
+
 VERNAC COMMAND EXTEND ExtractionBlacklist
 (* Force Extraction to not use some filenames *)
 | [ "Extraction" "Blacklist" ne_ident_list(l) ]
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index effc7af46..e936d2dbf 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -18,7 +18,8 @@ open Libnames
    object. *)
 
 (* We eliminate from terms:  1) types 2) logical parts.
-   [Kother] stands both for logical or unknown reason. *)
+   [Kother] stands both for logical or other reasons
+   (for instance user-declared implicit arguments w.r.t. extraction). *)
 
 type kill_reason = Ktype | Kother
 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 630a59e9d..89254d8dc 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -315,8 +315,7 @@ let sign_of_id = function
 
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
-let type_expunge env t =
-  let s = type_to_signature env t in
+let type_expunge_from_sign env s t =
   if s = [] then t
   else if List.mem Keep s then
     let rec f t s =
@@ -337,6 +336,9 @@ let type_expunge env t =
     Tarr (Tdummy Kother, snd (type_decomp (type_weak_expand env t)))
   else snd (type_decomp (type_weak_expand env t))
 
+let type_expunge env t =
+  type_expunge_from_sign env (type_to_signature env t) t
+
 (*S Generic functions over ML ast terms. *)
 
 let mlapp f a = if a = [] then f else MLapp (f,a)
@@ -489,13 +491,17 @@ let ast_subst e =
    [v] array: [(Rel i)] becomes [v.(i-1)]. [d] is the correction applies
    to [Rel] greater than [Array.length v]. *)
 
+exception Occurs of int
+
 let gen_subst v d t =
   let rec subst n = function
     | MLrel i as a ->
 	let i'= i-n in
 	if i' < 1 then a
 	else if i' <= Array.length v then
-	  ast_lift n v.(i'-1)
+	  match v.(i'-1) with
+	    | None -> raise (Occurs i')
+	    | Some u -> ast_lift n u
 	else MLrel (i+d)
     | a -> ast_map_lift subst n a
   in subst 0 t
@@ -881,12 +887,12 @@ let kill_some_lams bl (ids,c) =
   if n = n' then ids,c
   else if n' = 0 then [],ast_lift (-n) c
   else begin
-    let v = Array.make n MLdummy in
+    let v = Array.make n None in
     let rec parse_ids i j = function
       | [] -> ()
-      | Keep :: l -> v.(i) <- MLrel j; parse_ids (i+1) (j+1) l
+      | Keep :: l -> v.(i) <- Some (MLrel j); parse_ids (i+1) (j+1) l
       | Kill _ :: l -> parse_ids (i+1) j l
-    in parse_ids 0 1 bl ;
+    in parse_ids 0 1 bl;
     select_via_bl bl ids, gen_subst v (n'-n) c
   end
 
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 8691d0181..f4ab66746 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -63,6 +63,7 @@ val type_expand : abbrev_map -> ml_type -> ml_type
 val type_to_sign : abbrev_map -> ml_type -> sign
 val type_to_signature : abbrev_map -> ml_type -> signature
 val type_expunge : abbrev_map -> ml_type -> ml_type
+val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type
 
 val isDummy : ml_type -> bool
 val isKill : sign -> bool
@@ -111,5 +112,5 @@ val normalize : ml_ast -> ml_ast
 val optimize_fix : ml_ast -> ml_ast
 val inline : global_reference -> ml_ast -> bool
 
-
+exception Occurs of int
 
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
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index b8cdea3b6..f02e73190 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -31,6 +31,7 @@ val error_record : global_reference -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 val check_loaded_modfile : module_path -> unit
+val error_non_implicit : global_reference -> int -> name option -> 'a
 
 val info_file : string -> unit
 
@@ -120,6 +121,10 @@ val modular : unit -> bool
 val to_inline : global_reference -> bool
 val to_keep : global_reference -> bool
 
+(*s Table for implicits arguments *)
+
+val implicits_of_global : global_reference -> int list
+
 (*s Table for user-given custom ML extractions. *)
 
 (* UGLY HACK: registration of a function defined in [extraction.ml] *)
@@ -139,6 +144,7 @@ val reset_extraction_inline : unit -> unit
 val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
 val extract_inductive : reference -> string * string list -> unit
+val extraction_implicit : reference -> int list -> unit
 
 (*s Table of blacklisted filenames *)