diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-12-15 18:56:08 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-12-15 19:04:44 +0100 |
| commit | 0a89d4805a29628c82b994958362dc9d92709020 (patch) | |
| tree | d4857b563a5f063a7a6a9a3f47ea15f84a823ba8 /plugins/extraction/table.mli | |
| parent | 34ea06f2f31cebf00bc7620fac34d963afe6a1dc (diff) | |
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.
Diffstat (limited to 'plugins/extraction/table.mli')
| -rw-r--r-- | plugins/extraction/table.mli | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index a6734dae8..916cf3ad6 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 |