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/mlutil.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'plugins/extraction/mlutil.mli') diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 0a71d2c838..c380dfb3e3 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -67,7 +67,8 @@ val type_expunge : abbrev_map -> ml_type -> ml_type val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type val eq_ml_type : ml_type -> ml_type -> bool -val isDummy : ml_type -> bool +val isTdummy : ml_type -> bool +val isMLdummy : ml_ast -> bool val isKill : sign -> bool val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast @@ -125,8 +126,8 @@ exception Impossible type sign_kind = | EmptySig | NonLogicalSig (* at least a [Keep] *) - | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *) | SafeLogicalSig (* only [Kill Ktype] *) + | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *) val sign_kind : signature -> sign_kind -- cgit v1.2.3 From 4b197ed247d1f30ff40fa59f85b070766f305bea Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 15 Dec 2015 11:15:00 +0100 Subject: Extraction: replace unused variable names by _ in funs and matchs (fix #2842) This is done via a unique pass which seems roughly linear in practice, even on big developments like CompCert. There's a List.nth in an env at each MLrel, that could be made logarithmic if necessary via Okasaki's skew list for instance. Another approach would be to keep names (as a form of documentation), but prefix them by _ to please OCaml's warnings. For now, let's be radical and use the _ pattern. --- plugins/extraction/mlutil.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'plugins/extraction/mlutil.mli') diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index c380dfb3e3..c07cee7136 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -111,6 +111,8 @@ val ast_subst : ml_ast -> ml_ast -> ml_ast val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast +val dump_unused_vars : ml_ast -> ml_ast + val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast val inline : global_reference -> ml_ast -> bool -- 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/mlutil.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/mlutil.mli') diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index c07cee7136..c667552490 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*