Mark arrays, products, and plain constants, as potentially needing a …

…delayed evaluation during native_compute (fix coq#18703).

The following statements would otherwise cause a stack overflow if the
module were to be compiled and then loaded, even if the constant was
completely unrelated to the term being normalized.

  Definition large := [|fact 100|0|].
  Definition large := (0 <= fact 100) -> Prop.
  Definition large := large'.

Note that the following statements are still eagerly evaluated, on purpose.

  Definition small := [|0|0|].
  Definition small := Prop -> Prop.

Note also that the translation of the following code is a bit suboptimal:

  Definition large := large'.
  (* let large = lazy (Lazy.force large') *)

kernel/nativecode.ml

@@ -52,22 +52,29 @@ let fresh_lname n =
   incr lname_ctr;
   { lname = n; luid = !lname_ctr }
 
-let rec is_lazy t = match Constr.kind t with
-| App _ | LetIn _ | Case _ | Proj _ -> true
-| Cast (c,_, _) -> is_lazy c
-| Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _ | Int _
-| Float _ | Prod _ | Lambda _ | Evar _ | Fix _ | CoFix _ | Array _ ->
-  false
-
-let is_lazy_constant cb =
+let rec is_lazy env t =
+  match Constr.kind t with
+  | App _ | LetIn _ | Case _ | Proj _ -> true
+  | Array (_, t, d, _) -> Array.exists (fun t -> is_lazy env t) t || is_lazy env d
+  | Cast (c, _, _) | Prod (_, c, _) -> is_lazy env c
+  | Const (c, _) -> get_const_lazy env c
+  | Rel _ | Meta _ | Var _ | Sort _ | Ind _ | Construct _ | Int _
+  | Float _ | Lambda _ | Evar _ | Fix _ | CoFix _ ->
+    false
+
+and is_lazy_constant env cb =
   (* Bound universes are turned into lambda-abstractions *)
   UVars.AbstractContext.is_constant (Declareops.constant_polymorphic_context cb) &&
   (* So are context variables *)
   List.is_empty cb.const_hyps &&
   match cb.const_body with
-  | Def body -> is_lazy body
+  | Def body -> is_lazy env body
   | Undef _ | OpaqueDef _ | Primitive _ | Symbol _ -> false
 
+and get_const_lazy env c =
+  let cb = Environ.lookup_constant c env in
+  is_lazy_constant env cb
+
 type prefix = string
 
 (* Linked code location utilities *)
@@ -83,10 +90,6 @@ let get_const_prefix env c =
    | NotLinked -> ""
    | Linked s -> s
 
-let get_const_lazy env c =
-  let cb = Environ.lookup_constant c env in
-  is_lazy_constant cb
-
 (** Global names **)
 type gname =
   | Gind of string * inductive (* prefix, inductive name *)
@@ -2091,7 +2094,7 @@ let compile_constant env sigma con cb =
     | Def t ->
       let code = lambda_of_constr env sigma t in
       debug_native_compiler (fun () -> Pp.str "Generated lambda code");
-      let is_lazy = is_lazy_constant cb in
+      let is_lazy = is_lazy_constant env cb in
       let wrap t = if is_lazy then MLprimitive (Lazy, [|t|]) else t in
       let l = Constant.label con in
       let auxdefs,code =

kernel/nativecode.mli

@@ -62,7 +62,7 @@ val register_native_file : string -> unit
 val is_loaded_native_file : string -> bool
 
 val compile_constant_field : env -> Constant.t ->
-  global list -> ('a, 'b) pconstant_body -> global list
+  global list -> constant_body -> global list
 
 val compile_mind_field : ModPath.t -> Label.t ->
   global list -> mutual_inductive_body -> global list