Small cleaning of interface in Univ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16006 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 68 insertions, 12 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0429618794..ada7c2c512 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -374,7 +374,8 @@ if Int.equal nmr 0 then 0 else
   in find 0 (n-1) (lpar,List.rev hyps)
 
 let lambda_implicit_lift n a =
-  let implicit_sort = mkType (make_univ (make_dirpath [id_of_string "implicit"], 0)) in
+  let level = UniverseLevel.make (make_dirpath [id_of_string "implicit"]) 0 in
+  let implicit_sort = mkType (Universe.make level) in
   let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
   iterate lambda_implicit n (lift n a)
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 12ec4e222b..10d7b26275 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -61,6 +61,8 @@ module UniverseLevel = struct
       Int.equal i1 i2 && Int.equal (Names.dir_path_ord dp1 dp2) 0
     | _ -> false
 
+  let make m n = Level (n, m)
+
   let to_string = function
     | Set -> "Set"
     | Level (n,d) -> Names.string_of_dirpath d^"."^string_of_int n
@@ -85,13 +87,33 @@ let compare_levels = UniverseLevel.compare
    maximum of two algebraic universes
 *)
 
-type universe =
+module Universe =
+struct
+  type t =
   | Atom of UniverseLevel.t
   | Max of UniverseLevel.t list * UniverseLevel.t list
 
-let make_universe_level (m,n) = UniverseLevel.Level (n,m)
-let make_universe l = Atom l
-let make_univ c = Atom (make_universe_level c)
+  let compare u1 u2 =
+    if u1 == u2 then 0 else
+    match u1, u2 with
+    | Atom l1, Atom l2 -> UniverseLevel.compare l1 l2
+    | Max (lt1, le1), Max (lt2, le2) ->
+      let c = List.compare UniverseLevel.compare lt1 lt2 in
+      if Int.equal c 0 then
+        List.compare UniverseLevel.compare le1 le2
+      else c
+    | Atom _, Max _ -> -1
+    | Max _, Atom _ -> 1
+
+  let equal u1 u2 = Int.equal (compare u1 u2) 0
+
+  let make l = Atom l
+
+end
+
+open Universe
+
+type universe = Universe.t
 
 let universe_level = function
   | Atom l -> Some l
diff --git a/kernel/univ.mli b/kernel/univ.mli
index c53a3c54d5..860e3f1551 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -8,8 +8,46 @@
 
 (** Universes. *)
 
-type universe_level
-type universe
+module UniverseLevel :
+sig
+  type t
+  (** Type of universe levels. A universe level is essentially a unique name
+      that will be associated to constraints later on. *)
+
+  val compare : t -> t -> int
+  (** Comparison function *)
+
+  val equal : t -> t -> bool
+  (** Equality function *)
+
+  val make : Names.dir_path -> int -> t
+  (** Create a new universe level from a unique identifier and an associated
+      module path. *)
+
+end
+
+type universe_level = UniverseLevel.t
+(** Alias name. *)
+
+module Universe :
+sig
+  type t
+  (** Type of universes. A universe is defined as a set of constraints w.r.t.
+      other universes. *)
+
+  val compare : t -> t -> int
+  (** Comparison function *)
+
+  val equal : t -> t -> bool
+  (** Equality function *)
+
+  val make : UniverseLevel.t -> t
+  (** Create a constraint-free universe out of a given level. *)
+
+end
+
+type universe = Universe.t
+(** Alias name. *)
 
 module UniverseLSet : Set.S with type elt = universe_level
 
@@ -20,16 +58,11 @@ val type0m_univ : universe  (** image of Prop in the universes hierarchy *)
 val type0_univ : universe  (** image of Set in the universes hierarchy *)
 val type1_univ : universe  (** the universe of the type of Prop/Set *)
 
-val make_universe_level : Names.dir_path * int -> universe_level
-val make_universe : universe_level -> universe
-val make_univ : Names.dir_path * int -> universe
-
 val is_type0_univ : universe -> bool
 val is_type0m_univ : universe -> bool
 val is_univ_variable : universe -> bool
 
 val universe_level : universe -> universe_level option
-val compare_levels : universe_level -> universe_level -> int
 
 (** The type of a universe *)
 val super : universe -> universe