Actually store the bound name information in the abstract universe context.

4 files changed, 43 insertions, 64 deletions

diff --git a/checker/values.ml b/checker/values.ml
index 8f6b24ec26..68bac10839 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -122,8 +122,7 @@ let v_cstrs =
 let v_variance = v_enum "variance" 3
 
 let v_instance = Annot ("instance", Array v_level)
-let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|]
-let v_abs_context = v_context (* only for clarity *)
+let v_abs_context = v_tuple "abstract_universe_context" [|List v_name; v_cstrs|]
 let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
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
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 *)