Merge PR #8601: Move bound universe names to abstract contexts

6 files changed, 59 insertions, 30 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index c5bcd74072..58bb782f15 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -30,8 +30,8 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 
 type inductive_universes =
   | Monomorphic_ind_entry of Univ.ContextSet.t
-  | Polymorphic_ind_entry of Univ.UContext.t
-  | Cumulative_ind_entry of Univ.CumulativityInfo.t
+  | Polymorphic_ind_entry of Name.t array * Univ.UContext.t
+  | Cumulative_ind_entry of Name.t array * Univ.CumulativityInfo.t
 
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
@@ -60,7 +60,7 @@ type 'a const_entry_body = 'a proof_output Future.computation
 
 type constant_universes_entry =
   | Monomorphic_const_entry of Univ.ContextSet.t
-  | Polymorphic_const_entry of Univ.UContext.t
+  | Polymorphic_const_entry of Name.t array * Univ.UContext.t
 
 type 'a in_constant_universes_entry = 'a * constant_universes_entry
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0346026aa4..20c90bc05a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -268,8 +268,8 @@ let typecheck_inductive env mie =
   let env' =
     match mie.mind_entry_universes with
     | Monomorphic_ind_entry ctx -> push_context_set ctx env
-    | Polymorphic_ind_entry ctx -> push_context ctx env
-    | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
+    | Polymorphic_ind_entry (_, ctx) -> push_context ctx env
+    | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env
   in
   let env_params = check_context env' mie.mind_entry_params in
   let paramsctxt = mie.mind_entry_params in
@@ -407,7 +407,7 @@ let typecheck_inductive env mie =
     match mie.mind_entry_universes with
     | Monomorphic_ind_entry _ -> ()
     | Polymorphic_ind_entry _ -> ()
-    | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds
+    | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds
   in (env_arities, env_ar_par, paramsctxt, inds)
 
 (************************************************************************)
@@ -851,12 +851,12 @@ let compute_projections (kn, i as ind) mib =
 let abstract_inductive_universes iu =
   match iu with
   | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
-  | Polymorphic_ind_entry ctx -> 
-    let (inst, auctx) = Univ.abstract_universes ctx in
+  | Polymorphic_ind_entry (nas, ctx) ->
+    let (inst, auctx) = Univ.abstract_universes nas ctx in
     let inst = Univ.make_instance_subst inst in
     (inst, Polymorphic_ind auctx)
-  | Cumulative_ind_entry cumi -> 
-    let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+  | Cumulative_ind_entry (nas, cumi) ->
+    let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in
     let inst = Univ.make_instance_subst inst in
     (inst, Cumulative_ind acumi)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8b11851bbb..df10398b2f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -682,7 +682,7 @@ let constant_entry_of_side_effect cb u =
     | Monomorphic_const uctx ->
       Monomorphic_const_entry uctx
     | Polymorphic_const auctx ->
-      Polymorphic_const_entry (Univ.AUContext.repr auctx)
+      Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
   in
   let pt =
     match cb.const_body, u with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index fb1b3e236c..35fa871b4e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -68,8 +68,8 @@ let feedback_completion_typecheck =
 let abstract_constant_universes = function
   | Monomorphic_const_entry uctx ->
     Univ.empty_level_subst, Monomorphic_const uctx
-  | Polymorphic_const_entry uctx ->
-    let sbst, auctx = Univ.abstract_universes uctx in
+  | Polymorphic_const_entry (nas, uctx) ->
+    let sbst, auctx = Univ.abstract_universes nas uctx in
     let sbst = Univ.make_instance_subst sbst in
     sbst, Polymorphic_const auctx
 
@@ -78,7 +78,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
     | ParameterEntry (ctx,(t,uctx),nl) ->
       let env = match uctx with
         | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
-        | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
+        | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env
       in
       let j = infer env t in
       let usubst, univs = abstract_constant_universes uctx in
@@ -150,7 +150,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let ctx = Univ.ContextSet.union univs ctx in
         let env = push_context_set ~strict:true ctx env in
         env, Univ.empty_level_subst, Monomorphic_const ctx
-      | Polymorphic_const_entry uctx ->
+      | Polymorphic_const_entry (nas, uctx) ->
         (** Ensure not to generate internal constraints in polymorphic mode.
             The only way for this to happen would be that either the body
             contained deferred universes, or that it contains monomorphic
@@ -160,7 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
             i.e. [trust] is always [Pure]. *)
         let () = assert (Univ.ContextSet.is_empty ctx) in
         let env = push_context ~strict:false uctx env in
