From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: Using UInfoInd for universes in inductive types It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. --- vernac/command.ml | 2 +- vernac/discharge.ml | 16 +++++----------- vernac/record.ml | 8 ++++---- vernac/record.mli | 2 +- 4 files changed, 11 insertions(+), 17 deletions(-) (limited to 'vernac') diff --git a/vernac/command.ml b/vernac/command.ml index 5f95a42a3..b76c2247b 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -656,7 +656,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = (uctx, Univ.UContext.empty); + mind_entry_universes = Universes.univ_inf_ind_from_universe_context uctx; }, pl, impls diff --git a/vernac/discharge.ml b/vernac/discharge.ml index 9c70eb97e..91e126ef1 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -81,17 +81,10 @@ 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 mib.mind_universes in - let cstrs = Univ.UContext.constraints mib.mind_universes in + 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, mib.mind_universes - in - let substsbt, univssbt = - if mib.mind_polymorphic then - let inst = Univ.UContext.instance mib.mind_subtyping in - let cstrs = Univ.UContext.constraints mib.mind_subtyping in - inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) - else Univ.Instance.empty, Univ.UContext.empty + else Univ.Instance.empty, (Univ.UInfoInd.univ_context mib.mind_universes) in let inds = Array.map_to_list @@ -112,6 +105,7 @@ 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 (* Here we must re-infer subtyping constraints. For now we just revert to trivial subtyping. *) let record = match mib.mind_record with | Some (Some (id, _, _)) -> Some (Some id) | Some None -> Some None @@ -123,5 +117,5 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_inds = inds'; mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; - mind_entry_universes = (univs, univssbt); + mind_entry_universes = univ_info_ind } diff --git a/vernac/record.ml b/vernac/record.ml index 5c76bb4b2..64f5e81d4 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -268,7 +268,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let u = Declareops.inductive_instance mib in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let poly = mib.mind_polymorphic in - let ctx = Univ.instantiate_univ_context mib.mind_universes in + let ctx = Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) 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 @@ -466,7 +466,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly (ctx, Univ.UContext.empty) (snd id) idbuild paramimpls + let ind = declare_structure BiFinite poly (Universes.univ_inf_ind_from_universe_context ctx) (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -515,7 +515,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 mind.mind_universes in + let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in let ty = Inductive.type_of_inductive (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) @@ -571,7 +571,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure finite poly (ctx, Univ.UContext.empty) idstruc + let ind = declare_structure finite poly (Universes.univ_inf_ind_from_universe_context ctx) 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 a380b041a..ec5d2cf83 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -27,7 +27,7 @@ val declare_projections : val declare_structure : Decl_kinds.recursivity_kind -> bool (** polymorphic?*) -> - (Univ.universe_context * Univ.universe_context) (** universe and subtyping constraints *) -> + Univ.universe_info_ind (** universe and subtyping constraints *) -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) bool (** template arity ? *) -> -- cgit v1.2.3