From 3f7f3a9bc9fde8e1d44d1179fa8dd16221ebf526 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 25 Jul 2014 17:52:46 +0200 Subject: - Do module substitution inside mind_record. - Distinguish between primitive and non-primitive records in the kernel declaration, so as to try eta-conversion on primitive records only. --- kernel/declareops.ml | 8 +++++++- kernel/entries.mli | 3 ++- kernel/indtypes.ml | 23 ++++++++++++----------- library/declare.ml | 2 +- toplevel/command.ml | 2 +- toplevel/discharge.ml | 6 +++++- toplevel/record.ml | 2 +- 7 files changed, 29 insertions(+), 17 deletions(-) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 51b7b6f97..9d2382f6e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -223,8 +223,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 (c, ps as r) = + let c' = subst_mps sub c in + let ps' = Array.smartmap (subst_constant sub) ps in + if c' == c && ps' == ps then r + else (c', ps') + let subst_mind_body sub mib = - { mind_record = mib.mind_record ; + { mind_record = 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 c672ba731..244637acd 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -41,7 +41,8 @@ type one_inductive_entry = { mind_entry_lc : constr list } type mutual_inductive_entry = { - mind_entry_record : bool; + mind_entry_record : bool option; + (** Some true: primitive record, Some false: non-primitive record *) mind_entry_finite : bool; 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 6e87a0444..9c83ba1a9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -742,17 +742,18 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re } in let packets = Array.map2 build_one_packet inds recargs in let isrecord = - let pkt = packets.(0) in - if isrecord (* || (Array.length pkt.mind_consnames = 1 && *) - (* inductive_sort_family pkt <> InProp) *) then - let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in - let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in - try - let exp = compute_expansion ((kn, 0), u) params - (List.firstn pkt.mind_consnrealdecls.(0) rctx) - in Some exp - with UndefinableExpansion -> None - else None + match isrecord with + | Some true -> (* || (Array.length pkt.mind_consnames = 1 && *) + let pkt = packets.(0) in + let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in + let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in + (try + let exp = compute_expansion ((kn, 0), u) params + (List.firstn pkt.mind_consnrealdecls.(0) rctx) + in Some exp + with UndefinableExpansion -> (Some (mkProp, [||]))) + | Some false -> Some (mkProp, [||]) + | None -> None in (* Build the mutual inductive *) { mind_record = isrecord; diff --git a/library/declare.ml b/library/declare.ml index f746282d1..bacd9e2c1 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -366,7 +366,7 @@ let dummy_one_inductive_entry mie = { (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_inductive_entry (_,m) = ([],{ mind_entry_params = []; - mind_entry_record = false; + mind_entry_record = None; mind_entry_finite = true; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; diff --git a/toplevel/command.ml b/toplevel/command.ml index 0e4d6e330..a675fe028 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -525,7 +525,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = in (* Build the mutual inductive entry *) { mind_entry_params = List.map prepare_param ctx_params; - mind_entry_record = false; + mind_entry_record = None; mind_entry_finite = finite; mind_entry_inds = entries; mind_entry_polymorphic = poly; diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 3015eab25..bd5218eff 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -91,7 +91,11 @@ let process_inductive (sechyps,abs_ctx) modlist mib = let sechyps' = map_named_context (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in let univs = Univ.UContext.union abs_ctx mib.mind_universes in - { mind_entry_record = mib.mind_record <> None; + let record = match mib.mind_record with + | None -> None + | Some (_, a) -> Some (Array.length a > 0) + in + { mind_entry_record = record; mind_entry_finite = mib.mind_finite; mind_entry_params = params'; mind_entry_inds = inds'; diff --git a/toplevel/record.ml b/toplevel/record.ml index d2aa48db9..896cc41c7 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -330,7 +330,7 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f end; let mie = { mind_entry_params = List.map degenerate_decl params; - mind_entry_record = true; + mind_entry_record = Some !primitive_flag; mind_entry_finite = finite != CoFinite; mind_entry_inds = [mie_ind]; mind_entry_polymorphic = poly; -- cgit v1.2.3