From ccf995fd843f14ae8dfaf18177be6c2494faea35 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 18 Oct 2018 13:08:23 +0200
Subject: Automatically generate names for universes.

The names are `uXXX` with `XXX` some number avoiding collision.

Note that there may be some collisions with polymorphic binders, eg
something like

~~~
Set Universe Polymorphism.
Section foo.
  Universe u0.
  Definition bar := Type.
  (* bar@{u0} = Type@{u0} but this isn't the section u0 *)

  Definition baz := Type@{u0}. (* this one is the section u0 *)
  Definition foobar := Eval compute in baz -> Type.
  (* Type@{u0} -> Type@{u0} but these aren't the same u0 *)
~~~
So maybe we should do a nametab lookup too. This is strictly a
printing issue (polymorphic binder names have no other use).

In the monomorphic case names are qualified by the parent definition
so it should be fine (barring module/definition collision but we
already have those).

Note that there are still unnamed universes as they didn't go through
UState (eg schemes).
---
 engine/uState.ml                  | 20 +++++++++++++++++++-
 test-suite/output/UnivBinders.out |  4 ++--
 2 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/engine/uState.ml b/engine/uState.ml
index 41905feab7..15bd0335f4 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/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 2501ce4f26..d63b6dbfce 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -191,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]
-- 
cgit v1.2.3