Merge PR #8760: Automatically generate names for universes.

8 files changed, 49 insertions, 39 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index dc760e7f97..5747ae2ad4 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -148,7 +148,25 @@ let of_binders b =
   in
   { ctx with uctx_names = b, rmap }
 
-let universe_binders ctx = fst ctx.uctx_names
+let invent_name (named,cnt) u =
+  let rec aux i =
+    let na = Id.of_string ("u"^(string_of_int i)) in
+    if Id.Map.mem na named then aux (i+1)
+    else Id.Map.add na u named, i+1
+  in
+  aux cnt
+
+let universe_binders ctx =
+  let open Univ in
+  let named, rev = ctx.uctx_names in
+  let named, _ = LSet.fold (fun u named ->
+      match LMap.find u rev with
+      | exception Not_found -> (* not sure if possible *) invent_name named u
+      | { uname = None } -> invent_name named u
+      | { uname = Some _ } -> named)
+      (ContextSet.levels ctx.uctx_local) (named, 0)
+  in
+  named
 
 let instantiate_variable l b v =
   try v := Univ.LMap.set l (Some b) !v
diff --git a/interp/declare.ml b/interp/declare.ml
index fe8fc7c969..a9bfe8cabb 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -473,36 +473,33 @@ type universe_source =
 type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list
 
 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 (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
   else ()
 
-let qualify_univ i sp src id =
-  let open Libnames in
+let qualify_univ i dp src id =
   match src with
   | BoundUniv | UnqualifiedUniv ->
-    let sp = dirpath sp in
-    i, make_path sp id
+    i,  Libnames.make_path dp id
   | QualifiedUniv l ->
-    let sp = dirpath sp in
-    let sp = DirPath.repr sp in
-    Nametab.map_visibility succ i, make_path (DirPath.make (l::sp)) id
+    let dp = DirPath.repr dp in
+    Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id
 
-let do_univ_name ~check i sp src (id,univ) =
-  let i, sp = qualify_univ i sp src id in
+let do_univ_name ~check i dp src (id,univ) =
+  let i, sp = qualify_univ i dp src id in
   if check then check_exists sp;
   Nametab.push_universe i sp univ
 
 let cache_univ_names ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:true (Nametab.Until 1) sp src) univs
+  let depth = sections_depth () in
+  let dp = pop_dirpath_n depth (dirpath sp) in
+  List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs
 
 let load_univ_names i ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:false (Nametab.Until i) sp src) univs
+  List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs
 
 let open_univ_names i ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:false (Nametab.Exactly i) sp src) univs
+  List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs
 
 let discharge_univ_names = function
   | _, (BoundUniv, _) -> None
@@ -525,7 +522,7 @@ let declare_univ_binders gr pl =
     let l = match gr with
       | ConstRef c -> Label.to_id @@ Constant.label c
       | IndRef (c, _) -> Label.to_id @@ MutInd.label c
-      | VarRef id -> id
+      | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
       | ConstructRef _ ->
         anomaly ~label:"declare_univ_binders"
           Pp.(str "declare_univ_binders on an constructor reference")
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 178116c580..d63b6dbfce 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -79,8 +79,9 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 Monomorphic bobmorane = 
-let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
-     : Type@{max(tt.u,ff.u)}
+let tt := Type@{UnivBinders.32} in
+let ff := Type@{UnivBinders.34} in tt -> ff
+     : Type@{max(UnivBinders.31,UnivBinders.33)}
 
 bobmorane is not universe polymorphic
 The command has indeed failed with message:
@@ -190,12 +191,12 @@ Type@{UnivBinders.57} -> Type@{i}
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axbar
-axfoo' : Type@{UnivBinders.59} -> Type@{axbar'.i}
+axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo'
-axbar' : Type@{UnivBinders.59} -> Type@{axbar'.i}
+axbar' : Type@{axbar'.u0} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index ad901da72f..582a5e969a 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -74,19 +74,10 @@ Module SecLet.
     (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
     Unset Strict Universe Declaration.
     Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
-    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *)
+    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *)
     Definition bobmorane := tt -> ff.
   End foo.
-  Print bobmorane. (*
-                     bobmorane@{UnivBinders.15 UnivBinders.16 ff.u ff.v} =
-                     let tt := Type@{UnivBinders.16} in let ff := Type@{ff.v} in tt -> ff
-                     : Type@{max(UnivBinders.15,ff.u)}
-                     (* UnivBinders.15 UnivBinders.16 ff.u ff.v |= UnivBinders.16 < UnivBinders.15
-                     ff.v < ff.u
-                    *)
-
-                    bobmorane is universe polymorphic
-                    *)
+  Print bobmorane.
 End SecLet.
 
 (* fun x x => foo is nonsense with local binders *)
diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v
index 7c298c98b6..1bc565cbb5 100644
--- a/test-suite/success/unidecls.v
+++ b/test-suite/success/unidecls.v
@@ -1,4 +1,4 @@
-(* coq-prog-args: ("-top" "unidecls") *)
+(* -*- coq-prog-args: ("-top" "unidecls"); -*- *)
 Set Printing Universes.
 
 Module decls.
@@ -46,12 +46,12 @@ Universe secfoo.
 Section Foo'.
   Fail Universe secfoo.
   Universe secfoo2.
-  Check Type@{Foo'.secfoo2}.
+  Fail Check Type@{Foo'.secfoo2}.
+  Check Type@{secfoo2}.
   Constraint secfoo2 < a.
 End Foo'.
 
 Check Type@{secfoo2}.
-Fail Check Type@{Foo'.secfoo2}.
 Fail Check eq_refl : Type@{secfoo2} = Type@{a}.
 
 (** Below, u and v are global, fixed universes *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 0c39458a57..f405c4d5a9 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -535,11 +535,11 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
   let (_, kn), prim = declare_mind mie in
   let mind = Global.mind_of_delta_kn kn in
+  Declare.declare_univ_binders (IndRef (mind,0)) pl;
   List.iteri (fun i (indimpls, constrimpls) ->
               let ind = (mind,i) in
               let gr = IndRef ind in
               maybe_declare_manual_implicits false gr indimpls;
-              Declare.declare_univ_binders gr pl;
               List.iteri
                 (fun j impls ->
                  maybe_declare_manual_implicits false
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 35fb18e292..2fe03a8ec5 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -43,9 +43,11 @@ let declare_definition ident (local, p, k) ce pl imps hook =
   | Discharge | Local | Global ->
       let local = get_locality ident ~kind:"definition" local in
       let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
-      ConstRef kn in
+      let gr = ConstRef kn in
+      let () = Declare.declare_univ_binders gr pl in
+      gr
+  in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = Declare.declare_univ_binders gr pl in
   let () = definition_message ident in
   Lemmas.call_hook fix_exn hook local gr; gr
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 150f2c6ee9..3b041b7065 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -197,10 +197,11 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
           let () = if should_suggest
             then Proof_using.suggest_constant (Global.env ()) kn
           in
-          ConstRef kn
+          let gr = ConstRef kn in
+          Declare.declare_univ_binders gr (UState.universe_binders uctx);
+          gr
     in
     definition_message id;
-    Declare.declare_univ_binders r (UState.universe_binders uctx);
     call_hook (fun exn -> exn) hook locality r
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in