Towards unifying parsing/printing for universe instances and Type's argument.

We consistently use:
- UUnknown: to mean a rigid anonymous universe
  (written Type in instances and Type as a sort)
  [was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
  (written _ in instances and Type@{_} as a sort)
  [was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
  (written id or qualid in instances and Type@{id} or Type@{qualid} or more
   generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)

There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.

There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.

4 files changed, 35 insertions, 29 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 82726eccf0..901a1bd342 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -689,7 +689,7 @@ let hack_qualid_of_univ_level sigma l =
 let detype_universe sigma u =
   let fn (l, n) =
     let qid = hack_qualid_of_univ_level sigma l in
-    Some (qid, n)
+    (qid, n)
   in
   Univ.Universe.map fn u
 
@@ -700,8 +700,8 @@ let detype_sort sigma = function
   | Type u ->
     GType
       (if !print_universes
-       then detype_universe sigma u
-       else [])
+       then UNamed (detype_universe sigma u)
+       else UUnknown)
 
 type binder_kind = BProd | BLambda | BLetIn
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 85b9faac77..656b987942 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -45,14 +45,19 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp2 = f ty in
   (na,k,comp1,comp2)
 
-
-let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
-| GSProp, GSProp
-| GProp, GProp
-| GSet, GSet -> true
-| GType l1, GType l2 ->
-   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2
-| (GSProp|GProp|GSet|GType _), _ -> false
+let univ_name_eq u1 u2 = match u1, u2 with
+  | UUnknown, UUnknown -> true
+  | UAnonymous, UAnonymous -> true
+  | UNamed l1, UNamed l2 ->
+    List.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n) l1 l2
+  | (UNamed _ | UAnonymous | UUnknown), _ -> false
+
+let glob_sort_eq g1 g2 = match g1, g2 with
+  | GSProp, GSProp
+  | GProp, GProp
+  | GSet, GSet -> true
+  | GType u1, GType u2 -> univ_name_eq u1 u2
+  | (GSProp|GProp|GSet|GType _), _ -> false
 
 let glob_sort_family = let open Sorts in function
 | GSProp -> InSProp
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 02cb294f6d..37bacbdeb2 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -30,15 +30,15 @@ type 'a glob_sort_gen =
   | GType of 'a (** representation of [Type] literal *)
 
 type 'a universe_kind =
-  | UAnonymous
-  | UUnknown
-  | UNamed of 'a
+  | UAnonymous (** a flexible universe (collapsable by minimization) *)
+  | UUnknown (** a rigid universe *)
+  | UNamed of 'a (** a named universe or a universe expression *)
 
-type level_info = Libnames.qualid universe_kind
+type level_info = Libnames.qualid universe_kind (** levels, occurring in universe instances *)
 type glob_level = level_info glob_sort_gen
 type glob_constraint = glob_level * Univ.constraint_type * glob_level
 
-type sort_info = (Libnames.qualid * int) option list
+type sort_info = (Libnames.qualid * int) list universe_kind (** sorts: Prop, Set, Type@{...} *)
 type glob_sort = sort_info glob_sort_gen
 
 type glob_recarg = int option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c7b657f96c..48aba8edf4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -165,26 +165,27 @@ let interp_universe_level_name ~anon_rigidity evd qid =
       in evd, level
 
 let interp_universe ?loc evd = function
-  | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
-	    evd, Univ.Universe.make l
-  | l ->
-    List.fold_left (fun (evd, u) l ->
+  | UUnknown ->
+    let evd, l = new_univ_level_variable ?loc univ_rigid evd in
+    evd, Univ.Universe.make l
+  | UAnonymous ->
+    let evd, l = new_univ_level_variable ?loc univ_flexible evd in
+    evd, Univ.Universe.make l
+  | UNamed l ->
+    List.fold_left (fun (evd, u) (l,n) ->
       let evd', u' =
-        match l with
-        | Some (l,n) ->
+        let evd',u' =
            (* [univ_flexible_alg] can produce algebraic universes in terms *)
            let anon_rigidity = univ_flexible in
            let evd', l = interp_universe_level_name ~anon_rigidity evd l in
-           let u' = Univ.Universe.make l in
-           (match n with
+           evd', Univ.Universe.make l
+        in
+        match n with
             | 0 -> evd', u'
             | 1 -> evd', Univ.Universe.super u'
-            | _ ->
+            | n ->
                user_err ?loc ~hdr:"interp_universe"
-                        (Pp.(str "Cannot interpret universe increment +" ++ int n)))
-        | None ->
-           let evd, l = new_univ_level_variable ?loc univ_flexible evd in
-           evd, Univ.Universe.make l
+                        (Pp.(str "Cannot interpret universe increment +" ++ int n))
       in (evd', Univ.sup u u'))
     (evd, Univ.Universe.type0m) l