diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-30 14:33:42 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-30 14:33:42 +0000 |
commit | 5d5a92c9d6da1c1b23ca64e40c17e9c5f4772daa (patch) | |
tree | 2b75a08cb085577ff85e27180212457b3460116a | |
parent | 61edbfce11285443be098bbceddb7f8f04d2a5b0 (diff) |
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
-rw-r--r-- | plugins/extraction/extraction.ml | 59 | ||||
-rw-r--r-- | plugins/extraction/g_extraction.ml4 | 6 | ||||
-rw-r--r-- | plugins/extraction/miniml.mli | 3 | ||||
-rw-r--r-- | plugins/extraction/mlutil.ml | 18 | ||||
-rw-r--r-- | plugins/extraction/mlutil.mli | 3 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 42 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 6 |
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 *) |