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.

---
 engine/uState.ml     | 19 +++++++++++++++----
 engine/univNames.ml  | 17 +++++++++++------
 engine/univNames.mli |  2 ++
 3 files changed, 28 insertions(+), 10 deletions(-)

(limited to 'engine')

diff --git a/engine/uState.ml b/engine/uState.ml
index aa7ec63a6f..41905feab7 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -101,13 +101,21 @@ let context ctx = Univ.ContextSet.to_context ctx.uctx_local
 
 let const_univ_entry ~poly uctx =
   let open Entries in
-  if poly then Polymorphic_const_entry (context uctx)
+  if poly then
+    let (binders, _) = uctx.uctx_names in
+    let uctx = context uctx in
+    let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+    Polymorphic_const_entry (nas, uctx)
   else Monomorphic_const_entry (context_set uctx)
 
 (* does not support cumulativity since you need more info *)
 let ind_univ_entry ~poly uctx =
   let open Entries in
-  if poly then Polymorphic_ind_entry (context uctx)
+  if poly then
+    let (binders, _) = uctx.uctx_names in
+    let uctx = context uctx in
+    let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+    Polymorphic_ind_entry (nas, uctx)
   else Monomorphic_ind_entry (context_set uctx)
 
 let of_context_set ctx = { empty with uctx_local = ctx }
@@ -394,8 +402,11 @@ let check_univ_decl ~poly uctx decl =
   let ctx =
     let names = decl.univdecl_instance in
     let extensible = decl.univdecl_extensible_instance in
-    if poly
-    then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx)
+    if poly then
+      let (binders, _) = uctx.uctx_names in
+      let uctx = universe_context ~names ~extensible uctx in
+      let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+      Entries.Polymorphic_const_entry (nas, uctx)
     else
       let () = check_universe_context_set ~names ~extensible uctx in
       Entries.Monomorphic_const_entry uctx.uctx_local
diff --git a/engine/univNames.ml b/engine/univNames.ml
index a71f9c5736..a037e577c4 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -81,18 +81,23 @@ let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj =
     discharge_function = discharge_ubinder;
     rebuild_function = (fun x -> x); }
 
+let compute_instance_binders inst ubinders =
+  let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
+  let map lvl =
+    try Name (LMap.find lvl revmap)
+    with Not_found -> Name (name_universe lvl)
+  in
+  Array.map_to_list map (Instance.to_array inst)
+
 let register_universe_binders ref ubinders =
   (** TODO: change the API to register a [Name.t list] instead. This is the last
       part of the code that depends on the internal representation of names in
       abstract contexts, but removing it requires quite a rework of the
       callers. *)
   let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in
-  let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
-  let map lvl =
-    try LMap.find lvl revmap
-    with Not_found -> name_universe lvl
-  in
-  let ubinders = Array.map_to_list map (Instance.to_array univs) in
+  let ubinders = compute_instance_binders univs ubinders in
+  (** FIXME: the function above always generate names but this may change *)
+  let ubinders = List.map (function Name id -> id | Anonymous -> assert false) ubinders in
   if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders))
 
 type univ_name_list = Names.lname list
diff --git a/engine/univNames.mli b/engine/univNames.mli
index bd4062ade4..634db9581c 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -19,6 +19,8 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 val empty_binders : universe_binders
 
+val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t list
+
 val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
 
 type univ_name_list = Names.lname list
-- 
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.

---
 engine/univNames.ml | 58 ++++++++---------------------------------------------
 1 file changed, 8 insertions(+), 50 deletions(-)

(limited to 'engine')

diff --git a/engine/univNames.ml b/engine/univNames.ml
index a037e577c4..5c87fed31c 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -36,51 +36,15 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
-let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders"
-
-let universe_binders_of_global ref : Id.t list =
-  try
-    let l = GlobRef.Map.find ref !universe_binders_table in l
+let universe_binders_of_global ref : Name.t list =
+  try AUContext.names (Environ.universes_of_global (Global.env ()) ref)
   with Not_found -> []
 
-let cache_ubinder (_,(ref,l)) =
-  universe_binders_table := GlobRef.Map.add ref l !universe_binders_table
-
-let subst_ubinder (subst,(ref,l as orig)) =
-  let ref' = fst (Globnames.subst_global subst ref) in
-  if ref == ref' then orig else ref', l
-
 let name_universe lvl =
   (** Best-effort naming from the string representation of the level. This is
       completely hackish and should be solved in upper layers instead. *)
   Id.of_string_soft (Level.to_string lvl)
 
