From 74d700e9f7fcb14e7136e87b5efab25d5adb194b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 1 Jun 2018 16:23:29 +0200 Subject: Getting rid of the const_proj field in the kernel. This field used to signal that a constant was the compatibility eta-expansion of a primitive projections, but since a previous cleanup in the kernel it had become useless. --- kernel/cooking.ml | 2 -- kernel/cooking.mli | 1 - kernel/declarations.ml | 1 - kernel/declareops.ml | 1 - kernel/environ.ml | 2 +- kernel/term_typing.ml | 5 ----- 6 files changed, 1 insertion(+), 11 deletions(-) (limited to 'kernel') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 5783453e66..68057b389f 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 0d907f3dea..76c79335f1 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 7bd70c0502..02871153b0 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -87,7 +87,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 75c0e5b4cc..fc6dc8b9ef 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -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/environ.ml b/kernel/environ.ml index fb89576dd0..2d6c9117b3 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/term_typing.ml b/kernel/term_typing.ml index db1109e75e..d29f2ca826 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,7 +341,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 = univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -370,7 +367,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { 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; @@ -464,7 +460,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; -- cgit v1.2.3 From 4513b7735779fb440223e6f22079994528249047 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 2 Jun 2018 15:11:09 +0200 Subject: Remove special declaration of primitive projections in the kernel. This reduces kernel bloat and removes code from the TCB, as compatibility projections are now retypechecked as normal definitions would have been. This should have no effect on efficiency as this only happens once at definition time. --- kernel/entries.ml | 5 ----- kernel/term_typing.ml | 26 -------------------------- 2 files changed, 31 deletions(-) (limited to 'kernel') diff --git a/kernel/entries.ml b/kernel/entries.ml index 94da00c7eb..3c555f8c7b 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/term_typing.ml b/kernel/term_typing.ml index d29f2ca826..37bf679c51 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -346,32 +346,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = 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_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 = -- cgit v1.2.3 From a4839aa1ff076a8938ca182615a93d6afe748860 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 4 Jun 2018 13:32:35 +0200 Subject: Remove the proj_eta field of the kernel. This field was not used inside the kernel and not used in performance-critical code where caching is essential, so we extrude the code that computes it out of the kernel. --- kernel/declarations.ml | 1 - kernel/indtypes.ml | 6 +----- 2 files changed, 1 insertion(+), 6 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 02871153b0..abebec156c 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_eta : constr * types; (* Eta-expanded term and type *) proj_body : constr; (* For compatibility with VMs only, the match version *) } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 439acd15bf..4bc7ea1988 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -869,14 +869,10 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params (* 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 + proj_arg = i; proj_type = projty; proj_body = compat } in (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst, fterm :: letsubst) | Anonymous -> raise UndefinableExpansion -- cgit v1.2.3 From e43710b391c278ac7fcb808ec28d720b4317660c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 4 Jun 2018 15:26:20 +0200 Subject: Remove the proj_body field from the kernel. This was completely wrong, such a term could not even be type-checked by the kernel as it was internally using a match construct over a negative record. They were luckily only used in upper layers, namley printing and extraction. Recomputing the projection body might be costly in detyping, but this only happens when the compatibility flag is turned on, which is not the default. Such flag is probably bound to disappear anyways. Extraction should be fixed though so as to define directly primitive projections, similarly to what has been done in native compute. --- kernel/declarations.ml | 1 - kernel/declareops.ml | 2 +- kernel/indtypes.ml | 53 ++++++++++---------------------------------------- kernel/indtypes.mli | 2 +- 4 files changed, 12 insertions(+), 46 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index abebec156c..7bd7d6c9ca 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 fc6dc8b9ef..1b73096f7f 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 4bc7ea1988..14f2a3d8f4 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 5a38172c2d..45228e35e8 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) -- cgit v1.2.3