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.

1 files changed, 22 insertions, 22 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index cd0b52eca..3f4bfe7af 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -283,8 +283,8 @@ type evar_universe_context =
    (** The subset of unification variables that
 	can be instantiated with algebraic universes as they appear in types 
 	and universe instances only. *)
-   uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
-   uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
+   uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
+   uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
  }
   
 let empty_evar_universe_context = 
@@ -292,8 +292,8 @@ let empty_evar_universe_context =
     uctx_local = Univ.ContextSet.empty;
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
-    uctx_universes = Univ.initial_universes;
-    uctx_initial_universes = Univ.initial_universes }
+    uctx_universes = UGraph.initial_universes;
+    uctx_initial_universes = UGraph.initial_universes }
 
 let evar_universe_context_from e = 
   let u = universes e in
@@ -314,7 +314,7 @@ let union_evar_universe_context ctx ctx' =
 			       (Univ.ContextSet.levels ctx.uctx_local) in
     let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
     let declarenew g =
-      Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g
+      Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
     in
     let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
@@ -328,7 +328,7 @@ let union_evar_universe_context ctx ctx' =
 	  if local == ctx.uctx_local then ctx.uctx_universes
 	  else
 	    let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-	      Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
+	      UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
 
 (* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *)
 (* let union_evar_universe_context =  *)
@@ -374,7 +374,7 @@ let process_universe_constraints univs vars alg cstrs =
 	  | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg)
 	in
 	  if d == Universes.ULe then
-	    if Univ.check_leq univs l r then
+	    if UGraph.check_leq univs l r then
 	      (** Keep Prop/Set <= var around if var might be instantiated by prop or set
 		  later. *)
 	      if Univ.Universe.is_level l then 
@@ -413,7 +413,7 @@ let process_universe_constraints univs vars alg cstrs =
 		  instantiate_variable l' r vars
 		else if rloc then 
 		  instantiate_variable r' l vars
-		else if not (Univ.check_eq univs l r) then
+		else if not (UGraph.check_eq univs l r) then
 		  (* Two rigid/global levels, none of them being local,
 		     one of them being Prop/Set, disallow *)
 		  if Univ.Level.is_small l' || Univ.Level.is_small r' then
@@ -433,7 +433,7 @@ let process_universe_constraints univs vars alg cstrs =
 		     Univ.enforce_leq inst lu local
 		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
             | _, _ (* One of the two is algebraic or global *) -> 
-	     if Univ.check_eq univs l r then local
+	     if UGraph.check_eq univs l r then local
 	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
   in
   let local = 
@@ -459,7 +459,7 @@ let add_constraints_context ctx cstrs =
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
+      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
 (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
 (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
@@ -473,7 +473,7 @@ let add_universe_constraints_context ctx cstrs =
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
+      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
 (* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
 (* let add_universe_constraints_context =  *)
@@ -1012,13 +1012,13 @@ let merge_uctx sideff rigid uctx ctx' =
   in
   let declare g =
     LSet.fold (fun u g ->
-	       try Univ.add_universe u false g
-	       with Univ.AlreadyDeclared when sideff -> g)
+	       try UGraph.add_universe u false g
+	       with UGraph.AlreadyDeclared when sideff -> g)
 	      levels g
   in
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare uctx.uctx_universes in
-  let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in
+  let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
     { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
 
 let merge_context_set rigid evd ctx' = 
@@ -1079,11 +1079,11 @@ let uctx_new_univ_variable rigid name predicative
     | None -> uctx.uctx_names
   in
   let initial =
-    Univ.add_universe u false uctx.uctx_initial_universes
+    UGraph.add_universe u false uctx.uctx_initial_universes
   in						     
   let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
-		uctx_universes = Univ.add_universe u false uctx.uctx_universes;
+		uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
 		uctx_initial_universes = initial}
   in uctx', u
 						     
@@ -1102,10 +1102,10 @@ let new_sort_variable ?name ?(predicative=true) rigid d =
 let add_global_univ d u =
   let uctx = d.universes in
   let initial =
-    Univ.add_universe u true uctx.uctx_initial_universes
+    UGraph.add_universe u true uctx.uctx_initial_universes
   in
   let univs = 
-    Univ.add_universe u true uctx.uctx_universes
+    UGraph.add_universe u true uctx.uctx_universes
   in
     { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
 				     uctx_initial_universes = initial;
@@ -1245,10 +1245,10 @@ let set_leq_sort env evd s1 s2 =
       else evd
 	    
 let check_eq evd s s' =
-  Univ.check_eq evd.universes.uctx_universes s s'
+  UGraph.check_eq evd.universes.uctx_universes s s'
 
 let check_leq evd s s' =
-  Univ.check_leq evd.universes.uctx_universes s s'
+  UGraph.check_leq evd.universes.uctx_universes s s'
 
 let subst_univs_context_with_def def usubst (ctx, cst) =
   (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
@@ -1301,10 +1301,10 @@ let refresh_undefined_univ_variables uctx =
           (Option.map (Univ.subst_univs_level_universe subst) v) acc)
       uctx.uctx_univ_variables Univ.LMap.empty
   in
-  let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g)
+  let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g)
 				   (Univ.ContextSet.levels ctx') g in
   let initial = declare uctx.uctx_initial_universes in
-  let univs = declare Univ.initial_universes in
+  let univs = declare UGraph.initial_universes in
   let uctx' = {uctx_names = uctx.uctx_names;
 	       uctx_local = ctx'; 
 	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;