aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/detyping.ml42
-rw-r--r--pretyping/evarconv.ml16
-rw-r--r--pretyping/glob_ops.ml10
-rw-r--r--pretyping/glob_ops.mli1
-rw-r--r--pretyping/inductiveops.ml36
-rw-r--r--pretyping/inductiveops.mli8
-rw-r--r--pretyping/inferCumulativity.ml44
-rw-r--r--pretyping/inferCumulativity.mli2
8 files changed, 50 insertions, 109 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6746e4b902..99cd89cc2a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -8,8 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-module CVars = Vars
-
open Pp
open CErrors
open Util
@@ -175,16 +173,6 @@ let () = declare_bool_option
optread = print_primproj_params;
optwrite = (:=) print_primproj_params_value }
-let print_primproj_compatibility_value = ref false
-let print_primproj_compatibility () = !print_primproj_compatibility_value
-
-let () = declare_bool_option
- { optdepr = false;
- optname = "backwards-compatible printing of primitive projections";
- optkey = ["Printing";"Primitive";"Projection";"Compatibility"];
- optread = print_primproj_compatibility;
- optwrite = (:=) print_primproj_compatibility_value }
-
(* Auxiliary function for MutCase printing *)
(* [computable] tries to tell if the predicate typing the result is inferable*)
@@ -702,30 +690,12 @@ and detype_r d flags avoid env sigma t =
GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
[detype d flags avoid env sigma c])
else
- if print_primproj_compatibility () && Projection.unfolded p then
- (* Print the compatibility match version *)
- let c' =
- try
- let ind = Projection.inductive p in
- let bodies = Inductiveops.legacy_match_projection (snd env) ind in
- let body = bodies.(Projection.arg p) in
- let ty = Retyping.get_type_of (snd env) sigma c in
- let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
- let body' = strip_lam_assum body in
- let u = EInstance.kind sigma u in
- let body' = CVars.subst_instance_constr u body' in
- let body' = EConstr.of_constr body' in
- substl (c :: List.rev args) body'
- with Retyping.RetypeError _ | Not_found ->
- anomaly (str"Cannot detype an unfolded primitive projection.")
- in DAst.get (detype d flags avoid env sigma c')
- else
- if print_primproj_params () then
- try
- let c = Retyping.expand_projection (snd env) sigma p c [] in
- DAst.get (detype d flags avoid env sigma c)
- with Retyping.RetypeError _ -> noparams ()
- else noparams ()
+ if print_primproj_params () then
+ try
+ let c = Retyping.expand_projection (snd env) sigma p c [] in
+ DAst.get (detype d flags avoid env sigma c)
+ with Retyping.RetypeError _ -> noparams ()
+ else noparams ()
| Evar (evk,cl) ->
let bound_to_itself_or_letin decl c =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index aa30ed8d2e..bb163ddaee 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -468,17 +468,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
let mind = Environ.lookup_mind mi env in
let open Declarations in
- begin match mind.mind_universes with
- | Monomorphic_ind _ -> assert false
- | Polymorphic_ind _ -> check_strict evd u u'
- | Cumulative_ind cumi ->
+ begin match mind.mind_variance with
+ | None -> check_strict evd u u'
+ | Some variances ->
let nparamsaplied = Stack.args_size sk in
let nparamsaplied' = Stack.args_size sk' in
let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
then check_strict evd u u'
else
- compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u'
+ compare_cumulative_instances evd variances u u'
end
| Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
| Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
@@ -488,10 +487,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
let mind = Environ.lookup_mind mi env in
let open Declarations in
- begin match mind.mind_universes with
- | Monomorphic_ind _ -> assert false
- | Polymorphic_ind _ -> check_strict evd u u'
- | Cumulative_ind cumi ->
+ begin match mind.mind_variance with
+ | None -> check_strict evd u u'
+ | Some variances ->
let nparamsaplied = Stack.args_size sk in
let nparamsaplied' = Stack.args_size sk' in
let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6b61b1452e..68626597fc 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -485,7 +485,11 @@ let is_gvar id c = match DAst.get c with
| GVar id' -> Id.equal id id'
| _ -> false
-let rec cases_pattern_of_glob_constr na = DAst.map (function
+let rec cases_pattern_of_glob_constr na c =
+ (* Forcing evaluation to ensure that the possible raising of
+ Not_found is not delayed *)
+ let c = DAst.force c in
+ DAst.map (function
| GVar id ->
begin match na with
| Name _ ->
@@ -498,6 +502,8 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
| GApp (c, l) ->
begin match DAst.get c with
| GRef (ConstructRef cstr,_) ->
+ let nparams = Inductiveops.inductive_nparams (fst cstr) in
+ let _,l = List.chop nparams l in
PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
| _ -> raise Not_found
end
@@ -505,7 +511,7 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
(* A canonical encoding of aliases *)
DAst.get (cases_pattern_of_glob_constr na' b)
| _ -> raise Not_found
- )
+ ) c
open Declarations
open Term
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 91a2ef9c1e..c189a3bcb2 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -89,6 +89,7 @@ val map_pattern : (glob_constr -> glob_constr) ->
(** Conversion from glob_constr to cases pattern, if possible
+ Evaluation is forced.
Take the current alias as parameter,
@raise Not_found if translation is impossible *)
val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ff552c7caf..4c02dc0f09 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -453,12 +453,7 @@ let build_branch_type env sigma dep p cs =
let compute_projections env (kn, i as ind) =
let open Term in
let mib = Environ.lookup_mind kn env in
- let u = match mib.mind_universes with
- | Monomorphic_ind _ -> Instance.empty
- | Polymorphic_ind auctx -> make_abstract_instance auctx
- | Cumulative_ind acumi ->
- make_abstract_instance (ACumulativityInfo.univ_context acumi)
- in
+ let u = make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
let x = match mib.mind_record with
| NotRecord | FakeRecord ->
anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
@@ -480,25 +475,6 @@ let compute_projections env (kn, i as ind) =
(* [Ind inst] is typed in context [params-wo-let] *)
ty
in
- let ci =
- let print_info =
- { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
- { ci_ind = ind;
- ci_npar = nparamargs;
- ci_cstr_ndecls = pkt.mind_consnrealdecls;
- ci_cstr_nargs = pkt.mind_consnrealargs;
- ci_pp_info = print_info }
- in
- let len = List.length ctx in
- let compat_body ccl i =
- (* [ccl] is defined in context [params;x:indty] *)
- (* [ccl'] is defined in context [params;x:indty;x:indty] *)
- let ccl' = liftn 1 2 ccl in
- let p = mkLambda (x, lift 1 indty, ccl') in
- let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
- let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
- it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
- in
let projections decl (proj_arg, j, pbs, subst) =
match decl with
| LocalDef (na,c,t) ->
@@ -528,10 +504,9 @@ let compute_projections env (kn, i as ind) =
let ty = substl subst t in
let term = mkProj (Projection.make kn true, mkRel 1) in
let fterm = mkProj (Projection.make kn false, mkRel 1) in
- let compat = compat_body ty (j - 1) in
let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
- let body = (etab, etat, compat) in
+ let body = (etab, etat) in
(proj_arg + 1, j + 1, body :: pbs, fterm :: subst)
| Anonymous ->
anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
@@ -541,13 +516,6 @@ let compute_projections env (kn, i as ind) =
in
Array.rev_of_list pbs
-let legacy_match_projection env ind =
- Array.map pi3 (compute_projections env ind)
-
-let compute_projections ind mib =
- let ans = compute_projections ind mib in
- Array.map (fun (prj, ty, _) -> (prj, ty)) ans
-
(**************************************************)
let extract_mrectype sigma t =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b2e205115f..5a4257e175 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,14 +194,6 @@ val compute_projections : Environ.env -> inductive -> (constr * types) array
(** Given a primitive record type, for every field computes the eta-expanded
projection and its type. *)
-val legacy_match_projection : Environ.env -> inductive -> constr array
-(** Given a record type, computes the legacy match-based projection of the
- projections.
-
- BEWARE: such terms are ill-typed, and should thus only be used in upper
- layers. The kernel will probably badly fail if presented with one of
- those. *)
-
(********************)
val type_of_inductive_knowing_conclusion :
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index b5a6ba6be5..bf8a38a353 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -41,33 +41,31 @@ let variance_pb cv_pb var =
| CONV, Covariant -> Invariant
| CUMUL, Covariant -> Covariant
-let infer_cumulative_ind_instance cv_pb cumi variances u =
+let infer_cumulative_ind_instance cv_pb mind_variance variances u =
Array.fold_left2 (fun variances varu u ->
match LMap.find u variances with
| exception Not_found -> variances
| varu' ->
LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances)
- variances (ACumulativityInfo.variance cumi) (Instance.to_array u)
+ variances mind_variance (Instance.to_array u)
let infer_inductive_instance cv_pb env variances ind nargs u =
let mind = Environ.lookup_mind (fst ind) env in
- match mind.mind_universes with
- | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
- | Polymorphic_ind _ -> infer_generic_instance_eq variances u
- | Cumulative_ind cumi ->
+ match mind.mind_variance with
+ | None -> infer_generic_instance_eq variances u
+ | Some mind_variance ->
if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs)
then infer_generic_instance_eq variances u
- else infer_cumulative_ind_instance cv_pb cumi variances u
+ else infer_cumulative_ind_instance cv_pb mind_variance variances u
let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u =
let mind = Environ.lookup_mind mi env in
- match mind.mind_universes with
- | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
- | Polymorphic_ind _ -> infer_generic_instance_eq variances u
- | Cumulative_ind cumi ->
+ match mind.mind_variance with
+ | None -> infer_generic_instance_eq variances u
+ | Some _ ->
if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs)
then infer_generic_instance_eq variances u
- else infer_cumulative_ind_instance CONV cumi variances u
+ else variances (* constructors are convertible at common supertype *)
let infer_sort cv_pb variances s =
match cv_pb with
@@ -189,12 +187,14 @@ let infer_inductive env mie =
let { mind_entry_params = params;
mind_entry_inds = entries; } = mie
in
- let univs =
- match mie.mind_entry_universes with
- | Monomorphic_ind_entry _
- | Polymorphic_ind_entry _ as univs -> univs
- | Cumulative_ind_entry (nas, cumi) ->
- let uctx = CumulativityInfo.univ_context cumi in
+ let variances =
+ match mie.mind_entry_variance with
+ | None -> None
+ | Some _ ->
+ let uctx = match mie.mind_entry_universes with
+ | Monomorphic_entry _ -> assert false
+ | Polymorphic_entry (_,uctx) -> uctx
+ in
let uarray = Instance.to_array @@ UContext.instance uctx in
let env = Environ.push_context uctx env in
let variances =
@@ -212,6 +212,10 @@ let infer_inductive env mie =
entries
in
let variances = Array.map (fun u -> LMap.find u variances) uarray in
- Cumulative_ind_entry (nas, CumulativityInfo.make (uctx, variances))
+ Some variances
in
- { mie with mind_entry_universes = univs }
+ { mie with mind_entry_variance = variances }
+
+let dummy_variance = let open Entries in function
+ | Monomorphic_entry _ -> assert false
+ | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Variance.Irrelevant
diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli
index a0c8d339ac..6e5bf30f6b 100644
--- a/pretyping/inferCumulativity.mli
+++ b/pretyping/inferCumulativity.mli
@@ -10,3 +10,5 @@
val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
Entries.mutual_inductive_entry
+
+val dummy_variance : Entries.universes_entry -> Univ.Variance.t array
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 06:43:31 +0000