From 601ce3738253e4bb197900ee6dad271c4e3666d6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 14:23:25 +0200
Subject: Adding universe names to polymorphic entry instances.

---
 kernel/entries.ml     |  6 +++---
 kernel/indtypes.ml    | 12 +++++++-----
 kernel/safe_typing.ml |  2 +-
 kernel/term_typing.ml |  8 +++++---
 kernel/univ.ml        |  3 +++
 kernel/univ.mli       |  3 +++
 6 files changed, 22 insertions(+), 12 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index c5bcd74072..87fa385a60 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 list * Univ.UContext.t
+  | Cumulative_ind_entry of Name.t list * 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 list * 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..2d74f99c15 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,14 @@ 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 -> 
+  | Polymorphic_ind_entry (nas, ctx) ->
+    let () = assert (Int.equal (List.length nas) (UContext.size ctx)) in
     let (inst, auctx) = Univ.abstract_universes ctx in
     let inst = Univ.make_instance_subst inst in
     (inst, Polymorphic_ind auctx)
-  | Cumulative_ind_entry cumi -> 
+  | Cumulative_ind_entry (nas, cumi) ->
     let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+    let () = assert (Int.equal (List.length nas) (Instance.length inst)) 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..4759625e8a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -68,7 +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 ->
+  | Polymorphic_const_entry (nas, uctx) ->
+    let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in
     let sbst, auctx = Univ.abstract_universes uctx in
     let sbst = Univ.make_instance_subst sbst in
     sbst, Polymorphic_const auctx
@@ -78,7 +79,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 +151,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
@@ -159,6 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
             unconditionally export side-effects from polymorphic definitions,
             i.e. [trust] is always [Pure]. *)
         let () = assert (Univ.ContextSet.is_empty ctx) in
+        let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in
         let env = push_context ~strict:false uctx env in
         let sbst, auctx = Univ.abstract_universes uctx in
         let sbst = Univ.make_instance_subst sbst in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d09b54e7ec..35566019a8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -948,6 +948,9 @@ struct
     assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
 
+  (** FIXME: Actually store this information in the type *)
+  let names (u, _) = Array.map_to_list (fun _ -> Names.Anonymous) u
+
 end
 
 let hcons_abstract_universe_context = AUContext.hcons
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7ac8247ca4..bc902d8f4b 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -347,6 +347,9 @@ sig
   val instantiate : Instance.t -> t -> Constraint.t
   (** Generate the set of instantiated Constraint.t **)
 
+  val names : t -> Names.Name.t list
+  (** Return the names of the bound universe variables *)
+
 end
 
 (** Universe info for cumulative inductive types: A context of
-- 
cgit v1.2.3


From 168af2ba6ae1facf948c7c7bee725ac0f0cd3b41 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 15:34:28 +0200
Subject: Force the user to provide names when generating abstract universe
 contexts.

For now this data is not stored, but the code checks that indeed the number
of names provided coincide with the instance length.

I had to reimplement the same kind of workaround hack in section handling as
the one already performed in UnivNames because the name information is not
present in the section data structure. This deserves a FIXME.
---
 kernel/indtypes.ml    | 6 ++----
 kernel/term_typing.ml | 6 ++----
 kernel/univ.ml        | 7 ++++---
 kernel/univ.mli       | 4 ++--
 4 files changed, 10 insertions(+), 13 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 2d74f99c15..20c90bc05a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -852,13 +852,11 @@ let abstract_inductive_universes iu =
   match iu with
   | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
   | Polymorphic_ind_entry (nas, ctx) ->
-    let () = assert (Int.equal (List.length nas) (UContext.size ctx)) in
-    let (inst, auctx) = Univ.abstract_universes ctx in
+    let (inst, auctx) = Univ.abstract_universes nas ctx in
     let inst = Univ.make_instance_subst inst in
     (inst, Polymorphic_ind auctx)
   | Cumulative_ind_entry (nas, cumi) ->
-    let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
-    let () = assert (Int.equal (List.length nas) (Instance.length inst)) in
+    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/term_typing.ml b/kernel/term_typing.ml
index 4759625e8a..35fa871b4e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -69,8 +69,7 @@ let abstract_constant_universes = function
   | Monomorphic_const_entry uctx ->
     Univ.empty_level_subst, Monomorphic_const uctx
   | Polymorphic_const_entry (nas, uctx) ->
-    let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) 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
     sbst, Polymorphic_const auctx
 
@@ -160,9 +159,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
             unconditionally export side-effects from polymorphic definitions,
             i.e. [trust] is always [Pure]. *)
         let () = assert (Univ.ContextSet.is_empty ctx) in
-        let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) 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 35566019a8..a8359bc4a7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1150,8 +1150,9 @@ let make_inverse_instance_subst i =
 let make_abstract_instance (ctx, _) = 
   Array.mapi (fun i _l -> Level.var i) ctx
 
-let abstract_universes ctx =
+let abstract_universes nas ctx =
   let instance = UContext.instance ctx in
+  let () = assert (Int.equal (List.length nas) (Instance.length instance)) in
   let subst = make_instance_subst instance in
   let cstrs = subst_univs_level_constraints subst 
       (UContext.constraints ctx)
