diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-08 14:07:46 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-08 14:07:46 +0000 |
commit | 9a69dd9a3f0b4ffe94d5ef4670858f7a7e99f405 (patch) | |
tree | fb68b099fa629185bd1f48d82d0e3b0d10a3d246 | |
parent | d9c825b5b5925be962d8d8d38a8534997f30a97b (diff) |
Extraction: Unset Extraction AutoInline is now the default
The auto-inlining has always been cumbersome. We only keep the
inlining of recursors (foo_rect for inductive foo), and a short
list of specific constants declared in mlutil.ml. In particular
we inline andb and orb to keep their lazy behavior.
The previous behavior is available via Set Extraction AutoInline
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13266 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | plugins/extraction/mlutil.ml | 41 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 2 |
2 files changed, 30 insertions, 13 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index ed4b17dda..1cd226616 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1177,18 +1177,35 @@ let is_not_strict t = Futhermore we don't expand fixpoints. *) let inline_test t = - let t1 = eta_red t in - let t2 = snd (collect_lams t1) in - not (is_fix t2) && ml_size t < 12 && is_not_strict t - -let manual_inline_list = - let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in - List.map (fun s -> (make_con mp empty_dirpath (mk_label s))) - [ "well_founded_induction_type"; "well_founded_induction"; - "Acc_rect"; "Acc_rec" ; "Acc_iter" ; "Fix" ] + if auto_inline () then + let t1 = eta_red t in + let t2 = snd (collect_lams t1) in + not (is_fix t2) && ml_size t < 12 && is_not_strict t + else false + +let con_of_string s = + let null = empty_dirpath in + match repr_dirpath (dirpath_of_string s) with + | id :: d -> make_con (MPfile (make_dirpath d)) null (label_of_id id) + | [] -> assert false + +let manual_inline_set = + List.fold_right (fun x -> Cset.add (con_of_string x)) + [ "Coq.Init.Wf.well_founded_induction_type"; + "Coq.Init.Wf.well_founded_induction"; + "Coq.Init.Wf.Acc_iter"; + "Coq.Init.Wf.Fix_F"; + "Coq.Init.Wf.Fix"; + "Coq.Init.Datatypes.andb"; + "Coq.Init.Datatypes.orb"; + "Coq.Init.Logic.eq_rec_r"; + "Coq.Init.Logic.eq_rect_r"; + "Coq.Init.Specif.proj1_sig"; + ] + Cset.empty let manual_inline = function - | ConstRef c -> List.mem c manual_inline_list + | ConstRef c -> Cset.mem c manual_inline_set | _ -> false (* If the user doesn't say he wants to keep [t], we inline in two cases: @@ -1202,6 +1219,6 @@ let inline r t = not (to_keep r) (* The user DOES want to keep it *) && not (is_inline_custom r) && (to_inline r (* The user DOES want to inline it *) - || (auto_inline () && lang () <> Haskell && not (is_projection r) - && (is_recursor r || manual_inline r || inline_test t))) + || (lang () <> Haskell && not (is_projection r) && + (is_recursor r || manual_inline r || inline_test t))) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index bd2aa6c91..83f33047e 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -349,7 +349,7 @@ let info_file f = (*s Extraction AutoInline *) -let auto_inline_ref = ref true +let auto_inline_ref = ref false let auto_inline () = !auto_inline_ref |