diff options
author | 2018-06-05 13:30:21 +0200 | |
---|---|---|
committer | 2018-06-05 13:30:21 +0200 | |
commit | 00a01f65be79bef8592928941646750968dbe648 (patch) | |
tree | ad742b6f4ed5c706308755f2a9bbff2fd261eb18 /kernel/nativecode.ml | |
parent | c7f8af076b3f9bcfd4ff84ca9a14fc65ab9b953d (diff) | |
parent | 7ada864b7728c9c94b7ca9856b6b2c89feb0214e (diff) |
Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8
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, _) = |