From ec5455d7351c05a58ae99d5a300dc8576f8c9360 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 4 Dec 2015 18:39:47 +0100 Subject: Extraction: nicer implementation of Implicits Instead of the original hacks (embedding implicits in string msg in MLexn !) we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use of the i-th argument of constant or constructor r when this argument has been declared as implicit. A new option Set/Unset Extraction SafeImplicits controls what happens when some implicits still occur after an extraction : fail in safe mode, or otherwise produce some code nonetheless. This code is probably buggish if the implicits are actually used to do anything relevant (match, function call, etc), but it might also be fine if the implicits are just passed along. And anyway, this unsafe mode could help figure what's going on. Note: the MLdummy now expected a kill_reason, just as Tdummy. These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit. Some minor refactoring on the fly. --- plugins/extraction/table.ml | 71 ++++++++++++++++++++++++++++++--------------- 1 file changed, 48 insertions(+), 23 deletions(-) (limited to 'plugins/extraction/table.ml') diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a57c39eef1..63d792e363 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -401,16 +401,34 @@ let error_MPfile_as_mod mp b = "Monolithic Extraction cannot deal with this situation.\n"^ "Please "^s2^"use (Recursive) Extraction Library instead.\n")) -let msg_non_implicit r n id = - let name = match id with - | Anonymous -> "" - | Name id -> "(" ^ Id.to_string id ^ ") " - in - "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r) - -let error_non_implicit msg = - err (str (msg ^ " still occurs after extraction.") ++ - fnl () ++ str "Please check the Extraction Implicit declarations.") +let argnames_of_global r = + let typ = Global.type_of_global_unsafe r in + let rels,_ = + decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in + List.rev_map fst rels + +let msg_of_implicit = function + | Kimplicit (r,i) -> + let name = match List.nth (argnames_of_global r) (i-1) with + | Anonymous -> "" + | Name id -> "(" ^ Id.to_string id ^ ") " + in + (String.ordinal i)^" argument "^name^"of "^(string_of_global r) + | Ktype | Kprop -> "" + +let error_remaining_implicit k = + let s = msg_of_implicit k in + err (str ("An implicit occurs after extraction : "^s^".") ++ fnl () ++ + str "Please check your Extraction Implicit declarations." ++ fnl() ++ + str "You might also try Unset Extraction SafeImplicits to force" ++ + fnl() ++ str "the extraction of unsafe code and review it manually.") + +let warning_remaining_implicit k = + let s = msg_of_implicit k in + msg_warning + (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++ + str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl () + ++ str "but this code is potentially unsafe, please review it manually.") let check_loaded_modfile mp = match base_mp mp with | MPfile dp -> @@ -635,32 +653,39 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) (*s Extraction Implicit *) +let safe_implicit = my_bool_option "SafeImplicits" true + +let err_or_warn_remaining_implicit k = + if safe_implicit () then + error_remaining_implicit k + else + warning_remaining_implicit k + type int_or_id = ArgInt of int | ArgId of Id.t let implicits_table = Summary.ref Refmap'.empty ~name:"ExtrImplicit" let implicits_of_global r = - try Refmap'.find r !implicits_table with Not_found -> [] + try Refmap'.find r !implicits_table with Not_found -> Int.Set.empty let add_implicits r l = - let typ = Global.type_of_global_unsafe r in - let rels,_ = - decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in - let names = List.rev_map fst rels in + let names = argnames_of_global r in let n = List.length names in - let check = function + let add_arg s = function | ArgInt i -> - if 1 <= i && i <= n then i + if 1 <= i && i <= n then Int.Set.add i s else err (int i ++ str " is not a valid argument number for " ++ safe_pr_global r) | ArgId id -> - (try List.index Name.equal (Name id) names - with Not_found -> - err (str "No argument " ++ pr_id id ++ str " for " ++ - safe_pr_global r)) + try + let i = List.index Name.equal (Name id) names in + Int.Set.add i s + 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 + let ints = List.fold_left add_arg Int.Set.empty l in + implicits_table := Refmap'.add r ints !implicits_table (* Registration of operations for rollback. *) -- cgit v1.2.3 From 0a89d4805a29628c82b994958362dc9d92709020 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 15 Dec 2015 18:56:08 +0100 Subject: Extraction: more cautious use of intermediate result caching (fix #3923) During an extraction, a few tables are maintained to cache intermediate results. Due to modules, the kernel_name index for these caching tables aren't enough. For instance, in bug #3923, a constant is first transparent (from inside the module) then opaque (when seen from the signature). The previous protections were actually obsolete (tests via visible_con), we now checks that the constant_body is still the same. --- plugins/extraction/table.ml | 48 +++++++++++++++++++++++++++++++-------------- 1 file changed, 33 insertions(+), 15 deletions(-) (limited to 'plugins/extraction/table.ml') diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 63d792e363..9feaea8cdb 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -72,8 +72,6 @@ let mp_length mp = | _ -> 1 in len mp -let visible_con kn = at_toplevel (base_mp (con_modpath kn)) - let rec prefixes_mp mp = match mp with | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp') | _ -> MPset.singleton mp @@ -105,17 +103,30 @@ let labels_of_ref r = (* Theses tables are not registered within coq save/undo mechanism since we reset their contents at each run of Extraction *) -(*s Constants tables. *) +(* We use [constant_body] (resp. [mutual_inductive_body]) as checksum + to ensure that the table contents aren't outdated. *) -let terms = ref (Cmap_env.empty : ml_decl Cmap_env.t) -let init_terms () = terms := Cmap_env.empty -let add_term kn d = terms := Cmap_env.add kn d !terms -let lookup_term kn = Cmap_env.find kn !terms +(*s Constants tables. *) -let types = ref (Cmap_env.empty : ml_schema Cmap_env.t) -let init_types () = types := Cmap_env.empty -let add_type kn s = types := Cmap_env.add kn s !types -let lookup_type kn = Cmap_env.find kn !types +let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t) +let init_typedefs () = typedefs := Cmap_env.empty +let add_typedef kn cb t = + typedefs := Cmap_env.add kn (cb,t) !typedefs +let lookup_typedef kn cb = + try + let (cb0,t) = Cmap_env.find kn !typedefs in + if cb0 == cb then Some t else None + with Not_found -> None + +let cst_types = + ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t) +let init_cst_types () = cst_types := Cmap_env.empty +let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types +let lookup_cst_type kn cb = + try + let (cb0,s) = Cmap_env.find kn !cst_types in + if cb0 == cb then Some s else None + with Not_found -> None (*s Inductives table. *) @@ -124,7 +135,14 @@ let inductives = let init_inductives () = inductives := Mindmap_env.empty let add_ind kn mib ml_ind = inductives := Mindmap_env.add kn (mib,ml_ind) !inductives -let lookup_ind kn = Mindmap_env.find kn !inductives +let lookup_ind kn mib = + try + let (mib0,ml_ind) = Mindmap_env.find kn !inductives in + if mib == mib0 then Some ml_ind + else None + with Not_found -> None + +let unsafe_lookup_ind kn = snd (Mindmap_env.find kn !inductives) let inductive_kinds = ref (Mindmap_env.empty : inductive_kind Mindmap_env.t) @@ -244,10 +262,10 @@ let safe_basename_of_global r = | ConstRef kn -> Label.to_id (con_label kn) | IndRef (kn,0) -> Label.to_id (mind_label kn) | IndRef (kn,i) -> - (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename + (try (unsafe_lookup_ind kn).ind_packets.(i).ip_typename with Not_found -> last_chance r) | ConstructRef ((kn,i),j) -> - (try (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1) + (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) with Not_found -> last_chance r) | VarRef _ -> assert false @@ -876,6 +894,6 @@ let extract_inductive r s l optstr = (*s Tables synchronization. *) let reset_tables () = - init_terms (); init_types (); init_inductives (); + init_typedefs (); init_cst_types (); init_inductives (); init_inductive_kinds (); init_recursors (); init_projs (); init_axioms (); init_opaques (); reset_modfile () -- cgit v1.2.3 From 602badcad9deec9224b78cd1e1033af30358ef2e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 22:35:09 +0100 Subject: Do not compose "str" and "to_string" whenever possible. For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read. --- plugins/extraction/table.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/table.ml') diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 9feaea8cdb..30486879ee 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -453,7 +453,7 @@ let check_loaded_modfile mp = match base_mp mp with if not (Library.library_is_loaded dp) then begin match base_mp (Lib.current_mp ()) with | MPfile dp' when not (DirPath.equal dp dp') -> - err (str ("Please load library "^(DirPath.to_string dp^" first."))) + err (str "Please load library " ++ pr_dirpath dp ++ str " first.") | _ -> () end | _ -> () -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- plugins/extraction/table.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/table.ml') diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 9feaea8cdb..d7842e127d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*