aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml2
-rw-r--r--kernel/cooking.mli1
-rw-r--r--kernel/declarations.ml3
-rw-r--r--kernel/declareops.ml3
-rw-r--r--kernel/entries.ml5
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/indtypes.ml57
-rw-r--r--kernel/indtypes.mli2
-rw-r--r--kernel/names.ml11
-rw-r--r--kernel/term_typing.ml31
10 files changed, 17 insertions, 100 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 5783453e6..68057b389 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -156,7 +156,6 @@ type inline = bool
type result = {
cook_body : constant_def;
cook_type : types;
- cook_proj : bool;
cook_universes : constant_universes;
cook_inline : inline;
cook_context : Context.Named.t option;
@@ -230,7 +229,6 @@ let cook_constant ~hcons env { from = cb; info } =
{
cook_body = body;
cook_type = typ;
- cook_proj = cb.const_proj;
cook_universes = univs;
cook_inline = cb.const_inline_code;
cook_context = Some const_hyps;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 0d907f3de..76c79335f 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,7 +21,6 @@ type inline = bool
type result = {
cook_body : constant_def;
cook_type : types;
- cook_proj : bool;
cook_universes : constant_universes;
cook_inline : inline;
cook_context : Context.Named.t option;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7bd70c050..7bd7d6c9c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -54,8 +54,6 @@ type projection_body = {
proj_npars : int;
proj_arg : int; (** Projection index, starting from 0 *)
proj_type : types; (* Type under params *)
- proj_eta : constr * types; (* Eta-expanded term and type *)
- proj_body : constr; (* For compatibility with VMs only, the match version *)
}
(* Global declarations (i.e. constants) can be either: *)
@@ -87,7 +85,6 @@ type constant_body = {
const_type : types;
const_body_code : Cemitcodes.to_patch_substituted option;
const_universes : constant_universes;
- const_proj : bool;
const_inline_code : bool;
const_typing_flags : typing_flags; (** The typing options which
were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 75c0e5b4c..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 *)
@@ -100,7 +100,6 @@ let subst_const_body sub cb =
{ const_hyps = [];
const_body = body';
const_type = type';
- const_proj = cb.const_proj;
const_body_code =
Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
const_universes = cb.const_universes;
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 94da00c7e..3c555f8c7 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -95,14 +95,9 @@ type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
Context.Named.t option * types in_constant_universes_entry * inline
-type projection_entry = {
- proj_entry_ind : MutInd.t;
- proj_entry_arg : int }
-
type 'a constant_entry =
| DefinitionEntry of 'a definition_entry
| ParameterEntry of parameter_entry
- | ProjectionEntry of projection_entry
(** {6 Modules } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index fb89576dd..2d6c9117b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -490,7 +490,7 @@ let lookup_projection cst env =
Cmap_env.find (Projection.constant cst) env.env_globals.env_projections
let is_projection cst env =
- (lookup_constant cst env).const_proj
+ Cmap_env.mem cst env.env_globals.env_projections
(* Mutual Inductives *)
let polymorphic_ind (mind,i) env =
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 439acd15b..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,21 +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 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 = { proj_ind = fst ind; proj_npars = nparamargs;
- proj_arg = i; proj_type = projty; proj_eta = etab, etat;
- 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)
@@ -987,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/kernel/names.ml b/kernel/names.ml
index 597061278..1d2a7c4ce 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -17,7 +17,7 @@
the module system, Aug 2002 *)
(* Abstraction over the type of constant for module inlining by Claudio
Sacerdoti, Nov 2004 *)
-(* Miscellaneous features or improvements by Hugo Herbelin,
+(* Miscellaneous features or improvements by Hugo Herbelin,
Élie Soubiran, ... *)
open Pp
@@ -364,7 +364,6 @@ module MPmap = CMap.Make(ModPath)
module KerName = struct
type t = {
- canary : Canary.t;
modpath : ModPath.t;
dirpath : DirPath.t;
knlabel : Label.t;
@@ -372,16 +371,14 @@ module KerName = struct
(** Lazily computed hash. If unset, it is set to negative values. *)
}
- let canary = Canary.obj
-
type kernel_name = t
let make modpath dirpath knlabel =
- { modpath; dirpath; knlabel; refhash = -1; canary; }
+ { modpath; dirpath; knlabel; refhash = -1; }
let repr kn = (kn.modpath, kn.dirpath, kn.knlabel)
let make2 modpath knlabel =
- { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; canary; }
+ { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; }
let modpath kn = kn.modpath
let label kn = kn.knlabel
@@ -437,7 +434,7 @@ module KerName = struct
* (string -> string)
let hashcons (hmod,hdir,hstr) kn =
let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
- { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; }
+ { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; }
let eq kn1 kn2 =
kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
kn1.knlabel == kn2.knlabel
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index db1109e75..37bf679c5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -250,7 +250,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = Undef nl;
cook_type = t;
- cook_proj = false;
cook_universes = univs;
cook_inline = false;
cook_context = ctx;
@@ -291,7 +290,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = def;
cook_type = typ;
- cook_proj = false;
cook_universes = Monomorphic_const univs;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
@@ -343,39 +341,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = def;
cook_type = typ;
- cook_proj = false;
cook_universes = univs;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
}
- | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
- let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
- let kn, pb =
- match mib.mind_record with
- | Some (Some (id, kns, pbs)) ->
- if i < Array.length pbs then
- kns.(i), pbs.(i)
- else assert false
- | _ -> assert false
- in
- let univs =
- match mib.mind_universes with
- | Monomorphic_ind ctx -> Monomorphic_const ctx
- | Polymorphic_ind auctx -> Polymorphic_const auctx
- | Cumulative_ind acumi ->
- Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi)
- in
- let term, typ = pb.proj_eta in
- {
- Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term));
- cook_type = typ;
- cook_proj = true;
- cook_universes = univs;
- cook_inline = false;
- cook_context = None;
- }
-
let record_aux env s_ty s_bo =
let in_ty = keep_hyps env s_ty in
let v =
@@ -464,7 +434,6 @@ let build_constant_declaration kn env result =
{ const_hyps = hyps;
const_body = def;
const_type = typ;
- const_proj = result.cook_proj;
const_body_code = tps;
const_universes = univs;
const_inline_code = result.cook_inline;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 20:32:53 +0000