diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/constr.ml | 16 | ||||
-rw-r--r-- | kernel/constr.mli | 30 | ||||
-rw-r--r-- | kernel/cooking.ml | 2 | ||||
-rw-r--r-- | kernel/cooking.mli | 1 | ||||
-rw-r--r-- | kernel/declarations.ml | 3 | ||||
-rw-r--r-- | kernel/declareops.ml | 3 | ||||
-rw-r--r-- | kernel/entries.ml | 5 | ||||
-rw-r--r-- | kernel/environ.ml | 2 | ||||
-rw-r--r-- | kernel/indtypes.ml | 57 | ||||
-rw-r--r-- | kernel/indtypes.mli | 2 | ||||
-rw-r--r-- | kernel/mod_subst.ml | 11 | ||||
-rw-r--r-- | kernel/mod_subst.mli | 2 | ||||
-rw-r--r-- | kernel/modops.ml | 3 | ||||
-rw-r--r-- | kernel/names.ml | 11 | ||||
-rw-r--r-- | kernel/term_typing.ml | 31 |
15 files changed, 51 insertions, 128 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index c11b9ebf4..418229330 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -107,21 +107,13 @@ type t = (t, t, Sorts.t, Instance.t) kind_of_term type constr = t type existential = existential_key * constr array -type rec_declaration = Name.t array * constr array * constr array -type fixpoint = (int array * int) * rec_declaration - (* The array of [int]'s tells for each component of the array of - mutual fixpoints the number of lambdas to skip before finding the - recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) - (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is - the recursive argument); - The second component [int] tells which component of the block is - returned *) -type cofixpoint = int * rec_declaration - (* The component [int] tells which component of the block of - cofixpoint is returned *) type types = constr +type rec_declaration = (constr, types) prec_declaration +type fixpoint = (constr, types) pfixpoint +type cofixpoint = (constr, types) pcofixpoint + (*********************) (* Term constructors *) (*********************) diff --git a/kernel/constr.mli b/kernel/constr.mli index 742a13919..bf7b5e87b 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -161,8 +161,26 @@ val mkCase : case_info * constr * constr * constr array -> constr where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) -type rec_declaration = Name.t array * types array * constr array -type fixpoint = (int array * int) * rec_declaration +type ('constr, 'types) prec_declaration = + Name.t array * 'types array * 'constr array +type ('constr, 'types) pfixpoint = + (int array * int) * ('constr, 'types) prec_declaration + (* The array of [int]'s tells for each component of the array of + mutual fixpoints the number of lambdas to skip before finding the + recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) + (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is + the recursive argument); + The second component [int] tells which component of the block is + returned *) + +type ('constr, 'types) pcofixpoint = + int * ('constr, 'types) prec_declaration + (* The component [int] tells which component of the block of + cofixpoint is returned *) + +type rec_declaration = (constr, types) prec_declaration + +type fixpoint = (constr, types) pfixpoint val mkFix : fixpoint -> constr (** If [funnames = [|f1,.....fn|]] @@ -176,7 +194,7 @@ val mkFix : fixpoint -> constr ... with fn = bn.] *) -type cofixpoint = int * rec_declaration +type cofixpoint = (constr, types) pcofixpoint val mkCoFix : cofixpoint -> constr @@ -185,12 +203,6 @@ val mkCoFix : cofixpoint -> constr (** [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) type 'constr pexistential = Evar.t * 'constr array -type ('constr, 'types) prec_declaration = - Name.t array * 'types array * 'constr array -type ('constr, 'types) pfixpoint = - (int array * int) * ('constr, 'types) prec_declaration -type ('constr, 'types) pcofixpoint = - int * ('constr, 'types) prec_declaration type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) 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/mod_subst.ml b/kernel/mod_subst.ml index 0027ebecf..a47af56ca 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -24,7 +24,7 @@ open Constr is the term into which we should inline. *) type delta_hint = - | Inline of int * constr option + | Inline of int * (Univ.AUContext.t * constr) option | Equiv of KerName.t (* NB: earlier constructor Prefix_equiv of ModPath.t @@ -158,7 +158,7 @@ let find_prefix resolve mp = (** Applying a resolver to a kernel name *) -exception Change_equiv_to_inline of (int * constr) +exception Change_equiv_to_inline of (int * (Univ.AUContext.t * constr)) let solve_delta_kn resolve kn = try @@ -300,9 +300,10 @@ let subst_con0 sub (cst,u) = let knu = KerName.make mpu dir l in let knc = if mpu == mpc then knu else KerName.make mpc dir l in match search_delta_inline resolve knu knc with - | Some t -> + | Some (ctx, t) -> (* In case of inlining, discard the canonical part (cf #2608) *) - Constant.make1 knu, t + let () = assert (Int.equal (Univ.AUContext.size ctx) (Univ.Instance.length u)) in + Constant.make1 knu, Vars.subst_instance_constr u t | None -> let knc' = progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc @@ -482,7 +483,7 @@ let gen_subst_delta_resolver dom subst resolver = | Equiv kequ -> (try Equiv (subst_kn_delta subst kequ) with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c)) - | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t)) + | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t)) | Inline (_,None) -> hint in Deltamap.add_kn kkey' hint' rslv diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index b14d39207..76a1d173b 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -28,7 +28,7 @@ val add_kn_delta_resolver : KerName.t -> KerName.t -> delta_resolver -> delta_resolver val add_inline_delta_resolver : - KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver + KerName.t -> (int * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver diff --git a/kernel/modops.ml b/kernel/modops.ml index 203817118..22f523a9a 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -403,7 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta = | Undef _ | OpaqueDef _ -> l | Def body -> let constr = Mod_subst.force_constr body in - add_inline_delta_resolver kn (lev, Some constr) l + let ctx = Declareops.constant_polymorphic_context constant in + add_inline_delta_resolver kn (lev, Some (ctx, constr)) l with Not_found -> error_no_such_label_sub (Constant.label con) (ModPath.to_string (Constant.modpath con)) 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; |