diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-12-04 18:39:47 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-12-12 18:51:37 +0100 |
| commit | ec5455d7351c05a58ae99d5a300dc8576f8c9360 (patch) | |
| tree | e6a743dd1ba73d7da849d4d08374d7df81500120 /plugins/extraction/mlutil.mli | |
| parent | a4d48ce98d7ae0cf07c653ed75700ed6f182936a (diff) | |
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.
Diffstat (limited to 'plugins/extraction/mlutil.mli')
| -rw-r--r-- | plugins/extraction/mlutil.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 0a71d2c83..c380dfb3e 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 |