Optimizing Int31 support in native compiler, by not tagging

applications of I31 constructor as lazy.

1 files changed, 19 insertions, 3 deletions

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index c9733c5fd..acf115466 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -499,8 +499,24 @@ module Renv =
 	r
   end
 
-let is_lazy t = (* APPROXIMATION *)
-  isApp t || isLetIn t
+(* What about pattern matching ?*)
+let is_lazy prefix t =
+  match kind_of_term t with
+  | App (f,args) ->
+     begin match kind_of_term f with
+     | Construct c ->
+	let entry = mkInd (fst c) in
+	(try
+	    let _ =
+	      Retroknowledge.get_native_before_match_info (!global_env).retroknowledge
+							  entry prefix c Llazy;
+	    in
+	    false
+	  with Not_found -> true)
+     | _ -> true
+     end
+  | LetIn _ -> true
+  | _ -> false
 
 let evar_value sigma ev = sigma.evars_val ev
 
@@ -642,7 +658,7 @@ and lambda_of_app env sigma f args =
           else
           let prefix = get_const_prefix !global_env kn in
           let t =
-            if is_lazy (Mod_subst.force_constr csubst) then
+            if is_lazy prefix (Mod_subst.force_constr csubst) then
               mkLapp Lforce [|Lconst (prefix, kn)|]
             else Lconst (prefix, kn)
           in