-let discharge_ubinder (_,(ref,l)) =
-  (** Expand polymorphic binders with the section context *)
-  let info = Lib.section_segment_of_reference ref in
-  let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in
-  let map lvl = match Level.name lvl with
-    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
-      assert false
-    | Some na ->
-      try
-        let qid = Nametab.shortest_qualid_of_universe na in
-        snd (Libnames.repr_qualid qid)
-      with Not_found -> name_universe lvl
-  in
-  let l = List.map map sec_inst @ l in
-  Some (ref, l)
-
-let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj =
-  let open Libobject in
-  declare_object { (default_object "universe binder") with
-    cache_function = cache_ubinder;
-    load_function = (fun _ x -> cache_ubinder x);
-    classify_function = (fun x -> Substitute x);
-    subst_function = subst_ubinder;
-    discharge_function = discharge_ubinder;
-    rebuild_function = (fun x -> x); }
-
 let compute_instance_binders inst ubinders =
   let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
   let map lvl =
@@ -89,16 +53,7 @@ let compute_instance_binders inst ubinders =
   in
   Array.map_to_list map (Instance.to_array inst)
 
-let register_universe_binders ref ubinders =
-  (** TODO: change the API to register a [Name.t list] instead. This is the last
-      part of the code that depends on the internal representation of names in
-      abstract contexts, but removing it requires quite a rework of the
-      callers. *)
-  let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in
-  let ubinders = compute_instance_binders univs ubinders in
-  (** FIXME: the function above always generate names but this may change *)
-  let ubinders = List.map (function Name id -> id | Anonymous -> assert false) ubinders in
-  if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders))
+let register_universe_binders ref ubinders = ()
 
 type univ_name_list = Names.lname list
 
@@ -111,11 +66,14 @@ let universe_binders_with_opt_names ref names =
       List.map2 (fun orig {CAst.v = na} ->
           match na with
           | Anonymous -> orig
-          | Name id -> id) orig udecl
+          | Name id -> Name id) orig udecl
     with Invalid_argument _ ->
       let len = List.length orig in
       CErrors.user_err ~hdr:"universe_binders_with_opt_names"
         Pp.(str "Universe instance should have length " ++ int len)
   in
-  let fold i acc na = Names.Id.Map.add na (Level.var i) acc in
+  let fold i acc na = match na with
+  | Name id -> Names.Id.Map.add id (Level.var i) acc
+  | Anonymous -> acc
+  in
   List.fold_left_i fold 0 empty_binders udecl
-- 
cgit v1.2.3


From 6e5dd2ee8bc014d1f99cef3156a5114b11510398 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 17:00:10 +0200
Subject: Remove remnants of polymorphic instance name registration.

---
 engine/univNames.ml  | 2 --
 engine/univNames.mli | 2 --
 2 files changed, 4 deletions(-)

(limited to 'engine')

diff --git a/engine/univNames.ml b/engine/univNames.ml
index 5c87fed31c..b7ccd2372f 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -53,8 +53,6 @@ let compute_instance_binders inst ubinders =
   in
   Array.map_to_list map (Instance.to_array inst)
 
-let register_universe_binders ref ubinders = ()
-
 type univ_name_list = Names.lname list
 
 let universe_binders_with_opt_names ref names =
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 634db9581c..b00c5fda95 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -21,8 +21,6 @@ val empty_binders : universe_binders
 
 val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t list
 
-val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
-
 type univ_name_list = Names.lname list
 
 (** [universe_binders_with_opt_names ref l]
-- 
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.
---
 engine/univNames.ml  | 7 ++++---
 engine/univNames.mli | 2 +-
 2 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'engine')

diff --git a/engine/univNames.ml b/engine/univNames.ml
index b7ccd2372f..ad91d31f87 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -36,9 +36,9 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
-let universe_binders_of_global ref : Name.t list =
+let universe_binders_of_global ref : Name.t array =
   try AUContext.names (Environ.universes_of_global (Global.env ()) ref)
-  with Not_found -> []
+  with Not_found -> [||]
 
 let name_universe lvl =
   (** Best-effort naming from the string representation of the level. This is
@@ -51,12 +51,13 @@ let compute_instance_binders inst ubinders =
     try Name (LMap.find lvl revmap)
     with Not_found -> Name (name_universe lvl)
   in
-  Array.map_to_list map (Instance.to_array inst)
+  Array.map map (Instance.to_array inst)
 
 type univ_name_list = Names.lname list
 
 let universe_binders_with_opt_names ref names =
   let orig = universe_binders_of_global ref in
+  let orig = Array.to_list orig in
   let udecl = match names with
   | None -> orig
   | Some udecl ->
diff --git a/engine/univNames.mli b/engine/univNames.mli
index b00c5fda95..dc669f45d6 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -19,7 +19,7 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 val empty_binders : universe_binders
 
-val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t list
+val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array
 
 type univ_name_list = Names.lname list
 
-- 
cgit v1.2.3