Merge PR #11455: Small API additions to kernel/univ

Reviewed-by: ppedrot

4 files changed, 23 insertions, 20 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 33336079bb..4d15ce741c 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -128,7 +128,7 @@ let enforce_leq_alg u v g =
          | exception (UniverseInconsistency _ as e) -> Inr e)
   in
   (* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *)
-  let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in
+  let c = List.map (fun u -> List.map (fun v -> (u,v)) (Universe.repr v)) (Universe.repr u) in
   let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in
   (* We pick a best constraint: smallest number of constraints, not an error if possible. *)
   let order x y = match x, y with
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0712774576..94f7076c02 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -42,6 +42,8 @@ struct
 
     let make dp i = (DirPath.hcons dp,i)
 
+    let repr x : t = x
+
     let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
 
     let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d)
@@ -320,8 +322,9 @@ struct
       if u == v then 0
       else
         let (x, n) = u and (x', n') = v in
-          if Int.equal n n' then Level.compare x x'
-          else n - n'
+        let c = Int.compare n n' in
+        if Int.equal 0 c then  Level.compare x x'
+        else c
 
     let sprop = hcons (Level.sprop, 0)
     let prop = hcons (Level.prop, 0)
@@ -427,6 +430,10 @@ struct
 
   let hcons = Hashcons.recursive_hcons Huniv.generate Huniv.hcons Expr.hcons
 
+  module Self = struct type nonrec t = t let compare = compare end
+  module Map = CMap.Make(Self)
+  module Set = CSet.Make(Self)
+
   let make l = tip (Expr.make l)
   let tip x = tip x
 
@@ -524,15 +531,10 @@ struct
      Used to type the products. *)
   let sup x y = merge_univs x y
 
-  let empty = []
-
   let exists = List.exists
 
   let for_all = List.for_all
-
-  let smart_map = List.Smart.map
-
-  let map = List.map
+  let repr x : t = x
 end
 
 type universe = Universe.t
@@ -550,8 +552,6 @@ let pr_uni = Universe.pr
 let sup = Universe.sup
 let super = Universe.super
 
-open Universe
-
 let universe_level = Universe.level
 
 
@@ -576,7 +576,7 @@ type univ_inconsistency = constraint_type * universe * universe * explanation La
 exception UniverseInconsistency of univ_inconsistency
 
 let error_inconsistency o u v p =
-  raise (UniverseInconsistency (o,make u,make v,p))
+  raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
 
 (* Constraints and sets of constraints. *)
 
@@ -677,7 +677,7 @@ let enforce_eq u v c =
 
 let constraint_add_leq v u c =
   (* We just discard trivial constraints like u<=u *)
-  if Expr.equal v u then c
+  if Universe.Expr.equal v u then c
   else
     match v, u with
     | (x,n), (y,m) ->
@@ -695,13 +695,13 @@ let constraint_add_leq v u c =
         else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
         else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *)
 
-let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
+let check_univ_leq_one u v = Universe.exists (Universe.Expr.leq u) v
 
 let check_univ_leq u v =
   Universe.for_all (fun u -> check_univ_leq_one u v) u
 
 let enforce_leq u v c =
-  match is_sprop u, is_sprop v with
+  match Universe.is_sprop u, Universe.is_sprop v with
   | true, true -> c
   | true, false | false, true ->
     raise (UniverseInconsistency (Le, u, v, None))
@@ -925,7 +925,7 @@ let subst_instance_instance s i =
 
 let subst_instance_universe s u =
   let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smart_map f u in
+  let u' = List.Smart.map f u in
     if u == u' then u
     else Universe.sort u'
 
@@ -1108,7 +1108,7 @@ let subst_univs_level_level subst l =
 
 let subst_univs_level_universe subst u =
   let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in
-  let u' = Universe.smart_map f u in
+  let u' = List.Smart.map f u in
     if u == u' then u
     else Universe.sort u'
 
@@ -1150,7 +1150,7 @@ let subst_univs_universe fn ul =
     if CList.is_empty subst then ul
     else
       let substs =
-        List.fold_left Universe.merge_univs Universe.empty subst
+        List.fold_left Universe.merge_univs [] subst
       in
         List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
           substs nosubst
diff --git a/kernel/univ.mli b/kernel/univ.mli
index f7c984870f..94e57b9efc 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -16,6 +16,7 @@ sig
     type t
 
     val make : Names.DirPath.t -> int -> t
+    val repr : t -> Names.DirPath.t * int
     val equal : t -> t -> bool
     val hash : t -> int
     val compare : t -> t -> int
@@ -138,8 +139,10 @@ sig
 
   val exists : (Level.t * int -> bool) -> t -> bool
   val for_all : (Level.t * int -> bool) -> t -> bool
+  val repr : t -> (Level.t * int) list
 
-  val map : (Level.t * int -> 'a) -> t -> 'a list
+  module Set : CSet.S with type elt  = t
+  module Map : CMap.ExtS with type key = t and module Set := Set
 
 end
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 037006bc47..b042437a22 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -696,7 +696,7 @@ let detype_universe sigma u =
       if Univ.Level.is_set l then GSet else
       GType (hack_qualid_of_univ_level sigma l) in
     (s, n) in
-  Univ.Universe.map fn u
+  List.map fn (Univ.Universe.repr u)
 
 let detype_sort sigma = function
   | SProp -> UNamed [GSProp,0]