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

1 files changed, 24 insertions, 8 deletions

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)))