Splitting kernel universe code in two modules.

1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.

3 files changed, 23 insertions, 23 deletions

diff --git a/library/global.mli b/library/global.mli
index ac231f7fd..455751d41 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -19,7 +19,7 @@ val env : unit -> Environ.env
 
 val env_is_initial : unit -> bool
 
-val universes : unit -> Univ.universes
+val universes : unit -> UGraph.t
 val named_context_val : unit -> Environ.named_context_val
 val named_context : unit -> Context.named_context
 
diff --git a/library/universes.ml b/library/universes.ml
index bc42cc044..067558c8a 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -113,7 +113,7 @@ let to_constraints g s =
       | _, ULe, Some l' -> enforce_leq x y acc
       | _, ULub, _ -> acc
       | _, d, _ -> 
-	let f = if d == ULe then check_leq else check_eq in
+	let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in
 	  if f g x y then acc else 
 	    raise (Invalid_argument 
 		   "to_constraints: non-trivial algebraic constraint between universes")
@@ -123,12 +123,12 @@ let eq_constr_univs_infer univs m n =
   if m == n then true, Constraints.empty
   else 
     let cstrs = ref Constraints.empty in
-    let eq_universes strict = Univ.Instance.check_eq univs in
+    let eq_universes strict = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
+	  if UGraph.check_eq univs u1 u2 then true
 	  else
 	    (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
 	     true)
@@ -149,12 +149,12 @@ let eq_constr_univs_infer_with kind1 kind2 univs m n =
      [kind1,kind2], because [kind1] and [kind2] may be different,
      typically evaluating [m] and [n] in different evar maps. *)
   let cstrs = ref Constraints.empty in
-  let eq_universes strict = Univ.Instance.check_eq univs in
+  let eq_universes strict = UGraph.check_eq_instances univs in
   let eq_sorts s1 s2 = 
     if Sorts.equal s1 s2 then true
     else
       let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-      if Univ.check_eq univs u1 u2 then true
+      if UGraph.check_eq univs u1 u2 then true
       else
 	(cstrs := Constraints.add (u1, UEq, u2) !cstrs;
 	 true)
@@ -169,12 +169,12 @@ let leq_constr_univs_infer univs m n =
   if m == n then true, Constraints.empty
   else 
     let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in
+    let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if Univ.check_eq univs u1 u2 then true
+	if UGraph.check_eq univs u1 u2 then true
 	else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
 	      true)
     in
@@ -182,7 +182,7 @@ let leq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_leq univs u1 u2 then
+	  if UGraph.check_leq univs u1 u2 then
 	    ((if Univ.is_small_univ u1 then
 		cstrs := Constraints.add (u1, ULe, u2) !cstrs);
 	     true)
@@ -845,27 +845,27 @@ let normalize_context_set ctx us algs =
   let csts = 
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
-    let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g)
-			   ctx Univ.empty_universes
+    let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
+			   ctx UGraph.empty_universes
     in
     let g =
       Univ.Constraint.fold
 	(fun (l, d, r) g ->
 	 let g =
 	   if not (Level.is_small l || LSet.mem l ctx) then
-	     try Univ.add_universe l false g
-	     with Univ.AlreadyDeclared -> g
+	     try UGraph.add_universe l false g
+	     with UGraph.AlreadyDeclared -> g
 	   else g
 	 in
 	 let g =
 	   if not (Level.is_small r || LSet.mem r ctx) then
-	     try Univ.add_universe r false g
-	     with Univ.AlreadyDeclared -> g
+	     try UGraph.add_universe r false g
+	     with UGraph.AlreadyDeclared -> g
 	   else g
 	 in g) csts g
     in
-    let g = Univ.Constraint.fold Univ.enforce_constraint csts g in
-      Univ.constraints_of_universes g
+    let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in
+      UGraph.constraints_of_universes g
   in
   let noneqs =
     Constraint.fold (fun (l,d,r as cstr) noneqs ->
@@ -995,7 +995,7 @@ let refresh_constraints univs (ctx, cstrs) =
     Univ.Constraint.fold (fun c (cstrs', univs as acc) -> 
       let c = translate_cstr c in
       if is_trivial_leq c then acc
-      else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
+      else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs))
       cstrs (Univ.Constraint.empty, univs)
   in ((ctx, cstrs'), univs')
 
diff --git a/library/universes.mli b/library/universes.mli
index 5527da090..c897a88a9 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -60,11 +60,11 @@ val subst_univs_universe_constraints : universe_subst_fn ->
 
 val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function
 
-val to_constraints : universes -> universe_constraints -> constraints
+val to_constraints : UGraph.t -> universe_constraints -> constraints
 
 (** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping, the universe constraints in [u] and additional constraints [c]. *)
-val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool universe_constrained
 
 (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
     {!eq_constr_univs_infer} taking kind-of-term functions, to expose
@@ -72,12 +72,12 @@ val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_
 val eq_constr_univs_infer_with :
   (constr -> (constr,types) kind_of_term) ->
   (constr -> (constr,types) kind_of_term) ->
-  Univ.universes -> constr -> constr -> bool universe_constrained
+  UGraph.t -> constr -> constr -> bool universe_constrained
 
 (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
     modulo alpha, casts, application grouping, the universe constraints
     in [u] and additional constraints [c]. *)
-val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+val leq_constr_univs_infer : UGraph.t -> constr -> constr -> bool universe_constrained
 
 (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
     application grouping and the universe constraints in [c]. *)
@@ -212,7 +212,7 @@ val restrict_universe_context : universe_context_set -> universe_set -> universe
 val simplify_universe_context : universe_context_set -> 
   universe_context_set * universe_level_subst
 
-val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes
+val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t
 
 (** Pretty-printing *)