From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- vernac/command.ml | 17 ++++++++++------ vernac/discharge.ml | 25 +++++++++++++---------- vernac/discharge.mli | 3 ++- vernac/himsg.ml | 4 ++++ vernac/ind_tables.ml | 4 ++-- vernac/obligations.ml | 4 ++-- vernac/record.ml | 55 +++++++++++++++++++++++++++++++++++++++------------ vernac/record.mli | 4 +--- vernac/search.ml | 2 +- 9 files changed, 80 insertions(+), 38 deletions(-) (limited to 'vernac') diff --git a/vernac/command.ml b/vernac/command.ml index 2345cb4c5..406477356 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -649,20 +649,25 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in - let ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx in + let univs = + if poly then + if cum then + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) + else Polymorphic_ind_entry uctx + else + Monomorphic_ind_entry uctx + in (* Build the mutual inductive entry *) - let mind_ent = + let mind_ent = { mind_entry_params = List.map prepare_param ctx_params; mind_entry_record = None; mind_entry_finite = finite; mind_entry_inds = entries; - mind_entry_polymorphic = poly; - mind_entry_cumulative = cum; mind_entry_private = if prv then Some false else None; - mind_entry_universes = ground_uinfind; + mind_entry_universes = univs; } in - (if poly then + (if poly && cum then Inductiveops.infer_inductive_subtyping env_ar evd mind_ent else mind_ent), pl, impls diff --git a/vernac/discharge.ml b/vernac/discharge.ml index 738e27f63..18f93334b 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -79,12 +79,14 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let process_inductive (sechyps,abs_ctx) modlist mib = let nparams = mib.mind_nparams in - let subst, univs = - if mib.mind_polymorphic then - let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) in - let cstrs = Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes) in - inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) - else Univ.Instance.empty, (Univ.UInfoInd.univ_context mib.mind_universes) + let subst, univs = + match mib.mind_universes with + | Monomorphic_ind ctx -> Univ.Instance.empty, ctx + | Polymorphic_ind auctx -> + Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx + | Cumulative_ind cumi -> + let auctx = Univ.ACumulativityInfo.univ_context cumi in + Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx in let inds = Array.map_to_list @@ -105,7 +107,12 @@ let process_inductive (sechyps,abs_ctx) modlist mib = let (params',inds') = abstract_inductive sechyps' nparams inds in let abs_ctx = Univ.instantiate_univ_context abs_ctx in let univs = Univ.UContext.union abs_ctx univs in - let univ_info_ind = Universes.univ_inf_ind_from_universe_context univs in + let ind_univs = + match mib.mind_universes with + | Monomorphic_ind _ -> Monomorphic_ind_entry univs + | Polymorphic_ind _ -> Polymorphic_ind_entry univs + | Cumulative_ind _ -> + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) in let record = match mib.mind_record with | Some (Some (id, _, _)) -> Some (Some id) | Some None -> Some None @@ -115,9 +122,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_finite = mib.mind_finite; mind_entry_params = params'; mind_entry_inds = inds'; - mind_entry_polymorphic = mib.mind_polymorphic; - mind_entry_cumulative = mib.mind_cumulative; mind_entry_private = mib.mind_private; - mind_entry_universes = univ_info_ind + mind_entry_universes = ind_univs } diff --git a/vernac/discharge.mli b/vernac/discharge.mli index 18d1b6776..3845c04a1 100644 --- a/vernac/discharge.mli +++ b/vernac/discharge.mli @@ -11,4 +11,5 @@ open Entries open Opaqueproof val process_inductive : - Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry + ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context) + -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 6d8dd82ac..ce91e1a09 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -889,6 +889,10 @@ let explain_not_match_error = function | NoTypeConstraintExpected -> strbrk "a definition whose type is constrained can only be subtype " ++ strbrk "of a definition whose type is itself constrained" + | CumulativeStatusExpected b -> + let status b = if b then str"cumulative" else str"non-cumulative" in + str "a " ++ status b ++ str" declaration was expected, but a " ++ + status (not b) ++ str" declaration was found" | PolymorphicStatusExpected b -> let status b = if b then str"polymorphic" else str"monomorphic" in str "a " ++ status b ++ str" declaration was expected, but a " ++ diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml index f3259f1f3..65d42b626 100644 --- a/vernac/ind_tables.ml +++ b/vernac/ind_tables.ml @@ -148,7 +148,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define mode id c mib.mind_polymorphic ctx in + let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in declare_scheme kind [|ind,const|]; const, Safe_typing.add_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff @@ -166,7 +166,7 @@ let define_mutual_scheme_base kind suff f mode names mind = try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in let consts = Array.map2 (fun id cl -> - define mode id cl mib.mind_polymorphic ctx) ids cl in + define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e03e9b803..135e4c63a 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -365,8 +365,8 @@ let get_body obl = match obl.obl_body with | None -> None | Some (DefinedObl c) -> - let ctx = Environ.constant_context (Global.env ()) c in - let pc = (c, Univ.UContext.instance ctx) in + let u = Environ.constant_instance (Global.env ()) c in + let pc = (c, u) in Some (DefinedObl pc) | Some (TermObl c) -> Some (TermObl c) diff --git a/vernac/record.ml b/vernac/record.ml index b95131b72..7dd70d013 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -265,10 +265,16 @@ let warn_non_primitive_record = let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in - let u = Declareops.inductive_instance mib in + let u = Declareops.inductive_polymorphic_instance mib in let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let poly = mib.mind_polymorphic in - let ctx = Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) in + let poly = Declareops.inductive_is_polymorphic mib in + let ctx = + match mib.mind_universes with + | Monomorphic_ind ctx -> ctx + | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx + | Cumulative_ind cumi -> + Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) + in let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in @@ -377,12 +383,18 @@ let structure_signature ctx = open Typeclasses -let declare_structure finite cum poly ctx id idbuild paramimpls params arity template +let declare_structure finite univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in + let poly, ctx = + match univs with + | Monomorphic_ind_entry ctx -> false, ctx + | Polymorphic_ind_entry ctx -> true, ctx + | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi) + in let binder_name = match name with | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) @@ -400,17 +412,15 @@ let declare_structure finite cum poly ctx id idbuild paramimpls params arity tem mind_entry_record = Some (if !primitive_flag then Some binder_name else None); mind_entry_finite = finite; mind_entry_inds = [mie_ind]; - mind_entry_polymorphic = poly; - mind_entry_cumulative = cum; mind_entry_private = None; - mind_entry_universes = ctx; + mind_entry_universes = univs; } in let mie = if poly then begin let env = Global.env () in - let env' = Environ.push_context (Univ.UInfoInd.univ_context ctx) env in + let env' = Environ.push_context ctx env in (* let env'' = Environ.push_rel_context params env' in *) let evd = Evd.from_env env' in Inductiveops.infer_inductive_subtyping env' evd mie @@ -479,7 +489,16 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite cum poly (Universes.univ_inf_ind_from_universe_context ctx) (snd id) idbuild paramimpls + let univs = + if poly then + if cum then + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + else + Polymorphic_ind_entry ctx + else + Monomorphic_ind_entry ctx + in + let ind = declare_structure BiFinite univs (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -528,7 +547,7 @@ let add_inductive_class ind = let mind, oneind = Global.lookup_inductive ind in let k = let ctx = oneind.mind_arity_ctxt in - let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in + let inst = Declareops.inductive_polymorphic_instance mind in let ty = Inductive.type_of_inductive (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) @@ -581,10 +600,20 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> - let implfs = List.map + let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits - (succ (List.length params)) impls) implfs in - let ind = declare_structure finite cum poly (Universes.univ_inf_ind_from_universe_context ctx) idstruc + (succ (List.length params)) impls) implfs + in + let univs = + if poly then + if cum then + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + else + Polymorphic_ind_entry ctx + else + Monomorphic_ind_entry ctx + in + let ind = declare_structure finite univs idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind diff --git a/vernac/record.mli b/vernac/record.mli index c43d833b0..aa530fd61 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -26,9 +26,7 @@ val declare_projections : val declare_structure : Decl_kinds.recursivity_kind -> - Decl_kinds.cumulative_inductive_flag -> - Decl_kinds.polymorphic -> - Univ.universe_info_ind (** universe and subtyping constraints *) -> + Entries.inductive_universes -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) bool (** template arity ? *) -> diff --git a/vernac/search.ml b/vernac/search.ml index 0ff78f439..5e56ada8a 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -85,7 +85,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = let mib = Global.lookup_mind mind in let iter_packet i mip = let ind = (mind, i) in - let u = Declareops.inductive_instance mib in + let u = Declareops.inductive_polymorphic_instance mib in let i = (ind, u) in let typ = Inductiveops.type_of_inductive env i in let () = fn (IndRef ind) env typ in -- cgit v1.2.3