Fix exponential behavior in native compiler with retroknowledge.

3 files changed, 31 insertions, 7 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 2cbe9cd22..f38a2c314 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1767,6 +1767,7 @@ let compile_constant env sigma prefix ~interactive con body =
   | Def t ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
+      if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
       let is_lazy = is_lazy prefix t in
       let code = if is_lazy then mk_lazy code else code in
       let name =
@@ -1775,9 +1776,11 @@ let compile_constant env sigma prefix ~interactive con body =
       in
       let l = con_label con in
       let auxdefs,code = compile_with_fv env sigma [] (Some l) code in
+      if !Flags.debug then Pp.msg_debug (Pp.str "Generated mllambda code");
       let code =
         optimize_stk (Glet(Gconstant ("",con),code)::auxdefs)
       in
+      if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code");
       code, name
   | _ -> 
       let i = push_symbol (SymbConst con) in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index acf115466..8ea28ddff 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -647,9 +647,11 @@ and lambda_of_app env sigma f args =
       let cb = lookup_constant kn !global_env in
       (try
           let prefix = get_const_prefix !global_env kn in
+	  (* We delay the compilation of arguments to avoid an exponential behavior *)
+	  let f = Retroknowledge.get_native_compiling_info
+		    (!global_env).retroknowledge (mkConst kn) prefix in
 	  let args = lambda_of_args env sigma 0 args in
-	  Retroknowledge.get_native_compiling_info
-		    (!global_env).retroknowledge (mkConst kn) prefix args
+	  f args
       with Not_found ->
       begin match cb.const_body with
       | Def csubst ->
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 6418ac450..6749dbfdb 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -27,14 +27,33 @@ let rec translate_mod prefix mp env mod_expr acc =
 and translate_field prefix mp env acc (l,x) =
   match x with
   | SFBconst cb ->
-      let con = make_con mp empty_dirpath l in
-      compile_constant_field (pre_env env) prefix con acc cb
+     let con = make_con mp empty_dirpath l in
+     (if !Flags.debug then
+	let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
+	Pp.msg_debug (Pp.str msg));
+     compile_constant_field (pre_env env) prefix con acc cb
   | SFBmind mb ->
-      compile_mind_field prefix mp l acc mb
+     (if !Flags.debug then
+	let id = mb.mind_packets.(0).mind_typename in
+	let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
+	Pp.msg_debug (Pp.str msg));
+     compile_mind_field prefix mp l acc mb
   | SFBmodule md ->
-      translate_mod prefix md.mod_mp env md.mod_type acc
+     let mp = md.mod_mp in
+     (if !Flags.debug then
+	let msg =
+	  Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
+	in
+	Pp.msg_debug (Pp.str msg));
+     translate_mod prefix mp env md.mod_type acc
   | SFBmodtype mdtyp ->
-      translate_mod prefix mdtyp.typ_mp env mdtyp.typ_expr acc
+     let mp = mdtyp.typ_mp in
+     (if !Flags.debug then
+	let msg =
+	  Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
+	in
+	Pp.msg_debug (Pp.str msg));
+     translate_mod prefix mp env mdtyp.typ_expr acc
 
 let dump_library mp dp env mod_expr =
   if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");