diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-05-30 18:20:52 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-04 22:45:22 +0200 |
commit | 7ada864b7728c9c94b7ca9856b6b2c89feb0214e (patch) | |
tree | 0bcb36c170ae6f3c960bdc9a7bab9e3fefcc42bb /kernel/nativecode.ml | |
parent | f6538f1a7f8ad2bdc0bc446d4ca35078d55d63ee (diff) |
Fix #7631: native_compute fails to compile an example in Coq 8.8
Dependency analysis for separate compilation was not iterated properly
on rel_context and named_context.
Diffstat (limited to 'kernel/nativecode.ml')
-rw-r--r-- | kernel/nativecode.ml | 43 |
1 files changed, 31 insertions, 12 deletions
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, _) = |