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.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 648f232114..a6734dae86 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -38,8 +38,8 @@ val error_MPfile_as_mod : module_path -> bool -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit val check_loaded_modfile : module_path -> unit -val msg_non_implicit : global_reference -> int -> Name.t -> string -val error_non_implicit : string -> 'a +val msg_of_implicit : kill_reason -> string +val err_or_warn_remaining_implicit : kill_reason -> unit val info_file : string -> unit @@ -166,7 +166,7 @@ val to_keep : global_reference -> bool (*s Table for implicits arguments *) -val implicits_of_global : global_reference -> int list +val implicits_of_global : global_reference -> Int.Set.t (*s Table for user-given custom ML extractions. *) -- 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.mli | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index a6734dae86..916cf3ad6b 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -55,7 +55,6 @@ val string_of_modfile : module_path -> string val file_of_modfile : module_path -> string val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool -val visible_con : constant -> bool val mp_length : module_path -> int val prefixes_mp : module_path -> MPset.t val common_prefix_from_list : @@ -65,14 +64,22 @@ val labels_of_ref : global_reference -> module_path * Label.t list (*s Some table-related operations *) -val add_term : constant -> ml_decl -> unit -val lookup_term : constant -> ml_decl +(* For avoiding repeated extraction of the same constant or inductive, + we use cache functions below. Indexing by constant name isn't enough, + due to modules we could have a same constant name but different + content. So we check that the [constant_body] hasn't changed from + recording time to retrieving time. Same for inductive : we store + [mutual_inductive_body] as checksum. In both case, we should ideally + also check the env *) -val add_type : constant -> ml_schema -> unit -val lookup_type : constant -> ml_schema +val add_typedef : constant -> constant_body -> ml_type -> unit +val lookup_typedef : constant -> constant_body -> ml_type option + +val add_cst_type : constant -> constant_body -> ml_schema -> unit +val lookup_cst_type : constant -> constant_body -> ml_schema option val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit -val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind +val lookup_ind : mutual_inductive -> mutual_inductive_body -> ml_ind option val add_inductive_kind : mutual_inductive -> inductive_kind -> unit val is_coinductive : global_reference -> bool -- cgit v1.2.3 From 23cbf43f353c50fa72b72d694611c5c14367cea2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 6 Jan 2016 00:58:42 +0100 Subject: Protect code against changes in Map interface. The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps. --- plugins/extraction/table.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 916cf3ad6b..4e638a0ace 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -13,7 +13,7 @@ open Miniml open Declarations module Refset' : CSig.SetS with type elt = global_reference -module Refmap' : Map.S with type key = global_reference +module Refmap' : CSig.MapS with type key = global_reference val safe_basename_of_global : global_reference -> Id.t -- 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.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 4e638a0ace..2b163610e9 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*