aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.ml3
-rw-r--r--pretyping/classops.ml49
-rw-r--r--pretyping/classops.mli4
-rw-r--r--pretyping/coercion.ml9
-rw-r--r--pretyping/dune6
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/inferCumulativity.ml2
-rw-r--r--pretyping/nativenorm.ml16
-rw-r--r--pretyping/pretyping.ml4
9 files changed, 63 insertions, 32 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..332ecd2c91 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -16,7 +16,6 @@ open Constr
open Libnames
open Globnames
open Nametab
-open Environ
open Libobject
open Mod_subst
@@ -118,6 +117,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 +133,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" *)
@@ -316,16 +319,16 @@ let lookup_pattern_path_between env (s,t) =
(* rajouter une coercion dans le graphe *)
-let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
- ref (fun _ _ _ -> str "<a class path>")
+let path_printer : ((Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
+ ref (fun _ -> str "<a class path>")
let install_path_printer f = path_printer := f
-let print_path env sigma x = !path_printer env sigma x
+let print_path x = !path_printer x
-let message_ambig env sigma l =
+let message_ambig l =
str"Ambiguous paths:" ++ spc () ++
- prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l
+ prlist_with_sep fnl print_path l
(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
coercion,source,target *)
@@ -339,7 +342,7 @@ let different_class_params i =
| CL_CONST c -> Global.is_polymorphic (ConstRef c)
| _ -> false
-let add_coercion_in_graph env sigma (ic,source,target) =
+let add_coercion_in_graph (ic,source,target) =
let old_inheritance_graph = !inheritance_graph in
let ambig_paths =
(ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
@@ -381,7 +384,7 @@ let add_coercion_in_graph env sigma (ic,source,target) =
end;
let is_ambig = match !ambig_paths with [] -> false | _ -> true in
if is_ambig && not !Flags.quiet then
- Feedback.msg_info (message_ambig env sigma !ambig_paths)
+ Feedback.msg_info (message_ambig !ambig_paths)
type coercion = {
coercion_type : coe_typ;
@@ -426,7 +429,7 @@ let _ =
optread = (fun () -> !automatically_import_coercions);
optwrite = (:=) automatically_import_coercions }
-let cache_coercion env sigma (_, c) =
+let cache_coercion (_, c) =
let () = add_class c.coercion_source in
let () = add_class c.coercion_target in
let is, _ = class_info c.coercion_source in
@@ -439,15 +442,22 @@ let cache_coercion env sigma (_, c) =
coe_param = c.coercion_params;
} in
let () = add_new_coercion c.coercion_type xf in
- add_coercion_in_graph env sigma (xf,is,it)
+ add_coercion_in_graph (xf,is,it)
let load_coercion _ o =
if !automatically_import_coercions then
- cache_coercion (Global.env ()) Evd.empty o
+ cache_coercion 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 o
+ end
let subst_coercion (subst, c) =
let coe = subst_coe_typ subst c.coercion_type in
@@ -492,8 +502,8 @@ 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
- );
+ set_coercion_in_scope objn;
+ cache_coercion objn);
subst_function = subst_coercion;
classify_function = classify_coercion;
discharge_function = discharge_coercion }
@@ -553,3 +563,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..7c4842c8ae 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -99,7 +99,7 @@ val lookup_pattern_path_between :
(**/**)
(* Crade *)
val install_path_printer :
- (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+ ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
(**/**)
(** {6 This is for printing purpose } *)
@@ -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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 07:32:57 +0000