From 35fba70509d9fb219b2a88f8e7bd246b2671b39b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 9 Nov 2017 17:27:58 +0100 Subject: Simplification: cumulativity information is variance information. Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *) --- vernac/comInductive.ml | 2 +- vernac/record.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac') diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 1c8677e9cd..3f8d413b75 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -340,7 +340,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = match uctx with | Polymorphic_const_entry uctx -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) + Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx) else Polymorphic_ind_entry uctx | Monomorphic_const_entry uctx -> Monomorphic_ind_entry uctx diff --git a/vernac/record.ml b/vernac/record.ml index 1e464eb8bf..31c0483b4c 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -501,7 +501,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari match univs with | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) + Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs) else Polymorphic_ind_entry univs | Monomorphic_const_entry univs -> @@ -632,7 +632,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf match univs with | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) + Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs) else Polymorphic_ind_entry univs | Monomorphic_const_entry univs -> -- cgit v1.2.3 From 1ed0836a7e0c8e05b0288f85e344ef5249d5d228 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 10 Nov 2017 13:23:32 +0100 Subject: Inference of inductive subtyping does not need an evar map. --- vernac/comInductive.ml | 2 +- vernac/record.ml | 11 +---------- 2 files changed, 2 insertions(+), 11 deletions(-) (limited to 'vernac') diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 3f8d413b75..faac16802a 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -356,7 +356,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = } in (if poly && cum then - Inductiveops.infer_inductive_subtyping env_ar sigma mind_ent + Inductiveops.infer_inductive_subtyping env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls (* Very syntactical equality *) diff --git a/vernac/record.ml b/vernac/record.ml index 31c0483b4c..6e35ac4dbb 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -423,16 +423,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t mind_entry_universes = univs; } in - let mie = - match ctx with - | Polymorphic_const_entry ctx -> - let env = Global.env () in - let env' = Environ.push_context ctx env in - let evd = Evd.from_env env' in - Inductiveops.infer_inductive_subtyping env' evd mie - | Monomorphic_const_entry _ -> - mie - in + let mie = Inductiveops.infer_inductive_subtyping (Global.env ()) mie in let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in -- cgit v1.2.3 From 6c2d10b93b819f0735a43453c78566795de8ba5a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 10 Nov 2017 15:05:21 +0100 Subject: Use specialized function for inductive subtyping inference. This ensures by construction that we never infer constraints outside the variance model. --- vernac/comInductive.ml | 2 +- vernac/record.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index faac16802a..41474fc638 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -356,7 +356,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = } in (if poly && cum then - Inductiveops.infer_inductive_subtyping env_ar mind_ent + InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls (* Very syntactical equality *) diff --git a/vernac/record.ml b/vernac/record.ml index 6e35ac4dbb..d9af5378f4 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -423,7 +423,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t mind_entry_universes = univs; } in - let mie = Inductiveops.infer_inductive_subtyping (Global.env ()) mie in + let mie = InferCumulativity.infer_inductive (Global.env ()) mie in let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in -- cgit v1.2.3