diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cbv.ml | 3 | ||||
| -rw-r--r-- | pretyping/classops.ml | 28 | ||||
| -rw-r--r-- | pretyping/classops.mli | 2 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 9 | ||||
| -rw-r--r-- | pretyping/dune | 6 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 2 | ||||
| -rw-r--r-- | pretyping/inferCumulativity.ml | 2 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 16 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
9 files changed, 53 insertions, 19 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/classops.ml b/pretyping/classops.ml index 542fb5456c..52e02c87fd 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -118,6 +118,9 @@ let class_tab = let coercion_tab = ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t) +let coercions_in_scope = + ref Refset_env.empty + module ClPairOrd = struct type t = cl_index * cl_index @@ -131,12 +134,13 @@ module ClPairMap = Map.Make(ClPairOrd) let inheritance_graph = ref (ClPairMap.empty : inheritance_path ClPairMap.t) -let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph) +let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope) -let unfreeze (fcl,fco,fig) = +let unfreeze (fcl,fco,fig,in_scope) = class_tab:=fcl; coercion_tab:=fco; - inheritance_graph:=fig + inheritance_graph:=fig; + coercions_in_scope:=in_scope (* ajout de nouveaux "objets" *) @@ -445,9 +449,16 @@ let load_coercion _ o = if !automatically_import_coercions then cache_coercion (Global.env ()) Evd.empty o +let set_coercion_in_scope (_, c) = + let r = c.coercion_type in + coercions_in_scope := Refset_env.add r !coercions_in_scope + let open_coercion i o = - if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion (Global.env ()) Evd.empty o + if Int.equal i 1 then begin + set_coercion_in_scope o; + if not !automatically_import_coercions then + cache_coercion (Global.env ()) Evd.empty o + end let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -492,7 +503,9 @@ let inCoercion : coercion -> obj = open_function = open_coercion; load_function = load_coercion; cache_function = (fun objn -> - let env = Global.env () in cache_coercion env Evd.empty objn + let env = Global.env () in + set_coercion_in_scope objn; + cache_coercion env Evd.empty objn ); subst_function = subst_coercion; classify_function = classify_coercion; @@ -553,3 +566,6 @@ let hide_coercion coe = let coe_info = coercion_info coe in Some coe_info.coe_param else None + +let is_coercion_in_scope r = + Refset_env.mem r !coercions_in_scope diff --git a/pretyping/classops.mli b/pretyping/classops.mli index af00c0a8dc..dc193c4e74 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -113,3 +113,5 @@ val coercions : unit -> coe_info_typ list (** [hide_coercion] returns the number of params to skip if the coercion must be hidden, [None] otherwise; it raises [Not_found] if not a coercion *) val hide_coercion : coe_typ -> int option + +val is_coercion_in_scope : GlobRef.t -> bool diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5e3821edf1..e15c00f7dc 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -363,12 +363,20 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd +let warn_coercion_not_in_scope = + CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated" + Pp.(fun r -> str "Coercion used but not in scope: " ++ + Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use " + ++ str "this coercion, please Import the module that contains it.") + (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = try let j,t,evd = List.fold_left (fun (ja,typ_cl,sigma) i -> + if not (is_coercion_in_scope i.coe_value) then + warn_coercion_not_in_scope i.coe_value; let isid = i.coe_is_identity in let isproj = i.coe_is_projection in let sigma, c = new_global sigma i.coe_value in @@ -386,7 +394,6 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = 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/inductiveops.ml b/pretyping/inductiveops.ml index b379cdf410..ec0ff73062 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -633,7 +633,7 @@ let is_predicate_explicitly_dep env sigma pred arsign = dependency status (of course, Anonymous implies non dependent, but not conversely). - From Coq > 8.2, using or not the the effective dependency of + From Coq > 8.2, using or not the effective dependency of the predicate is parametrable! *) begin match na with diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index eb283a0220..be79b8b07d 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk = | FEvar ((_,args),e) -> let variances = infer_stack infos variances stk in infer_vect infos variances (Array.map (mk_clos e) args) - | FRel _ -> variances + | FRel _ -> infer_stack infos variances stk | FFlex fl -> let variances = infer_table_key infos variances fl in infer_stack infos variances stk 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) |