diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cbv.ml | 3 | ||||
| -rw-r--r-- | pretyping/dune | 6 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 16 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
4 files changed, 19 insertions, 10 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index da6e26cc4b..fc24e9b3a9 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -455,7 +455,8 @@ let cbv_norm infos constr = (* constant bodies are normalized at the first expansion *) let create_cbv_infos flgs env sigma = let infos = create - (fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) + ~share:true (** Not used by cbv *) + ~repr:(fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) flgs env (Reductionops.safe_evar_value sigma) in diff --git a/pretyping/dune b/pretyping/dune new file mode 100644 index 0000000000..6609b4e328 --- /dev/null +++ b/pretyping/dune @@ -0,0 +1,6 @@ +(library + (name pretyping) + (synopsis "Coq's Type Inference Component (Pretyper)") + (public_name coq.pretyping) + (wrapped false) + (libraries camlp5.gramlib engine)) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 5df41ef76a..246acfc92e 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -354,9 +354,8 @@ and nf_atom_type env sigma atom = let env = push_rel (LocalAssum (n,dom)) env in let codom,s2 = nf_type_sort env sigma (codom vn) in mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2 - | Aevar(evk,ty,args) -> - let ty = nf_type env sigma ty in - nf_evar env sigma evk ty args + | Aevar(evk,args) -> + nf_evar env sigma evk args | Ameta(mv,ty) -> let ty = nf_type env sigma ty in mkMeta mv, ty @@ -398,22 +397,27 @@ and nf_predicate env sigma ind mip params v pT = mkLambda(name,dom,body) | _ -> nf_type env sigma v -and nf_evar env sigma evk ty args = +and nf_evar env sigma evk args = let evi = try Evd.find sigma evk with Not_found -> assert false in let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in + let ty = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in if List.is_empty hyps then begin assert (Int.equal (Array.length args) 0); mkEvar (evk, [||]), ty end else + (** Let-bound arguments are present in the evar arguments but not in the + type, so we turn the let into a product. *) + let hyps = Context.Named.drop_bodies hyps in let fold accu d = Term.mkNamedProd_or_LetIn d accu in let t = List.fold_left fold ty hyps in let ty, args = nf_args env sigma args t in - mkEvar (evk, Array.of_list args), ty + (** nf_args takes arguments in the reverse order but produces them in the + correct one, so we have to reverse them again for the evar node *) + mkEvar (evk, Array.rev_of_list args), ty let evars_of_evar_map sigma = { Nativelambda.evars_val = Evd.existential_opt_value0 sigma; - Nativelambda.evars_typ = Evd.existential_type0 sigma; Nativelambda.evars_metas = Evd.meta_type0 sigma } (* fork perf process, return profiler's process id *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3b9a8e6a1d..a315376aca 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -68,9 +68,7 @@ type t = { } let get_extra env sigma = - let open Context.Named.Declaration in - let ids = List.map get_id (named_context env) in - let avoid = List.fold_right Id.Set.add ids Id.Set.empty in + let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) (rel_context env) ~init:(empty_csubst, avoid, named_context env) |