From 82f8e76c38f7d5904ee78bfed3cfddb87efa9f92 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 8 Jul 2010 19:28:20 +0000 Subject: Extraction: restrict autoinling to csts whose body is globally visible (fix #2241) Here, the constants "without body" we don't want to autoinline are constants made opaque by the rigid signature of their module. As mentionned by X.L. inlining them might lead to untypable code. The current solution is safe, but not ideal: we could want to inline such constants at least inside their own module, and we could also want to inline constants that are not globally visible (functors...). NB: AutoInline is anyway not activated by default anymore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13273 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/mlutil.ml | 32 ++++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 6a5a83b1d..f876ad6b8 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1225,14 +1225,30 @@ let is_not_strict t = We expand small terms with at least one non-strict variable (i.e. a variable that may not be evaluated). - Futhermore we don't expand fixpoints. *) + Futhermore we don't expand fixpoints. + + Moreover, as mentionned by X. Leroy (bug #2241), + inling a constant from inside an opaque module might + break types. To avoid that, we require below that + both [r] and its body are globally visible. This isn't + fully satisfactory, since [r] might not be visible (functor), + and anyway it might be interesting to inline [r] at least + inside its own structure. But to be safe, we adopt this + restriction for the moment. +*) + +open Declarations -let inline_test t = - 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 inline_test r t = + if not (auto_inline ()) then false + else + let c = match r with ConstRef c -> c | _ -> assert false in + let body = try (Global.lookup_constant c).const_body with _ -> None in + if body = None then false + else + 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 con_of_string s = let null = empty_dirpath in @@ -1271,5 +1287,5 @@ let inline r t = && not (is_inline_custom r) && (to_inline r (* The user DOES want to inline it *) || (lang () <> Haskell && not (is_projection r) && - (is_recursor r || manual_inline r || inline_test t))) + (is_recursor r || manual_inline r || inline_test r t))) -- cgit v1.2.3