Small cleaning of interface in Univ

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

5 files changed, 71 insertions, 15 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 042961879..ada7c2c51 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 12ec4e222..10d7b2627 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 c53a3c54d..860e3f155 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
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 98f8230a6..1c9573ca3 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -499,7 +499,7 @@ let collect_evars c =
 let new_univ_variable ({ evars = (sigma,(us,sm)) } as d) =
   let u = Termops.new_univ_level () in
   let us' = Univ.UniverseLSet.add u us in
-    ({d with evars = (sigma, (us', sm))}, Univ.make_universe u)
+    ({d with evars = (sigma, (us', sm))}, Univ.Universe.make u)
   
 let new_sort_variable d =
   let (d', u) = new_univ_variable d in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index b147637f0..c9a6d0b5b 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -149,9 +149,9 @@ let new_univ_level =
   let univ_gen = ref 0 in
   (fun sp ->
     incr univ_gen;
-    Univ.make_universe_level (Lib.library_dp(),!univ_gen))
+    Univ.UniverseLevel.make (Lib.library_dp()) !univ_gen)
 
-let new_univ () = Univ.make_universe (new_univ_level ())
+let new_univ () = Univ.Universe.make (new_univ_level ())
 let new_Type () = mkType (new_univ ())
 let new_Type_sort () = Type (new_univ ())