Proper nametab handling of global universe names

They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced

2 files changed, 55 insertions, 38 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 1b4645aff..8fc959b0f 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -453,28 +453,51 @@ let input_universe_context : universe_context_decl -> Libobject.obj =
 let declare_universe_context poly ctx =
   Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
 
-(* Discharged or not *)
-type universe_decl = polymorphic * Universes.universe_binders
-
-let cache_universes (p, l) =
-  let glob = Global.global_universe_names () in
-  let glob', ctx =
-    Id.Map.fold (fun id lev ((idl,lid),ctx) ->
-        ((Id.Map.add id (p, lev) idl,
-          Univ.LMap.add lev id lid),
-         Univ.ContextSet.add_universe lev ctx))
-      l (glob, Univ.ContextSet.empty)
-  in
-  cache_universe_context (p, ctx);
-  Global.set_global_universe_names glob'
+(** Global universes are not substitutive objects but global objects
+   bound at the *library* or *module* level. The polymorphic flag is
+   used to distinguish universes declared in polymorphic sections, which
+   are discharged and do not remain in scope. *)
+
+type universe_decl = polymorphic * Nametab.universe_id
+
+let add_universe p (dp, i) =
+  let level = Univ.Level.make dp i in
+  let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
+  Global.push_context_set p ctx;
+  Universes.add_global_universe level p;
+  if p then Lib.add_section_context ctx
+
+let check_exists sp =
+  let depth = sections_depth () in
+  let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in
+  if Nametab.exists_universe sp then alreadydeclared (Id.print (basename sp) ++ str " already exists")
+  else ()
 
-let input_universes : universe_decl -> Libobject.obj =
+let cache_universe ((sp, _), (poly, id)) =
+  let () = check_exists sp in
+  let () = Nametab.push_universe (Nametab.Until 1) sp id in
+    add_universe poly id
+
+let load_universe i ((sp, _), (poly, id)) =
+  let () = Nametab.push_universe (Nametab.Until i) sp id in
+  add_universe poly id
+
+let open_universe i ((sp, _), (poly, id)) =
+  let () = Nametab.push_universe (Nametab.Exactly i) sp id in
+  ()(** add_universe p id Necessary ? *)
+
+let input_universe : universe_decl -> Libobject.obj =
   declare_object
     { (default_object "Global universe name state") with
-      cache_function = (fun (na, pi) -> cache_universes pi);
-      load_function = (fun _ (_, pi) -> cache_universes pi);
+      cache_function = cache_universe;
+      load_function = load_universe;
+      open_function = open_universe;
       discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
-      classify_function = (fun a -> Keep a) }
+      subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
+      classify_function = (fun a -> Substitute a) }
+
+let add_universe poly (id, lev) =
+  ignore(Lib.add_leaf id (input_universe (poly, lev)))
 
 let do_universe poly l =
   let in_section = Lib.sections_are_opened () in
@@ -484,11 +507,11 @@ let do_universe poly l =
                    (str"Cannot declare polymorphic universes outside sections")
   in
   let l =
-    List.fold_left (fun acc (l, id) ->
-	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
-              Id.Map.add id lev acc) Id.Map.empty l
+    List.map (fun (l, id) ->
+      let lev = Universes.new_univ_id () in
+      (id, lev)) l
   in
-    Lib.add_anonymous_leaf (input_universes (poly, l))
+  List.iter (add_universe poly) l
 
 type constraint_decl = polymorphic * Univ.constraints
 
@@ -510,20 +533,15 @@ let input_constraints : constraint_decl -> Libobject.obj =
       discharge_function = discharge_constraints;
       classify_function = (fun a -> Keep a) }
 
+let loc_of_glob_level = function
+  | Misctypes.GType (Misctypes.UNamed n) -> Libnames.loc_of_reference n
+  | _ -> None
+
 let do_constraint poly l =
-  let open Misctypes in
   let u_of_id x =
-    match x with
-    | GProp -> Loc.tag (false, Univ.Level.prop)
-    | GSet  -> Loc.tag (false, Univ.Level.set)
-    | GType None | GType (Some (_, Anonymous)) ->
-       user_err ~hdr:"Constraint"
-                     (str "Cannot declare constraints on anonymous universes")
-    | GType (Some (loc, Name id)) ->
-       let names, _ = Global.global_universe_names () in
-       try loc, Id.Map.find id names
-       with Not_found ->
-         user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ Id.print id)
+    let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
+    let loc = loc_of_glob_level x in
+    loc, Universes.is_polymorphic level, level
   in
   let in_section = Lib.sections_are_opened () in
   let () =
@@ -541,7 +559,7 @@ let do_constraint poly l =
                     ++ str "Polymorphic Constraint instead")
   in
   let constraints = List.fold_left (fun acc (l, d, r) ->
-     let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in
+     let ploc, p, lu = u_of_id l and rloc, p', ru = u_of_id r in
      check_poly ?loc:ploc p rloc p';
      Univ.Constraint.add (lu, d, ru) acc)
     Univ.Constraint.empty l
diff --git a/interp/declare.mli b/interp/declare.mli
index d50d37368..31883c9d7 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -87,6 +87,5 @@ val exists_name : Id.t -> bool
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
 val do_universe : polymorphic -> Id.t Loc.located list -> unit
-val do_constraint : polymorphic ->
-  (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
-  unit
+val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
+                    unit