Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8

3 files changed, 68 insertions, 12 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 8f83d6baa..c11b9ebf4 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -479,6 +479,34 @@ let iter_with_binders g f n c = match kind c with
       Array.Fun1.iter f n tl;
       Array.Fun1.iter f (iterate g (Array.length tl) n) bl
 
+(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
+   subterms of [c] starting from [acc] and proceeding from left to
+   right according to the usual representation of the constructions as
+   [fold_constr] but it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive *)
+
+let fold_constr_with_binders g f n acc c =
+  match kind c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> acc
+  | Cast (c,_, t) -> f n (f n acc c) t
+  | Prod (na,t,c) -> f (g  n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g  n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g  n) (f n (f n acc b) t) c
+  | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+  | Proj (p,c) -> f n acc c
+  | Evar (_,l) -> Array.fold_left (f n) acc l
+  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+  | Fix (_,(lna,tl,bl)) ->
+      let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | CoFix (_,(lna,tl,bl)) ->
+      let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+
 (* [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
    not specified *)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index b35ea6653..742a13919 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -402,6 +402,15 @@ val iter : (constr -> unit) -> constr -> unit
 val iter_with_binders :
   ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
 
+(** [iter_with_binders g f n c] iters [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
+val fold_constr_with_binders :
+  ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
+
 type constr_compare_fn = int -> constr -> constr -> bool
 
 (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 036cd4847..5174eeea8 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2017,21 +2017,22 @@ let compile_mind_deps env prefix ~interactive
 
 (* This function compiles all necessary dependencies of t, and generates code in
    reverse order, as well as linking information updates *)
-let rec compile_deps env sigma prefix ~interactive init t =
+let compile_deps env sigma prefix ~interactive init t =
+  let rec aux env lvl init t =
   match kind t with
   | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
-      let c,u = get_alias env c in
-      let cb,(nameref,_) = lookup_constant_key c env in
-      let (_, (_, const_updates)) = init in
-      if is_code_loaded ~interactive nameref
-        || (Cmap_env.mem c const_updates)
-      then init
-      else
+    let c,u = get_alias env c in
+    let cb,(nameref,_) = lookup_constant_key c env in
+    let (_, (_, const_updates)) = init in
+    if is_code_loaded ~interactive nameref
+    || (Cmap_env.mem c const_updates)
+    then init
+    else
       let comp_stack, (mind_updates, const_updates) =
 	match cb.const_proj, cb.const_body with
         | false, Def t ->
-	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
+           aux env lvl init (Mod_subst.force_constr t)
         | true, _ ->
           let pb = lookup_projection (Projection.make c false) env in
           let mind = pb.proj_ind in
@@ -2047,12 +2048,30 @@ let rec compile_deps env sigma prefix ~interactive init t =
   | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
     let term = mkApp (mkConst (Projection.constant p), [|c|]) in
-      compile_deps env sigma prefix ~interactive init term
+    aux env lvl init term
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
-      Constr.fold (compile_deps env sigma prefix ~interactive) init t
-  | _ -> Constr.fold (compile_deps env sigma prefix ~interactive) init t
+      fold_constr_with_binders succ (aux env) lvl init t
+  | Var id ->
+    let open Context.Named.Declaration in
+    begin match lookup_named id env with
+      | LocalDef (_,t,_) ->
+        aux env lvl init t
+      | _ -> init
+    end
+  | Rel n when n > lvl ->
+    let open Context.Rel.Declaration in
+    let decl = lookup_rel n env in
+    let env = env_of_rel n env in
+    begin match decl with
+    | LocalDef (_,t,_) ->
+      aux env lvl init t
+    | LocalAssum _ -> init
+    end
+  | _ -> fold_constr_with_binders succ (aux env) lvl init t
+  in
+  aux env 0 init t
 
 let compile_constant_field env prefix con acc cb =
     let (gl, _) =