aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/cic.mli1
-rw-r--r--checker/subtyping.ml2
-rw-r--r--checker/values.ml4
-rw-r--r--kernel/declarations.ml1
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/indtypes.ml53
-rw-r--r--kernel/indtypes.mli2
-rw-r--r--plugins/extraction/extraction.ml12
-rw-r--r--pretyping/detyping.ml5
-rw-r--r--pretyping/inductiveops.ml3
-rw-r--r--pretyping/inductiveops.mli8
11 files changed, 40 insertions, 53 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index 94958447e..3304b032e 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -211,7 +211,6 @@ type projection_body = {
proj_npars : int;
proj_arg : int;
proj_type : constr; (* Type under params *)
- proj_body : constr; (* For compatibility, the match version *)
}
type constant_def =
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 6f9bf8fce..f4ae02084 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -130,7 +130,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
check (==) (fun x -> x.proj_npars);
check (==) (fun x -> x.proj_arg);
check (eq_constr) (fun x -> x.proj_type);
- check (eq_constr) (fun x -> x.proj_body); true
+ true
in
let check_inductive_type t1 t2 =
diff --git a/checker/values.ml b/checker/values.ml
index 12fbf1ff0..45f04f88d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 125f04aeb55b2fa027db6bfb9dffc6a2 checker/cic.mli
+MD5 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli
*)
@@ -225,7 +225,7 @@ let v_cst_def =
let v_projbody =
v_tuple "projection_body"
- [|v_cst;Int;Int;v_constr;v_constr|]
+ [|v_cst;Int;Int;v_constr|]
let v_typing_flags =
v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index abebec156..7bd7d6c9c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -54,7 +54,6 @@ type projection_body = {
proj_npars : int;
proj_arg : int; (** Projection index, starting from 0 *)
proj_type : types; (* Type under params *)
- proj_body : constr; (* For compatibility with VMs only, the match version *)
}
(* Global declarations (i.e. constants) can be either: *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index fc6dc8b9e..1b73096f7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -86,7 +86,7 @@ let subst_const_def sub def = match def with
let subst_const_proj sub pb =
{ pb with proj_ind = subst_mind sub pb.proj_ind;
proj_type = subst_mps sub pb.proj_type;
- proj_body = subst_const_type sub pb.proj_body }
+ }
let subst_const_body sub cb =
assert (List.is_empty cb.const_hyps); (* we're outside sections *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4bc7ea198..14f2a3d8f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -797,16 +797,13 @@ exception UndefinableExpansion
build an expansion function.
The term built is expecting to be substituted first by
a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
+let compute_projections ((kn, _ as ind), u) nparamargs params
mind_consnrealdecls mind_consnrealargs paramslet ctx =
let mp, dp, l = MutInd.repr3 kn in
(** We build a substitution smashing the lets in the record parameters so
that typechecking projections requires just a substitution and not
matching with a parameter context. *)
- let indty, paramsletsubst =
- (* [ty] = [Ind inst] is typed in context [params] *)
- let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
- let ty = mkApp (mkIndU indu, inst) in
+ let paramsletsubst =
(* [Ind inst] is typed in context [params-wo-let] *)
let inst' = rel_list 0 nparamargs in
(* {params-wo-let |- subst:params] *)
@@ -814,48 +811,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
(* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *)
let subst = (* For the record parameter: *)
mkRel 1 :: List.map (lift 1) subst in
- ty, subst
+ subst
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 = mind_consnrealdecls;
- ci_cstr_nargs = mind_consnrealargs;
- ci_pp_info = print_info }
- in
- let len = List.length ctx in
- let x = Name x 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 (i, j, kns, pbs, subst, letsubst) =
+ let projections decl (i, j, kns, pbs, letsubst) =
match decl with
| LocalDef (na,c,t) ->
(* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
let c = liftn 1 j c in
(* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
- to [params, x:I |- c(params,proj1 x,..,projj x)] *)
- let c1 = substl subst c in
- (* From [params, x:I |- subst:field1,..,fieldj]
- to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
- is represented with instance of field1 last *)
- let subst = c1 :: subst in
- (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *)
let c2 = substl letsubst c in
(* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)]
to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
let letsubst = c2 :: letsubst in
- (i, j+1, kns, pbs, subst, letsubst)
+ (i, j+1, kns, pbs, letsubst)
| LocalAssum (na,t) ->
match na with
| Name id ->
@@ -868,17 +838,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
let projty = substl letsubst t in
(* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
to [params, x:I |- t(proj1 x,..,projj x)] *)
- let ty = substl subst t in
let fterm = mkProj (Projection.make kn false, mkRel 1) in
- let compat = compat_body ty (j - 1) in
let body = { proj_ind = fst ind; proj_npars = nparamargs;
- proj_arg = i; proj_type = projty; proj_body = compat } in
- (i + 1, j + 1, kn :: kns, body :: pbs,
- fterm :: subst, fterm :: letsubst)
+ proj_arg = i; proj_type = projty; } in
+ (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
| Anonymous -> raise UndefinableExpansion
in
- let (_, _, kns, pbs, subst, letsubst) =
- List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+ let (_, _, kns, pbs, letsubst) =
+ List.fold_right projections ctx (0, 1, [], [], paramsletsubst)
in
Array.of_list (List.rev kns),
Array.of_list (List.rev pbs)
@@ -983,7 +950,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
(try
let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
let kns, projs =
- compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt
+ compute_projections indsp nparamargs paramsctxt
pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
in Some (Some (rid, kns, projs))
with UndefinableExpansion -> Some None)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 5a38172c2..45228e35e 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,7 +43,7 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct
val enforce_indices_matter : unit -> unit
val is_indices_matter : unit -> bool
-val compute_projections : pinductive -> Id.t -> Id.t ->
+val compute_projections : pinductive ->
int -> Context.Rel.t -> int array -> int array ->
Context.Rel.t -> Context.Rel.t ->
(Constant.t array * projection_body array)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b1ee21536..3a61c7747 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1069,7 +1069,11 @@ let extract_constant env kn cb =
| false -> mk_typ (get_body c)
| true ->
let pb = lookup_projection (Projection.make kn false) env in
- mk_typ (EConstr.of_constr pb.proj_body))
+ (** FIXME: handle mutual records *)
+ let ind = (pb.Declarations.proj_ind, 0) in
+ let bodies = Inductiveops.legacy_match_projection env ind in
+ let body = bodies.(pb.Declarations.proj_arg) in
+ mk_typ (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
if access_opaque () then mk_typ (get_opaque env c)
@@ -1082,7 +1086,11 @@ let extract_constant env kn cb =
| false -> mk_def (get_body c)
| true ->
let pb = lookup_projection (Projection.make kn false) env in
- mk_def (EConstr.of_constr pb.proj_body))
+ (** FIXME: handle mutual records *)
+ let ind = (pb.Declarations.proj_ind, 0) in
+ let bodies = Inductiveops.legacy_match_projection env ind in
+ let body = bodies.(pb.Declarations.proj_arg) in
+ mk_def (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
if access_opaque () then mk_def (get_opaque env c)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index df89d9eac..5a54c6f05 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -690,7 +690,10 @@ and detype_r d flags avoid env sigma t =
let c' =
try
let pb = Environ.lookup_projection p (snd env) in
- let body = pb.Declarations.proj_body in
+ (** FIXME: handle mutual records *)
+ let ind = (pb.Declarations.proj_ind, 0) in
+ let bodies = Inductiveops.legacy_match_projection (snd env) ind in
+ let body = bodies.(pb.Declarations.proj_arg) 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
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 4ad32fc66..1a790be64 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -549,6 +549,9 @@ let compute_projections env (kn, _ 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
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 506cdd8c9..aa53f7e67 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -198,6 +198,14 @@ 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 :
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 23:10:31 +0000