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

1 files changed, 8 insertions, 4 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index df9f02dfd..866f499b5 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -400,10 +400,14 @@ let flag_of_int n =
       opt_lin_let = kth_digit n 9;
       opt_lin_beta = kth_digit n 10 }
 
-(* For the moment, we allow by default everything except the type-unsafe
-   optimization [opt_case_idg]. *)
-
-let int_flag_init = 1 + 2 + 4 + 8 + 32 + 64 + 128 + 256 + 512 + 1024
+(* For the moment, we allow by default everything except :
+   - the type-unsafe optimization [opt_case_idg]
+   - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta]
+     (may lead to complexity blow-up, subsumed by finer reductions
+      when inlining recursors).
+*)
+
+let int_flag_init = 1 + 2 + 4 + 8 (*+ 16*) + 32 + 64 + 128 + 256 (*+ 512 + 1024*)
 
 let int_flag_ref = ref int_flag_init
 let opt_flag_ref = ref (flag_of_int int_flag_init)