From 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 23:39:11 +0200 Subject: Fix defining non primitive projections with abstracted universes. I think this only affects printing (in the new test you would get [Var (0)] when printing runwrap) but is still ugly. --- test-suite/output/UnivBinders.out | 51 ++++++++++++++++++++++++++++++++++++--- test-suite/output/UnivBinders.v | 26 ++++++++++++++++++-- vernac/record.ml | 16 +++--------- 3 files changed, 75 insertions(+), 18 deletions(-) diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 904ff68aa..1bacb7513 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,12 +1,55 @@ +NonCumulative Inductive Empty@{u} : Type@{u} := +NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } + +PWrap has primitive projections with eta conversion. +For PWrap: Argument scope is [type_scope] +For pwrap: Argument scopes are [type_scope _] +punwrap@{u} = +fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p + : forall A : Type@{u}, PWrap@{u} A -> A +(* u |= *) + +punwrap is universe polymorphic +Argument scopes are [type_scope _] +NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } + +For RWrap: Argument scope is [type_scope] +For rwrap: Argument scopes are [type_scope _] +runwrap@{u} = +fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap + : forall A : Type@{u}, RWrap@{u} A -> A +(* u |= *) + +runwrap is universe polymorphic +Argument scopes are [type_scope _] +Wrap@{u} = fun A : Type@{u} => A + : Type@{u} -> Type@{u} +(* u |= *) + +Wrap is universe polymorphic +Argument scope is [type_scope] +wrap@{u} = +fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap + : forall A : Type@{u}, Wrap@{u} A -> A +(* u |= *) + +wrap is universe polymorphic +Arguments A, Wrap are implicit and maximally inserted +Argument scopes are [type_scope _] bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) bar is universe polymorphic -foo@{u Top.8 v} = -Type@{Top.8} -> Type@{v} -> Type@{u} - : Type@{max(u+1, Top.8+1, v+1)} -(* u Top.8 v |= *) +foo@{u Top.17 v} = +Type@{Top.17} -> Type@{v} -> Type@{u} + : Type@{max(u+1, Top.17+1, v+1)} +(* u Top.17 v |= *) foo is universe polymorphic +Monomorphic mono = Type@{u} + : Type@{u+1} +(* u |= *) + +mono is not universe polymorphic diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 8656ff1a3..2c378e795 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -2,12 +2,34 @@ Set Universe Polymorphism. Set Printing Universes. Unset Strict Universe Declaration. -Class Wrap A := wrap : A. +(* universe binders on inductive types and record projections *) +Inductive Empty@{u} : Type@{u} := . +Print Empty. -Instance bar@{u} : Wrap@{u} Set. Proof nat. +Set Primitive Projections. +Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }. +Print PWrap. +Print punwrap. + +Unset Primitive Projections. +Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }. +Print RWrap. +Print runwrap. + +(* universe binders also go on the constants for operational typeclasses. *) +Class Wrap@{u} (A:Type@{u}) := wrap : A. +Print Wrap. +Print wrap. + +(* Instance in lemma mode used to ignore the binders. *) +Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed. Print bar. (* The universes in the binder come first, then the extra universes in order of appearance. *) Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. Print foo. + +(* Binders even work with monomorphic definitions! *) +Monomorphic Definition mono@{u} := Type@{u}. +Print mono. diff --git a/vernac/record.ml b/vernac/record.ml index e465e0616..0819dadb4 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -266,11 +266,10 @@ let warn_non_primitive_record = strbrk" could not be defined as a primitive record"))) (* We build projections *) -let declare_projections indsp ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields = +let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in - let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in let u = Univ.UContext.instance ctx in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let indu = indsp, u in @@ -394,7 +393,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let type_constructor = it_mkProd_or_LetIn ind fields in let poly, ctx = match univs with - | Monomorphic_ind_entry ctx -> false, ctx + | Monomorphic_ind_entry ctx -> false, Univ.UContext.empty | Polymorphic_ind_entry ctx -> true, ctx | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi) in @@ -430,20 +429,13 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t else mie in - let kn = Command.declare_mutual_inductive_with_eliminations mie Universes.empty_binders [(paramimpls,[])] in + let kn = Command.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 - let fields = - if poly then - let subst, _ = Univ.abstract_universes ctx in - Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields - else fields - in - let kinds,sp_projs = declare_projections rsp ~kind binder_name coers ubinders fieldimpls fields in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); - Universes.register_universe_binders (IndRef rsp) ubinders; rsp let implicits_of_context ctx = -- cgit v1.2.3