-        let sbst, auctx = Univ.abstract_universes uctx in
+        let sbst, auctx = Univ.abstract_universes nas uctx in
         let sbst = Univ.make_instance_subst sbst in
         env, sbst, Polymorphic_const auctx
       in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d09b54e7ec..0edf750997 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -937,17 +937,30 @@ let hcons_universe_context = UContext.hcons
 
 module AUContext =
 struct
-  include UContext
+  type t = Names.Name.t array constrained
 
   let repr (inst, cst) =
-    (Array.mapi (fun i _l -> Level.var i) inst, cst)
+    (Array.init (Array.length inst) (fun i -> Level.var i), cst)
 
-  let pr f ?variance ctx = pr f ?variance (repr ctx)
+  let pr f ?variance ctx = UContext.pr f ?variance (repr ctx)
 
   let instantiate inst (u, cst) =
     assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
 
+  let names (nas, _) = nas
+
+  let hcons (univs, cst) =
+    (Array.map Names.Name.hcons univs, hcons_constraints cst)
+
+  let empty = ([||], Constraint.empty)
+
+  let is_empty (nas, cst) = Array.is_empty nas && Constraint.is_empty cst
+
+  let union (nas, cst) (nas', cst') = (Array.append nas nas', Constraint.union cst cst')
+
+  let size (nas, _) = Array.length nas
+
 end
 
 let hcons_abstract_universe_context = AUContext.hcons
@@ -993,7 +1006,22 @@ end
 
 let hcons_cumulativity_info = CumulativityInfo.hcons
 
-module ACumulativityInfo = CumulativityInfo
+module ACumulativityInfo =
+struct
+  type t = AUContext.t * Variance.t array
+
+  let pr prl (univs, variance) =
+    AUContext.pr prl ~variance univs
+
+  let hcons (univs, variance) = (* should variance be hconsed? *)
+    (AUContext.hcons univs, variance)
+
+  let univ_context (univs, _subtypcst) = univs
+  let variance (_univs, variance) = variance
+
+  let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
+  let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
+end
 
 let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
 
@@ -1145,19 +1173,20 @@ let make_inverse_instance_subst i =
       LMap.empty arr
 
 let make_abstract_instance (ctx, _) = 
-  Array.mapi (fun i _l -> Level.var i) ctx
+  Array.init (Array.length ctx) (fun i -> Level.var i)
 
-let abstract_universes ctx =
+let abstract_universes nas ctx =
   let instance = UContext.instance ctx in
+  let () = assert (Int.equal (Array.length nas) (Instance.length instance)) in
   let subst = make_instance_subst instance in
   let cstrs = subst_univs_level_constraints subst 
       (UContext.constraints ctx)
   in
-  let ctx = UContext.make (instance, cstrs) in
+  let ctx = (nas, cstrs) in
   instance, ctx
 
-let abstract_cumulativity_info (univs, variance) =
-  let subst, univs = abstract_universes univs in
+let abstract_cumulativity_info nas (univs, variance) =
+  let subst, univs = abstract_universes nas univs in
   subst, (univs, variance)
 
 let rec compact_univ s vars i u =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7ac8247ca4..de7b334ae4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -336,9 +336,6 @@ sig
   val empty : t
   val is_empty : t -> bool
 
-  (** Don't use. *)
-  val instance : t -> Instance.t
-
   val size : t -> int
 
   (** Keeps the order of the instances *)
@@ -347,6 +344,9 @@ sig
   val instantiate : Instance.t -> t -> Constraint.t
   (** Generate the set of instantiated Constraint.t **)
 
+  val names : t -> Names.Name.t array
+  (** Return the names of the bound universe variables *)
+
 end
 
 (** Universe info for cumulative inductive types: A context of
@@ -466,8 +466,8 @@ val make_instance_subst : Instance.t -> universe_level_subst
 
 val make_inverse_instance_subst : Instance.t -> universe_level_subst
 
-val abstract_universes : UContext.t -> Instance.t * AUContext.t
-val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
+val abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t
+val abstract_cumulativity_info : Names.Name.t array -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
 (** TODO: move universe abstraction out of the kernel *)
 
 val make_abstract_instance : AUContext.t -> Instance.t