From f57a38bb53dc06cef1cee78c60946aa5e6d3cf0b Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 16 Apr 2010 14:12:57 +0000 Subject: 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 --- plugins/extraction/table.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'plugins/extraction/table.ml') diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index df9f02dfd6..866f499b59 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) -- cgit v1.2.3