@@ -1159,8 +1160,8 @@ let abstract_universes ctx =
   let ctx = UContext.make (instance, 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 bc902d8f4b..e665ed94e7 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -469,8 +469,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 list -> UContext.t -> Instance.t * AUContext.t
+val abstract_cumulativity_info : Names.Name.t list -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
 (** TODO: move universe abstraction out of the kernel *)
 
 val make_abstract_instance : AUContext.t -> Instance.t
-- 
cgit v1.2.3


From 27048fb3ef7a10ffde1ee368f6fb7ef354431fe8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 16:23:28 +0200
Subject: Actually store the bound name information in the abstract universe
 context.

---
 kernel/univ.ml  | 43 ++++++++++++++++++++++++++++++++++---------
 kernel/univ.mli |  3 ---
 2 files changed, 34 insertions(+), 12 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index a8359bc4a7..ec6dcee834 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -937,19 +937,29 @@ let hcons_universe_context = UContext.hcons
 
 module AUContext =
 struct
-  include UContext
+  type t = Names.Name.t list constrained
 
   let repr (inst, cst) =
-    (Array.mapi (fun i _l -> Level.var i) inst, cst)
+    (Array.init (List.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);
+    assert (List.length u = Array.length inst);
     subst_instance_constraints inst cst
 
-  (** FIXME: Actually store this information in the type *)
-  let names (u, _) = Array.map_to_list (fun _ -> Names.Anonymous) u
+  let names (nas, _) = nas
+
+  let hcons (univs, cst) =
+    (List.map Names.Name.hcons univs, hcons_constraints cst)
+
+  let empty = ([], Constraint.empty)
+
+  let is_empty (nas, cst) = List.is_empty nas && Constraint.is_empty cst
+
+  let union (nas, cst) (nas', cst') = (nas @ nas', Constraint.union cst cst')
+
+  let size (nas, _) = List.length nas
 
 end
 
@@ -996,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
 
@@ -1148,7 +1173,7 @@ 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 (List.length ctx) (fun i -> Level.var i)
 
 let abstract_universes nas ctx =
   let instance = UContext.instance ctx in
@@ -1157,7 +1182,7 @@ let abstract_universes nas ctx =
   let cstrs = subst_univs_level_constraints subst 
       (UContext.constraints ctx)
   in
-  let ctx = UContext.make (instance, cstrs) in
+  let ctx = UContext.make (nas, cstrs) in
   instance, ctx
 
 let abstract_cumulativity_info nas (univs, variance) =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e665ed94e7..3788d8f90d 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 *)
-- 
cgit v1.2.3


From 23ef45aa14308aa0b1e1b1f6061ec9e7e7634e49 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 1 Oct 2018 13:40:45 +0200
Subject: Use arrays of names instead of lists in abstract universe names.

There is little point in having a list, as there is virtually no sharing
nor expansion of bound universe names. This representation is thus more
compact.
---
 kernel/entries.ml |  6 +++---
 kernel/univ.ml    | 22 +++++++++++-----------
 kernel/univ.mli   |  6 +++---
 3 files changed, 17 insertions(+), 17 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 87fa385a60..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 Name.t list * Univ.UContext.t
-  | Cumulative_ind_entry of Name.t list * 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 Name.t list * 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/univ.ml b/kernel/univ.ml
index ec6dcee834..0edf750997 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -937,29 +937,29 @@ let hcons_universe_context = UContext.hcons
 
 module AUContext =
 struct
-  type t = Names.Name.t list constrained
+  type t = Names.Name.t array constrained
 
   let repr (inst, cst) =
-    (Array.init (List.length inst) (fun i -> Level.var i), cst)
+    (Array.init (Array.length inst) (fun i -> Level.var i), cst)
 
   let pr f ?variance ctx = UContext.pr f ?variance (repr ctx)
 
   let instantiate inst (u, cst) =
-    assert (List.length u = Array.length inst);
+    assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
 
   let names (nas, _) = nas
 
   let hcons (univs, cst) =
-    (List.map Names.Name.hcons univs, hcons_constraints cst)
+    (Array.map Names.Name.hcons univs, hcons_constraints cst)
 
-  let empty = ([], Constraint.empty)
+  let empty = ([||], Constraint.empty)
 
-  let is_empty (nas, cst) = List.is_empty nas && Constraint.is_empty cst
+  let is_empty (nas, cst) = Array.is_empty nas && Constraint.is_empty cst
 
-  let union (nas, cst) (nas', cst') = (nas @ nas', Constraint.union cst cst')
+  let union (nas, cst) (nas', cst') = (Array.append nas nas', Constraint.union cst cst')
 
-  let size (nas, _) = List.length nas
+  let size (nas, _) = Array.length nas
 
 end
 
@@ -1173,16 +1173,16 @@ let make_inverse_instance_subst i =
       LMap.empty arr
 
 let make_abstract_instance (ctx, _) = 
-  Array.init (List.length ctx) (fun i -> Level.var i)
+  Array.init (Array.length ctx) (fun i -> Level.var i)
 
 let abstract_universes nas ctx =
   let instance = UContext.instance ctx in
-  let () = assert (Int.equal (List.length nas) (Instance.length instance)) 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 (nas, cstrs) in
+  let ctx = (nas, cstrs) in
   instance, ctx
 
 let abstract_cumulativity_info nas (univs, variance) =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 3788d8f90d..de7b334ae4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -344,7 +344,7 @@ sig
   val instantiate : Instance.t -> t -> Constraint.t
   (** Generate the set of instantiated Constraint.t **)
 
-  val names : t -> Names.Name.t list
+  val names : t -> Names.Name.t array
   (** Return the names of the bound universe variables *)
 
 end
@@ -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 : Names.Name.t list -> UContext.t -> Instance.t * AUContext.t
-val abstract_cumulativity_info : Names.Name.t list -> 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
-- 
cgit v1.2.3