diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:12:57 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:12:57 +0000 |
| commit | f57a38bb53dc06cef1cee78c60946aa5e6d3cf0b (patch) | |
| tree | b8e8006cb5ecd58174fcc76ccb2e90d437906996 /plugins/extraction/mlutil.mli | |
| parent | a36fe20505fee708d8d88700aa7fedd4d4157364 (diff) | |
Extraction: ad-hoc identifier type with annotations for reductions
* An inductive constructor Dummy instead of a constant dummy_name
* The Tmp constructor indicates that the corresponding MLlam or
MLletin is extraction-specific and can be reduced if possible
* When inlining a glob (for instance a recursor), we tag some
lambdas as reducible. In (nat_rect Fo Fs n), the head lams of
Fo and Fs are treated this way, in order for the recursive call
inside nat_rect to be correctly pushed as deeper as possible.
* This way, we can stop allowing by default linear beta/let
reduction even under binders (can be activated back via
Set Extraction Flag).
* Btw, fix the strange definition of non_stricts for (x y).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12938 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/mlutil.mli')
| -rw-r--r-- | plugins/extraction/mlutil.mli | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 9c5feac82..7fd8006a5 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -69,22 +69,24 @@ val type_expunge : abbrev_map -> ml_type -> ml_type val isDummy : ml_type -> bool val isKill : sign -> bool -val case_expunge : signature -> ml_ast -> identifier list * ml_ast -val term_expunge : signature -> identifier list * ml_ast -> ml_ast +val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast +val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast (*s Special identifiers. [dummy_name] is to be used for dead code and will be printed as [_] in concrete (Caml) code. *) -val anonymous : identifier +val anonymous_name : identifier val dummy_name : identifier val id_of_name : name -> identifier +val id_of_mlid : ml_ident -> identifier +val tmp_id : ml_ident -> ml_ident (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns the list [idn;...;id1] and the term [t]. *) -val collect_lams : ml_ast -> identifier list * ml_ast -val collect_n_lams : int -> ml_ast -> identifier list * ml_ast +val collect_lams : ml_ast -> ml_ident list * ml_ast +val collect_n_lams : int -> ml_ast -> ml_ident list * ml_ast val nb_lams : ml_ast -> int val dummy_lams : ml_ast -> int -> ml_ast |