diff options
| author | letouzey | 2010-04-16 14:12:57 +0000 |
|---|---|---|
| committer | letouzey | 2010-04-16 14:12:57 +0000 |
| commit | f57a38bb53dc06cef1cee78c60946aa5e6d3cf0b (patch) | |
| tree | b8e8006cb5ecd58174fcc76ccb2e90d437906996 /plugins/extraction/miniml.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/miniml.mli')
| -rw-r--r-- | plugins/extraction/miniml.mli | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 91c60d2055..00df1a98d3 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -92,15 +92,20 @@ type ml_ind = { (*s ML terms. *) +type ml_ident = + | Dummy + | Id of identifier + | Tmp of identifier + type ml_ast = | MLrel of int | MLapp of ml_ast * ml_ast list - | MLlam of identifier * ml_ast - | MLletin of identifier * ml_ast * ml_ast + | MLlam of ml_ident * ml_ast + | MLletin of ml_ident * ml_ast * ml_ast | MLglob of global_reference | MLcons of inductive_info * global_reference * ml_ast list | MLcase of (inductive_info*case_info) * ml_ast * - (global_reference * identifier list * ml_ast) array + (global_reference * ml_ident list * ml_ast) array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy |