diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 4 | ||||
| -rw-r--r-- | kernel/declarations.mli | 14 | ||||
| -rw-r--r-- | kernel/declareops.ml | 6 | ||||
| -rw-r--r-- | kernel/entries.mli | 7 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 14 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 4 |
8 files changed, 30 insertions, 23 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 23861347a8..545325a2a9 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -871,8 +871,8 @@ let rec get_parameters depth n argstk = let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (projs,pbs) when Array.length projs > 0 - && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> + | Some (Some (_,projs,pbs)) when + mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.Declarations.mind_nparams in diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 6b3f6c72f4..d908bcbe21 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -97,6 +97,15 @@ type wf_paths = recarg Rtree.t v} *) +(** Record information: + If the record is not primitive, then None + Otherwise, we get: + - The identifier for the binder name of the record in primitive projections. + - The constants associated to each projection. + - The checked projection bodies. *) + +type record_body = (Id.t * constant array * projection_body array) option + type regular_inductive_arity = { mind_user_arity : types; mind_sort : sorts; @@ -153,10 +162,7 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : (constant array * projection_body array) option; - (** Whether the inductive type has been declared as a record, - In the case it is primitive we get its projection names and checked - projection bodies, otherwise both arrays are empty. *) + mind_record : record_body option; (** The record information *) mind_finite : Decl_kinds.recursivity_kind; (** Whether the type is inductive or coinductive *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 5b937207fd..51e435d796 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -237,14 +237,14 @@ let subst_mind_packet sub mbp = mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } -let subst_mind_record sub (ps, pb as r) = +let subst_mind_record sub (id, ps, pb as r) = let ps' = Array.smartmap (subst_constant sub) ps in let pb' = Array.smartmap (subst_const_proj sub) pb in if ps' == ps && pb' == pb then r - else (ps', pb') + else (id, ps', pb') let subst_mind_body sub mib = - { mind_record = Option.smartmap (subst_mind_record sub) mib.mind_record ; + { mind_record = Option.smartmap (Option.smartmap (subst_mind_record sub)) mib.mind_record ; mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); diff --git a/kernel/entries.mli b/kernel/entries.mli index bf47ff90ee..f6958849b0 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -41,9 +41,10 @@ type one_inductive_entry = { mind_entry_lc : constr list } type mutual_inductive_entry = { - mind_entry_record : bool option; - (** Some true: primitive record - Some false: non-primitive record *) + mind_entry_record : (Id.t option) option; + (** Some (Some id): primitive record with id the binder name of the record + in projections. + Some None: non-primitive record *) mind_entry_finite : Decl_kinds.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 73a23ef059..39455a7d2a 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -661,7 +661,7 @@ 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 indsp) n nparamargs params +let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params mind_consnrealdecls mind_consnrealargs ctx = let mp, dp, l = repr_mind kn in let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in @@ -674,7 +674,7 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params ci_pp_info = print_info } in let len = List.length ctx in - let x = Name (Id.of_string (Unicode.lowercase_first_char (Id.to_string n))) in + let x = Name x in let compat_body ccl i = (* [ccl] is defined in context [params;x:rp] *) (* [ccl'] is defined in context [params;x:rp;x:rp] *) @@ -780,7 +780,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let pkt = packets.(0) in let isrecord = match isrecord with - | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 -> + | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 -> (** The elimination criterion ensures that all projections can be defined. *) let u = if p then @@ -792,11 +792,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re (try let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in let kns, projs = - compute_projections indsp pkt.mind_typename nparamargs params + compute_projections indsp pkt.mind_typename rid nparamargs params pkt.mind_consnrealdecls pkt.mind_consnrealargs fields - in Some (kns, projs) - with UndefinableExpansion -> Some ([||], [||])) - | Some _ -> Some ([||], [||]) + in Some (Some (rid, kns, projs)) + with UndefinableExpansion -> Some None) + | Some _ -> Some None | None -> None in (* Build the mutual inductive *) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 0d5b034049..a231b6cf9d 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -41,7 +41,7 @@ val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutua val enforce_indices_matter : unit -> unit val is_indices_matter : unit -> bool -val compute_projections : pinductive -> Id.t -> +val compute_projections : pinductive -> Id.t -> Id.t -> int -> Context.rel_context -> int array -> int array -> Context.rel_context -> (constant array * projection_body array) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 58909ce012..a08184ed5e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -297,7 +297,7 @@ let elim_sorts (_,mip) = mip.mind_kelim let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = match mib.mind_record with - | Some (projs, _) when Array.length projs > 0 -> true + | Some (Some _) -> true | _ -> false let extended_rel_list n hyps = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a3c4d98490..232508bc82 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -169,11 +169,11 @@ let infer_declaration env kn dcl = let mib, _ = Inductive.lookup_mind_specif env (ind,0) in let kn, pb = match mib.mind_record with - | Some (kns, pbs) -> + | Some (Some (id, kns, pbs)) -> if i < Array.length pbs then kns.(i), pbs.(i) else assert false - | None -> assert false + | _ -> assert false in let term, typ = pb.proj_eta in Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, |